Add global monad notation using Instances

This was mostly inspired by the std++ library.

5 files changed, 81 insertions, 11 deletions

diff --git a/src/common/Errormonad.v b/src/common/Errormonad.v
index 09c5c1c..201a101 100644
--- a/src/common/Errormonad.v
+++ b/src/common/Errormonad.v
@@ -26,13 +26,13 @@ Module ErrorMonad <: Monad.
     | Error m => Error m
     end.
 
-  Definition bind {A B : Type} (f : mon A) (g : A -> mon B) : mon B :=
+  Definition bind {A B : Type} (g : A -> mon B) (f : mon A) : 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 :=
+  Definition bind2 {A B C : Type} (g : A -> B -> mon C) (f : mon (A * B)) : mon C :=
     match f with
     | OK (a, b) => g a b
     | Error m => Error m
@@ -44,6 +44,11 @@ Module ErrorMonad <: Monad.
     | OK a' => a'
     end.
 
+  #[global] Instance error_ret : MRet res := @ret.
+  #[global] Instance error_bind : MBind res := @bind.
+  #[global] Instance error_join : MJoin res := @join.
+  #[global] Instance error_map : FMap res := @map.
+
 End ErrorMonad.
 
 Module ErrorMonadExtra := MonadExtra(ErrorMonad).
diff --git a/src/common/Monad.v b/src/common/Monad.v
index b7d97a1..cf3180b 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -18,6 +18,9 @@
 
 From Coq Require Import Lists.List.
 
+Declare Scope vericert_scope.
+#[local] Open Scope vericert_scope.
+
 Declare Scope monad_scope.
 
 Module Type Monad.
@@ -27,10 +30,10 @@ Module Type Monad.
   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.
+  Parameter bind : forall (A B : Type) (g : A -> mon B) (f : mon A), mon B.
   Arguments bind [A B].
 
-  Parameter bind2 : forall (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C), mon C.
+  Parameter bind2 : forall (A B C: Type) (g: A -> B -> mon C) (f: mon (A * B)), mon C.
   Arguments bind2 [A B C].
 
 End Monad.
@@ -41,10 +44,10 @@ Module MonadExtra(M : Monad).
   Module Import MonadNotation.
 
     Notation "'do' X <- A ; B" :=
-      (bind A (fun X => B))
+      (bind (fun X => B) A)
         (at level 200, X name, A at level 100, B at level 200) : monad_scope.
     Notation "'do' ( X , Y ) <- A ; B" :=
-      (bind2 A (fun X Y => B))
+      (bind2 (fun X Y => B) A)
         (at level 200, X name, Y name, A at level 100, B at level 200) : monad_scope.
 
   End MonadNotation.
@@ -70,3 +73,53 @@ Module MonadExtra(M : Monad).
     fold_left (fun a b => do a' <- a; f a' b) l s.
 
 End MonadExtra.
