bugfix in Ground tactic

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

8 files changed, 133 insertions, 75 deletions

diff --git a/contrib/first-order/engine.ml4 b/contrib/first-order/engine.ml4
index 8b85316a90..133fbe1229 100644
--- a/contrib/first-order/engine.ml4
+++ b/contrib/first-order/engine.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "parsing/grammar.cma"  i*)
 
 (* $Id$ *)
 
@@ -19,7 +19,7 @@ open Tactics
 open Tacticals
 open Util
 
-let mytac ninst solver gl=
+let ground_tac ninst solver gl=
   let metagen=newcnt () in
   let rec toptac ninst seq gl=
     match seq.gl with 
@@ -66,13 +66,13 @@ let mytac ninst solver gl=
 	      (left_tac ninst seq1 (hd::ctx)) gl
 	  | Lexists ->left_exists_tac hd.id seq1 (toptac ninst) metagen gl
 	  | LAatom a->
-	      let pat,atoms=
-		match seq1.gl with 
-		    Atomic t->assert false
-		  | Complex (pat,atoms)->pat,atoms in
-	      tclORELSE 
+	      tclORELSE
 	      (ll_atom_tac a hd.id (re_add seq1) (toptac ninst) metagen)
-	      (right_tac ninst seq1 pat atoms (hd::ctx)) gl
+	      (match seq1.gl with 
+		  Atomic t->
+		    (left_tac ninst seq1 (hd::ctx))
+		| Complex (pat,atoms)->
+		    (right_tac ninst seq1 pat atoms (hd::ctx))) gl
 	  | LAfalse->ll_false_tac hd.id seq1 (toptac ninst) metagen gl
 	  | LAand (ind,largs) | LAor(ind,largs) ->
 	      ll_ind_tac ind largs hd.id seq1 (toptac ninst) metagen gl
@@ -89,17 +89,28 @@ let mytac ninst solver gl=
 	      (ll_arrow_tac a b c hd.id (re_add seq1) 
 		   (toptac ninst) metagen)
 	      (left_tac ninst seq1 (hd::ctx)) gl in
+  let startseq=create_with_auto_hints gl metagen in
     wrap (List.length (pf_hyps gl)) true empty_seq (toptac ninst) metagen gl
 
-let default_solver=Tacinterp.interp <:tactic<Auto with *>>
-    
-let default_depth=5
+let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
+		     
+let gen_ground_tac io taco=
+   let depth=
+     match io with 
+	 Some i->i
+       | None-> !Auto.default_search_depth in
+   let solver= 
+     match taco with 
+	 Some t->snd t
+       | None-> default_solver in
+     ground_tac depth default_solver
 
 TACTIC EXTEND Ground
-   [ "Ground" ] -> [ mytac default_depth default_solver]
-|  [ "Ground" integer(n)] -> [ mytac n default_solver]
-|  [ "Ground" tactic(t)] -> [ mytac default_depth (snd t)]    
-|  [ "Ground" integer(n) tactic(t)] -> [ mytac n (snd t)]
+   [ "Ground" ] -> [ gen_ground_tac None None ]    
+|  [ "Ground" integer(n)] -> [ gen_ground_tac (Some n) None]
+|  [ "Ground" tactic(t)] -> [ gen_ground_tac None (Some t)]    
+|  [ "Ground" integer(n) tactic(t)] -> 
+     [ gen_ground_tac (Some n) (Some t) ]
 END
 
  
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index aee1c01d07..e6406f107b 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -16,6 +16,7 @@ open Reductionops
 open Tacmach
 open Util
 open Declarations
+open Libnames
 
 type ('a,'b)sum=Left of 'a|Right of 'b
 
@@ -73,7 +74,7 @@ let rec nb_prod_after n c=
   match kind_of_term c with
     | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else 
 	1+(nb_prod_after 0 b)
