@@ -284,6 +284,8 @@ data STrans : (m : Type -> Type) ->
284 STrans m b (st2_fn result) st3_fn) ->
284 STrans m b (st2_fn result) st3_fn) ->
285 STrans m b st1 st3_fn
285 STrans m b st1 st3_fn
286 Lift : Monad m => m t -> STrans m t ctxt (const ctxt)
286 Lift : Monad m => m t -> STrans m t ctxt (const ctxt)
287+ RunAs : Applicative m => STrans m t in_res (const out_res) ->
288+ STrans m (m t) in_res (const out_res)
288 New : (val : state) ->
290 New : (val : state) ->
289 STrans m Var ctxt (\lbl => (lbl ::: state) :: ctxt)
291 STrans m Var ctxt (\lbl => (lbl ::: state) :: ctxt)
@@ -347,6 +349,7 @@ runST env (Bind prog next) k
347runST env (Lift action) k
349runST env (Lift action) k
348 = do res <- action
350 = do res <- action
349 k res env
351 k res env
352+runST env (RunAs prog) k = runST env prog (\res, env' => k (pure res) env')
350runST env (New val) k = k MkVar (val :: env)
353runST env (New val) k = k MkVar (val :: env)
351runST env (Delete lbl prf) k = k () (dropVal prf env)
354runST env (Delete lbl prf) k = k () (dropVal prf env)
352runST env (DropSubCtxt prf) k = k (dropEnv env prf) (keepEnv env prf)
355runST env (DropSubCtxt prf) k = k (dropEnv env prf) (keepEnv env prf)
@@ -384,6 +387,11 @@ export
384lift : Monad m => m t -> STrans m t ctxt (const ctxt)
387lift : Monad m => m t -> STrans m t ctxt (const ctxt)
385lift = Lift
388lift = Lift
391+runAs : Applicative m => STrans m t in_res (const out_res) ->
392+ STrans m (m t) in_res (const out_res)
388new : (val : state) ->
396new : (val : state) ->
389 STrans m Var ctxt (\lbl => (lbl ::: State state) :: ctxt)
397 STrans m Var ctxt (\lbl => (lbl ::: State state) :: ctxt)