Ground update.

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

7 files changed, 150 insertions, 120 deletions

diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index dea7c552e..156ef7ae2 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -84,13 +84,13 @@ let match_with_evaluable gl t=
 	
 type kind_of_formula=
     Arrow of constr*constr
+  | False of inductive*constr list
   | And of inductive*constr list
   | Or of inductive*constr list
   | Exists of inductive*constr list
   | Forall of constr*constr
   | Atom of constr
-  | Evaluable of evaluable_global_reference*constr
-  | False
+  | Evaluable of evaluable_global_reference*constr 
       
 let rec kind_of_formula gl term =
   let cciterm=whd_betaiotazeta term in
@@ -108,7 +108,7 @@ let rec kind_of_formula gl term =
 			Atom cciterm 
 		      else
 			(match Array.length mip.mind_consnames with
-			     0->False
+			     0->False(ind,l)
 			   | 1->And(ind,l)
 			   | _->Or(ind,l)) 
 		| _ ->  
@@ -130,7 +130,7 @@ let build_atoms gl metagen polarity cciterm =
   let pfenv=lazy (pf_env gl) in
   let rec build_rec env polarity cciterm =
     match kind_of_formula gl cciterm with
-	False->if not polarity then trivial:=true
+	False(_,_)->if not polarity then trivial:=true
       | Arrow (a,b)->
 	  build_rec env (not polarity) a;
 	  build_rec env polarity b
@@ -184,7 +184,7 @@ type right_formula =
       
 type left_arrow_pattern=
     LLatom
-  | LLfalse
+  | LLfalse of inductive*constr list
   | LLand of inductive*constr list
   | LLor of inductive*constr list
   | LLforall of constr
@@ -216,7 +216,7 @@ let build_left_entry nam typ internal gl metagen=
       else no_atoms in
     let pattern=
       match kind_of_formula gl typ with
-	  False        ->  Lfalse
+	  False(i,_)        ->  Lfalse
 	| Atom a       ->  raise (Is_atom a)
 	| And(i,_)         ->  Land i
 	| Or(i,_)          ->  Lor i
@@ -226,7 +226,7 @@ let build_left_entry nam typ internal gl metagen=
 	| Evaluable (egc,_) ->Levaluable egc 
 	| Arrow (a,b) ->LA (a, 
 			    match kind_of_formula gl a with
-				False->      LLfalse
+				False(i,l)-> LLfalse(i,l)
 			      | Atom t->     LLatom
 			      | And(i,l)->      LLand(i,l)
 			      | Or(i,l)->       LLor(i,l)
@@ -250,7 +250,7 @@ let build_right_entry typ gl metagen=
       else no_atoms in
     let pattern=
       match kind_of_formula gl typ with
-	  False        -> raise (Is_atom typ)
+	  False(_,_)        -> raise (Is_atom typ)
 	| Atom a       -> raise (Is_atom a)
 	| And(_,_)        -> Rand
 	| Or(_,_)         -> Ror
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index b2c4e2499..7b5e9d826 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -33,13 +33,13 @@ val match_with_evaluable : Proof_type.goal Tacmach.sigma ->
 
 type kind_of_formula=
     Arrow of constr*constr
+  | False of inductive*constr list
   | And of inductive*constr list
   | Or of inductive*constr list
   | Exists of inductive*constr list
   | Forall of constr*constr
   | Atom of constr
   | Evaluable of Names.evaluable_global_reference * Term.constr
-  | False
 
 val kind_of_formula : Proof_type.goal Tacmach.sigma -> 
   constr -> kind_of_formula
@@ -63,7 +63,7 @@ type right_formula =
       
 type left_arrow_pattern=
     LLatom
-  | LLfalse
+  | LLfalse of inductive*constr list
   | LLand of inductive*constr list
   | LLor of inductive*constr list
   | LLforall of constr
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4
index 926a7918a..f0cd3afa6 100644
--- a/contrib/first-order/ground.ml4
+++ b/contrib/first-order/ground.ml4
@@ -66,8 +66,9 @@ let ground_tac solver startseq gl=
   and right_tac seq ctx gl=
     let re_add s=re_add_left_list ctx s in
       match seq.gl with
-	  Complex (pat,_,atoms)->
-	    (match pat with
+	  Atomic _ -> left_tac seq ctx gl
+	| Complex (pat,_,atoms)->
+	    match pat with
 		 Ror->
 		   tclORELSE
 		   (or_tac toptac (re_add seq))
@@ -79,13 +80,12 @@ let ground_tac solver startseq gl=
 		     else 
 		       (match 
 			  Unify.give_right_instances i dom triv atoms seq with
-			    Some l -> tclORELSE
-			      (exists_tac l toptac (re_add seq)) cont_tac gl
-			  | None ->
-			      tclORELSE cont_tac
-			      (dummy_exists_tac dom  toptac (re_add seq)) gl)
-	       | _-> anomaly "unreachable place")
-	| Atomic _ -> left_tac seq ctx gl
+			      Some l -> tclORELSE
+				(exists_tac l toptac (re_add seq)) cont_tac gl
+			    | None ->
+				tclORELSE cont_tac
+				(dummy_exists_tac dom  toptac (re_add seq)) gl)
+	       | _-> anomaly "unreachable place"
   and left_tac seq ctx gl=
     if is_empty_left seq then 
       solver gl
