Getting further

1 files changed, 26 insertions, 13 deletions

diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs
index dd121fa..c7668e7 100644
--- a/src/AST/Weaken.hs
+++ b/src/AST/Weaken.hs
@@ -5,12 +5,17 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeApplications #-}
 
 -- The reason why this is a separate module with little in it:
 {-# LANGUAGE AllowAmbiguousTypes #-}
 
 module AST.Weaken where
 
+import Data.Functor.Const
+
+import Data
+
 
 data env :> env' where
   WId :: env :> env
@@ -18,7 +23,7 @@ data env :> env' where
   WCopy :: env :> env' -> (t : env) :> (t : env')
   WPop :: (t : env) :> env' -> env :> env'
   WThen :: env1 :> env2 -> env2 :> env3 -> env1 :> env3
-  WClosed :: '[] :> env
+  WClosed :: SList (Const ()) env -> '[] :> env
 deriving instance Show (env :> env')
 
 (.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3
@@ -28,17 +33,25 @@ type family Append a b where
   Append '[] l = l
   Append (x : xs) l = x : Append xs l
 
-data ListSpine list where
-  LSNil :: ListSpine '[]
-  LSCons :: ListSpine list -> ListSpine (t : list)
+class KnownListSpine list where knownListSpine :: SList (Const ()) list
+instance KnownListSpine '[] where knownListSpine = SNil
+instance KnownListSpine list => KnownListSpine (t : list) where knownListSpine = SCons (Const ()) knownListSpine
+
+wSinks' :: forall list env. KnownListSpine list => env :> Append list env
+wSinks' = wSinks (knownListSpine :: SList (Const ()) list)
+
+wSinks :: SList f list' -> env :> Append list' env
+wSinks SNil = WId
+wSinks (SCons _ spine) = WSink .> wSinks spine
 
-class KnownListSpine list where knownListSpine :: ListSpine list
-instance KnownListSpine '[] where knownListSpine = LSNil
-instance KnownListSpine list => KnownListSpine (t : list) where knownListSpine = LSCons knownListSpine
+wStack :: forall env b1 b2. b1 :> b2 -> Append b1 env :> Append b2 env
+wStack WId = WId
+wStack WSink = WSink
+wStack (WCopy w) = WCopy (wStack @env w)
+wStack (WPop w) = WPop (wStack @env w)
+wStack (WThen w1 w2) = WThen (wStack @env w1) (wStack @env w2)
+wStack (WClosed s) = wSinks s
 
-wSinks :: forall list env. KnownListSpine list => env :> Append list env
-wSinks = go (knownListSpine :: ListSpine list)
-  where
-    go :: forall list'. ListSpine list' -> env :> Append list' env
-    go LSNil = WId
-    go (LSCons spine) = WSink .> go spine
+wRaiseAbove :: SList f env1 -> SList (Const ()) env -> env1 :> Append env1 env
+wRaiseAbove SNil env = WClosed env
+wRaiseAbove (SCons _ s) env = WCopy (wRaiseAbove s env)