diff options
Diffstat (limited to 'src/AST/Weaken.hs')
| -rw-r--r-- | src/AST/Weaken.hs | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs index aa88c8e..e0b5232 100644 --- a/src/AST/Weaken.hs +++ b/src/AST/Weaken.hs @@ -46,7 +46,7 @@ data env :> env' where WIdx :: Idx env t -> (t : env) :> env WPick :: forall t pre env env'. SList (Const ()) pre -> env :> env' -> Append pre (t : env) :> t : Append pre env' - WSwap :: SList (Const ()) as -> SList (Const ()) bs -> SList (Const ()) env + WSwap :: forall env as bs. SList (Const ()) as -> SList (Const ()) bs -> Append as (Append bs env) :> Append bs (Append as env) deriving instance Show (env :> env') infix 4 :> @@ -65,12 +65,20 @@ WIdx _ @> IS i = i WPick SNil w @> i = WCopy w @> i WPick (_ `SCons` _) _ @> IZ = IS IZ WPick @t (_ `SCons` pre) w @> IS i = WCopy WSink .> WPick @t pre w @> i -WSwap (as :: SList _ as) (bs :: SList _ bs) (env :: SList _ env) @> i = +WSwap @env (as :: SList _ as) (bs :: SList _ bs) @> i = case splitIdx @(Append bs env) as i of - Left i' -> wSinks bs .> wRaiseAbove as env @> i' - Right j -> case splitIdx @env bs j of - Left j' -> wRaiseAbove bs (sappend as env) @> j' - Right k -> wSinks bs .> wSinks as @> k + Left i' -> skipOver bs (stack @env i' as) + Right i' -> case splitIdx @env bs i' of + Left j -> stack @(Append as env) j bs + Right j -> skipOver bs (skipOver as j) + 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') infixr 3 .> (.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3 |