-    | _            -> 0
+    | _ -> 0
 
 let nhyps mip = 
   let constr_types = mip.mind_nf_lc in 
@@ -81,21 +82,23 @@ let nhyps mip =
     Array.map nhyps constr_types
 
 let construct_nhyps ind= nhyps (snd (Global.lookup_inductive ind))
-      
+    
+exception Dependent_Inductive
+
 (* builds the array of arrays of constructor hyps for (ind Vargs)*)
 let ind_hyps ind largs= 
   let (mib,mip) = Global.lookup_inductive ind in
-    if Inductiveops.mis_is_recursive (ind,mib,mip) then 
-      failwith "no_recursion" else      
-	let n=mip.mind_nparams in
-	  if n<>(List.length largs) then anomaly "params ?" else
-	    let p=nhyps mip in
-	    let lp=Array.length p in
-	    let types= mip.mind_nf_lc in   
-	    let myhyps i=
-	      let t1=Term.prod_applist types.(i) largs in
-		fst (Sign.decompose_prod_n_assum p.(i) t1) in
-	      Array.init lp myhyps
+  let n = mip.mind_nparams in
+    if n<>(List.length largs) then 
+      raise Dependent_Inductive
+    else
+      let p=nhyps mip in
+      let lp=Array.length p in
+      let types= mip.mind_nf_lc in   
+      let myhyps i=
+	let t1=Term.prod_applist types.(i) largs in
+	  fst (Sign.decompose_prod_n_assum p.(i) t1) in
+	Array.init lp myhyps
 
 let kind_of_formula cciterm =
   match match_with_imp_term cciterm with
@@ -128,12 +131,15 @@ let build_atoms metagen=
 	  (build_rec env (not polarity) a)@
 	  (build_rec env polarity b)
       | And(i,l) | Or(i,l)->
-	  let v = ind_hyps i l in
-	    Array.fold_right
-	      (fun l accu->
-		 List.fold_right 
-		 (fun (_,_,t) accu0->
-		    (build_rec env polarity t)@accu0) l accu) v []
+	  (try
+	    let v = ind_hyps i l in
+	      Array.fold_right
+		(fun l accu->
+		   List.fold_right 
+		   (fun (_,_,t) accu0->
+		      (build_rec env polarity t)@accu0) l accu) v []
+	  with Dependent_Inductive ->
+	    [polarity,(substnl env 0 cciterm)])
       | Forall(_,b)|Exists(_,_,b,_)->
 	  let var=mkMeta (metagen true) in
 	    build_rec (var::env) polarity b 
@@ -166,13 +172,14 @@ type left_pattern=
   | LAexists of inductive*constr*constr*constr
   | LAarrow of constr*constr*constr
       
-type left_formula={id:identifier;
+type left_formula={id:global_reference;
 		   pat:left_pattern;
-		   atoms:(bool*constr) list}
+		   atoms:(bool*constr) list;
+		   internal:bool}
     
 exception Is_atom of constr
 
-let build_left_entry nam typ metagen=
+let build_left_entry nam typ internal metagen=
   try 
     let pattern=
       match kind_of_formula typ with
@@ -192,7 +199,7 @@ let build_left_entry nam typ metagen=
 	       | Exists(i,a,_,p)->LAexists(i,a,p,b)
 	       | Forall(_,_)->LAforall a) in    
     let l=build_atoms metagen false typ in
-      Left {id=nam;pat=pattern;atoms=l}
+      Left {id=nam;pat=pattern;atoms=l;internal=internal}
   with Is_atom a-> Right a
 
 let build_right_entry typ metagen=
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index bb6dc030aa..dfc90a1bf7 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -10,6 +10,7 @@
 
 open Term
 open Names
+open Libnames
 
 type ('a,'b) sum = Left of 'a | Right of 'b
 
@@ -27,7 +28,9 @@ type counter = bool -> int
 val newcnt : unit -> counter
 
 val construct_nhyps : inductive -> int array
