Various rewriting, mostly for speed purposes.

- A variant of tclEVARS directly in the language of the monad
- A variant of tclDISPATCHGEN (tclINDEPENDENT) hopefully faster in the case there is only one tactic to copy
- A better written tclDISPATCHGEN (which may make thing actually a little slower)
- A special case in tclDISPATCHGEN and tclINDEPENDENT for the case when they are 0 or 1 goals (adaptation of a patch sent by Pierre-Marie Pédrot)

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

5 files changed, 194 insertions, 71 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 6aae038b0a..4c800d48c6 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -1,7 +1,5 @@
 (* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *)
 
-(* arnaud: on ne doit pas en avoir besoin normalement. *)
-
 Reserved Notation "'do' M x ':=' e 'in' u" (at level 200, M at level 0, x ident, e at level 200, u at level 200).
 (*Reserved Notation "'do' e ; u" (at level 200, e at level 200, u at level 200).*)
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 3e05b60f0d..fb8796dbd5 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -263,6 +263,7 @@ let tclFOCUS i j t =
        of course I haven't made them algebraic yet. *)
     tclZERO e
 
+
 (* Dispatch tacticals are used to apply a different tactic to each goal under
    consideration. They come in two flavours:
    [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic].
@@ -278,57 +279,155 @@ let _ = Errors.register_handler begin function
   | SizeMismatch -> Errors.error "Incorrect number of goals."
   | _ -> raise Errors.Unhandled
 end
+
+(* A monadic list iteration function *)
+(* spiwack: may be moved to a generic libray, or maybe as extracted
+   code for extra efficiency? *)
+(* val list_iter : 'a list -> 'b -> ('a -> 'b -> 'b tactic) -> 'b tactic *)
+let rec list_iter l s i =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = tclBIND in
+  match l with
+  | [] -> tclUNIT s
+  | [a] -> i a s
+  | a::l ->
+      i a s >>= fun r ->
+      list_iter l r i
+
+(* val list_iter : 'a list -> 'b list -> 'c -> ('a -> 'b -> 'c -> 'c tactic) -> 'c tactic *)
+let rec list_iter2 l1 l2 s i =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = tclBIND in
+  match l1 , l2 with
+  | [] , [] -> tclUNIT s
+  | [a] , [b] -> i a b s
+  | a::l1 , b::l2 ->
+      i a b s >>= fun r ->
+      list_iter2 l1 l2 r i
+  | _ , _ -> tclZERO SizeMismatch
+
+(* A variant of [Proof.set] specialized on the comb. Doesn't change
+   the underlying "solution" (i.e. [evar_map]) *)
+let set_comb c =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun step ->
+  Proof.set { step with comb = c }
+
+let on_advance g ~solved ~adv =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun step ->
+  match Goal.advance step.solution g with
+  | None -> solved (* If [first] has been solved by side effect: do nothing. *)
+  | Some g -> adv g
+
+(* A variant of list_iter where we iter over the focused list of
+   goals. The argument tactic is executed in a focus comprising only
+   of the current goal, a goal which has been solved by side effect is
+   skipped. The generated subgoals are concatenated in order.  *)
+(* val list_iter_goal : 'a -> (Goal.goal -> 'a -> 'a tactic) -> 'a tactic *)
+let list_iter_goal s i =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  let (>>) = Proof.seq in
+  Proof.get >>= fun initial ->
+  list_iter initial.comb (s,[]) begin fun goal ((r,subgoals) as cur) ->
+    on_advance goal
+      ~solved: ( Proof.ret cur )
+      ~adv: begin fun goal ->
+        set_comb [goal] >>
+        i goal r >>= fun r ->
+        Proof.get >>= fun step ->
+        Proof.ret ( r , step.comb::subgoals )
+      end
+  end >>= fun (r,subgoals) ->
+  set_comb (List.flatten (List.rev subgoals)) >>
+  Proof.ret r
+
+(* spiwack: essentially a copy/paste of the above… *)
+(* val list_iter_goal : 'a list -> 'b -> (Goal.goal -> 'a -> 'b -> 'b tactic) -> 'b tactic *)
+let list_iter_goal2 l s i =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  let (>>) = Proof.seq in
+  Proof.get >>= fun initial ->
+  list_iter2 initial.comb l (s,[]) begin fun goal a ((r,subgoals) as cur) ->
+    on_advance goal
+      ~solved: ( Proof.ret cur )
+      ~adv: begin fun goal ->
+        set_comb [goal] >>
+        i goal a r >>= fun r ->
+        Proof.get >>= fun step ->
+        Proof.ret ( r , step.comb::subgoals )
+      end
+  end >>= fun (r,subgoals) ->
+  set_comb (List.flatten (List.rev subgoals)) >>
+  Proof.ret r
+
 (* spiwack: we use an parametrised function to generate the dispatch tacticals.
    [tclDISPATCHGEN] takes a [null] argument to generate the return value
    if there are no goal under focus, and a [join] argument to explain how
    the return value at two given lists of subgoals are combined when
    both lists are being concatenated.
    [join] and [null] need be some sort of comutative monoid. *)
-
-let rec tclDISPATCHGEN null join tacs =
+(* arnaud: commentaire obsolète *)
+let tclDISPATCHGEN join tacs =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  let (>>) = Proof.seq in
-  Proof.get >>= fun initial ->
-  match tacs,initial.comb with
-  | [], [] -> tclUNIT null
-  | t::tacs , first::goals ->
-      begin match Goal.advance initial.solution first with
-      | None -> Proof.ret null (* If [first] has been solved by side effect: do nothing. *)
-      | Some first ->
-          Proof.set {initial with comb=[first]} >>
-          t
-      end >>= fun y ->
-      Proof.get >>= fun step ->
-      Proof.set {step with comb=goals} >>
-      tclDISPATCHGEN null join tacs >>= fun x ->
-      Proof.get >>= fun step' ->
-      Proof.set {step' with comb=step.comb@step'.comb} >>
-      Proof.ret (join y x)
-  | _ , _ -> tclZERO SizeMismatch
+  match tacs with
+  | [] ->
+      begin 
+        Proof.get >>= fun initial ->
+        match initial.comb with
+        | [] -> tclUNIT (join [])
+        | _ -> tclZERO SizeMismatch
+      end
+  | [tac] ->
+      begin
+        Proof.get >>= fun initial ->
+        match initial.comb with
+        | [goal] ->
+            on_advance goal
+              ~solved:( tclUNIT (join []) )
+              ~adv:begin fun _ ->
+                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 )
+      end >>= fun res ->
+      Proof.ret (join (List.rev res))
 
-let unitK () () = ()
-let tclDISPATCH = tclDISPATCHGEN () unitK
+let tclDISPATCH tacs = tclDISPATCHGEN (fun _ -> ()) tacs
 
 let tclDISPATCHL tacs =
-  let tacs =
-    List.map begin fun tac ->
-      tclBIND tac (fun a -> tclUNIT [a])
-    end tacs
-  in
-  tclDISPATCHGEN [] (@) tacs
+  tclDISPATCHGEN Util.identity tacs
 
-let extend_to_list =
-  let rec copy n x l =
-    if n < 0 then raise SizeMismatch
-    else if Int.equal n 0 then l
-    else copy (n-1) x (x::l)
+let extend_to_list startxs rx endxs l =
+  (* spiwack: I use [l] essentially as a natural number *)
+  let rec duplicate acc = function
+    | [] -> acc
+    | _::rest -> duplicate (rx::acc) rest
   in
-  fun startxs rx endxs l ->
-    let ns = List.length startxs in
-    let ne = List.length endxs in
-    let n = List.length l in
-    startxs@(copy (n-ne-ns) rx endxs)
+  let rec tail to_match rest =
+    match rest, to_match with
+    | [] , _::_ -> raise SizeMismatch
+    | _::rest , _::to_match -> tail to_match rest
+    | _ , [] -> duplicate endxs rest
+  in
+  let rec copy pref rest =
+    match rest,pref with
+    | [] , _::_ -> raise SizeMismatch
+    | _::rest, a::pref -> a::(copy pref rest)
+    | _ , [] -> tail endxs rest
+  in
+  copy startxs l
+
 let tclEXTEND tacs1 rtac tacs2 =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
@@ -336,6 +435,16 @@ let tclEXTEND tacs1 rtac tacs2 =
   let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
   tclDISPATCH tacs
 
+(* arnaud: À première vue, ça ne change franchement pas grand chose:
+   J'observe genre 2 secondes de mieux avec ça sur l'intégralité de la stdlib… *)
+let tclINDEPENDENT tac =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun initial ->
+  match initial.comb with
+  | [] -> tclUNIT ()
+  | [_] -> tac
+  | _ -> list_iter_goal () (fun _ () -> tac)
 
 (* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
     everything is done in one step. *)
@@ -459,8 +568,8 @@ let rec list_map f = function
   | [] -> tclUNIT []
   | a::l ->
       f a >= fun a' ->
-        list_map f l >= fun l' ->
-          tclUNIT (a'::l')
+      list_map f l >= fun l' ->
+      tclUNIT (a'::l')
 
 
 (*** Compatibility layer with <= 8.2 tactics ***)
@@ -491,6 +600,14 @@ module V82 = struct
     with e when catchable_exception e ->
       tclZERO e
 
+  (* A [Proofview.tactic] version of [Refiner.tclEVARS] *)
+  let tclEVARS evd =
+    (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+    let (>>=) = Proof.bind in
+    Proof.get >>= fun ps ->
+    Proof.set { ps with solution = evd }
+    
+
   let has_unresolved_evar pv =
     Evd.has_undefined pv.solution
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 5caffa8bdc..3f80768d83 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -178,6 +178,11 @@ val tclDISPATCHL : 'a tactic list -> 'a list tactic
     is applied to every goal in between. *)
 val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
 
+(* [tclINDEPENDENT tac] runs [tac] on each goal successively, from the
+   first one to the last one. Backtracking in one goal is independent of
+   backtracking in another. *)
+val tclINDEPENDENT : unit tactic -> unit tactic
+
 (* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*)
 val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic 
 
@@ -241,6 +246,8 @@ module V82 : sig
   type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma 
   val tactic : tac -> unit tactic
 
+  val tclEVARS : Evd.evar_map -> unit tactic
+
   val has_unresolved_evar : proofview -> bool
 
   (* Main function in the implementation of Grab Existential Variables.
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 668b47e16e..aec8e27f87 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1127,8 +1127,11 @@ and eval_tactic ist = function
         (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) gl
       end
   | TacThen (t1,tf,t,tl) ->
-      Tacticals.New.tclTHENS3PARTS (interp_tactic ist t1)
-	(Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
+      if Array.length tf = 0 && Array.length tl = 0 then
+        Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
+      else
+        Tacticals.New.tclTHENS3PARTS (interp_tactic ist t1)
+	  (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
   | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl)
   | TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
   | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac)
@@ -1175,7 +1178,7 @@ and interp_ltac_reference loc' mustbetac ist = function
 and interp_tacarg ist arg =
   let tac_of_old f =
     Tacmach.New.of_old f >>== fun (sigma,v) ->
-    Proofview.V82.tactic (tclEVARS sigma) <*>
+    Proofview.V82.tclEVARS sigma <*>
     (Proofview.Goal.return v)
   in
   match arg with
@@ -1827,7 +1830,7 @@ and interp_atomic ist tac =
               let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in
               Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>= fun patt ->
               Tacticals.New.tclTHEN
-	        (Proofview.V82.tactic (tclEVARS sigma))
+	        (Proofview.V82.tclEVARS sigma)
                 (Tactics.forward (Option.map (interp_tactic ist) t)
 	           (Option.map patt ipat) c)
         with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
@@ -1855,7 +1858,7 @@ and interp_atomic ist tac =
         (* We try to fully-typecheck the term *)
         Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
 	Tacticals.New.tclTHEN
-	  (Proofview.V82.tactic (tclEVARS sigma))
+	  (Proofview.V82.tclEVARS sigma)
           (h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
       else
         (* We try to keep the pattern structure as much as possible *)
@@ -1909,18 +1912,18 @@ and interp_atomic ist tac =
   | TacDecomposeAnd c ->
       Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
       Tacticals.New.tclTHEN
-	(Proofview.V82.tactic (tclEVARS sigma))
+	(Proofview.V82.tclEVARS sigma)
 	(Elim.h_decompose_and c_interp)
   | TacDecomposeOr c ->
       Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
       Tacticals.New.tclTHEN
-	(Proofview.V82.tactic (tclEVARS sigma))
+	(Proofview.V82.tclEVARS sigma)
 	(Elim.h_decompose_or c_interp)
   | TacDecompose (l,c) ->
       let l = List.map (interp_inductive ist) l in
       Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
       Tacticals.New.tclTHEN
-	(Proofview.V82.tactic (tclEVARS sigma))
+	(Proofview.V82.tclEVARS sigma)
 	(Elim.h_decompose l c_interp)
   | TacSpecialize (n,cb) ->
       Proofview.tclEVARMAP >= fun sigma ->
@@ -2049,7 +2052,7 @@ and interp_atomic ist tac =
       | Some c ->
           Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
           Tacticals.New.tclTHEN
-	    (Proofview.V82.tactic (tclEVARS sigma))
+	    (Proofview.V82.tclEVARS sigma)
 	    (h_transitivity (Some c_interp))
       end
 
@@ -2100,7 +2103,7 @@ and interp_atomic ist tac =
 	  sigma , a_interp::acc
 	end l (goal_sigma,[])
       end >>= fun (sigma,args) ->
-      Proofview.V82.tactic (tclEVARS sigma) <*>
+      Proofview.V82.tclEVARS sigma <*>
       tac args ist
   | TacAlias (loc,s,l,(_,body)) ->
       Proofview.Goal.env >>= fun env ->
@@ -2121,15 +2124,15 @@ and interp_atomic ist tac =
           | GenArgType -> f (out_gen (glbwit wit_genarg) x)
           | ConstrArgType ->
               Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) >>== fun (sigma,v) ->
-              Proofview.V82.tactic (tclEVARS sigma) <*>
+              (Proofview.V82.tclEVARS sigma) <*>
 	      (Proofview.Goal.return v)
           | OpenConstrArgType false ->
               Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) >>== fun (sigma,v) ->
-              Proofview.V82.tactic (tclEVARS sigma) <*>
+              (Proofview.V82.tclEVARS sigma) <*>
 	      (Proofview.Goal.return v)
           | ConstrMayEvalArgType ->
               Tacmach.New.of_old (fun gl -> interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x)) >>== fun (sigma,c_interp) ->
-              Proofview.V82.tactic (tclEVARS sigma) <*>
+              Proofview.V82.tclEVARS sigma <*>
 	      Proofview.Goal.return (Value.of_constr c_interp)
           | ListArgType ConstrArgType ->
               let wit = glbwit (wit_list wit_constr) in
@@ -2139,7 +2142,7 @@ and interp_atomic ist tac =
 	          sigma , c_interp::acc
 	        end (out_gen wit x) (project gl,[])
               end >>== fun (sigma,l_interp) ->
-              Proofview.V82.tactic (tclEVARS sigma) <*>
+              (Proofview.V82.tclEVARS sigma) <*>
               (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) l_interp))
           | ListArgType VarArgType ->
               let wit = glbwit (wit_list wit_var) in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 2553b9bf93..8156c898ec 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -384,20 +384,20 @@ module New = struct
       tclUNIT ()
     with e -> tclZERO e
   let tclORELSE0 t1 t2 =
