diff options
Diffstat (limited to 'src/AST/Weaken.hs')
| -rw-r--r-- | src/AST/Weaken.hs | 35 |
1 files changed, 23 insertions, 12 deletions
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs index 78276ca..0a1e4ce 100644 --- a/src/AST/Weaken.hs +++ b/src/AST/Weaken.hs @@ -48,6 +48,9 @@ data env :> env' where -> Append pre (t : env) :> t : Append pre env' WSwap :: forall env as bs. SList (Const ()) as -> SList (Const ()) bs -> Append as (Append bs env) :> Append bs (Append as env) + WStack :: forall as bs env1 env2. SList (Const ()) as -> SList (Const ()) bs + -> as :> bs -> env1 :> env2 + -> Append as env1 :> Append bs env2 deriving instance Show (env :> env') infix 4 :> @@ -67,18 +70,25 @@ WPick (_ `SCons` _) _ @> IZ = IS IZ WPick @t (_ `SCons` pre) w @> IS i = WCopy WSink .> WPick @t pre w @> i WSwap @env (as :: SList _ as) (bs :: SList _ bs) @> i = case splitIdx @(Append bs env) as i of - Left i' -> skipOver bs (stack @env i' as) + Left i' -> indexSinks bs (indexRaiseAbove @env as i') Right i' -> case splitIdx @env bs i' of - Left j -> stack @(Append as env) j bs - Right j -> skipOver bs (skipOver as j) + Left j -> indexRaiseAbove @(Append as env) bs j + Right j -> indexSinks bs (indexSinks as j) +WStack @as @bs @env1 @env2 as bs wlo whi @> i = + case splitIdx @env1 as i of + Left i' -> indexRaiseAbove @env2 bs (wlo @> i') + Right i' -> indexSinks bs (whi @> i') + +indexSinks :: SList f as -> Idx bs t -> Idx (Append as bs) t +indexSinks SNil j = j +indexSinks (_ `SCons` bs') j = IS (indexSinks bs' j) + +indexRaiseAbove :: forall env as t f. SList f as -> Idx as t -> Idx (Append as env) t +indexRaiseAbove = flip go where - skipOver :: SList (Const ()) as' -> Idx bs' t -> Idx (Append as' bs') t - skipOver SNil j = j - skipOver (_ `SCons` bs') j = IS (skipOver bs' j) - - stack :: forall env' as' t. Idx as' t -> SList (Const ()) as' -> Idx (Append as' env') t - stack IZ (_ `SCons` _) = IZ - stack (IS j) (_ `SCons` as') = IS (stack @env' j as') + go :: forall as'. Idx as' t -> SList f as' -> Idx (Append as' env) t + go IZ (_ `SCons` _) = IZ + go (IS i) (_ `SCons` as) = IS (go i as) infixr 3 .> (.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3 @@ -100,8 +110,9 @@ wSinksAnd SNil w = w wSinksAnd (SCons _ spine) w = WSink .> wSinksAnd spine w wCopies :: SList f bs -> env1 :> env2 -> Append bs env1 :> Append bs env2 -wCopies SNil w = w -wCopies (SCons _ spine) w = WCopy (wCopies spine w) +wCopies bs w = + let bs' = slistMap (\_ -> Const ()) bs + in WStack bs' bs' WId w wRaiseAbove :: SList f env1 -> SList g env -> env1 :> Append env1 env wRaiseAbove SNil env = WClosed (slistMap (\_ -> Const ()) env) |