diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-24 13:36:05 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-24 13:36:05 +0100 |
commit | d1bea5e0f88ad2cfcd0b0667fb11279100d02e6b (patch) | |
tree | 892fdd7d4d241cd456689463707cc50f8564da56 /src/common/Monad.v | |
parent | 39a4348657c2f3efb3feafe9cf65b0f2a1a263c2 (diff) | |
download | vericert-d1bea5e0f88ad2cfcd0b0667fb11279100d02e6b.tar.gz vericert-d1bea5e0f88ad2cfcd0b0667fb11279100d02e6b.zip |
Add statemonad declaration
Diffstat (limited to 'src/common/Monad.v')
-rw-r--r-- | src/common/Monad.v | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/src/common/Monad.v b/src/common/Monad.v new file mode 100644 index 0000000..773918a --- /dev/null +++ b/src/common/Monad.v @@ -0,0 +1,42 @@ +From Coq Require Import Lists.List. + +Module Type Monad. + + Parameter mon : Type -> Type. + + Parameter ret : forall (A : Type) (x : A), mon A. + Arguments ret [A]. + + Parameter bind : forall (A B : Type) (f : mon A) (g : A -> mon B), mon B. + Arguments bind [A B]. + + Parameter bind2 : forall (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C), mon C. + Arguments bind2 [A B C]. + +End Monad. + +Module MonadExtra(M : Monad). + Import M. + + Module MonadNotation. + + Notation "'do' X <- A ; B" := + (bind A (fun X => B)) + (at level 200, X ident, A at level 100, B at level 200). + Notation "'do' ( X , Y ) <- A ; B" := + (bind2 A (fun X Y => B)) + (at level 200, X ident, Y ident, A at level 100, B at level 200). + + End MonadNotation. + Import MonadNotation. + + Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) := + match l with + | nil => ret nil + | x::xs => + do r <- f x; + do rs <- traverselist f xs; + ret (r::rs) + end. + +End MonadExtra. |