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