More stuff

1 files changed, 66 insertions, 39 deletions

diff --git a/src/CHAD.hs b/src/CHAD.hs
index a5f9bb3..209ed3b 100644
--- a/src/CHAD.hs
+++ b/src/CHAD.hs
@@ -12,6 +12,7 @@
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE UndecidableInstances #-}
 module CHAD where
 
 import Data.Bifunctor (first, second)
@@ -38,6 +39,10 @@ weakenBindings wf w (BPush b (t, x)) =
   let (b', w') = weakenBindings wf w b
   in (BPush b' (t, wf w' x), WCopy w')
 
+sinkOver :: SList STy ts -> env :> Append ts env
+sinkOver SNil = WId
+sinkOver (SCons _ ts) = WSink .> sinkOver ts
+
 sinkWithBindings :: Bindings f env binds -> env :> Append binds env
 sinkWithBindings BTop = WId
 sinkWithBindings (BPush b _) = WSink .> sinkWithBindings b
@@ -53,8 +58,16 @@ bconcat b1 (BPush (b2 :: Bindings f (Append binds1 env) binds2C) (t, x))
 --          -> (forall env12. Bindings f env env12 -> r) -> r
 -- bconcat' wf b1 b2 k = weakenBindings wf (sinkWithBindings b1) b2 $ \b2' _ -> k (bconcat b1 b2')
 
--- bsnoc :: STy t -> f env t -> Bindings f (t : env) env' -> Bindings f env env'
--- bsnoc t x b = bconcat (BTop `BPush` (t, x)) b
+type family Snoc l x where
+  Snoc '[] x = '[x]
+  Snoc (y : ys) x = y : Snoc ys x
+
+bsnoc :: (forall env1 env2 t'. env1 :> env2 -> f env1 t' -> f env2 t')
+      -> STy t -> f env t -> Bindings f env binds -> (Bindings f env (Snoc binds t), Append binds env :> Append (Snoc binds t) env)
+bsnoc _ t x BTop = (BPush BTop (t, x), WSink)
+bsnoc wf t x (BPush b (t', y)) =
+  let (b', w) = bsnoc wf t x b
+  in (BPush b' (t', wf w y), WCopy w)
 
 type family Tape binds where
   Tape '[] = TNil
@@ -66,29 +79,41 @@ data TupBinds f env binds =
            (forall env2. Append binds env :> env2 -> Ex env2 (Tape binds))
            (forall env2. Idx env2 (Tape binds) -> Bindings f env2 binds)
 
-tupBinds :: Bindings Ex env binds -> TupBinds Ex env binds
-tupBinds BTop = TupBinds SNil (\_ -> ENil ext) (\_ -> BTop)
-tupBinds (BPush binds (t, _))
-  | TupBinds tapelist collect recon <- tupBinds binds
-  = TupBinds (SCons t tapelist)
-             (\w -> EPair ext (EVar ext t (w @> IZ))
-                              (collect (w .> WSink)))
-             (\tapeidx ->
-                let b = recon tapeidx
-                in BPush _
-                         (t, _ (sinkWithBindings b) tapeidx))
-             -- (\w tapeidx ->
-             --   case recon (WSink .> w) IZ of
-             --     TupBindsReconstruct rebinds wunder ->
-             --       let rebinds1 = bsnoc tape (EFst ext (EVar ext (STPair tape t) tapeidx)) rebinds
-             --       in TupBindsReconstruct
-             --            (rebinds1 `BPush`
-             --              (t, ESnd ext (EVar ext (STPair tape t)
-             --                                 (sinkWithBindings rebinds1 @> tapeidx))))
-             --            (WCopy wunder))
-
-{-
-letBinds :: Bindings Ex env env' -> Ex env' t -> Ex env t
+bindingsBinds :: Bindings f env binds -> SList STy binds
+bindingsBinds BTop = SNil
+bindingsBinds (BPush binds (t, _)) = SCons t (bindingsBinds binds)
+
+tapeTy :: SList STy binds -> STy (Tape binds)
+tapeTy SNil = STNil
+tapeTy (SCons t ts) = STPair t (tapeTy ts)
+
+bindingsCollect :: Bindings f env binds -> Append binds env :> env2 -> Ex env2 (Tape binds)
+bindingsCollect BTop _ = ENil ext
+bindingsCollect (BPush binds (t, _)) w =
+  EPair ext (EVar ext t (w @> IZ))
+            (bindingsCollect binds (w .> WSink))
+
+-- type family TapeUnfoldings binds where
+--   TapeUnfoldings '[] = '[]
+--   TapeUnfoldings (t : ts) = Snoc (TapeUnfoldings ts) (Tape (t : ts))
+
+-- -- The input Ex must be duplicable.
+-- -- This function is quadratic, and returns code whose internal representation is quadratic in size (due to types). It runtime should be linear, however.
+-- tapeUnfoldings :: forall binds env. SList STy binds -> Ex env (Tape binds) -> Bindings Ex env (TapeUnfoldings binds)
+-- tapeUnfoldings SNil _ = BTop
+-- tapeUnfoldings (SCons t ts) e = fst $ bsnoc weakenExpr (tapeTy (SCons t ts)) e (tapeUnfoldings ts (ESnd ext e))
+
+-- reconFromTape :: SList STy binds -> Bindings Ex env (TapeUnfoldings binds) -> Bindings Ex (Append (TapeUnfoldings binds) env) binds
+-- reconFromTape SNil BTop = BTop
+-- reconFromTape (SCons t ts) (BPush unfbinds (_, e)) = _
+-- reconFromTape SCons{} BTop = error "unreachable"
+
+-- TODO: This function produces quadratic code, but it must be linear. Need to fix this!
+reconstructBindings :: SList STy binds -> Ex env (Tape binds) -> Bindings Ex env binds
+reconstructBindings SNil _ = BTop
+reconstructBindings (SCons t ts) e = BPush (reconstructBindings ts (ESnd ext e)) (t, weakenExpr (sinkOver ts) (EFst ext e))
+
+letBinds :: Bindings Ex env binds -> Ex (Append binds env) t -> Ex env t
 letBinds BTop = id
 letBinds (BPush b (_, rhs)) = letBinds b . ELet ext rhs
 
@@ -248,24 +273,25 @@ data Subenv env env' where
 deriving instance Show (Subenv env env')
 
 data Ret env0 sto t =
-  forall justenv env0F.
-    Ret (Bindings Ex (D1E env0) justenv)
-        (Ex (Append justenv (D1E env0)) (D1 t))
-        (Subenv (Select env0 sto "merge") env0F)
-        (Ex (D2 t : justenv) (TEVM (D2E (Select env0 sto "accum")) (Tup (D2E env0F))))
+  forall shbinds env0Merge.
+    Ret (Bindings Ex (D1E env0) shbinds)  -- shared binds
+        (Ex (Append shbinds (D1E env0)) (D1 t))
+        (Subenv (Select env0 sto "merge") env0Merge)
+        (Ex (D2 t : shbinds) (TEVM (D2E (Select env0 sto "accum")) (Tup (D2E env0Merge))))
 deriving instance Show (Ret env0 sto t)
 
 data RetPair env0 sto env t =
-  forall env0F.
+  forall env0Merge.
     RetPair (Ex env (D1 t))
-            (Subenv (Select env0 sto "merge") env0F)
-            (Ex (D2 t : env) (TEVM (D2E (Select env0 sto "accum")) (Tup (D2E env0F))))
+            (Subenv (Select env0 sto "merge") env0Merge)
+            (Ex (D2 t : env) (TEVM (D2E (Select env0 sto "accum")) (Tup (D2E env0Merge))))
 deriving instance Show (RetPair env0 sto env t)
 
+TODO need to fix this data type still, I think?
 data Rets env0 sto env list =
-  forall env'.
-    Rets (Bindings Ex env env')
-         (SList (RetPair env0 sto env') list)
+  forall shbinds.
+    Rets (Bindings Ex env shbinds)
+         (SList (RetPair env0 sto shbinds) list)
 deriving instance Show (Rets env0 sto env list)
 
 subList :: SList f env -> Subenv env env' -> SList f env'
@@ -320,7 +346,7 @@ subenvPlus (SCons t env) (SEYes sub1) (SEYes sub2) k =
                     (ESnd ext (EVar ext (typeOf e1) (IS IZ)))
                     (ESnd ext (EVar ext (typeOf e2) IZ)))
 
-expandSubenvZeros :: SList STy env0 -> Subenv env0 env0F -> Ex env (Tup (D2E env0F)) -> Ex env (Tup (D2E env0))
+expandSubenvZeros :: SList STy env0 -> Subenv env0 env0Merge -> Ex env (Tup (D2E env0Merge)) -> Ex env (Tup (D2E env0))
 expandSubenvZeros _ SETop _ = ENil ext
 expandSubenvZeros (SCons t ts) (SEYes sub) e =
   ELet ext e $
@@ -362,9 +388,9 @@ weakenRets w (Rets binds list) =
   weakenBindings weakenExpr w binds $ \binds' wbinds' ->
     Rets binds' (slistMap (weakenRetPair wbinds') list)
 
-retConcat :: forall env sto list. SList (Ret env sto) list -> Rets env sto (D1E env) list
+retConcat :: forall env0 sto list. SList (Ret env0 sto) list -> Rets env0 sto (D1E env0) list
 retConcat SNil = Rets BTop SNil
-retConcat (SCons (Ret (b :: Bindings Ex (D1E env) env2) p sub d) list)
+retConcat (SCons (Ret (b :: Bindings Ex (D1E env0) env2) p sub d) list)
   | Rets binds pairs <- weakenRets (sinkWithBindings b) (retConcat list)
   = Rets (bconcat b binds)
          (SCons (RetPair (weakenExpr (sinkWithBindings binds) p)
@@ -455,6 +481,7 @@ d2e :: SList STy env -> SList STy (D2E env)
 d2e SNil = SNil
 d2e (SCons t ts) = SCons (d2 t) (d2e ts)
 
+{-
 drev :: forall env sto t.
         Descr env sto
      -> (forall env' sto' t'. Descr env' sto' -> STy t' -> Some Storage)