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 ++++++++++++++++++++++++++++++++++
 src/common/Statemonad.v | 61 +++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 103 insertions(+)
 create mode 100644 src/common/Monad.v
 create mode 100644 src/common/Statemonad.v

(limited to 'src')

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.
diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v
new file mode 100644
index 0000000..ed1b9e7
--- /dev/null
+++ b/src/common/Statemonad.v
@@ -0,0 +1,61 @@
+From compcert Require Errors.
+From coqup Require Import Monad.
+From Coq Require Import Lists.List.
+
+Module Type State.
+  Parameter st : Type.
+  Parameter st_prop : st -> st -> Prop.
+
+  Axiom st_refl : forall s, st_prop s s.
+  Axiom st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
+End State.
+
+Module Statemonad(S : State) <: Monad.
+
+  Inductive res (A: Type) (s: S.st): Type :=
+  | Error : Errors.errmsg -> res A s
+  | OK : A -> forall (s' : S.st), S.st_prop s s' -> res A s.
+
+  Arguments OK [A s].
+  Arguments Error [A s].
+
+  Definition mon (A: Type) : Type := forall (s: S.st), res A s.
+
+  Definition ret {A: Type} (x: A) : mon A :=
+    fun (s : S.st) => OK x s (S.st_refl s).
+
+  Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B :=
+    fun (s : S.st) =>
+      match f s with
+      | Error msg => Error msg
+      | OK a s' i =>
+        match g a s' with
+        | Error msg => Error msg
+        | OK b s'' i' => OK b s'' (S.st_trans s s' s'' i i')
+        end
+      end.
+
+  Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
+    bind f (fun xy => g (fst xy) (snd xy)).
+
+  Definition handle_error {A: Type} (f g: mon A) : mon A :=
+    fun (s : S.st) =>
+      match f s with
+      | OK a s' i => OK a s' i
+      | Error _ => g s
+      end.
+
+  Definition error {A: Type} (err: Errors.errmsg) : mon A := fun (s: S.st) => Error err.
+
+  Definition get : mon S.st := fun s => OK s s (S.st_refl s).
+
+  Definition set (s: S.st) (i: forall s', S.st_prop  s' s) : mon unit :=
+    fun s' => OK tt s (i s').
+
+  Definition run_mon {A: Type} (s: S.st) (m: mon A): Errors.res A :=
+    match m s with
+    | OK a s' i => Errors.OK a
+    | Error err => Errors.Error err
+    end.
+
+End Statemonad.
-- 
cgit