Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same time

the argument list is consumed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17062 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 9 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 950ee8a3cd..26a2985c68 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -404,7 +404,7 @@ let list_iter_goal2 l s i =
 (* spiwack: we use an parametrised function to generate the dispatch
    tacticals.  [tclDISPATCHGEN] takes an argument [join] to reify the
    list of produced value into the final value. *)
-let tclDISPATCHGEN join tacs =
+let tclDISPATCHGEN f join tacs =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   match tacs with
@@ -423,22 +423,22 @@ let tclDISPATCHGEN join tacs =
             on_advance goal
               ~solved:( tclUNIT (join []) )
               ~adv:begin fun _ ->
-                tac >>= fun res ->
+                f tac >>= fun res ->
                 Proof.ret (join [res])
               end
         | _ -> tclZERO SizeMismatch
       end
   | _ ->
       list_iter_goal2 tacs [] begin fun _ t cur ->
-        t >>= fun y ->
-        Proof.ret ( y::cur )
+        f t >>= fun y ->
+        Proof.ret ( y :: cur )
       end >>= fun res ->
-      Proof.ret (join (List.rev res))
+      Proof.ret (join res)
 
-let tclDISPATCH tacs = tclDISPATCHGEN (fun _ -> ()) tacs
+let tclDISPATCH tacs = tclDISPATCHGEN Util.identity ignore tacs
 
 let tclDISPATCHL tacs =
-  tclDISPATCHGEN Util.identity tacs
+  tclDISPATCHGEN Util.identity List.rev tacs
 
 let extend_to_list startxs rx endxs l =
   (* spiwack: I use [l] essentially as a natural number *)
@@ -619,11 +619,11 @@ module Notations = struct
   let (>=) = tclBIND
   let (>>=) t k =
     t >= fun l ->
-    tclDISPATCH (List.map k l)
+    tclDISPATCHGEN k ignore l
   let (>>==) t k =
     begin
       t >= fun l ->
-      tclDISPATCHL (List.map k l)
+      tclDISPATCHGEN k List.rev l
     end >= fun l' ->
     tclUNIT (List.flatten l')
   let (<*>) = tclTHEN