diff options
Diffstat (limited to 'src/AST/Weaken.hs')
| -rw-r--r-- | src/AST/Weaken.hs | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs index dbb37f7..d882e28 100644 --- a/src/AST/Weaken.hs +++ b/src/AST/Weaken.hs @@ -36,6 +36,15 @@ splitIdx SNil i = Right i splitIdx (SCons _ _) IZ = Left IZ splitIdx (SCons _ l) (IS i) = first IS (splitIdx l i) +slistIdx :: SList f list -> Idx list t -> f t +slistIdx (SCons x _) IZ = x +slistIdx (SCons _ list) (IS i) = slistIdx list i +slistIdx SNil i = case i of {} + +idx2int :: Idx env t -> Int +idx2int IZ = 0 +idx2int (IS n) = 1 + idx2int n + data env :> env' where WId :: env :> env WSink :: forall t env. env :> (t : env) @@ -117,3 +126,7 @@ wCopies bs w = wRaiseAbove :: SList f env1 -> SList g env -> env1 :> Append env1 env wRaiseAbove SNil _ = WClosed wRaiseAbove (SCons _ s) env = WCopy (wRaiseAbove s env) + +wPops :: SList f bs -> Append bs env1 :> env2 -> env1 :> env2 +wPops SNil w = w +wPops (_ `SCons` bs) w = wPops bs (WPop w) |