@@ -93,9 +93,9 @@ namespace VarList
9393public export
9494data SubCtxt : Context -> Context -> Type where
9595 SubNil : SubCtxt [] []
96+ Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
9697 InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->
9798 SubCtxt (x :: xs) ys
98− Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
9999
100100%hint
101101public export
@@ -112,9 +112,9 @@ subCtxtNil {xs = (x :: xs)} = Skip subCtxtNil
112112public export
113113data VarsIn : List Var -> Context -> Type where
114114 VarsNil : VarsIn [] []
115+ SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
115116 InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->
116117 VarsIn (x :: xs) ys
117− SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
118118
119119public export
120120Uninhabited (ElemCtxt x []) where
@@ -130,9 +130,9 @@ updateWith new [] (InCtxt el z) = absurd el
130130-- Don't add the ones which were consumed by the subctxt
131131updateWith [] (x :: xs) (InCtxt el p)
132132 = updateWith [] (dropEl _ el) p
133+-- A new item corresponding to an existing thing
133134updateWith (n :: ns) (x :: xs) (InCtxt el p)
134135 = n :: updateWith ns (dropEl _ el) p
135−-- Do add the ones we didn't use in the subctxt
136136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
137137
138138public export
@@ -164,6 +164,10 @@ namespace Env
164164 Nil : Env []
165165 (::) : ty -> Env xs -> Env ((lbl ::: ty) :: xs)
166166
167+ (++) : Env xs -> Env ys -> Env (xs ++ ys)
168+ (++) [] ys = ys
169+ (++) (x :: xs) ys = x :: xs ++ ys
170+
167171lookupEnv : InState lbl ty ctxt -> Env ctxt -> ty
168172lookupEnv Here (x :: xs) = x
169173lookupEnv (There p) (x :: xs) = lookupEnv p xs
@@ -304,6 +308,9 @@ data STrans : (m : Type -> Type) ->
304308 (prf : VarsIn (comp :: vs) ctxt) ->
305309 STrans m () ctxt
306310 (const (combineVarsIn ctxt prf))
311+ ToEnd : (lbl : Var) ->
312+ (prf : InState lbl state ctxt) ->
313+ STrans m () ctxt (const (drop ctxt prf ++ [lbl ::: state]))
307314
308315 Call : STrans m t sub new_f -> (ctxt_prf : SubCtxt sub old) ->
309316 STrans m t old (\res => updateWith (new_f res) old ctxt_prf)
@@ -373,6 +380,7 @@ runST env (Split lbl prf) k = let val = lookupEnv prf env
373380 addToEnv : (comp : Composite ts) -> Env xs -> Env (mkCtxt (mkVars comp) ++ xs)
374381 addToEnv CompNil env = env
375382 addToEnv (CompCons x xs) env = x :: addToEnv xs env
383+runST env (ToEnd var prf) k = k () (dropVal prf env ++ [lookupEnv prf env])
376384runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)
377385runST env (Call prog ctxt_prf) k
378386 = let env' = dropEnv env ctxt_prf in
@@ -448,6 +456,12 @@ combine : (comp : Var) -> (vs : List Var) ->
448456 STrans m () ctxt
449457 (const (combineVarsIn ctxt var_prf))
450458combine comp vs {var_prf} = Combine comp vs var_prf
459+
460+export
461+toEnd : (lbl : Var) ->
462+ {auto prf : InState lbl state ctxt} ->
463+ STrans m () ctxt (const (drop ctxt prf ++ [lbl ::: state]))
464+toEnd lbl {prf} = ToEnd lbl prf
451465
452466export -- implicit ???
453467call : STrans m t sub new_f ->