From ad2aeb613af02c9f59b0301540473742914b47e7 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Mon, 2 Sep 2024 21:38:04 +0200 Subject: WSwap needs no env singleton --- src/AST/Weaken/Auto.hs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'src/AST/Weaken/Auto.hs') 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. -- cgit v1.2.3-70-g09d2