git.iko.soy/Idris-dev
on master help sign in
Add 'update' for State in ST
195ad13Edwin Brady
libs/contrib/Control/ST.idr+8
compare with master
unifiedsplit
@@ -483,6 +483,14 @@ write : (lbl : Var) ->
483 STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
483 STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
484write lbl {prf} val = Write lbl prf (Value val)
484write lbl {prf} val = Write lbl prf (Value val)
485
485
486+export
487+update : (lbl : Var) ->
488+ {auto prf : InState lbl (State ty) ctxt} ->
489+ (ty -> ty') ->
490+ STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
491+update lbl f = do x <- read lbl
492+ write lbl (f x)
493+
486namespace Loop
494namespace Loop
487 export
495 export
488 (>>=) : STrans m a st1 st2_fn ->
496 (>>=) : STrans m a st1 st2_fn ->