1 files changed, 44 insertions, 0 deletions
diff --git a/src/AST/Accum.hs b/src/AST/Accum.hs
new file mode 100644
index 0000000..163f1c3
--- /dev/null
+++ b/src/AST/Accum.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module AST.Accum where
+
+import AST.Types
+import Data
+
+
+data AcPrj
+  = APHere
+  | APFst AcPrj
+  | APSnd AcPrj
+  | APLeft AcPrj
+  | APRight AcPrj
+  | APJust AcPrj
+  | APArrIdx AcPrj
+  | APArrSlice Nat
+
+-- | @b@ is a small part of @a@, indicated by the projection.
+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
+  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)
+deriving instance Show (SAcPrj p a b)
+
+type family AcIdx p t where
+  AcIdx APHere t = TNil
+  AcIdx (APFst p) (TPair a b) = AcIdx p a
+  AcIdx (APSnd p) (TPair a b) = AcIdx p b
+  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)