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

slightly more efficient in general.

4 files changed, 63 insertions, 22 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 40e26e20a2..a029df3147 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -123,7 +123,8 @@ Record Monad (T:Set->Set) := {
   ret : forall{A:Set}, A->T A;
   bind : forall{A B:Set}, T A -> (A -> T B) -> T B;
   ignore : forall{A:Set}, T A -> T unit;
-  seq : forall{A:Set}, T unit -> T A -> T A
+  seq : forall{A:Set}, T unit -> T A -> T A;
+  map : forall {A B : Set}, (A -> B) -> T A -> T B
 }.
 
 Notation "'do' M x ':=' e 'in' u" := (bind _ M e (fun x => u)).
@@ -175,7 +176,8 @@ Module Id.
    ret := fun _ x => x;
    bind := fun _ _ x k => k x;
    ignore := fun _ x => ();
-   seq := fun _ x k => k
+   seq := fun _ x k => k;
+   map := fun _ _ f x => f x
  |}.
 
 End Id.
@@ -199,6 +201,9 @@ Module IOBase.
  Parameter seq : forall A, T unit -> T A -> T A.
  Extract Constant seq => "fun a k -> (); fun () -> a (); k ()".
  Extraction Implicit seq [A].
+ Parameter map : forall (A B : Set), (A -> B) -> T A -> T B.
+ Extract Constant map => "fun f a -> (); fun () -> f (a ())".
+ Extraction Implicit map [A B].
 
  Parameter ref : forall (A:Set), A -> T (Ref A).
  Extract Constant ref => "fun a -> (); fun () -> Pervasives.ref a".
@@ -277,7 +282,8 @@ Module IO.
    ret := IOBase.ret;
    bind := IOBase.bind;
    ignore := IOBase.ignore;
-   seq := IOBase.seq
+   seq := IOBase.seq;
+   map := IOBase.map
  |}.
 
  Definition IO : S Ref T := {|
@@ -314,7 +320,8 @@ Section Common.
    ignore A x := fun R k s =>
             x R (fun _ s' => k tt s') s ;
    seq A x y := fun R k s =>
-           x R (fun _ s' => y R k s') s
+           x R (fun _ s' => y R k s') s;
+   map A B f x := fun R k s => x R (fun a s => k (f a) s) s
  |}.
 
  Definition State : State S T := {|
@@ -376,7 +383,8 @@ Section Common.
    ret A x := fun R k e => k x;
    bind A B x f := fun R k e => x _ (fun a => f a _ k e) e;
    ignore A x := fun R k e => x _ (fun _ => k tt) e;
-   seq A x y := fun R k e => x _ (fun _ => y _ k e) e
+   seq A x y := fun R k e => x _ (fun _ => y _ k e) e;
+   map A B f x := fun R k e => x _ (fun a => k (f a)) e
  |}.
 
  Definition Environment : Environment E T := {|
@@ -432,7 +440,8 @@ Section Common.
      x _ (fun a c => f a _ (fun b c' => k b (Monoid.prod _ m c c')));
    ignore A x := fun R k => x _ (fun _ c => k tt c);
    seq A x y := fun R k =>
-     x _ (fun _ c => y _ (fun b c' => k b (Monoid.prod _ m c c')))
+     x _ (fun _ c => y _ (fun b c' => k b (Monoid.prod _ m c c')));
+   map A B f x := fun R k => x _ (fun a c => k (f a) c)
  |}.
 
  Definition Writer : Writer C T := {|
@@ -507,7 +516,8 @@ Section Common.
    ignore A x R sk fk :=
       x _ (fun _ fk => sk () fk) fk;
    seq A x k R sk fk :=
-      x _ (fun _ fk => k _ sk fk) fk
+      x _ (fun _ fk => k _ sk fk) fk;
+   map A B f x R sk fk := x _ (fun a fk => sk (f a) fk) fk
  |}.
 
  Definition lift {A} (x:T₀ A) : T A := fun _ sk fk =>
@@ -637,6 +647,8 @@ Module NonLogical.
  Extraction Implicit ignore [a].
  Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in seq _ NonLogicalMonad x k.
  Extraction Implicit seq [a].
+ Definition map {a b:Set} (f:a -> b) (x:t a) : t b := Eval compute in freeze _ (map _ NonLogicalMonad f x).
+ Extraction Implicit map [a b].
 
  Definition new_ref {a:Set} (x:a) : t (ref a) := Eval compute in IO.ref _ _ NonLogicalIO x.
  Extraction Implicit new_ref [a].
@@ -679,6 +691,8 @@ Module Logical.
  Extraction Implicit ignore [a].
  Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in freeze _ (seq _ LogicalMonad x k).
  Extraction Implicit seq [a].
+ Definition map {a b:Set} (f:a -> b) (x:t a) : t b := Eval compute in freeze _ (map _ LogicalMonad f x).
+ Extraction Implicit map [a b].
 
  Definition set (s:LogicalState) : t unit := Eval compute in freeze _ (set _ _ LogicalStateM s).
  Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
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