From ad2aeb613af02c9f59b0301540473742914b47e7 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Mon, 2 Sep 2024 21:38:04 +0200
Subject: WSwap needs no env singleton
---
src/AST/Weaken.hs | 20 ++++++++++++++------
src/AST/Weaken/Auto.hs | 6 +-----
2 files changed, 15 insertions(+), 11 deletions(-)
(limited to 'src/AST')
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs
index aa88c8e..e0b5232 100644
--- a/src/AST/Weaken.hs
+++ b/src/AST/Weaken.hs
@@ -46,7 +46,7 @@ data env :> env' where
WIdx :: Idx env t -> (t : env) :> env
WPick :: forall t pre env env'. SList (Const ()) pre -> env :> env'
-> Append pre (t : env) :> t : Append pre env'
- WSwap :: SList (Const ()) as -> SList (Const ()) bs -> SList (Const ()) env
+ WSwap :: forall env as bs. SList (Const ()) as -> SList (Const ()) bs
-> Append as (Append bs env) :> Append bs (Append as env)
deriving instance Show (env :> env')
infix 4 :>
@@ -65,12 +65,20 @@ WIdx _ @> IS i = i
WPick SNil w @> i = WCopy w @> i
WPick (_ `SCons` _) _ @> IZ = IS IZ
WPick @t (_ `SCons` pre) w @> IS i = WCopy WSink .> WPick @t pre w @> i
-WSwap (as :: SList _ as) (bs :: SList _ bs) (env :: SList _ env) @> i =
+WSwap @env (as :: SList _ as) (bs :: SList _ bs) @> i =
case splitIdx @(Append bs env) as i of
- Left i' -> wSinks bs .> wRaiseAbove as env @> i'
- Right j -> case splitIdx @env bs j of
- Left j' -> wRaiseAbove bs (sappend as env) @> j'
- Right k -> wSinks bs .> wSinks as @> k
+ Left i' -> skipOver bs (stack @env i' as)
+ Right i' -> case splitIdx @env bs i' of
+ Left j -> stack @(Append as env) j bs
+ Right j -> skipOver bs (skipOver as j)
+ where
+ skipOver :: SList (Const ()) as' -> Idx bs' t -> Idx (Append as' bs') t
+ skipOver SNil j = j
+ skipOver (_ `SCons` bs') j = IS (skipOver bs' j)
+
+ stack :: forall env' as' t. Idx as' t -> SList (Const ()) as' -> Idx (Append as' env') t
+ stack IZ (_ `SCons` _) = IZ
+ stack (IS j) (_ `SCons` as') = IS (stack @env' j as')
infixr 3 .>
(.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3
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