diff options
Diffstat (limited to 'src/common/Monad.v')
-rw-r--r-- | src/common/Monad.v | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/src/common/Monad.v b/src/common/Monad.v index 8517186..03dd294 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -30,15 +30,26 @@ Module MonadExtra(M : Monad). End MonadNotation. Import MonadNotation. - Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) := + Fixpoint sequence {A: Type} (l: list (mon A)) {struct l}: mon (list A) := match l with | nil => ret nil | x::xs => - do r <- f x; - do rs <- traverselist f xs; + do r <- x; + do rs <- sequence xs; ret (r::rs) end. + Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) := + sequence (map f l). + + Fixpoint traverseoption {A B: Type} (f: A -> mon B) (opt: option A) {struct opt}: mon (option B) := + match opt with + | None => ret None + | Some x => + do r <- f x; + ret (Some r) + end. + Fixpoint collectlist {A : Type} (f : A -> mon unit) (l : list A) {struct l} : mon unit := match l with | nil => ret tt |