-      
+
+exception Dependent_Inductive
+
 val ind_hyps : inductive -> constr list -> Sign.rel_context array
 
 val kind_of_formula : constr -> kind_of_formula
@@ -57,12 +60,13 @@ type left_pattern=
   | LAexists of inductive*constr*constr*constr
   | LAarrow of constr*constr*constr
       
-type left_formula={id:identifier;
+type left_formula={id:global_reference;
 		   pat:left_pattern;
-		   atoms:(bool*constr) list}
+		   atoms:(bool*constr) list;
+		   internal:bool}
 
 val build_left_entry : 
-  identifier -> types -> counter -> (left_formula,types) sum
+  global_reference -> types -> bool -> counter -> (left_formula,types) sum
 
 val build_right_entry : types -> counter -> right_formula
 
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 5e2e0a72d6..13258818f8 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -20,10 +20,11 @@ open Declarations
 open Formula
 open Sequent
 open Unify
+open Libnames
 
 type hptac= Sequent.t -> (Sequent.t -> tactic) -> counter -> tactic
 
-type lhptac= identifier -> hptac
+type lhptac= global_reference -> hptac
   
 let wrap n b seq tacrec metagen gls=
   let nc=pf_hyps gls in
@@ -31,16 +32,22 @@ let wrap n b seq tacrec metagen gls=
     if i<=0 then seq else 
       match nc with
 	  []->anomaly "Not the expected number of hyps"
-	| (id,_,typ)::q-> (add_left (id,typ) (aux (i-1) q) metagen) in
+	| (id,_,typ)::q-> 
+	    let gr=VarRef id in 
+	    (add_left (gr,typ) (aux (i-1) q) true metagen) in
   let seq1=
     if b then
       (change_right (pf_concl gls) (aux n nc) metagen)
     else
       (aux n nc) in
     tacrec seq1 gls
+
+let clear_global=function
+    VarRef id->clear [id]
+  | _->tclIDTAC
       
 let axiom_tac t seq=
-  try exact_no_check (mkVar (find_left t seq)) 
+  try exact_no_check (constr_of_reference (find_left t seq)) 
   with Not_found->tclFAIL 0 "No axiom link" 
 
 let and_tac seq tacrec metagen=
@@ -49,8 +56,8 @@ let and_tac seq tacrec metagen=
 let left_and_tac ind id seq tacrec metagen=
   let n=(construct_nhyps ind).(0) in  
     tclTHENLIST 
