git.iko.soy/Idris-dev
on master help sign in
Add looping control to Control.ST
b1ba8cdEdwin Brady
libs/contrib/Control/ST.idr+56
compare with master
unifiedsplit
@@ -316,6 +316,15 @@ data STrans : (m : Type -> Type) ->
316 (val : ty') ->
316 (val : ty') ->
317 STrans m () ctxt (const (updateCtxt ctxt prf ty'))
317 STrans m () ctxt (const (updateCtxt ctxt prf ty'))
318
318
319+namespace Loop
320+ export
321+ data STransLoop : (m : Type -> Type) -> (ty : Type) ->
322+ Context -> (ty -> Context) -> Type where
323+ Bind : STrans m a st1 st2_fn ->
324+ ((result : a) -> Inf (STransLoop m b (st2_fn result) st3_fn)) ->
325+ STransLoop m b st1 st3_fn
326+ Pure : (result : ty) -> STransLoop m ty (out_fn result) out_fn
327+
319export
328export
320dropEnv : Env ys -> SubCtxt xs ys -> Env xs
329dropEnv : Env ys -> SubCtxt xs ys -> Env xs
321dropEnv [] SubNil = []
330dropEnv [] SubNil = []
@@ -372,6 +381,20 @@ runST env (Call prog ctxt_prf) k
372runST env (Read lbl prf) k = k (lookupEnv prf env) env
381runST env (Read lbl prf) k = k (lookupEnv prf env) env
373runST env (Write lbl prf val) k = k () (updateEnv prf env val)
382runST env (Write lbl prf val) k = k () (updateEnv prf env val)
374
383
384+export
385+data Fuel = Empty | More (Lazy Fuel)
386+
387+export partial
388+forever : Fuel
389+forever = More forever
390+
391+runSTLoop : Fuel -> Env invars -> STransLoop m a invars outfn ->
392+ (k : (x : a) -> Env (outfn x) -> m b) ->
393+ (onDry : m b) -> m b
394+runSTLoop Empty _ _ _ onDry = onDry
395+runSTLoop (More x) env (Bind prog next) k onDry
396+ = runST env prog (\prog', env' => runSTLoop x env' (next prog') k onDry)
397+runSTLoop (More x) env (Pure result) k onDry = k result env
375
398
376export
399export
377pure : (result : ty) -> STrans m ty (out_fn result) out_fn
400pure : (result : ty) -> STrans m ty (out_fn result) out_fn
@@ -445,6 +468,17 @@ write : (lbl : Var) ->
445 (val : ty') ->
468 (val : ty') ->
446 STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
469 STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
447write lbl {prf} val = Write lbl prf (Value val)
470write lbl {prf} val = Write lbl prf (Value val)
471+
472+namespace Loop
473+ export
474+ (>>=) : STrans m a st1 st2_fn ->
475+ ((result : a) -> Inf (STransLoop m b (st2_fn result) st3_fn)) ->
476+ STransLoop m b st1 st3_fn
477+ (>>=) = Bind
478+
479+ export
480+ pure : (result : ty) -> STransLoop m ty (out_fn result) out_fn
481+ pure = Pure
448
482
449public export %error_reduce
483public export %error_reduce
450out_res : ty -> (as : List (Action ty)) -> Context
484out_res : ty -> (as : List (Action ty)) -> Context
@@ -470,6 +504,13 @@ ST : (m : Type -> Type) ->
470 List (Action ty) -> Type
504 List (Action ty) -> Type
471ST m ty xs = STrans m ty (in_res xs) (\result : ty => out_res result xs)
505ST m ty xs = STrans m ty (in_res xs) (\result : ty => out_res result xs)
472
506
507+public export
508+%error_reduce -- always evaluate this before showing errors
509+STLoop : (m : Type -> Type) ->
510+ (ty : Type) ->
511+ List (Action ty) -> Type
512+STLoop m ty xs = STransLoop m ty (in_res xs) (\result : ty => out_res result xs)
513+
473-- Console IO is useful sufficiently often that let's have it here
514-- Console IO is useful sufficiently often that let's have it here
474public export
515public export
475interface ConsoleIO (m : Type -> Type) where
516interface ConsoleIO (m : Type -> Type) where
@@ -486,6 +527,13 @@ export
486run : Applicative m => ST m a [] -> m a
527run : Applicative m => ST m a [] -> m a
487run prog = runST [] prog (\res, env' => pure res)
528run prog = runST [] prog (\res, env' => pure res)
488
529
530+export
531+runLoop : Applicative m => Fuel -> STLoop m a [] ->
532+ (onEmpty : m a) ->
533+ m a
534+runLoop fuel prog onEmpty
535+ = runSTLoop fuel [] prog (\res, env' => pure res) onEmpty
536+
489||| runWith allows running an STrans program with an initial environment,
537||| runWith allows running an STrans program with an initial environment,
490||| which must be consumed.
538||| which must be consumed.
491||| It's only allowed in the IO monad, because it's inherently unsafe, so
539||| It's only allowed in the IO monad, because it's inherently unsafe, so
@@ -499,6 +547,14 @@ runWith : {ctxtf : _} ->
499 IO (res ** Env (ctxtf res))
547 IO (res ** Env (ctxtf res))
500runWith env prog = runST env prog (\res, env' => pure (res ** env'))
548runWith env prog = runST env prog (\res, env' => pure (res ** env'))
501
549
550+export
551+runWithLoop : {ctxtf : _} ->
552+ Env ctxt -> Fuel -> STransLoop IO a ctxt (\res => ctxtf res) ->
553+ IO (Maybe (res ** Env (ctxtf res)))
554+runWithLoop env fuel prog
555+ = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))
556+ (pure Nothing)
557+
502export
558export
503runPure : ST Basics.id a [] -> a
559runPure : ST Basics.id a [] -> a
504runPure prog = runST [] prog (\res, env' => res)
560runPure prog = runST [] prog (\res, env' => res)
libs/prelude/Prelude/Maybe.idr+1−1
@@ -112,7 +112,7 @@ Semigroup (Maybe a) where
112 m <+> Nothing = m
112 m <+> Nothing = m
113 (Just m1) <+> (Just m2) = Just (m1 <+> m2)
113 (Just m1) <+> (Just m2) = Just (m1 <+> m2)
114
114
115− Monoid (Maybe a) where
115+Monoid (Maybe a) where
116 neutral = Nothing
116 neutral = Nothing
117
117
118(Monoid a, Eq a) => Cast a (Maybe a) where
118(Monoid a, Eq a) => Cast a (Maybe a) where