-    tclEXTEND [] begin
+    tclINDEPENDENT begin
       tclORELSE
         t1
         begin fun e ->
           catch_failerror e <*> t2
         end
-    end []
+    end
   let tclORELSE t1 t2 =
     tclORELSE0 (tclPROGRESS t1) t2
 
   let tclTHENS3PARTS t1 l1 repeat l2 =
-    tclEXTEND [] begin
+    tclINDEPENDENT begin
       t1 <*> tclEXTEND (Array.to_list l1) repeat (Array.to_list l2)
-    end []
+    end
   let tclTHENSFIRSTn t1 l repeat =
     tclTHENS3PARTS t1 l repeat [||]
   let tclTHENFIRSTn t1 l =
@@ -407,14 +407,14 @@ module New = struct
       t1 <*> tclFOCUS 1 1 t2
     end []
   let tclTHENLASTn t1 l =
-    tclEXTEND [] begin
+    tclINDEPENDENT begin
       t1 <*> tclEXTEND [] (tclUNIT()) (Array.to_list l)
-    end []
+    end
   let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
   let tclTHENS t l =
-    tclEXTEND [] begin
+    tclINDEPENDENT begin
       t <*> tclDISPATCH l
-    end []
+    end
   let tclTHENLIST l =
     List.fold_left tclTHEN (tclUNIT()) l
 
