From 137eaa13144c2599ac29da9ebd3af24ac1ce8968 Mon Sep 17 00:00:00 2001
From: Tom Smeding <t.j.smeding@uu.nl>
Date: Fri, 7 Mar 2025 15:11:59 +0100
Subject: WIP revamp accumulator projection type repr

I stopped working on this because I realised that having sparse products
(and coproducts, prehaps) everywhere is a very bad idea in general, and
that we need to fix that first before really being able to do anything
else productive with performance.
---
 src/AST/Accum.hs | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 src/AST/Accum.hs

(limited to 'src/AST/Accum.hs')

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)
-- 
cgit v1.2.3-70-g09d2