diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-09-02 21:38:04 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-09-02 21:38:04 +0200 |
| commit | ad2aeb613af02c9f59b0301540473742914b47e7 (patch) | |
| tree | ae5757edd9762eba5fc87485d03faf86002d1574 /src/AST/Weaken/Auto.hs | |
| parent | 54198e8ab3be3b83507c448ffdad27c2491d2161 (diff) | |
WSwap needs no env singleton
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. |