@@ -427,11 +427,11 @@ module New = struct
     tclORELSE0 t (tclUNIT ())
 
   let tclIFTHENELSE t1 t2 t3 =
-    tclEXTEND [] begin
+    tclINDEPENDENT begin
       tclIFCATCH t1
         (fun () -> t2)
         (fun _ -> t3)
-    end []
+    end
   let tclIFTHENSVELSE t1 a t3 =
     tclIFCATCH t1
       (fun () -> tclDISPATCH (Array.to_list a))
@@ -460,11 +460,11 @@ module New = struct
     else tclTHEN t (tclDO (n-1) t)
 
   let rec tclREPEAT0 t =
-    tclEXTEND [] begin
+    tclINDEPENDENT begin
       tclIFCATCH t
         (fun () -> tclREPEAT0 t)
         (fun _ -> tclUNIT ())
-    end []
+    end
   let tclREPEAT t =
     tclREPEAT0 (tclPROGRESS t)
   let rec tclREPEAT_MAIN0 t =
@@ -476,10 +476,8 @@ module New = struct
 
   let tclCOMPLETE t =
     t >= fun res ->
-      (tclEXTEND
-         []
+      (tclINDEPENDENT
          (tclZERO (Errors.UserError ("",str"Proof is not complete.")))
-         []
       ) <*>
         tclUNIT res