@@ -39,37 +39,37 @@ data InState : lbl -> Type -> Resources -> Type where
3939
4040{- Update an entry in a context with a new state -}
4141public export
42−updateCtxt : (ctxt : Resources) ->
43− InState lbl st ctxt -> Type -> Resources
44−updateCtxt (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)
45−updateCtxt (r :: rs) (There x) ty = r :: updateCtxt rs x ty
42+updateRes : (res : Resources) ->
43+ InState lbl st res -> Type -> Resources
44+updateRes (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)
45+updateRes (r :: rs) (There x) ty = r :: updateRes rs x ty
4646
4747{- Remove an entry from a context -}
4848public export
49−drop : (ctxt : Resources) -> (prf : InState lbl st ctxt) ->
49+drop : (res : Resources) -> (prf : InState lbl st res) ->
5050 Resources
5151drop (MkRes lbl st :: rs) Here = rs
5252drop (r :: rs) (There p) = r :: drop rs p
5353
5454{- Proof that a resource state (label/type) is in a context -}
5555public export
56−data ElemCtxt : Resource -> Resources -> Type where
57− HereCtxt : ElemCtxt a (a :: as)
58− ThereCtxt : ElemCtxt a as -> ElemCtxt a (b :: as)
56+data ElemRes : Resource -> Resources -> Type where
57+ HereRes : ElemRes a (a :: as)
58+ ThereRes : ElemRes a as -> ElemRes a (b :: as)
5959
6060public export %error_reduce
61−dropEl : (ys: _) -> ElemCtxt x ys -> Resources
62−dropEl (x :: as) HereCtxt = as
63−dropEl (x :: as) (ThereCtxt p) = x :: dropEl as p
61+dropEl : (ys: _) -> ElemRes x ys -> Resources
62+dropEl (x :: as) HereRes = as
63+dropEl (x :: as) (ThereRes p) = x :: dropEl as p
6464
6565{- Proof that a variable name is in a context -}
6666public export
67−data VarInCtxt : Var -> Resources -> Type where
68− VarHere : VarInCtxt a (MkRes a st :: as)
69− VarThere : VarInCtxt a as -> VarInCtxt a (b :: as)
67+data VarInRes : Var -> Resources -> Type where
68+ VarHere : VarInRes a (MkRes a st :: as)
69+ VarThere : VarInRes a as -> VarInRes a (b :: as)
7070
7171public export %error_reduce
72−dropVarIn : (ys: _) -> VarInCtxt x ys -> Resources
72+dropVarIn : (ys: _) -> VarInRes x ys -> Resources
7373dropVarIn ((MkRes x _) :: as) VarHere = as
7474dropVarIn (x :: as) (VarThere p) = x :: dropVarIn as p
7575
@@ -85,77 +85,77 @@ namespace VarList
8585 (::) : Var -> VarList ts -> VarList (t :: ts)
8686
8787 public export
88− mkCtxt : VarList tys -> Resources
89− mkCtxt [] = []
90− mkCtxt {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkCtxt vs
88+ mkRes : VarList tys -> Resources
89+ mkRes [] = []
90+ mkRes {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkRes vs
9191
92−{- Proof that a context is a subset of another context -}
92+{- Proof that a list of resources is a subset of another list -}
9393public export
94−data SubCtxt : Resources -> Resources -> Type where
95− SubNil : SubCtxt [] []
96− Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
97− InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->
98− SubCtxt (x :: xs) ys
94+data SubRes : Resources -> Resources -> Type where
95+ SubNil : SubRes [] []
96+ Skip : SubRes xs ys -> SubRes xs (y :: ys)
97+ InRes : (el : ElemRes x ys) -> SubRes xs (dropEl ys el) ->
98+ SubRes (x :: xs) ys
9999
100100%hint
101101public export
102−subCtxtId : SubCtxt xs xs
103−subCtxtId {xs = []} = SubNil
104−subCtxtId {xs = (x :: xs)} = InCtxt HereCtxt subCtxtId
102+subResId : SubRes xs xs
103+subResId {xs = []} = SubNil
104+subResId {xs = (x :: xs)} = InRes HereRes subResId
105105
106106public export
107−subCtxtNil : SubCtxt [] xs
108−subCtxtNil {xs = []} = SubNil
109−subCtxtNil {xs = (x :: xs)} = Skip subCtxtNil
107+subResNil : SubRes [] xs
108+subResNil {xs = []} = SubNil
109+subResNil {xs = (x :: xs)} = Skip subResNil
110110
111111{- Proof that every variable in the list appears once in the context -}
112112public export
113113data VarsIn : List Var -> Resources -> Type where
114114 VarsNil : VarsIn [] []
115115 SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
116− InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->
116+ InResVar : (el : VarInRes x ys) -> VarsIn xs (dropVarIn ys el) ->
117117 VarsIn (x :: xs) ys
118118
119119public export
120−Uninhabited (ElemCtxt x []) where
121− uninhabited HereCtxt impossible
122− uninhabited (ThereCtxt _) impossible
120+Uninhabited (ElemRes x []) where
121+ uninhabited HereRes impossible
122+ uninhabited (ThereRes _) impossible
123123
124124public export %error_reduce
125125updateWith : (new : Resources) -> (xs : Resources) ->
126− SubCtxt ys xs -> Resources
126+ SubRes ys xs -> Resources
127127-- At the end, add the ones which were updated by the subctxt
128128updateWith new [] SubNil = new
129−updateWith new [] (InCtxt el z) = absurd el
129+updateWith new [] (InRes el z) = absurd el
130130-- Don't add the ones which were consumed by the subctxt
131−updateWith [] (x :: xs) (InCtxt el p)
131+updateWith [] (x :: xs) (InRes el p)
132132 = updateWith [] (dropEl _ el) p
133133-- A new item corresponding to an existing thing
134−updateWith (n :: ns) (x :: xs) (InCtxt el p)
134+updateWith (n :: ns) (x :: xs) (InRes el p)
135135 = n :: updateWith ns (dropEl _ el) p
136136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
137137
138138public export
139−getVarType : (xs : Resources) -> VarInCtxt v xs -> Type
139+getVarType : (xs : Resources) -> VarInRes v xs -> Type
140140getVarType ((MkRes v st) :: as) VarHere = st
141141getVarType (b :: as) (VarThere x) = getVarType as x
142142
143143public export
144144getCombineType : VarsIn ys xs -> List Type
145145getCombineType VarsNil = []
146−getCombineType (InCtxtVar el y) = getVarType _ el :: getCombineType y
146+getCombineType (InResVar el y) = getVarType _ el :: getCombineType y
147147getCombineType (SkipVar x) = getCombineType x
148148
149149public export
150−dropCombined : VarsIn vs ctxt -> Resources
151−dropCombined {ctxt = []} VarsNil = []
152−dropCombined {ctxt} (InCtxtVar el y) = dropCombined y
153−dropCombined {ctxt = (y :: ys)} (SkipVar x) = y :: dropCombined x
150+dropCombined : VarsIn vs res -> Resources
151+dropCombined {res = []} VarsNil = []
152+dropCombined {res} (InResVar el y) = dropCombined y
153+dropCombined {res = (y :: ys)} (SkipVar x) = y :: dropCombined x
154154
155155public export
156−combineVarsIn : (ctxt : Resources) -> VarsIn (comp :: vs) ctxt -> Resources
157−combineVarsIn {comp} ctxt (InCtxtVar el x)
158− = ((comp ::: Composite (getCombineType x)) :: dropCombined (InCtxtVar el x))
156+combineVarsIn : (res : Resources) -> VarsIn (comp :: vs) res -> Resources
157+combineVarsIn {comp} res (InResVar el x)
158+ = ((comp ::: Composite (getCombineType x)) :: dropCombined (InResVar el x))
159159combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x
160160
161161namespace Env
@@ -168,51 +168,51 @@ namespace Env
168168 (++) [] ys = ys
169169 (++) (x :: xs) ys = x :: xs ++ ys
170170
171−lookupEnv : InState lbl ty ctxt -> Env ctxt -> ty
171+lookupEnv : InState lbl ty res -> Env res -> ty
172172lookupEnv Here (x :: xs) = x
173173lookupEnv (There p) (x :: xs) = lookupEnv p xs
174174
175−updateEnv : (prf : InState lbl ty ctxt) -> Env ctxt -> ty' ->
176− Env (updateCtxt ctxt prf ty')
175+updateEnv : (prf : InState lbl ty res) -> Env res -> ty' ->
176+ Env (updateRes res prf ty')
177177updateEnv Here (x :: xs) val = val :: xs
178178updateEnv (There p) (x :: xs) val = x :: updateEnv p xs val
179179
180−dropVal : (prf : InState lbl st ctxt) -> Env ctxt -> Env (drop ctxt prf)
180+dropVal : (prf : InState lbl st res) -> Env res -> Env (drop res prf)
181181dropVal Here (x :: xs) = xs
182182dropVal (There p) (x :: xs) = x :: dropVal p xs
183183
184−envElem : ElemCtxt x xs -> Env xs -> Env [x]
185−envElem HereCtxt (x :: xs) = [x]
186−envElem (ThereCtxt p) (x :: xs) = envElem p xs
184+envElem : ElemRes x xs -> Env xs -> Env [x]
185+envElem HereRes (x :: xs) = [x]
186+envElem (ThereRes p) (x :: xs) = envElem p xs
187187
188−dropDups : Env xs -> (el : ElemCtxt x xs) -> Env (dropEl xs el)
189−dropDups (y :: ys) HereCtxt = ys
190−dropDups (y :: ys) (ThereCtxt p) = y :: dropDups ys p
188+dropDups : Env xs -> (el : ElemRes x xs) -> Env (dropEl xs el)
189+dropDups (y :: ys) HereRes = ys
190+dropDups (y :: ys) (ThereRes p) = y :: dropDups ys p
191191
192192
193−dropEntry : Env ctxt -> (prf : VarInCtxt x ctxt) -> Env (dropVarIn ctxt prf)
193+dropEntry : Env res -> (prf : VarInRes x res) -> Env (dropVarIn res prf)
194194dropEntry (x :: env) VarHere = env
195195dropEntry (x :: env) (VarThere y) = x :: dropEntry env y
196196
197−dropVarsIn : Env ctxt -> (prf : VarsIn vs ctxt) -> Env (dropCombined prf)
197+dropVarsIn : Env res -> (prf : VarsIn vs res) -> Env (dropCombined prf)
198198dropVarsIn [] VarsNil = []
199−dropVarsIn env (InCtxtVar el z) = dropVarsIn (dropEntry env el) z
199+dropVarsIn env (InResVar el z) = dropVarsIn (dropEntry env el) z
200200dropVarsIn (x :: env) (SkipVar z) = x :: dropVarsIn env z
201201
202−getVarEntry : Env ctxt -> (prf : VarInCtxt v ctxt) -> getVarType ctxt prf
202+getVarEntry : Env res -> (prf : VarInRes v res) -> getVarType res prf
203203getVarEntry (x :: xs) VarHere = x
204204getVarEntry (x :: env) (VarThere p) = getVarEntry env p
205205
206−mkComposite : Env ctxt -> (prf : VarsIn vs ctxt) -> Composite (getCombineType prf)
206+mkComposite : Env res -> (prf : VarsIn vs res) -> Composite (getCombineType prf)
207207mkComposite [] VarsNil = CompNil
208−mkComposite env (InCtxtVar el z)
208+mkComposite env (InResVar el z)
209209 = CompCons (getVarEntry env el) (mkComposite (dropEntry env el) z)
210210mkComposite (x :: env) (SkipVar z) = mkComposite env z
211211
212−rebuildVarsIn : Env ctxt -> (prf : VarsIn (comp :: vs) ctxt) ->
213− Env (combineVarsIn ctxt prf)
214−rebuildVarsIn env (InCtxtVar el p)
215− = mkComposite (dropEntry env el) p :: dropVarsIn env (InCtxtVar el p)
212+rebuildVarsIn : Env res -> (prf : VarsIn (comp :: vs) res) ->
213+ Env (combineVarsIn res prf)
214+rebuildVarsIn env (InResVar el p)
215+ = mkComposite (dropEntry env el) p :: dropVarsIn env (InResVar el p)
216216rebuildVarsIn (x :: env) (SkipVar p) = x :: rebuildVarsIn env p
217217
218218{- Some things to make STrans interfaces look prettier -}
@@ -264,9 +264,9 @@ addIfJust : Type -> Action (Maybe a)
264264addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
265265
266266public export
267−kept : SubCtxt xs ys -> Resources
267+kept : SubRes xs ys -> Resources
268268kept SubNil = []
269−kept (InCtxt el p) = kept p
269+kept (InRes el p) = kept p
270270kept (Skip {y} p) = y :: kept p
271271
272272-- We can only use new/delete/read/write on things wrapped in State. Only an
@@ -287,41 +287,41 @@ data STrans : (m : Type -> Type) ->
287287 ((result : a) ->
288288 STrans m b (st2_fn result) st3_fn) ->
289289 STrans m b st1 st3_fn
290− Lift : Monad m => m t -> STrans m t ctxt (const ctxt)
290+ Lift : Monad m => m t -> STrans m t res (const res)
291291 RunAs : Applicative m => STrans m t in_res (const out_res) ->
292292 STrans m (m t) in_res (const out_res)
293293
294294 New : (val : state) ->
295− STrans m Var ctxt (\lbl => (lbl ::: state) :: ctxt)
295+ STrans m Var res (\lbl => (lbl ::: state) :: res)
296296 Delete : (lbl : Var) ->
297− (prf : InState lbl st ctxt) ->
298− STrans m () ctxt (const (drop ctxt prf))
299− DropSubCtxt : (prf : SubCtxt ys xs) ->
300− STrans m (Env ys) xs (const (kept prf))
297+ (prf : InState lbl st res) ->
298+ STrans m () res (const (drop res prf))
299+ DropSubRes : (prf : SubRes ys xs) ->
300+ STrans m (Env ys) xs (const (kept prf))
301301
302302 Split : (lbl : Var) ->
303− (prf : InState lbl (Composite vars) ctxt) ->
304− STrans m (VarList vars) ctxt
305− (\ vs => mkCtxt vs ++
306− updateCtxt ctxt prf (State ()))
303+ (prf : InState lbl (Composite vars) res) ->
304+ STrans m (VarList vars) res
305+ (\ vs => mkRes vs ++
306+ updateRes res prf (State ()))
307307 Combine : (comp : Var) -> (vs : List Var) ->
308− (prf : VarsIn (comp :: vs) ctxt) ->
309− STrans m () ctxt
310− (const (combineVarsIn ctxt prf))
308+ (prf : VarsIn (comp :: vs) res) ->
309+ STrans m () res
310+ (const (combineVarsIn res prf))
311311 ToEnd : (lbl : Var) ->
312− (prf : InState lbl state ctxt) ->
313− STrans m () ctxt (const (drop ctxt prf ++ [lbl ::: state]))
312+ (prf : InState lbl state res) ->
313+ STrans m () res (const (drop res prf ++ [lbl ::: state]))
314314
315− Call : STrans m t sub new_f -> (ctxt_prf : SubCtxt sub old) ->
316− STrans m t old (\res => updateWith (new_f res) old ctxt_prf)
315+ Call : STrans m t sub new_f -> (res_prf : SubRes sub old) ->
316+ STrans m t old (\res => updateWith (new_f res) old res_prf)
317317
318318 Read : (lbl : Var) ->
319− (prf : InState lbl ty ctxt) ->
320− STrans m ty ctxt (const ctxt)
319+ (prf : InState lbl ty res) ->
320+ STrans m ty res (const res)
321321 Write : (lbl : Var) ->
322− (prf : InState lbl ty ctxt) ->
322+ (prf : InState lbl ty res) ->
323323 (val : ty') ->
324− STrans m () ctxt (const (updateCtxt ctxt prf ty'))
324+ STrans m () res (const (updateRes res prf ty'))
325325
326326namespace Loop
327327 export
@@ -333,27 +333,27 @@ namespace Loop
333333 Pure : (result : ty) -> STransLoop m ty (out_fn result) out_fn
334334
335335export
336−dropEnv : Env ys -> SubCtxt xs ys -> Env xs
336+dropEnv : Env ys -> SubRes xs ys -> Env xs
337337dropEnv [] SubNil = []
338−dropEnv [] (InCtxt idx rest) = absurd idx
339−dropEnv (z :: zs) (InCtxt idx rest)
338+dropEnv [] (InRes idx rest) = absurd idx
339+dropEnv (z :: zs) (InRes idx rest)
340340 = let [e] = envElem idx (z :: zs) in
341341 e :: dropEnv (dropDups (z :: zs) idx) rest
342342dropEnv (z :: zs) (Skip p) = dropEnv zs p
343343
344−keepEnv : Env ys -> (prf : SubCtxt xs ys) -> Env (kept prf)
344+keepEnv : Env ys -> (prf : SubRes xs ys) -> Env (kept prf)
345345keepEnv env SubNil = env
346−keepEnv env (InCtxt el prf) = keepEnv (dropDups env el) prf
346+keepEnv env (InRes el prf) = keepEnv (dropDups env el) prf
347347keepEnv (z :: zs) (Skip prf) = z :: keepEnv zs prf
348348
349349-- Corresponds pretty much exactly to 'updateWith'
350−rebuildEnv : Env new -> Env old -> (prf : SubCtxt sub old) ->
350+rebuildEnv : Env new -> Env old -> (prf : SubRes sub old) ->
351351 Env (updateWith new old prf)
352352rebuildEnv new [] SubNil = new
353−rebuildEnv new [] (InCtxt el p) = absurd el
354−rebuildEnv [] (x :: xs) (InCtxt el p)
353+rebuildEnv new [] (InRes el p) = absurd el
354+rebuildEnv [] (x :: xs) (InRes el p)
355355 = rebuildEnv [] (dropDups (x :: xs) el) p
356−rebuildEnv (e :: es) (x :: xs) (InCtxt el p)
356+rebuildEnv (e :: es) (x :: xs) (InRes el p)
357357 = e :: rebuildEnv es (dropDups (x :: xs) el) p
358358rebuildEnv new (x :: xs) (Skip p) = x :: rebuildEnv new xs p
359359
@@ -368,7 +368,7 @@ runST env (Lift action) k
368368runST env (RunAs prog) k = runST env prog (\res, env' => k (pure res) env')
369369runST env (New val) k = k MkVar (val :: env)
370370runST env (Delete lbl prf) k = k () (dropVal prf env)
371−runST env (DropSubCtxt prf) k = k (dropEnv env prf) (keepEnv env prf)
371+runST env (DropSubRes prf) k = k (dropEnv env prf) (keepEnv env prf)
372372runST env (Split lbl prf) k = let val = lookupEnv prf env
373373 env' = updateEnv prf env (Value ()) in
374374 k (mkVars val) (addToEnv val env')
@@ -377,15 +377,15 @@ runST env (Split lbl prf) k = let val = lookupEnv prf env
377377 mkVars CompNil = []
378378 mkVars (CompCons x xs) = MkVar :: mkVars xs
379379
380− addToEnv : (comp : Composite ts) -> Env xs -> Env (mkCtxt (mkVars comp) ++ xs)
380+ addToEnv : (comp : Composite ts) -> Env xs -> Env (mkRes (mkVars comp) ++ xs)
381381 addToEnv CompNil env = env
382382 addToEnv (CompCons x xs) env = x :: addToEnv xs env
383383runST env (ToEnd var prf) k = k () (dropVal prf env ++ [lookupEnv prf env])
384384runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)
385−runST env (Call prog ctxt_prf) k
386− = let env' = dropEnv env ctxt_prf in
385+runST env (Call prog res_prf) k
386+ = let env' = dropEnv env res_prf in
387387 runST env' prog
388− (\prog', envk => k prog' (rebuildEnv envk env ctxt_prf))
388+ (\prog', envk => k prog' (rebuildEnv envk env res_prf))
389389runST env (Read lbl prf) k = k (lookupEnv prf env) env
390390runST env (Write lbl prf val) k = k () (updateEnv prf env val)
391391
@@ -415,14 +415,14 @@ export
415415(>>=) = Bind
416416
417417export
418−returning : (result : ty) -> STrans m () ctxt (const (out_fn result)) ->
419− STrans m ty ctxt out_fn
418+returning : (result : ty) -> STrans m () res (const (out_fn result)) ->
419+ STrans m ty res out_fn
420420returning res prog = do prog
421421 pure res
422422
423423
424424export
425−lift : Monad m => m t -> STrans m t ctxt (const ctxt)
425+lift : Monad m => m t -> STrans m t res (const res)
426426lift = Lift
427427
428428export
@@ -432,69 +432,69 @@ runAs = RunAs
432432
433433export
434434new : (val : state) ->
435− STrans m Var ctxt (\lbl => (lbl ::: State state) :: ctxt)
435+ STrans m Var res (\lbl => (lbl ::: State state) :: res)
436436new val = New (Value val)
437437
438438export
439439delete : (lbl : Var) ->
440− {auto prf : InState lbl (State st) ctxt} ->
441− STrans m () ctxt (const (drop ctxt prf))
440+ {auto prf : InState lbl (State st) res} ->
441+ STrans m () res (const (drop res prf))
442442delete lbl {prf} = Delete lbl prf
443443
444444-- Keep only a subset of the current set of resources. Returns the
445445-- environment corresponding to the dropped portion.
446446export
447−dropSubCtxt : {auto prf : SubCtxt ys xs} ->
448− STrans m (Env ys) xs (const (kept prf))
449−dropSubCtxt {prf} = DropSubCtxt prf
447+dropSub : {auto prf : SubRes ys xs} ->
448+ STrans m (Env ys) xs (const (kept prf))
449+dropSub {prf} = DropSubRes prf
450450
451451export
452452split : (lbl : Var) ->
453− {auto prf : InState lbl (Composite vars) ctxt} ->
454− STrans m (VarList vars) ctxt
455− (\ vs => mkCtxt vs ++
456− updateCtxt ctxt prf (State ()))
453+ {auto prf : InState lbl (Composite vars) res} ->
454+ STrans m (VarList vars) res
455+ (\ vs => mkRes vs ++
456+ updateRes res prf (State ()))
457457split lbl {prf} = Split lbl prf
458458
459459export
460460combine : (comp : Var) -> (vs : List Var) ->
461− {auto prf : InState comp (State ()) ctxt} ->
462− {auto var_prf : VarsIn (comp :: vs) ctxt} ->
463− STrans m () ctxt
464− (const (combineVarsIn ctxt var_prf))
461+ {auto prf : InState comp (State ()) res} ->
462+ {auto var_prf : VarsIn (comp :: vs) res} ->
463+ STrans m () res
464+ (const (combineVarsIn res var_prf))
465465combine comp vs {var_prf} = Combine comp vs var_prf
466466
467467export
468468toEnd : (lbl : Var) ->
469− {auto prf : InState lbl state ctxt} ->
470− STrans m () ctxt (const (drop ctxt prf ++ [lbl ::: state]))
469+ {auto prf : InState lbl state res} ->
470+ STrans m () res (const (drop res prf ++ [lbl ::: state]))
471471toEnd lbl {prf} = ToEnd lbl prf
472472
473473export -- implicit ???
474474call : STrans m t sub new_f ->
475− {auto ctxt_prf : SubCtxt sub old} ->
476− STrans m t old (\res => updateWith (new_f res) old ctxt_prf)
477−call prog {ctxt_prf} = Call prog ctxt_prf
475+ {auto res_prf : SubRes sub old} ->
476+ STrans m t old (\res => updateWith (new_f res) old res_prf)
477+call prog {res_prf} = Call prog res_prf
478478
479479export
480480read : (lbl : Var) ->
481− {auto prf : InState lbl (State ty) ctxt} ->
482− STrans m ty ctxt (const ctxt)
481+ {auto prf : InState lbl (State ty) res} ->
482+ STrans m ty res (const res)
483483read lbl {prf} = do Value x <- Read lbl prf
484484 pure x
485485
486486export
487487write : (lbl : Var) ->
488− {auto prf : InState lbl ty ctxt} ->
488+ {auto prf : InState lbl ty res} ->
489489 (val : ty') ->
490− STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
490+ STrans m () res (const (updateRes res prf (State ty')))
491491write lbl {prf} val = Write lbl prf (Value val)
492492
493493export
494494update : (lbl : Var) ->
495− {auto prf : InState lbl (State ty) ctxt} ->
495+ {auto prf : InState lbl (State ty) res} ->
496496 (ty -> ty') ->
497− STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
497+ STrans m () res (const (updateRes res prf (State ty')))
498498update lbl f = do x <- read lbl
499499 write lbl (f x)
500500
@@ -575,15 +575,15 @@ runLoop fuel prog onEmpty
575575||| responsibility of an implementation of an interface in IO which uses it
576576||| to ensure that it isn't duplicated.
577577export
578−runWith : {ctxtf : _} ->
579− Env ctxt -> STrans IO a ctxt (\res => ctxtf res) ->
580− IO (res ** Env (ctxtf res))
578+runWith : {resf : _} ->
579+ Env res -> STrans IO a res (\result => resf result) ->
580+ IO (result ** Env (resf result))
581581runWith env prog = runST env prog (\res, env' => pure (res ** env'))
582582
583583export
584−runWithLoop : {ctxtf : _} ->
585− Env ctxt -> Fuel -> STransLoop IO a ctxt (\res => ctxtf res) ->
586− IO (Maybe (res ** Env (ctxtf res)))
584+runWithLoop : {resf : _} ->
585+ Env res -> Fuel -> STransLoop IO a res (\result => resf result) ->
586+ IO (Maybe (result ** Env (resf result)))
587587runWithLoop env fuel prog
588588 = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))
589589 (pure Nothing)
@@ -597,7 +597,7 @@ runPure prog = runST [] prog (\res, env' => res)
597597%error_handler
598598export
599599st_precondition : Err -> Maybe (List ErrorReportPart)
600−st_precondition (CantSolveGoal `(SubCtxt ~sub ~all) _)
600+st_precondition (CantSolveGoal `(SubRes ~sub ~all) _)
601601 = pure
602602 [TextPart "'call' is not valid here. ",
603603 TextPart "The operation has preconditions ",