From 20aae726fa959272ed1568b39b78a0ff501b4882 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 24 Sep 2022 18:37:04 +0100
Subject: Add more monads

---
 src/common/Errormonad.v  | 49 ++++++++++++++++++++++++++++++++++++++++++++++++
 src/common/Monad.v       |  3 +++
 src/common/Optionmonad.v | 12 +++++++++++-
 3 files changed, 63 insertions(+), 1 deletion(-)
 create mode 100644 src/common/Errormonad.v

diff --git a/src/common/Errormonad.v b/src/common/Errormonad.v
new file mode 100644
index 0000000..09c5c1c
--- /dev/null
+++ b/src/common/Errormonad.v
@@ -0,0 +1,49 @@
+From compcert Require Export Errors.
+From vericert Require Import Monad.
+From Coq Require Import Lists.List.
+
+Module ErrorMonad <: Monad.
+
+  Definition mon := res.
+
+  Definition ret {A: Type} (x: A) := OK x.
+
+  Definition default {T : Type} (x : T) (u : res T) : T :=
+    match u with
+    | OK y => y
+    | _ => x
+    end.
+
+  Definition map {S : Type} {T : Type} (f : S -> T) (u : mon S) : mon T :=
+    match u with
+    | OK y => OK (f y)
+    | Error m => Error m
+    end.
+
+  Definition liftA2 {T : Type} (f : T -> T -> T) (a : mon T) (b : mon T) : mon T :=
+    match a with
+    | OK x => map (f x) b
+    | Error m => Error m
+    end.
+
+  Definition bind {A B : Type} (f : mon A) (g : A -> mon B) : mon B :=
+    match f with
+    | OK a => g a
+    | Error m => Error m
+    end.
+
+  Definition bind2 {A B C : Type} (f : mon (A * B)) (g : A -> B -> mon C) : mon C :=
+    match f with
+    | OK (a, b) => g a b
+    | Error m => Error m
+    end.
+
+  Definition join {A : Type} (a : mon (mon A)) : mon A :=
+    match a with
+    | Error m => Error m
+    | OK a' => a'
+    end.
+
+End ErrorMonad.
+
+Module ErrorMonadExtra := MonadExtra(ErrorMonad).
diff --git a/src/common/Monad.v b/src/common/Monad.v
index ece047c..b7d97a1 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -66,4 +66,7 @@ Module MonadExtra(M : Monad).
     | x::xs => do _ <- f x; collectlist f xs
     end.
 
+  Definition mfold_left {A B} (f: A -> B -> mon A) (l: list B) (s: mon A): mon A :=
+    fold_left (fun a b => do a' <- a; f a' b) l s.
+
 End MonadExtra.
diff --git a/src/common/Optionmonad.v b/src/common/Optionmonad.v
index 14a41ef..4a80ff8 100644
--- a/src/common/Optionmonad.v
+++ b/src/common/Optionmonad.v
@@ -63,4 +63,14 @@ Module Option <: Monad.
 
 End Option.
 
-Module OptionExtra := MonadExtra(Option).
+Module OptionExtra.
+  Module OE := MonadExtra(Option).
+  Export OE.
+
+  Lemma mfold_left_Some :
+    forall A B f x n y,
+      @mfold_left A B f x n = Some y ->
+      exists n', n = Some n'.
+  Proof. induction x; intros; destruct n; eauto. Qed.
+
+End OptionExtra.
-- 
cgit