diff options
Diffstat (limited to 'src/AST/Weaken/Auto.hs')
| -rw-r--r-- | src/AST/Weaken/Auto.hs | 6 |
1 files changed, 1 insertions, 5 deletions
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. |