diff options
Diffstat (limited to 'src/AST/Accum.hs')
| -rw-r--r-- | src/AST/Accum.hs | 33 |
1 files changed, 24 insertions, 9 deletions
diff --git a/src/AST/Accum.hs b/src/AST/Accum.hs index 163f1c3..6c46ad5 100644 --- a/src/AST/Accum.hs +++ b/src/AST/Accum.hs @@ -21,16 +21,17 @@ data AcPrj | APArrIdx AcPrj | APArrSlice Nat --- | @b@ is a small part of @a@, indicated by the projection. +-- | @b@ is a small part of @a@, indicated by the projection @p@. data SAcPrj (p :: AcPrj) (a :: Ty) (b :: Ty) where SAPHere :: SAcPrj APHere a a - SAPFst :: SAcPrj p a b -> SAcPrj (APFst p) (TPair t a) b - SAPSnd :: SAcPrj p a b -> SAcPrj (APSnd p) (TPair a t) b - SAPLeft :: SAcPrj p a b -> SAcPrj (APLeft p) (TEither t a) b + SAPFst :: SAcPrj p a b -> SAcPrj (APFst p) (TPair a t) b + SAPSnd :: SAcPrj p a b -> SAcPrj (APSnd p) (TPair t a) b + SAPLeft :: SAcPrj p a b -> SAcPrj (APLeft p) (TEither a t) b SAPRight :: SAcPrj p a b -> SAcPrj (APRight p) (TEither t a) b - SAPJust :: SAcPrj p a b -> SAcPrj (APJust p) (TMaybe t) b - SAPArrIdx :: SAcPrj p a b -> SNat n -> SAcPrj (APArrIdx p) (TArr n t) b - SAPArrSlice :: SNat m -> SAcPrj (APArrSlice m) (TArr n t) (TArr (n - m) t) + SAPJust :: SAcPrj p a b -> SAcPrj (APJust p) (TMaybe a) b + SAPArrIdx :: SAcPrj p a b -> SNat n -> SAcPrj (APArrIdx p) (TArr n a) b + -- TODO: + -- SAPArrSlice :: SNat m -> SAcPrj (APArrSlice m) (TArr n t) (TArr (n - m) t) deriving instance Show (SAcPrj p a b) type family AcIdx p t where @@ -40,5 +41,19 @@ type family AcIdx p t where AcIdx (APLeft p) (TEither a b) = AcIdx p a AcIdx (APRight p) (TEither a b) = AcIdx p b AcIdx (APJust p) (TMaybe a) = AcIdx p a - AcIdx (APArrIdx p) (TArr n a) = TPair (Tup (Replicate n TIx)) (AcIdx p a) - AcIdx (APArrSlice m) (TArr n a) = Tup (Replicate m TIx) + AcIdx (APArrIdx p) (TArr n a) = + -- ((index, array shape), recursive info) + TPair (TPair (Tup (Replicate n TIx)) (Tup (Replicate n TIx))) + (AcIdx p a) + -- AcIdx (APArrSlice m) (TArr n a) = + -- -- (index, array shape) + -- TPair (Tup (Replicate m TIx)) (Tup (Replicate n TIx)) + +acPrjTy :: SAcPrj p a b -> STy a -> STy b +acPrjTy SAPHere t = t +acPrjTy (SAPFst prj) (STPair t _) = acPrjTy prj t +acPrjTy (SAPSnd prj) (STPair _ t) = acPrjTy prj t +acPrjTy (SAPLeft prj) (STEither t _) = acPrjTy prj t +acPrjTy (SAPRight prj) (STEither _ t) = acPrjTy prj t +acPrjTy (SAPJust prj) (STMaybe t) = acPrjTy prj t +acPrjTy (SAPArrIdx prj _) (STArr _ t) = acPrjTy prj t |