diff options
| -rw-r--r-- | src/AST/Weaken.hs | 20 | ||||
| -rw-r--r-- | src/AST/Weaken/Auto.hs | 6 |
2 files changed, 15 insertions, 11 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 diff --git a/src/AST/Weaken/Auto.hs b/src/AST/Weaken/Auto.hs index 93116b8..0deec71 100644 --- a/src/AST/Weaken/Auto.hs +++ b/src/AST/Weaken/Auto.hs @@ -110,10 +110,6 @@ lineariseLayout (LSeg @name :: Layout _ seg) = LinApp (symbolSing @name) LinEnd lineariseLayout (ly1 :++: ly2) = lineariseLayout ly1 `linLayoutAppend` lineariseLayout ly2 -linLayoutEnv :: SSegments segments -> LinLayout segments env -> SList (Const ()) env -linLayoutEnv _ LinEnd = SNil -linLayoutEnv segs (LinApp name lin) = sappend (segmentLookup segs name) (linLayoutEnv segs lin) - pullDown :: SSegments segments -> SSymbol name -> LinLayout segments env -> r -- Name was not found in source -> (forall env'. LinLayout segments env' -> env :> Append (Lookup name segments) env' -> r) @@ -125,7 +121,7 @@ pullDown segs name@SSymbol linlayout kNotFound k = | Just Refl <- sameSymbol name n' -> k lin WId | otherwise -> pullDown segs name lin kNotFound $ \(lin' :: LinLayout _ env') w -> - k (LinApp n' lin') (WSwap (segmentLookup segs n') (segmentLookup segs name) (linLayoutEnv segs lin') + k (LinApp n' lin') (WSwap @env' (segmentLookup segs n') (segmentLookup segs name) .> wCopies (segmentLookup segs n') w) sortLinLayouts :: forall segments env1 env2. |