+
+(** A [Params f n] instance forces the setoid rewriting mechanism not to
+rewrite in the first [n] arguments of the function [f]. We will declare such
+instances for all operational type classes in this development. *)
+From Coq Require Export Morphisms RelationClasses.
+
+From Coq Require Setoid.
+
+Global Instance: Params (@Relation_Definitions.equiv) 2 := {}.
+
+Class MRet (M : Type -> Type) := mret: forall {A}, A -> M A.
+Global Arguments mret {_ _ _} _ : assert.
+Global Instance: Params (@mret) 3 := {}.
+Global Hint Mode MRet ! : typeclass_instances.
+
+Class MBind (M : Type -> Type) := mbind : forall {A B}, (A -> M B) -> M A -> M B.
+Global Arguments mbind {_ _ _ _} _ !_ / : assert.
+Global Instance: Params (@mbind) 4 := {}.
+Global Hint Mode MBind ! : typeclass_instances.
+
+Class MJoin (M : Type -> Type) := mjoin: forall {A}, M (M A) -> M A.
+Global Arguments mjoin {_ _ _} !_ / : assert.
+Global Instance: Params (@mjoin) 3 := {}.
+Global Hint Mode MJoin ! : typeclass_instances.
+
+Class FMap (M : Type -> Type) := fmap : forall {A B}, (A -> B) -> M A -> M B.
+Global Arguments fmap {_ _ _ _} _ !_ / : assert.
+Global Instance: Params (@fmap) 4 := {}.
+Global Hint Mode FMap ! : typeclass_instances.
+
+Class OMap (M : Type -> Type) := omap: forall {A B}, (A -> option B) -> M A -> M B.
+Global Arguments omap {_ _ _ _} _ !_ / : assert.
+Global Instance: Params (@omap) 4 := {}.
+Global Hint Mode OMap ! : typeclass_instances.
+
+Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : vericert_scope.
+Notation "( m ≫=.)" := (fun f => mbind f m) (only parsing) : vericert_scope.
+Notation "(.≫= f )" := (mbind f) (only parsing) : vericert_scope.
+Notation "(≫=)" := (fun m f => mbind f m) (only parsing) : vericert_scope.
+
+Notation "x ← y ; z" := (y ≫= (fun x : _ => z))
+  (at level 20, y at level 100, z at level 200, only parsing) : vericert_scope.
+
+Notation "' x ← y ; z" := (y ≫= (fun x : _ => z))
+  (at level 20, x pattern, y at level 100, z at level 200, only parsing) : vericert_scope.
+
+Infix "<$>" := fmap (at level 61, left associativity) : vericert_scope.
+
+Notation "x ;; z" := (x ≫= fun _ => z)
+  (at level 100, z at level 200, only parsing, right associativity): vericert_scope.
diff --git a/src/common/Optionmonad.v b/src/common/Optionmonad.v
index 4a80ff8..037dd83 100644
--- a/src/common/Optionmonad.v
+++ b/src/common/Optionmonad.v
@@ -43,13 +43,13 @@ Module Option <: Monad.
     | _ => None
     end.
 
-  Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B :=
+  Definition bind {A B : Type} (g : A -> option B) (f : option A) : option B :=
     match f with
     | Some a => g a
     | _ => None
     end.
 
-  Definition bind2 {A B C : Type} (f : mon (A * B)) (g : A -> B -> option C) : option C :=
+  Definition bind2 {A B C : Type} (g : A -> B -> option C) (f : mon (A * B)) : option C :=
     match f with
     | Some (a, b) => g a b
     | _ => None
@@ -61,6 +61,12 @@ Module Option <: Monad.
     | Some a' => a'
     end.
 
+  #[global] Instance option_ret : MRet option := @ret.
+  #[global] Instance option_bind : MBind option := @bind.
+  #[global] Instance option_join : MJoin option := @join.
+  #[global] Instance option_map : FMap option := @map.
+  #[global] Instance option_omap : OMap option := @bind.
+
 End Option.
 
 Module OptionExtra.
diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v
index 16dcbbf..c667fd9 100644
--- a/src/common/Statemonad.v
+++ b/src/common/Statemonad.v
@@ -42,7 +42,7 @@ Module Statemonad(S : State) <: Monad.
   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 :=
+  Definition bind {A B: Type} (g: A -> mon B) (f: mon A) : mon B :=
     fun (s : S.st) =>
       match f s with
       | Error msg => Error msg
@@ -53,8 +53,8 @@ Module Statemonad(S : State) <: Monad.
         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 bind2 {A B C: Type} (g: A -> B -> mon C) (f: mon (A * B)) : mon C :=
+    bind (fun xy => g (fst xy) (snd xy)) (f: mon (A * B)).
 
   Definition handle_error {A: Type} (f g: mon A) : mon A :=
     fun (s : S.st) =>
@@ -76,4 +76,7 @@ Module Statemonad(S : State) <: Monad.
     | Error err => Errors.Error err
     end.
 
+  #[global] Instance statemonad_ret : MRet mon := @ret.
+  #[global] Instance statemonad_bind : MBind mon := @bind.
+
 End Statemonad.
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index 24abece..6f602fc 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -31,8 +31,11 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Show.
+Require Export vericert.common.Monad.
 Require Export vericert.common.Optionmonad.
 
+#[global] Open Scope vericert_scope.
+
 (* Depend on CompCert for the basic library, as they declare and prove some
    useful theorems. *)