@@ -119,17 +119,15 @@ let ground_tac solver startseq gl=
 	      (match lap with
 		   LLatom->
 		     right_tac seq1 (hd::ctx) 
-		 | LLfalse->
-		     ll_false_tac hd.id toptac (re_add seq1) 
-		 | LLand (ind,largs) | LLor(ind,largs) ->
+		 | LLfalse (ind,largs) | LLand (ind,largs) | LLor(ind,largs) ->
 		     ll_ind_tac ind largs hd.id toptac (re_add seq1) 
 		 | LLforall p ->	      
 		     tclORELSE
-		       (if seq.depth<=0 || not !qflag then 
-			  tclFAIL 0 "max depth" 
-			else 
-			  ll_forall_tac p hd.id toptac (re_add seq1))
-		       (left_tac seq1 (hd::ctx))
+		     (if seq.depth<=0 || not !qflag then 
+			tclFAIL 0 "max depth" 
+		      else 
+			ll_forall_tac p hd.id toptac (re_add seq1))
+		     (left_tac seq1 (hd::ctx))
 		 | LLexists (ind,l) ->
 		     if !qflag then
 		       ll_ind_tac ind l hd.id toptac (re_add seq1) 
@@ -140,8 +138,7 @@ let ground_tac solver startseq gl=
 		     (ll_arrow_tac a b c hd.id toptac (re_add seq1))
 		     (left_tac seq1 (hd::ctx))
 		 | LLevaluable egr->
-		     left_evaluable_tac egr hd.id toptac (re_add seq1))
-	      gl in
+		     left_evaluable_tac egr hd.id toptac (re_add seq1)) gl in
     wrap (List.length (pf_hyps gl)) true toptac (startseq gl) gl
       
 let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
@@ -161,10 +158,6 @@ let gen_ground_tac flag taco l gl=
 	set_qflag backup;result
     with e -> set_qflag backup;raise e
 	   
-open Genarg
-open Pcoq
-open Pp
-
 TACTIC EXTEND Ground
       |   [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> 
 	    [ gen_ground_tac true (Some (snd t)) l ]
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index dafef4efe..01ae688ad 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -52,10 +52,25 @@ let clear_global=function
     VarRef id->clear [id]
   | _->tclIDTAC
       
+
+(* connection rules *)
+
 let axiom_tac t seq=
   try exact_no_check (constr_of_reference (find_left t seq)) 
   with Not_found->tclFAIL 0 "No axiom link" 
 
+let ll_atom_tac a id tacrec seq=
+  try 
+    tclTHENLIST
+      [generalize [mkApp(constr_of_reference id,
+			 [|constr_of_reference (find_left a seq)|])];
+       clear_global id;
+       intro;
+       wrap 1 false tacrec seq] 
+  with Not_found->tclFAIL 0 "No link" 
+
+(* evaluation rules *)
+
 let evaluable_tac ec tacrec seq gl=
   tclTHEN
     (unfold_in_concl [[1],ec]) 
@@ -71,9 +86,19 @@ let left_evaluable_tac ec id tacrec seq gl=
 	  unfold_in_hyp [[1],ec] (Tacexpr.InHypType nid) gls);
      wrap 1 false tacrec seq] gl
 
+(* right connectives rules *)
+
 let and_tac tacrec seq=
   tclTHEN simplest_split (wrap 0 true tacrec seq)
 
+let or_tac tacrec seq=
+  any_constructor (Some (tclSOLVE [wrap 0 true tacrec seq]))
+
+let arrow_tac tacrec seq=
+  tclTHEN intro (wrap 1 true tacrec seq)
+   
+(* left connectives rules *)
+
 let left_and_tac ind id tacrec seq=
   let n=(construct_nhyps ind).(0) in  
     tclTHENLIST 
