diff options
Diffstat (limited to 'src/AST/Weaken')
| -rw-r--r-- | src/AST/Weaken/Auto.hs | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/AST/Weaken/Auto.hs b/src/AST/Weaken/Auto.hs index 8555516..6752c24 100644 --- a/src/AST/Weaken/Auto.hs +++ b/src/AST/Weaken/Auto.hs @@ -118,11 +118,6 @@ linLayoutAppend (LinAppPreW (name1 :: SSymbol name1) name2 w (lin1 :: LinLayout | Refl <- lemAppendAssoc @(Lookup name1 segments) @env1' @env2 = LinAppPreW name1 name2 w (linLayoutAppend lin1 lin2) -linLayoutEnv :: SSegments segments -> LinLayout withPre segments env -> SList (Const ()) env -linLayoutEnv _ LinEnd = SNil -linLayoutEnv segs (LinApp name lin) = sappend (segmentLookup segs name) (linLayoutEnv segs lin) -linLayoutEnv segs (LinAppPreW name1 _ _ lin) = sappend (segmentLookup segs name1) (linLayoutEnv segs lin) - lineariseLayout :: Layout withPre segments env -> LinLayout withPre segments env lineariseLayout (LSeg name :: Layout _ _ seg) | Refl <- lemAppendNil @seg @@ -171,7 +166,7 @@ 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 segs LinEnd lin2@LinApp{} = WClosed (linLayoutEnv segs lin2) +sortLinLayouts _ LinEnd LinApp{} = WClosed sortLinLayouts _ LinApp{} LinEnd = error "Segments in source that do not occur in target" autoWeak :: forall segments env1 env2. |