@@ -93,9 +93,9 @@ namespace VarList
93public export
93public export
94data SubCtxt : Context -> Context -> Type where
94data SubCtxt : Context -> Context -> Type where
95 SubNil : SubCtxt [] []
95 SubNil : SubCtxt [] []
96+ Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
96 InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->
97 InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->
97 SubCtxt (x :: xs) ys
98 SubCtxt (x :: xs) ys
98− Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
101public export
101public export
@@ -112,9 +112,9 @@ subCtxtNil {xs = (x :: xs)} = Skip subCtxtNil
112public export
112public export
113data VarsIn : List Var -> Context -> Type where
113data VarsIn : List Var -> Context -> Type where
114 VarsNil : VarsIn [] []
114 VarsNil : VarsIn [] []
115+ SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
115 InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->
116 InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->
116 VarsIn (x :: xs) ys
117 VarsIn (x :: xs) ys
117− SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
119public export
119public export
120Uninhabited (ElemCtxt x []) where
120Uninhabited (ElemCtxt x []) where
@@ -130,9 +130,9 @@ updateWith new [] (InCtxt el z) = absurd el
130-- Don't add the ones which were consumed by the subctxt
130-- Don't add the ones which were consumed by the subctxt
131updateWith [] (x :: xs) (InCtxt el p)
131updateWith [] (x :: xs) (InCtxt el p)
132 = updateWith [] (dropEl _ el) p
132 = updateWith [] (dropEl _ el) p
133+-- A new item corresponding to an existing thing
133updateWith (n :: ns) (x :: xs) (InCtxt el p)
134updateWith (n :: ns) (x :: xs) (InCtxt el p)
134 = n :: updateWith ns (dropEl _ el) p
135 = n :: updateWith ns (dropEl _ el) p
135−-- Do add the ones we didn't use in the subctxt
136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
138public export
138public export
@@ -164,6 +164,10 @@ namespace Env
164 Nil : Env []
164 Nil : Env []
165 (::) : ty -> Env xs -> Env ((lbl ::: ty) :: xs)
165 (::) : ty -> Env xs -> Env ((lbl ::: ty) :: xs)
167+ (++) : Env xs -> Env ys -> Env (xs ++ ys)
169+ (++) (x :: xs) ys = x :: xs ++ ys
167lookupEnv : InState lbl ty ctxt -> Env ctxt -> ty
171lookupEnv : InState lbl ty ctxt -> Env ctxt -> ty
168lookupEnv Here (x :: xs) = x
172lookupEnv Here (x :: xs) = x
169lookupEnv (There p) (x :: xs) = lookupEnv p xs
173lookupEnv (There p) (x :: xs) = lookupEnv p xs
@@ -304,6 +308,9 @@ data STrans : (m : Type -> Type) ->
304 (prf : VarsIn (comp :: vs) ctxt) ->
308 (prf : VarsIn (comp :: vs) ctxt) ->
305 STrans m () ctxt
309 STrans m () ctxt
306 (const (combineVarsIn ctxt prf))
310 (const (combineVarsIn ctxt prf))
311+ ToEnd : (lbl : Var) ->
312+ (prf : InState lbl state ctxt) ->
313+ STrans m () ctxt (const (drop ctxt prf ++ [lbl ::: state]))
308 Call : STrans m t sub new_f -> (ctxt_prf : SubCtxt sub old) ->
315 Call : STrans m t sub new_f -> (ctxt_prf : SubCtxt sub old) ->
309 STrans m t old (\res => updateWith (new_f res) old ctxt_prf)
316 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
373 addToEnv : (comp : Composite ts) -> Env xs -> Env (mkCtxt (mkVars comp) ++ xs)
380 addToEnv : (comp : Composite ts) -> Env xs -> Env (mkCtxt (mkVars comp) ++ xs)
374 addToEnv CompNil env = env
381 addToEnv CompNil env = env
375 addToEnv (CompCons x xs) env = x :: addToEnv xs env
382 addToEnv (CompCons x xs) env = x :: addToEnv xs env
383+runST env (ToEnd var prf) k = k () (dropVal prf env ++ [lookupEnv prf env])
376runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)
384runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)
377runST env (Call prog ctxt_prf) k
385runST env (Call prog ctxt_prf) k
378 = let env' = dropEnv env ctxt_prf in
386 = let env' = dropEnv env ctxt_prf in
@@ -448,6 +456,12 @@ combine : (comp : Var) -> (vs : List Var) ->
448 STrans m () ctxt
456 STrans m () ctxt
449 (const (combineVarsIn ctxt var_prf))
457 (const (combineVarsIn ctxt var_prf))
450combine comp vs {var_prf} = Combine comp vs var_prf
458combine comp vs {var_prf} = Combine comp vs var_prf
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
452export -- implicit ???
466export -- implicit ???
453call : STrans m t sub new_f ->
467call : STrans m t sub new_f ->