Move module hierarchy under CHAD.

1 files changed, 0 insertions, 191 deletions

diff --git a/src/AST/SplitLets.hs b/src/AST/SplitLets.hs
deleted file mode 100644
index 267dd87..0000000
--- a/src/AST/SplitLets.hs
+++ /dev/null
@@ -1,191 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-module AST.SplitLets (splitLets) where
-
-import Data.Type.Equality
-
-import AST
-import AST.Bindings
-import Lemmas
-
-
-splitLets :: Ex env t -> Ex env t
-splitLets = splitLets' (\t i w -> EVar ext t (w @> i))
-
-splitLets' :: (forall a env2. STy a -> Idx env a -> env' :> env2 -> Ex env2 a) -> Ex env t -> Ex env' t
-splitLets' = \sub -> \case
-  EVar _ t i -> sub t i WId
-  ELet _ rhs body -> ELet ext (splitLets' sub rhs) (split1 sub (typeOf rhs) body)
-  ECase x e a b ->
-    let STEither t1 t2 = typeOf e
-    in ECase x (splitLets' sub e) (split1 sub t1 a) (split1 sub t2 b)
-  EMaybe x a b e ->
-    let STMaybe t1 = typeOf e
-    in EMaybe x (splitLets' sub a) (split1 sub t1 b) (splitLets' sub e)
-  ELCase x e a b c ->
-    let STLEither t1 t2 = typeOf e
-    in ELCase x (splitLets' sub e) (splitLets' sub a) (split1 sub t1 b) (split1 sub t2 c)
-  EFold1Inner x cm a b c ->
-    let STArr _ t1 = typeOf c
-    in EFold1Inner x cm (split1 sub (STPair t1 t1) a) (splitLets' sub b) (splitLets' sub c)
-  EFold1InnerD1 x cm a b c ->
-    let STArr _ t1 = typeOf c
-    in EFold1InnerD1 x cm (split1 sub (STPair t1 t1) a) (splitLets' sub b) (splitLets' sub c)
-  EFold1InnerD2 x cm a b c ->
-    let STArr _ tB = typeOf b
-        STArr _ t2 = typeOf c
-    in EFold1InnerD2 x cm (split2 sub tB t2 a) (splitLets' sub b) (splitLets' sub c)
-
-  EPair x a b -> EPair x (splitLets' sub a) (splitLets' sub b)
-  EFst x e -> EFst x (splitLets' sub e)
-  ESnd x e -> ESnd x (splitLets' sub e)
-  ENil x -> ENil x
-  EInl x t e -> EInl x t (splitLets' sub e)
-  EInr x t e -> EInr x t (splitLets' sub e)
-  ENothing x t -> ENothing x t
-  EJust x e -> EJust x (splitLets' sub e)
-  ELNil x t1 t2 -> ELNil x t1 t2
-  ELInl x t e -> ELInl x t (splitLets' sub e)
-  ELInr x t e -> ELInr x t (splitLets' sub e)
-  EConstArr x n t a -> EConstArr x n t a
-  EBuild x n a b -> EBuild x n (splitLets' sub a) (splitLets' (sinkF sub) b)
-  EMap x a b -> EMap x (splitLets' (sinkF sub) a) (splitLets' sub b)
-  ESum1Inner x e -> ESum1Inner x (splitLets' sub e)
-  EUnit x e -> EUnit x (splitLets' sub e)
-  EReplicate1Inner x a b -> EReplicate1Inner x (splitLets' sub a) (splitLets' sub b)
-  EMaximum1Inner x e -> EMaximum1Inner x (splitLets' sub e)
-  EMinimum1Inner x e -> EMinimum1Inner x (splitLets' sub e)
-  EReshape x n a b -> EReshape x n (splitLets' sub a) (splitLets' sub b)
-  EZip x a b -> EZip x (splitLets' sub a) (splitLets' sub b)
-  EConst x t v -> EConst x t v
-  EIdx0 x e -> EIdx0 x (splitLets' sub e)
-  EIdx1 x a b -> EIdx1 x (splitLets' sub a) (splitLets' sub b)
-  EIdx x e es -> EIdx x (splitLets' sub e) (splitLets' sub es)
-  EShape x e -> EShape x (splitLets' sub e)
-  EOp x op e -> EOp x op (splitLets' sub e)
-  ECustom x s t p a b c e1 e2 -> ECustom x s t p a b c (splitLets' sub e1) (splitLets' sub e2)
-  ERecompute x e -> ERecompute x (splitLets' sub e)
-  EWith x t e1 e2 -> EWith x t (splitLets' sub e1) (splitLets' (sinkF sub) e2)
-  EAccum x t p e1 sp e2 e3 -> EAccum x t p (splitLets' sub e1) sp (splitLets' sub e2) (splitLets' sub e3)
-  EZero x t ezi -> EZero x t (splitLets' sub ezi)
-  EDeepZero x t ezi -> EDeepZero x t (splitLets' sub ezi)
-  EPlus x t a b -> EPlus x t (splitLets' sub a) (splitLets' sub b)
-  EOneHot x t p a b -> EOneHot x t p (splitLets' sub a) (splitLets' sub b)
-  EError x t s -> EError x t s
-  where
-    sinkF :: (forall a env2. STy a -> Idx env a -> env' :> env2 -> Ex env2 a)
-          -> STy t -> Idx (b : env) t -> (b : env') :> env3 -> Ex env3 t
-    sinkF _ t IZ w = EVar ext t (w @> IZ)
-    sinkF f t (IS i) w = f t i (w .> WSink)
-
-    split1 :: (forall a env2. STy a -> Idx env a -> env' :> env2 -> Ex env2 a)
-           -> STy bind -> Ex (bind : env) t -> Ex (bind : env') t
-    split1 sub (tbind :: STy bind) body =
-      let (ptrs, bs) = split tbind
-      in letBinds bs $
-           splitLets' (\cases _ IZ w -> subPointers ptrs w
-                              t (IS i) w -> sub t i (WPop @bind (wPops (bindingsBinds bs) w)))
-                      body
-
-    split2 :: forall bind1 bind2 env' env t.
-              (forall a env2. STy a -> Idx env a -> env' :> env2 -> Ex env2 a)
-           -> STy bind1 -> STy bind2 -> Ex (bind2 : bind1 : env) t -> Ex (bind2 : bind1 : env') t
-    split2 sub tbind1 tbind2 body =
-      let (ptrs1', bs1') = split @env' tbind1
-          bs1 = fst (weakenBindingsE WSink bs1')
-          (ptrs2, bs2) = split @(bind1 : env') tbind2
-      in letBinds bs1 $
-         letBinds (fst (weakenBindingsE (sinkWithBindings @(bind2 : bind1 : env') bs1) bs2)) $
-           splitLets' (\cases _ IZ w -> subPointers ptrs2 (w .> wCopies (bindingsBinds bs2) (wSinks @(bind2 : bind1 : env') (bindingsBinds bs1)))
-                              _ (IS IZ) w -> subPointers ptrs1' (w .> wSinks (bindingsBinds bs2) .> wCopies (bindingsBinds bs1) (WSink @bind2 @(bind1 : env')))
-                              t (IS (IS i)) w -> sub t i (WPop @bind1 (WPop @bind2 (wPops (bindingsBinds bs1) (wPops (bindingsBinds bs2) w)))))
-                      body
-
-    -- TODO: abstract this to splitN lol wtf
-    _split4 :: forall bind1 bind2 bind3 bind4 env' env t.
-               (forall a env2. STy a -> Idx env a -> env' :> env2 -> Ex env2 a)
-            -> STy bind1 -> STy bind2 -> STy bind3 -> STy bind4 -> Ex (bind4 : bind3 : bind2 : bind1 : env) t -> Ex (bind4 : bind3 : bind2 : bind1 : env') t
-    _split4 sub tbind1 tbind2 tbind3 tbind4 body =
-      let (ptrs1, bs1') = split @env' tbind1
-          (ptrs2, bs2') = split @(bind1 : env') tbind2
-          (ptrs3, bs3') = split @(bind2 : bind1 : env') tbind3
-          (ptrs4, bs4) = split @(bind3 : bind2 : bind1 : env') tbind4
-          bs1 = fst (weakenBindingsE (WSink .> WSink .> WSink) bs1')
-          bs2 = fst (weakenBindingsE (WSink .> WSink) bs2')
-          bs3 = fst (weakenBindingsE WSink bs3')
-          b1 = bindingsBinds bs1
-          b2 = bindingsBinds bs2
-          b3 = bindingsBinds bs3
-          b4 = bindingsBinds bs4
-      in letBinds bs1 $
-         letBinds (fst (weakenBindingsE (                                                sinkWithBindings @(bind4 : bind3 : bind2 : bind1 : env') bs1) bs2)) $
-         letBinds (fst (weakenBindingsE (                        sinkWithBindings bs2 .> sinkWithBindings @(bind4 : bind3 : bind2 : bind1 : env') bs1) bs3)) $
-         letBinds (fst (weakenBindingsE (sinkWithBindings bs3 .> sinkWithBindings bs2 .> sinkWithBindings @(bind4 : bind3 : bind2 : bind1 : env') bs1) bs4)) $
-           splitLets' (\cases _ IZ w ->                subPointers ptrs4 (w .> wCopies b4 (wSinks b3 .> wSinks b2 .> wSinks @(bind4 : bind3 : bind2 : bind1 : env') b1))
-                              _ (IS IZ) w ->           subPointers ptrs3 (w .> wSinks b4 .> wCopies b3 (wSinks b2 .> wSinks @(bind4 : bind3 : bind2 : bind1 : env') b1 .> WSink))
-                              _ (IS (IS IZ)) w ->      subPointers ptrs2 (w .> wSinks b4 .> wSinks b3 .> wCopies b2 (wSinks @(bind4 : bind3 : bind2 : bind1 : env') b1 .> WSink .> WSink))
-                              _ (IS (IS (IS IZ))) w -> subPointers ptrs1 (w .> wSinks b4 .> wSinks b3 .> wSinks b2 .> wCopies b1 (WSink @bind4 .> WSink @bind3 .> WSink @bind2 @(bind1 : env')))
-                              t (IS (IS (IS (IS i)))) w -> sub t i (WPop @bind1 (WPop @bind2 (WPop @bind3 (WPop @bind4 (wPops b1 (wPops b2 (wPops b3 (wPops b4 w)))))))))
-                      body
-
-type family Split t where
-  Split (TPair a b) = SplitRec (TPair a b)
-  Split _ = '[]
-
-type family SplitRec t where
-  SplitRec TNil = '[]
-  SplitRec (TPair a b) = Append (SplitRec b) (SplitRec a)
-  SplitRec t = '[t]
-
-data Pointers env t where
-  Point :: STy t -> Idx env t -> Pointers env t
-  PNil :: Pointers env TNil
-  PPair :: Pointers env a -> Pointers env b -> Pointers env (TPair a b)
-  PWeak :: env' :> env -> Pointers env' t -> Pointers env t
-
-subPointers :: Pointers env t -> env :> env' -> Ex env' t
-subPointers (Point t i) w = EVar ext t (w @> i)
-subPointers PNil _ = ENil ext
-subPointers (PPair a b) w = EPair ext (subPointers a w) (subPointers b w)
-subPointers (PWeak w' p) w = subPointers p (w .> w')
-
-split :: forall env t. STy t
-      -> (Pointers (Append (Split t) (t : env)) t, Bindings Ex (t : env) (Split t))
-split typ = case typ of
-  STPair{} -> splitRec (EVar ext typ IZ) typ
-  STNil -> other
-  STEither{} -> other
-  STLEither{} -> other
-  STMaybe{} -> other
-  STArr{} -> other
-  STScal{} -> other
-  STAccum{} -> other
-  where
-    other :: (Pointers (t : env) t, Bindings Ex (t : env) '[])
-    other = (Point typ IZ, BTop)
-
-splitRec :: forall env t. Ex env t -> STy t
-         -> (Pointers (Append (SplitRec t) env) t, Bindings Ex env (SplitRec t))
-splitRec rhs typ = case typ of
-  STNil -> (PNil, BTop)
-  STPair (a :: STy a) (b :: STy b)
-    | Refl <- lemAppendAssoc @(SplitRec b) @(SplitRec a) @env ->
-        let (p1, bs1) = splitRec (EFst ext rhs) a
-            (p2, bs2) = splitRec (ESnd ext (sinkWithBindings bs1 `weakenExpr` rhs)) b
-        in (PPair (PWeak (sinkWithBindings bs2) p1) p2, bconcat bs1 bs2)
-  STEither{} -> other
-  STLEither{} -> other
-  STMaybe{} -> other
-  STArr{} -> other
-  STScal{} -> other
-  STAccum{} -> other
-  where
-    other :: (Pointers (t : env) t, Bindings Ex env '[t])
-    other = (Point typ IZ, BPush BTop (typ, rhs))