diff options
Diffstat (limited to 'src/AST/Weaken.hs')
| -rw-r--r-- | src/AST/Weaken.hs | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs index c7668e7..07a90dc 100644 --- a/src/AST/Weaken.hs +++ b/src/AST/Weaken.hs @@ -40,10 +40,14 @@ instance KnownListSpine list => KnownListSpine (t : list) where 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 :: forall env bs f. SList f bs -> env :> Append bs env wSinks SNil = WId wSinks (SCons _ spine) = WSink .> wSinks spine +wCopies :: SList f bs -> env1 :> env2 -> Append bs env1 :> Append bs env2 +wCopies SNil w = w +wCopies (SCons _ spine) w = WCopy (wCopies spine w) + wStack :: forall env b1 b2. b1 :> b2 -> Append b1 env :> Append b2 env wStack WId = WId wStack WSink = WSink @@ -52,6 +56,6 @@ wStack (WPop w) = WPop (wStack @env w) wStack (WThen w1 w2) = WThen (wStack @env w1) (wStack @env w2) wStack (WClosed s) = wSinks s -wRaiseAbove :: SList f env1 -> SList (Const ()) env -> env1 :> Append env1 env -wRaiseAbove SNil env = WClosed env +wRaiseAbove :: SList f env1 -> SList g env -> env1 :> Append env1 env +wRaiseAbove SNil env = WClosed (slistMap (\_ -> Const ()) env) wRaiseAbove (SCons _ s) env = WCopy (wRaiseAbove s env) |