-      [simplest_elim (mkVar id);
-       clear [id]; 
+      [simplest_elim (constr_of_reference id);
+       clear_global id; 
        tclDO n intro;
        wrap n false seq tacrec metagen]
 
@@ -61,11 +68,11 @@ let left_or_tac ind id seq tacrec metagen=
   let v=construct_nhyps ind in  
   let f n=
     tclTHENLIST
-      [clear [id];
+      [clear_global id;
        tclDO n intro;
        wrap n false seq tacrec metagen] in
     tclTHENSV
-      (simplest_elim (mkVar id))
+      (simplest_elim (constr_of_reference id))
       (Array.map f v)
 
 let forall_tac seq tacrec metagen=
@@ -78,14 +85,14 @@ let left_forall_tac i dom atoms id seq tacrec metagen=
 	[tclTHENLIST
 	   [intro;
 	    (fun gls->generalize 
-	       [mkApp(mkVar id,[|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
+	       [mkApp(constr_of_reference id,[|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
 	    intro;
 	    tclSOLVE [wrap 1 false seq tacrec metagen]]
 	;tclIDTAC]
     else
       let tac t=
 	tclTHENLIST 
-	  [generalize [mkApp(mkVar id,[|t|])];
+	  [generalize [mkApp(constr_of_reference id,[|t|])];
 	   intro; 
 	   tclSOLVE [wrap 1 false seq tacrec metagen]] in
 	tclFIRST (List.map tac insts)
@@ -112,43 +119,44 @@ let exists_tac i dom atoms seq tacrec metagen=
 	       
 let left_exists_tac id seq tacrec metagen=
   tclTHENLIST
-    [simplest_elim (mkVar id);
-     clear [id];
+    [simplest_elim (constr_of_reference id);
+     clear_global id;
      tclDO 2 intro;
      (wrap 1 false seq tacrec metagen)]
 
 let ll_arrow_tac a b c id seq tacrec metagen=
   let cc=mkProd(Anonymous,a,(lift 1 b)) in
   let d=mkLambda (Anonymous,b,
-		  mkApp ((mkVar id),
+		  mkApp ((constr_of_reference id),
 			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclTHENS (cut c)
       [tclTHENLIST
 	 [intro;
-	  clear [id];
+	  clear_global id;
 	  wrap 1 false seq tacrec metagen];
        tclTHENS (cut cc) 
-         [exact_no_check (mkVar id); 
+         [exact_no_check (constr_of_reference id); 
 	  tclTHENLIST 
 	    [generalize [d];
 	     intro;
-	     clear [id];
+	     clear_global id;
 	     tclSOLVE [wrap 1 true seq tacrec metagen]]]]
 
 let ll_atom_tac a id seq tacrec metagen=
   try 
     tclTHENLIST
-      [generalize [mkApp(mkVar id,[|mkVar (find_left a seq)|])];
-       clear [id];
+      [generalize [mkApp(constr_of_reference id,
+			 [|constr_of_reference (find_left a seq)|])];
+       clear_global id;
        intro;
        wrap 1 false seq tacrec metagen] 
   with Not_found->tclFAIL 0 "No link" 
 
 let ll_false_tac id seq tacrec metagen=
-  tclTHEN (clear [id]) (wrap 0 false seq tacrec metagen)
+  tclTHEN (clear_global id) (wrap 0 false seq tacrec metagen)
 
 let left_false_tac id=
-  simplest_elim (mkVar id)
+  simplest_elim (constr_of_reference id)
 
 (*We use this function for and, or, exists*)
 
@@ -163,23 +171,24 @@ let ll_ind_tac ind largs id seq tacrec metagen gl=
        let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in
        let vars=Array.init p (fun j->mkRel (p-j)) in
        let capply=mkApp ((lift p cstr),vars) in
-       let head=mkApp ((lift p (mkVar id)),[|capply|]) in
+       let head=mkApp ((lift p (constr_of_reference id)),[|capply|]) in
 	 Sign.it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
        let newhyps=List.map myterm (interval 0 (lp-1)) in
 	 tclTHENLIST 
 	   [generalize newhyps;
-	    clear [id];
+	    clear_global id;
 	    tclDO lp intro;
 	    wrap lp false seq tacrec metagen]
-   with Invalid_argument _ ->tclFAIL 0 "") gl
+   with Dependent_Inductive | Invalid_argument _ ->tclFAIL 0 "") gl
 
 let ll_forall_tac prod id seq tacrec metagen=
   tclTHENS (cut prod)
     [tclTHENLIST
        [(fun gls->generalize 
-	   [mkApp(mkVar id,[|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
-	clear [id];
+	   [mkApp(constr_of_reference id,
+		  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
+	clear_global id;
 	intro;
 	tclSOLVE [wrap 1 false seq tacrec metagen]];
        tclSOLVE [wrap 0 true seq tacrec metagen]]
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index 98dc01bbed..ee224bc54c 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -11,13 +11,16 @@
 open Term
 open Tacmach
 open Names
+open Libnames
 
 type hptac= Sequent.t -> (Sequent.t -> tactic) -> Formula.counter -> tactic
 
-type lhptac= identifier -> hptac
+type lhptac= global_reference -> hptac
 
 val wrap : int -> bool -> hptac
 
+val clear_global: global_reference -> tactic
+
 val axiom_tac : constr -> Sequent.t -> tactic
 
 val and_tac : hptac
@@ -44,7 +47,7 @@ val ll_atom_tac : constr -> lhptac
 
 val ll_false_tac : lhptac
 
-val left_false_tac : identifier -> tactic
+val left_false_tac : global_reference -> tactic
 
 val ll_ind_tac : inductive -> constr list -> lhptac
 
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 84e3f18ed4..a229d8b86c 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -13,6 +13,7 @@ open Util
 open Formula
 open Tacmach
 open Names
+open Libnames
 
 let priority=function (* pure heuristics, <=0 for non reversible *)
       Lfalse             ->1000
@@ -57,10 +58,10 @@ module CM=Map.Make(OrderedConstr)
 module HP=Heap.Functional(OrderedFormula)
 
 type t=
-    {hyps:HP.t;hatoms:identifier CM.t;gl:right_formula}
+    {hyps:HP.t;hatoms:global_reference CM.t;gl:right_formula}
 
-let add_left (nam,t) seq metagen=
-  match build_left_entry nam t metagen with
+let add_left (nam,t) seq internal metagen=
+  match build_left_entry nam t internal metagen with
       Left f->{seq with hyps=HP.add f seq.hyps}
     | Right t->{seq with hatoms=CM.add t nam seq.hatoms}
 
@@ -95,3 +96,24 @@ let empty_seq=
    hatoms=CM.empty;
    gl=Atomic (mkMeta 1)}
 
+open Auto
+
+let create_with_auto_hints gl metagen=
+  let seqref=ref empty_seq in
+  let f p_a_t =
+    match p_a_t.code with
+	Res_pf (c,_) | Give_exact c
+      | Res_pf_THEN_trivial_fail (c,_) ->
+	  (try 
+	     let gr=reference_of_constr c in 
+	     let typ=(pf_type_of gl c) in
+	       seqref:=add_left (gr,typ) !seqref false metagen
+	   with Not_found->())
+      | _-> () in
+  let g _ l=List.iter f l in
+  let h str hdb=Hint_db.iter g hdb in
+    Util.Stringmap.iter h (!searchtable);
+    !seqref
+
+
+	
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
index 8b72b3f210..6b955adac4 100644
--- a/contrib/first-order/sequent.mli
+++ b/contrib/first-order/sequent.mli
@@ -13,6 +13,7 @@ open Util
 open Formula
 open Tacmach
 open Names
+open Libnames
 
 val right_reversible : right_pattern -> bool
 	
@@ -22,15 +23,15 @@ module CM: Map.S with type key=constr
 
 module HP: Heap.S with type elt=left_formula
 
-type t = {hyps:HP.t;hatoms: identifier CM.t;gl:right_formula}
+type t = {hyps:HP.t;hatoms: global_reference CM.t;gl:right_formula}
 
-val add_left : identifier * constr -> t -> counter -> t
+val add_left : global_reference * constr -> t -> bool -> counter -> t
 
 val re_add_left_list : left_formula list -> t -> t
 
 val change_right : constr -> t -> counter -> t
 
-val find_left : constr -> t -> identifier
+val find_left : constr -> t -> global_reference
 
 val rev_left : t -> bool
 
@@ -42,3 +43,4 @@ val take_right : t -> right_formula
 
 val empty_seq : t
 
+val create_with_auto_hints : Proof_type.goal sigma -> counter -> t
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index 9d6bb39d31..8dc0d96e6b 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -118,7 +118,7 @@ let match_lists i l1 l2=
       
 let find_instances i l seq=
   let match_hyp f accu=
-    CS.union (match_lists i l f.atoms) accu in
+    CS.union (if f.internal then match_lists i l f.atoms else CS.empty) accu in
   let match_atom t nam accu=
     CS.union (match_atom_list i (false,t) l) accu in
   let s1=