@@ -1,7 +1,9 @@
11module Control.ST
22
3−import Language.Reflection.Utils
43import Control.IOExcept
4+import Language.Reflection.Utils
5+
6+import public Data.Fuel
57
68%default total
79
@@ -394,13 +396,6 @@ runST env (Call prog res_prf) k
394396runST env (Read lbl prf) k = k (lookupEnv prf env) env
395397runST env (Write lbl prf val) k = k () (updateEnv prf env val)
396398
397−export
398−data Fuel = Empty | More (Lazy Fuel)
399−
400−export partial
401−forever : Fuel
402−forever = More forever
403−
404399runSTLoop : Fuel -> Env invars -> STransLoop m a invars outfn ->
405400 (k : (x : a) -> Env (outfn x) -> m b) ->
406401 (onDry : m b) -> m b
@@ -589,10 +584,10 @@ run prog = runST [] prog (\res, env' => pure res)
589584
590585export
591586runLoop : Applicative m => Fuel -> STLoop m a [] ->
592− (onEmpty : m a) ->
587+ (onDry : m a) ->
593588 m a
594−runLoop fuel prog onEmpty
595− = runSTLoop fuel [] prog (\res, env' => pure res) onEmpty
589+runLoop fuel prog onDry
590+ = runSTLoop fuel [] prog (\res, env' => pure res) onDry
596591
597592||| runWith allows running an STrans program with an initial environment,
598593||| which must be consumed.