IdrisDoc: Control.ST

Control.ST

write : (lbl : Var) -> {auto prf : InState lbl ty ctxt} -> (val : ty') -> STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
updateWith : (new : Context) -> (xs : Context) -> SubCtxt ys xs -> Context
updateCtxt : (ctxt : Context) -> InState lbl st ctxt -> Type -> Context
subCtxtNil : SubCtxt [] xs
subCtxtId : SubCtxt xs xs
st_precondition : Err -> Maybe (List ErrorReportPart)
split : (lbl : Var) -> {auto prf : InState lbl (Composite vars) ctxt} -> STrans m (VarList vars) ctxt (\vs => mkCtxt vs ++ updateCtxt ctxt prf (State ()))
runWith : Env ctxt -> STrans IO a ctxt (\res => ctxtf res) -> IO (res : a ** Env (ctxtf res))

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.

runPure : ST id a [] -> a
run : Applicative m => ST m a [] -> m a
read : (lbl : Var) -> {auto prf : InState lbl (State ty) ctxt} -> STrans m ty ctxt (const ctxt)
pure : (result : ty) -> STrans m ty (out_fn result) out_fn
out_res : ty -> (as : List (Action ty)) -> Context
or : a -> a -> Either b c -> a
new : (val : state) -> STrans m Var ctxt (\lbl => (lbl ::: State state) :: ctxt)
lift : Monad m => m t -> STrans m t ctxt (const ctxt)
kept : SubCtxt xs ys -> Context
in_res : (as : List (Action ty)) -> Context
getVarType : (xs : Context) -> VarInCtxt v xs -> Type
getCombineType : VarsIn ys xs -> List Type
dropVarIn : (ys : Context) -> VarInCtxt x ys -> Context
dropSubCtxt : {auto prf : SubCtxt ys xs} -> STrans m (Env ys) xs (const (kept prf))
dropEnv : Env ys -> SubCtxt xs ys -> Env xs
dropEl : (ys : Context) -> ElemCtxt x ys -> Context
dropCombined : VarsIn vs ctxt -> Context
drop : (ctxt : Context) -> (prf : InState lbl st ctxt) -> Context
delete : (lbl : Var) -> {auto prf : InState lbl (State st) ctxt} -> STrans m () ctxt (const (drop ctxt prf))
combineVarsIn : (ctxt : Context) -> VarsIn (comp :: vs) ctxt -> Context
combine : (comp : Var) -> (vs : List Var) -> {auto prf : InState comp (State ()) ctxt} -> {auto var_prf : VarsIn (comp :: vs) ctxt} -> STrans m () ctxt (const (combineVarsIn ctxt var_prf))
call : STrans m t sub new_f -> {auto ctxt_prf : SubCtxt sub old} -> STrans m t old (\res => updateWith (new_f res) old ctxt_prf)
addIfRight : Type -> Action (Either a b)
addIfJust : Type -> Action (Maybe a)
add : Type -> Action a
data VarsIn : List Var -> Context -> Type
VarsNil : VarsIn [] []
InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) -> VarsIn (x :: xs) ys
SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
data VarInCtxt : Var -> Context -> Type
VarHere : VarInCtxt a (MkRes a st :: as)
VarThere : VarInCtxt a as -> VarInCtxt a (b :: as)
data Var : Type
MkVar : Var
data SubCtxt : Context -> Context -> Type
SubNil : SubCtxt [] []
InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) -> SubCtxt (x :: xs) ys
Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
data State : Type -> Type
Value : ty -> State ty
data STrans : (m : Type -> Type) -> (ty : Type) -> Context -> (ty -> Context) -> 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 ctxt (const ctxt)
New : (val : state) -> STrans m Var ctxt (\lbl => (lbl ::: state) :: ctxt)
Delete : (lbl : Var) -> (prf : InState lbl st ctxt) -> STrans m () ctxt (const (drop ctxt prf))
DropSubCtxt : (prf : SubCtxt ys xs) -> STrans m (Env ys) xs (const (kept prf))
Split : (lbl : Var) -> (prf : InState lbl (Composite vars) ctxt) -> STrans m (VarList vars) ctxt (\vs => mkCtxt vs ++ updateCtxt ctxt prf (State ()))
Combine : (comp : Var) -> (vs : List Var) -> (prf : VarsIn (comp :: vs) ctxt) -> STrans m () ctxt (const (combineVarsIn ctxt prf))
Call : STrans m t sub new_f -> (ctxt_prf : SubCtxt sub old) -> STrans m t old (\res => updateWith (new_f res) old ctxt_prf)
Read : (lbl : Var) -> (prf : InState lbl ty ctxt) -> STrans m ty ctxt (const ctxt)
Write : (lbl : Var) -> (prf : InState lbl ty ctxt) -> (val : ty') -> STrans m () ctxt (const (updateCtxt ctxt prf ty'))
ST : (m : Type -> Type) -> (ty : Type) -> List (Action ty) -> Type
data Resource : Type
MkRes : label -> Type -> Resource
data InState : lbl -> Type -> Context -> Type
Here : InState lbl st (MkRes lbl st :: rs)
There : InState lbl st rs -> InState lbl st (r :: rs)
data ElemCtxt : Resource -> Context -> Type
HereCtxt : ElemCtxt a (a :: as)
ThereCtxt : ElemCtxt a as -> ElemCtxt a (b :: as)
interface ConsoleIO 
putStr : ConsoleIO m => String -> STrans m () xs (const xs)
getStr : ConsoleIO m => STrans m String xs (const xs)
data Composite : List Type -> Type
CompNil : Composite []
CompCons : (x : a) -> Composite as -> Composite (a :: as)
data Action : Type -> Type
Stable : lbl -> Type -> Action ty
Trans : lbl -> Type -> (ty -> Type) -> Action ty
Remove : lbl -> Type -> Action ty
Add : (ty -> Context) -> Action ty
(>>=) : 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 5
(:::) : label -> Type -> Resource
Fixity
Non-associative, precedence 5