IdrisDoc: Control.ST

Control.ST

(:::) : Var -> Type -> Resource
Fixity
Non-associative, precedence 5
(>>=) : STrans m a st1 st2_fn -> ((result : a) -> STrans m b (st2_fn result) st3_fn) -> STrans m b st1 st3_fn
Fixity
Left associative, precedence 1
data Action : Type -> Type
Stable : Var -> Type -> Action ty
Trans : Var -> Type -> (ty -> Type) -> Action ty
Remove : Var -> Type -> Action ty
Add : (ty -> Resources) -> Action ty
data Composite : List Type -> Type
CompNil : Composite []
CompCons : (x : a) -> Composite as -> Composite (a :: as)
interface ConsoleIO 
putStr : ConsoleIO m => String -> STrans m () xs (const xs)
getStr : ConsoleIO m => STrans m String xs (const xs)
putChar : ConsoleIO m => Char -> STrans m () xs (const xs)
getChar : ConsoleIO m => STrans m Char xs (const xs)
data ElemRes : Resource -> Resources -> Type
HereRes : ElemRes a (a :: as)
ThereRes : ElemRes a as -> ElemRes a (b :: as)
data InState : Var -> Type -> Resources -> Type
Here : InState lbl st (MkRes lbl st :: rs)
There : InState lbl st rs -> InState lbl st (r :: rs)
data Resource : Type
MkRes : label -> Type -> Resource
ST : (m : Type -> Type) -> (ty : Type) -> List (Action ty) -> Type
STLoop : (m : Type -> Type) -> (ty : Type) -> List (Action ty) -> Type
data STrans : (m : Type -> Type) -> (ty : Type) -> Resources -> (ty -> Resources) -> Type
Pure : (result : ty) -> STrans m ty (out_fn result) out_fn
Bind : STrans m a st1 st2_fn -> ((result : a) -> STrans m b (st2_fn result) st3_fn) -> STrans m b st1 st3_fn
Lift : Monad m => m t -> STrans m t res (const res)
RunAs : Applicative m => STrans m t in_res (const out_res) -> STrans m (m t) in_res (const out_res)
New : (val : state) -> STrans m Var res (\lbl => (lbl ::: state) :: res)
Delete : (lbl : Var) -> (prf : InState lbl st res) -> STrans m () res (const (drop res prf))
DropSubRes : (prf : SubRes ys xs) -> STrans m (Env ys) xs (const (kept prf))
Split : (lbl : Var) -> (prf : InState lbl (Composite vars) res) -> STrans m (VarList vars) res (\vs => mkRes vs ++ updateRes res prf (State ()))
Combine : (comp : Var) -> (vs : List Var) -> (prf : VarsIn (comp :: vs) res) -> STrans m () res (const (combineVarsIn res prf))
ToEnd : (lbl : Var) -> (prf : InState lbl state res) -> STrans m () res (const (drop res prf ++ [lbl ::: state]))
Call : STrans m t sub new_f -> (res_prf : SubRes sub old) -> STrans m t old (\res => updateWith (new_f res) old res_prf)
Read : (lbl : Var) -> (prf : InState lbl ty res) -> STrans m ty res (const res)
Write : (lbl : Var) -> (prf : InState lbl ty res) -> (val : ty') -> STrans m () res (const (updateRes res prf ty'))
data State : Type -> Type
Value : ty -> State ty
data SubRes : Resources -> Resources -> Type
SubNil : SubRes [] []
Skip : SubRes xs ys -> SubRes xs (y :: ys)
InRes : (el : ElemRes x ys) -> SubRes xs (dropEl ys el) -> SubRes (x :: xs) ys
data Var : Type
MkVar : Var
data VarInRes : Var -> Resources -> Type
VarHere : VarInRes a (MkRes a st :: as)
VarThere : VarInRes a as -> VarInRes a (b :: as)
data VarsIn : List Var -> Resources -> Type
VarsNil : VarsIn [] []
SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
InResVar : (el : VarInRes x ys) -> VarsIn xs (dropVarIn ys el) -> VarsIn (x :: xs) ys
add : Type -> Action Var
addIfJust : Type -> Action (Maybe Var)
addIfRight : Type -> Action (Either a Var)
call : STrans m t sub new_f -> {auto res_prf : SubRes sub old} -> STrans m t old (\res => updateWith (new_f res) old res_prf)
combine : (comp : Var) -> (vs : List Var) -> {auto prf : InState comp (State ()) res} -> {auto var_prf : VarsIn (comp :: vs) res} -> STrans m () res (const (combineVarsIn res var_prf))
combineVarsIn : (res : Resources) -> VarsIn (comp :: vs) res -> Resources
delete : (lbl : Var) -> {auto prf : InState lbl (State st) res} -> STrans m () res (const (drop res prf))
drop : (res : Resources) -> (prf : InState lbl st res) -> Resources
dropCombined : VarsIn vs res -> Resources
dropEl : (ys : Resources) -> ElemRes x ys -> Resources
dropEnv : Env ys -> SubRes xs ys -> Env xs
dropSub : {auto prf : SubRes ys xs} -> STrans m (Env ys) xs (const (kept prf))
dropVarIn : (ys : Resources) -> VarInRes x ys -> Resources
getCombineType : VarsIn ys xs -> List Type
getVarType : (xs : Resources) -> VarInRes v xs -> Type
in_res : (as : List (Action ty)) -> Resources
kept : SubRes xs ys -> Resources
lift : Monad m => m t -> STrans m t res (const res)
new : (val : state) -> STrans m Var res (\lbl => (lbl ::: State state) :: res)
or : a -> a -> Either b c -> a
out_res : ty -> (as : List (Action ty)) -> Resources
print : ConsoleIO m => Show a => a -> STrans m () xs (const xs)
printLn : ConsoleIO m => Show a => a -> STrans m () xs (const xs)
pure : (result : ty) -> STrans m ty (out_fn result) out_fn
putStrLn : ConsoleIO m => String -> STrans m () xs (const xs)
read : (lbl : Var) -> {auto prf : InState lbl (State ty) res} -> STrans m ty res (const res)
remove : Var -> Type -> Action ty
returning : (result : ty) -> STrans m () res (const (out_fn result)) -> STrans m ty res out_fn
run : Applicative m => ST m a [] -> m a
runAs : Applicative m => STrans m t in_res (const out_res) -> STrans m (m t) in_res (const out_res)
runLoop : Applicative m => Fuel -> STLoop m a [] -> (onDry : m a) -> m a
runPure : ST id a [] -> a
runWith : Env res -> STrans IO a res resf -> IO (result : a ** Env (resf result))

