Add more primitives to the [Monad.Make] arguments.

For optimisation purposes.

5 files changed, 42 insertions, 16 deletions

diff --git a/lib/monad.ml b/lib/monad.ml
index dc5809407b..2d305a3c97 100644
--- a/lib/monad.ml
+++ b/lib/monad.ml
@@ -10,17 +10,24 @@
 (** Combinators on monadic computations. *)
 
 
-(** A minimal definition necessary for the definition to go through. *)
+(** A definition of monads, each of the combinators is used in the
+    [Make] functor. *)
 module type Def = sig
 
   type +'a t
   val return : 'a -> 'a t
   val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+  val (>>) : unit t -> 'a t -> 'a t
+  val map : ('a -> 'b) -> 'a t -> 'b t
 
   (** The monadic laws must hold:
       - [(x>>=f)>>=g] = [x>>=fun x' -> (f x'>>=g)]
       - [return a >>= f] = [f a]
-      - [x>>=return] = [x]  *)
+      - [x>>=return] = [x]
+
+      As well as the following identities:
+      - [x >> y] = [x >>= fun () -> y]
+      - [map f x] = [x >>= fun x' -> f x'] *)
 
 end
 
@@ -93,24 +100,20 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct
     let rec map f = function
       | [] -> return []
       | [a] ->
-          f a >>= fun a' ->
-          return [a']
+          M.map (fun a' -> [a']) (f a)
       | a::b::l ->
           f a >>= fun a' ->
           f b >>= fun b' ->
-          map f l >>= fun l' ->
-          return (a'::b'::l')
+          M.map (fun l' -> a'::b'::l') (map f l)
 
     let rec map_right f = function
       | [] -> return []
       | [a] ->
-          f a >>= fun a' ->
-          return [a']
+          M.map (fun a' -> [a']) (f a)
       | a::b::l ->
           map f l >>= fun l' ->
           f b >>= fun b' ->
-          f a >>= fun a' ->
-          return (a'::b'::l')
+          M.map (fun a' -> a'::b'::l') (f a)
 
     let rec fold_right f l x =
       match l with
diff --git a/lib/monad.mli b/lib/monad.mli
index c72e584db1..d5c5cbc692 100644
--- a/lib/monad.mli
+++ b/lib/monad.mli
@@ -10,17 +10,24 @@
 (** Combinators on monadic computations. *)
 
 
-(** A minimal definition necessary for the definition to go through. *)
+(** A definition of monads, each of the combinators is used in the
+    [Make] functor. *)
 module type Def = sig
 
   type +'a t
   val return : 'a -> 'a t
   val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+  val (>>) : unit t -> 'a t -> 'a t
+  val map : ('a -> 'b) -> 'a t -> 'b t
 
-  (** The monadic laws must hold:
-      - [(x>>=f)>>=g] = [x>>=fun x' -> (f x'>>=g)]
-      - [return a >>= f] = [f a]
-      - [x>>=return] = [x]  *)
+(** The monadic laws must hold:
+    - [(x>>=f)>>=g] = [x>>=fun x' -> (f x'>>=g)]
+    - [return a >>= f] = [f a]
+    - [x>>=return] = [x]
+
+    As well as the following identities:
+    - [x >> y] = [x >>= fun () -> y]
+    - [map f x] = [x >>= fun x' -> f x'] *)
 
 end
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index a41db3f8f0..93d47d6b18 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1630,6 +1630,13 @@ module MonadR =
       let (s',a) = x s in
       f a s'
 
+    let (>>) x y = fun s ->
+      let (s',()) = x s in
+      y s'
+
+    let map f x = fun s ->
+      on_snd f (x s)
+
   end)
 
 module Monad =
@@ -1643,6 +1650,13 @@ module Monad =
       let (a,s') = x s in
       f a s'
 
+    let (>>) x y = fun s ->
+      let ((),s') = x s in
+      y s'
+
+    let map f x = fun s ->
+      on_fst f (x s)
+
   end)
 
 (**********************************************************)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 03355c4919..94a89aca37 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -96,7 +96,7 @@ module Giveup : Writer with type t = Evar.t list = struct
 end
 
 
-module Monad = Monad.Make(struct type 'a t = 'a Proof.t let (>>=) = Proof.bind let return = Proof.ret end)
+module Monad = Monad.Make(struct type 'a t = 'a Proof.t let (>>=) = Proof.bind let (>>) = Proof.seq let map = Proof.map let return = Proof.ret end)
 
 type entry = (Term.constr * Term.types) list
 
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index d8b12fc4e4..6d6e43b21d 100644
--- a/tactics/ftactic.ml
+++ b/tactics/ftactic.ml
@@ -67,6 +67,8 @@ struct
   type 'a t = 'a focus Proofview.tactic
   let return = return
   let (>>=) = bind
+  let (>>) = (<*>)
+  let map f x = x >>= fun a -> return (f a)
 end
 
 module Ftac = Monad.Make(Self)