1 files changed, 49 insertions, 0 deletions
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).