From 3847c6ae2d5eb581dac88629e7534aa42e143411 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Tue, 22 Oct 2024 23:46:39 +0200
Subject: Fix interpreter bug
---
src/AST/Weaken.hs | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
(limited to 'src/AST/Weaken.hs')
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs
index 0a1e4ce..ecd7bc9 100644
--- a/src/AST/Weaken.hs
+++ b/src/AST/Weaken.hs
@@ -48,7 +48,7 @@ data env :> env' where
-> Append pre (t : env) :> t : Append pre env'
WSwap :: forall env as bs. SList (Const ()) as -> SList (Const ()) bs
-> Append as (Append bs env) :> Append bs (Append as env)
- WStack :: forall as bs env1 env2. SList (Const ()) as -> SList (Const ()) bs
+ WStack :: forall env1 env2 as bs. SList (Const ()) as -> SList (Const ()) bs
-> as :> bs -> env1 :> env2
-> Append as env1 :> Append bs env2
deriving instance Show (env :> env')
@@ -74,7 +74,7 @@ WSwap @env (as :: SList _ as) (bs :: SList _ bs) @> i =
Right i' -> case splitIdx @env bs i' of
Left j -> indexRaiseAbove @(Append as env) bs j
Right j -> indexSinks bs (indexSinks as j)
-WStack @as @bs @env1 @env2 as bs wlo whi @> i =
+WStack @env1 @env2 as bs wlo whi @> i =
case splitIdx @env1 as i of
Left i' -> indexRaiseAbove @env2 bs (wlo @> i')
Right i' -> indexSinks bs (whi @> i')
--
cgit v1.2.3-70-g09d2