diff options
Diffstat (limited to 'src/AST/Weaken/Auto.hs')
| -rw-r--r-- | src/AST/Weaken/Auto.hs | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/AST/Weaken/Auto.hs b/src/AST/Weaken/Auto.hs index eecb6f3..0bf5780 100644 --- a/src/AST/Weaken/Auto.hs +++ b/src/AST/Weaken/Auto.hs @@ -93,6 +93,10 @@ linLayoutAppend (LinApp (name :: SSymbol name) (lin1 :: LinLayout segments env1' | Refl <- lemAppendAssoc @(Lookup name segments) @env1' @env2 = LinApp name (linLayoutAppend lin1 lin2) +linLayoutEnv :: SSegments segments -> LinLayout segments env -> SList (Const ()) env +linLayoutEnv _ LinEnd = SNil +linLayoutEnv segs (LinApp name lin) = sappend (segmentLookup segs name) (linLayoutEnv segs lin) + lineariseLayout :: Layout segments env -> LinLayout segments env lineariseLayout (LSeg @name :: Layout _ seg) | Refl <- lemAppendNil @seg @@ -128,8 +132,8 @@ sortLinLayouts segs lin1@(LinApp name1@SSymbol tail1) (LinApp name2@SSymbol tail -- vs (name2 : tail2). Thus we continue sorting tail1' vs tail2, and -- wCopies the name2 on top of that. wCopies (segmentLookup segs name2) (sortLinLayouts segs tail1' tail2) .> w) -sortLinLayouts _ LinEnd LinApp{} = error "Unequal number of segments: more in target than in source" -sortLinLayouts _ LinApp{} LinEnd = error "Unequal number of segments: more in source than in target" +sortLinLayouts segs LinEnd lin2@LinApp{} = WClosed (linLayoutEnv segs lin2) +sortLinLayouts _ LinApp{} LinEnd = error "Segments in source that do not occur in target" autoWeak :: forall segments env1 env2. SSegments segments -> Layout segments env1 -> Layout segments env2 -> env1 :> env2 |