runWith allows running an STrans program with an initial environment,
which must be consumed.
It's only allowed in the IO monad, because it's inherently unsafe, so
we don't want to be able to use it under a 'lift' in just any ST program -
if we have access to an 'Env' we can easily duplicate it - so it's the
responsibility of an implementation of an interface in IO which uses it
to ensure that it isn't duplicated.

runWithLoop : Env res -> Fuel -> STransLoop IO a res resf -> IO (Maybe (result : a ** Env (resf result)))
split : (lbl : Var) -> {auto prf : InState lbl (Composite vars) res} -> STrans m (VarList vars) res (\vs => mkRes vs ++ updateRes res prf (State ()))
st_precondition : Err -> Maybe (List ErrorReportPart)
subResId : SubRes xs xs
subResNil : SubRes [] xs
toEnd : (lbl : Var) -> {auto prf : InState lbl state res} -> STrans m () res (const (drop res prf ++ [lbl ::: state]))
update : (lbl : Var) -> {auto prf : InState lbl (State ty) res} -> (ty -> ty') -> STrans m () res (const (updateRes res prf (State ty')))
updateRes : (res : Resources) -> InState lbl st res -> Type -> Resources
updateWith : (new : Resources) -> (xs : Resources) -> SubRes ys xs -> Resources
write : (lbl : Var) -> {auto prf : InState lbl ty res} -> (val : ty') -> STrans m () res (const (updateRes res prf (State ty')))