@@ -82,9 +107,6 @@ let left_and_tac ind id tacrec seq=
        tclDO n intro;
        wrap n false tacrec seq]
 
-let or_tac tacrec seq=
-  any_constructor (Some (tclSOLVE [wrap 0 true tacrec seq]))
-
 let left_or_tac ind id tacrec seq=
   let v=construct_nhyps ind in  
   let f n=
@@ -96,9 +118,81 @@ let left_or_tac ind id tacrec seq=
       (simplest_elim (constr_of_reference id))
       (Array.map f v)
 
+let left_false_tac id=
+  simplest_elim (constr_of_reference id)
+
+(* left arrow connective rules *)
+
+(* We use this function for false, and, or, exists *)
+
+let ll_ind_tac ind largs id tacrec seq gl= 
+  (try
+     let rcs=ind_hyps 0 ind largs in
+     let vargs=Array.of_list largs in
+	     (* construire le terme  H->B, le generaliser etc *)   
+     let myterm i=
+       let rc=rcs.(i) in
+       let p=List.length rc in
+       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 (constr_of_reference id)),[|capply|]) in
+	 Sign.it_mkLambda_or_LetIn head rc in
+       let lp=Array.length rcs in
+       let newhyps=list_tabulate myterm lp in
+	 tclTHENLIST 
+	   [generalize newhyps;
+	    clear_global id;
+	    tclDO lp intro;
+	    wrap lp false tacrec seq]
+   with Invalid_argument _ ->tclFAIL 0 "") gl
+
+let ll_arrow_tac a b c id tacrec seq=
+  let cc=mkProd(Anonymous,a,(lift 1 b)) in
+  let d=mkLambda (Anonymous,b,
+		  mkApp ((constr_of_reference id),
+			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+    tclTHENS (cut c)
+      [tclTHENLIST
+	 [intro;
+	  clear_global id;
+	  wrap 1 false tacrec seq];
+       tclTHENS (cut cc) 
+         [exact_no_check (constr_of_reference id); 
+	  tclTHENLIST 
+	    [generalize [d];
+	     intro;
+	     clear_global id;
+	     tclSOLVE [wrap 1 true tacrec seq]]]]
+
+(* quantifier rules (easy side) *)
+
 let forall_tac tacrec seq=
   tclTHEN intro (wrap 0 true tacrec seq)
 
+let left_exists_tac ind id tacrec seq=
+  let n=(construct_nhyps ind).(0) in  
+    tclTHENLIST
+      [simplest_elim (constr_of_reference id);
+       clear_global id;
+       tclDO n intro;
+       (wrap (n-1) false tacrec seq)]
+
+let ll_forall_tac prod id tacrec seq=
+  tclTHENS (cut prod)
+    [tclTHENLIST
+       [intro;
+	(fun gls->
+	   let id0=pf_nth_hyp_id gls 1 in
+	   let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in
+	     tclTHEN (generalize [term]) (clear [id0]) gls);  
+	clear_global id;
+	intro;
+	tclSOLVE [wrap 1 false tacrec (deepen seq)]];
+     tclSOLVE [wrap 0 true tacrec (deepen seq)]]
+
+(* complicated stuff for instantiation with unification *)
+
 let rec collect_forall seq=
   if is_empty_left seq then ([],seq) 
   else
@@ -140,9 +234,6 @@ let left_forall_tac lfp tacrec seq gl=
   let insts=give_left_instances lfp seq in
     tclFIRST (List.map (fun inst->left_instance_tac inst tacrec seq) insts) gl
 	  
-let arrow_tac tacrec seq=
-  tclTHEN intro (wrap 1 true tacrec seq)
-   
 let dummy_exists_tac dom  tacrec seq=
 	tclTHENS (cut dom) 
 	[tclTHENLIST
@@ -161,84 +252,7 @@ let exists_tac insts tacrec seq gl=
     tclFIRST 
       (List.map (fun inst -> right_instance_tac inst tacrec seq) insts) gl
 
-let left_exists_tac ind id tacrec seq=
-  let n=(construct_nhyps ind).(0) in  
-    tclTHENLIST
-      [simplest_elim (constr_of_reference id);
-       clear_global id;
-       tclDO n intro;
-       (wrap (n-1) false tacrec seq)]
-
-let ll_arrow_tac a b c id tacrec seq=
-  let cc=mkProd(Anonymous,a,(lift 1 b)) in
-  let d=mkLambda (Anonymous,b,
-		  mkApp ((constr_of_reference id),
-			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
-    tclTHENS (cut c)
-      [tclTHENLIST
-	 [intro;
-	  clear_global id;
-	  wrap 1 false tacrec seq];
-       tclTHENS (cut cc) 
-         [exact_no_check (constr_of_reference id); 
-	  tclTHENLIST 
-	    [generalize [d];
-	     intro;
-	     clear_global id;
-	     tclSOLVE [wrap 1 true tacrec seq]]]]
-
-let ll_atom_tac a id tacrec seq=
-  try 
-    tclTHENLIST
-      [generalize [mkApp(constr_of_reference id,
-			 [|constr_of_reference (find_left a seq)|])];
-       clear_global id;
-       intro;
-       wrap 1 false tacrec seq] 
-  with Not_found->tclFAIL 0 "No link" 
-
-let ll_false_tac id tacrec seq =
-  tclTHEN (clear_global id) (wrap 0 false tacrec seq)
-
-let left_false_tac id=
-  simplest_elim (constr_of_reference id)
-
-(*We use this function for and, or, exists*)
-
-let ll_ind_tac ind largs id tacrec seq gl= 
-  (try
-     let rcs=ind_hyps 0 ind largs in
-     let vargs=Array.of_list largs in
-	     (* construire le terme  H->B, le generaliser etc *)   
-     let myterm i=
-       let rc=rcs.(i) in
-       let p=List.length rc in
-       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 (constr_of_reference id)),[|capply|]) in
-	 Sign.it_mkLambda_or_LetIn head rc in
-       let lp=Array.length rcs in
-       let newhyps=list_tabulate myterm lp in
-	 tclTHENLIST 
-	   [generalize newhyps;
-	    clear_global id;
-	    tclDO lp intro;
-	    wrap lp false tacrec seq]
-   with Invalid_argument _ ->tclFAIL 0 "") gl
-
-let ll_forall_tac prod id tacrec seq=
-  tclTHENS (cut prod)
-    [tclTHENLIST
-       [intro;
-	(fun gls->
-	   let id0=pf_nth_hyp_id gls 1 in
-	   let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in
-	     tclTHEN (generalize [term]) (clear [id0]) gls);  
-	clear_global id;
-	intro;
-	tclSOLVE [wrap 1 false tacrec (deepen seq)]];
-     tclSOLVE [wrap 0 true tacrec (deepen seq)]]
+(* special for compatibility with old Intuition *)
 
 let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
 
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index f47a40180..045316263 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -57,8 +57,6 @@ val ll_arrow_tac : constr -> constr -> constr -> lseqtac
 
 val ll_atom_tac : constr -> lseqtac
 
-val ll_false_tac : lseqtac
-
 val left_false_tac : global_reference -> tactic
 
 val ll_ind_tac : inductive -> constr list -> lseqtac
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 4587a3ddf..4ece7c8c5 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -30,7 +30,7 @@ let priority = function (* pure heuristics, <=0 for non reversible *)
     | LA(_,lap) ->
 	match lap with
 	    LLatom             ->   0
-	  | LLfalse            -> 100
+	  | LLfalse (_,_)      -> 100
 	  | LLand (_,_)        ->  80
 	  | LLor (_,_)         ->  70
 	  | LLforall _         -> -20
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index 1172d4cbe..b9c3a1a42 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -102,6 +102,24 @@ let value i t=
 type instance=
     Real of (constr*int) (* instance*valeur heuristique*)
   | Phantom of constr (* domaine de quantification *)
+
+let mk_rel_inst t=
+  let new_rel=ref 1 in
+  let rel_env=ref [] in
+  let rec renum_rec d t=
+    match kind_of_term t with 
+	Meta n->
+	  (try 
+	     mkRel (d+(List.assoc n !rel_env))
+	   with Not_found->
+	     let m= !new_rel in
+	       incr new_rel;
+	       rel_env:=(n,m) :: !rel_env;
+	       mkRel (m+d))
+      | _ -> map_constr_with_binders succ renum_rec d t
+  in 
+  let nt=renum_rec 0 t in
+    (!new_rel - 1,nt)
  	  
 let unif_atoms i dom t1 t2=
   if is_head_meta t1 || is_head_meta t2  then None else
@@ -113,6 +131,13 @@ let unif_atoms i dom t1 t2=
     with
 	UFAIL(_,_) ->None
       | Not_found ->Some (Phantom dom)
+
+(* ordre lexico:
+   nombre de metas dans terme;
+   profondeur de matching;
+   le reste
+*)
+
       
 let compare_instance inst1 inst2=
 	match inst1,inst2 with