From d1bea5e0f88ad2cfcd0b0667fb11279100d02e6b Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 24 May 2020 13:36:05 +0100
Subject: Add statemonad declaration

---
 src/common/Monad.v | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 src/common/Monad.v

(limited to 'src/common/Monad.v')

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.
-- 
cgit