diff options
Diffstat (limited to 'src/AST/Weaken.hs')
| -rw-r--r-- | src/AST/Weaken.hs | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs index 4b3016d..d992404 100644 --- a/src/AST/Weaken.hs +++ b/src/AST/Weaken.hs @@ -36,7 +36,7 @@ data env :> env' where WIdx :: Idx env t -> (t : env) :> env deriving instance Show (env :> env') -infixr @> +infixr 2 @> (@>) :: env :> env' -> Idx env t -> Idx env' t WId @> i = i WSink @> i = IS i @@ -48,6 +48,7 @@ WClosed _ @> i = case i of {} WIdx j @> IZ = j WIdx _ @> IS i = i +infixr 3 .> (.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3 (.>) = flip WThen @@ -70,14 +71,18 @@ wCopies :: SList f bs -> env1 :> env2 -> Append bs env1 :> Append bs env2 wCopies SNil w = w wCopies (SCons _ spine) w = WCopy (wCopies spine w) --- wStack :: forall env b1 b2. b1 :> b2 -> Append b1 env :> Append b2 env --- wStack WId = WId --- wStack WSink = WSink --- wStack (WCopy w) = WCopy (wStack @env w) --- wStack (WPop w) = WPop (wStack @env w) --- wStack (WThen w1 w2) = WThen (wStack @env w1) (wStack @env w2) --- wStack (WClosed s) = wSinks s --- wStack (WIdx i) = WIdx (_ i) +wStack :: forall env b1 b2. b1 :> b2 -> Append b1 env :> Append b2 env +wStack WId = WId +wStack WSink = WSink +wStack (WCopy w) = WCopy (wStack @env w) +wStack (WPop w) = WPop (wStack @env w) +wStack (WThen w1 w2) = WThen (wStack @env w1) (wStack @env w2) +wStack (WClosed s) = wSinks s +wStack (WIdx i) = WIdx (goIdx i) + where + goIdx :: Idx b t -> Idx (Append b env) t + goIdx IZ = IZ + goIdx (IS i') = IS (goIdx i') wRaiseAbove :: SList f env1 -> SList g env -> env1 :> Append env1 env wRaiseAbove SNil env = WClosed (slistMap (\_ -> Const ()) env) |