Adding a [map] primitive to the tactic monad. Hopefully this should be

slightly more efficient in general.

3 files changed, 42 insertions, 15 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index aac11ffc4c..055cd14b60 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -385,8 +385,7 @@ let list_iter_goal s i =
       ~adv: begin fun goal ->
         set_comb [goal] >>
         i goal r >>= fun r ->
-        Proof.get >>= fun step ->
-        Proof.ret ( r , step.comb::subgoals )
+        Proof.map (fun step -> (r, step.comb :: subgoals)) Proof.get
       end
   end >>= fun (r,subgoals) ->
   set_comb (List.flatten (List.rev subgoals)) >>
@@ -405,8 +404,7 @@ let list_iter_goal2 l s i =
       ~adv: begin fun goal ->
         set_comb [goal] >>
         i goal a r >>= fun r ->
-        Proof.get >>= fun step ->
-        Proof.ret ( r , step.comb::subgoals )
+        Proof.map (fun step -> (r, step.comb :: subgoals)) Proof.get
       end
   end >>= fun (r,subgoals) ->
   set_comb (List.flatten (List.rev subgoals)) >>
@@ -434,17 +432,14 @@ let tclDISPATCHGEN f join tacs =
             on_advance goal
               ~solved:( tclUNIT (join []) )
               ~adv:begin fun _ ->
-                f tac >>= fun res ->
-                Proof.ret (join [res])
+                Proof.map (fun res -> join [res]) (f tac)
               end
         | _ -> tclZERO SizeMismatch
       end
   | _ ->
-      list_iter_goal2 tacs [] begin fun _ t cur ->
-        f t >>= fun y ->
-        Proof.ret ( y :: cur )
-      end >>= fun res ->
-      Proof.ret (join res)
+      let iter _ t cur = Proof.map (fun y -> y :: cur) (f t) in
+      let ans = list_iter_goal2 tacs [] iter in
+      Proof.map join ans
 
 let tclDISPATCH tacs = tclDISPATCHGEN Util.identity ignore tacs
 
@@ -532,10 +527,7 @@ let tclPROGRESS t =
     tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
 
 let tclEVARMAP =
-  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Proof.bind in
-  Proof.get >>= fun initial ->
-  Proof.ret (initial.solution)
+  Proof.map (fun initial -> initial.solution) Proof.get
 
 let tclENV = Proof.current
 
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 8008e108b3..a686c528c3 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -31,6 +31,10 @@ module IOBase =
   
   let seq = fun a k -> (); fun () -> a (); k ()
   
+  (** val map : ('a1 -> 'a2) -> 'a1 coq_T -> 'a2 coq_T **)
+  
+  let map = fun f a -> (); fun () -> f (a ())
+  
   (** val ref : 'a1 -> 'a1 coq_Ref coq_T **)
   
   let ref = fun a -> (); fun () -> Pervasives.ref a
@@ -124,6 +128,11 @@ module NonLogical =
   let seq x k =
     IOBase.seq x k
   
+  (** val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t **)
+  
+  let map f x =
+    (); (IOBase.map f x)
+  
   (** val new_ref : 'a1 -> 'a1 ref t **)
   
   let new_ref x =
@@ -296,6 +305,30 @@ module Logical =
   let seq x k =
     (); (fun _ k0 s -> Obj.magic x __ (fun x1 s' -> Obj.magic k __ k0 s') s)
   
+  (** val map :
+      ('a1 -> 'a2) -> 'a1 t -> __ -> ('a2 -> proofview -> __ -> ('a3 -> __ ->
+      (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
+      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> proofview -> __ -> ('a3 -> __ -> ('a4 ->
+      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a4 -> (bool*(Goal.goal list*Goal.goal list)) ->
+      __ -> ('a5 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a5 -> (exn -> 'a6
+      IOBase.coq_T) -> 'a6 IOBase.coq_T) -> (exn -> 'a6 IOBase.coq_T) -> 'a6
+      IOBase.coq_T **)
+  
+  let map f x =
+    (); (fun _ k s -> Obj.magic x __ (fun a s0 -> k (f a) s0) s)
+  
   (** val set :
       logicalState -> __ -> (unit -> proofview -> __ -> ('a1 -> __ -> (__ ->
       (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 6a832e40f5..4d4e4470c0 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -23,6 +23,7 @@ module NonLogical : sig
 
   val ret : 'a -> 'a t
   val bind : 'a t -> ('a -> 'b t) -> 'b t
+  val map : ('a -> 'b) -> 'a t -> 'b t
   val ignore : 'a t -> unit t
   val seq : unit t -> 'a t -> 'a t
 
@@ -51,6 +52,7 @@ module Logical : sig
 
   val ret : 'a -> 'a t
   val bind : 'a t -> ('a -> 'b t) -> 'b t
+  val map : ('a -> 'b) -> 'a t -> 'b t
   val ignore : 'a t -> unit t
   val seq : unit t -> 'a t -> 'a t