diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-01-25 21:46:29 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-01-25 21:46:29 +0100 |
| commit | 2a53042c1ce8b593a6178696c03ac77c6b76b395 (patch) | |
| tree | cb7a8a82ac254980d3fbb1911d4a7d891647a561 /src/AST/Weaken.hs | |
| parent | 39b899b4951be5b78058d5c0e35977b065a63951 (diff) | |
Finish rewrite
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) |