Ground update, new files.

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

9 files changed, 267 insertions, 192 deletions

diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4
index f0cd3afa6..b8f684977 100644
--- a/contrib/first-order/ground.ml4
+++ b/contrib/first-order/ground.ml4
@@ -13,6 +13,7 @@
 open Formula
 open Sequent
 open Rules
+open Instances
 open Term
 open Tacmach
 open Tactics
@@ -79,7 +80,8 @@ let ground_tac solver startseq gl=
 		       cont_tac gl
 		     else 
 		       (match 
-			  Unify.give_right_instances i dom triv atoms seq with
+			  Instances.give_right_instances i dom triv atoms seq 
+			with
 			      Some l -> tclORELSE
 				(exists_tac l toptac (re_add seq)) cont_tac gl
 			    | None ->
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
new file mode 100644
index 000000000..8625c988d
--- /dev/null
+++ b/contrib/first-order/instances.ml
@@ -0,0 +1,178 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Formula
+open Sequent
+open Unify
+open Rules
+open Util
+open Term
+open Tacmach
+open Tactics
+open Tacticals
+open Termops
+open Reductionops
+open Declarations
+open Formula
+open Sequent
+open Libnames
+
+let rev_rels n t= (* requires n = max (free_rels t) *) 
+  let l=list_tabulate (fun i->mkRel (n-i)) n in
+    substl l t
+ 	  
+let renum_metas_from k n t=(* requires n = max (free_rels t) *)
+  let l=list_tabulate (fun i->mkMeta (k+i)) n in
+    substl l t
+
+(* ordre lexico:
+   nombre de metas dans terme;
+   profondeur de matching;
+   le reste
+*)
+      
+let compare_instance inst1 inst2=
+	match inst1,inst2 with
+	    Phantom(d1),Phantom(d2)->
+	      (OrderedConstr.compare d1 d2)
+	  | Real((m1,c1),n1),Real((m2,c2),n2)->
+	      ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n2 n1 c1 c2
+	  | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1
+	  | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1
+
+module OrderedRightInstance=
+struct 
+  type t = instance
+  let compare = compare_instance
+end
+
+module OrderedLeftInstance=
+struct
+  type t=instance * Libnames.global_reference
+  let compare (inst1,id1) (inst2,id2)=
+    (compare_instance =? Pervasives.compare) inst1 inst2 id1 id2
+    (* we want a __decreasing__ total order *)
+end
+  
+module RIS=Set.Make(OrderedRightInstance)
+module LIS=Set.Make(OrderedLeftInstance)
+
+let make_goal_atoms seq=
+  match seq.gl with
+      Atomic t->{negative=[];positive=[t]}
+    | Complex (_,_,l)->l 
+
+let make_left_atoms seq=
+    {negative=seq.latoms;positive=[]}
+
+let do_sequent setref triv add mkelt seq i dom atoms=
+  let flag=ref true in
+  let phref=ref triv in
+  let do_atoms a1 a2 =
+    let do_pair t1 t2 = 
+      match unif_atoms i dom t1 t2 with
+	  None->()
+	| Some (Phantom _) ->phref:=true
+	| Some c ->flag:=false;setref:=add (mkelt c) !setref in
+      List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive;
+      List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in
+    HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes;
+    do_atoms atoms (make_left_atoms seq);
+    do_atoms atoms (make_goal_atoms seq);
+    !flag && !phref 
+ 
+let give_right_instances i dom triv atoms seq=
+  let setref=ref RIS.empty in
+  let inj inst=inst in
+  if do_sequent setref triv RIS.add inj seq i dom atoms then
+    None
+  else
+    Some (RIS.elements !setref)
+
+let match_one_forall_hyp setref seq lf=
+  match lf.pat with 
+      Lforall(i,dom,triv)->
+	let inj x=(x,lf.id) in
+	  if do_sequent setref triv LIS.add inj seq i dom lf.atoms then
+	    setref:=LIS.add ((Phantom dom),lf.id) !setref 
+    | _ ->anomaly "can't happen" 
+
+let give_left_instances lfh seq=
+  let setref=ref LIS.empty in
+    List.iter (match_one_forall_hyp setref seq) lfh;
+    LIS.elements !setref
+	  	  
+(*tactics*)
+
+
+let rec collect_forall seq=
+  if is_empty_left seq then ([],seq) 
+  else
+    let hd,seq1=take_left seq in
+      (match hd.pat with 
+	   Lforall(_,_,_)-> 
+	     let (q,seq2)=collect_forall seq1 in
+	       ((hd::q),seq2)
+	 | _->[],seq)
+
+let left_instance_tac (inst,id) tacrec seq=
+  match inst with
+      Phantom dom->
+	if lookup (id,None) seq then 
+	  tclFAIL 0 "already done"
+	else
+	  tclTHENS (cut dom) 
+	    [tclTHENLIST
+	       [intro;
+		(fun gls->generalize 
+		   [mkApp(constr_of_reference id,
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
+		intro;
+		tclSOLVE [wrap 1 false tacrec 
+			    (deepen (record (id,None) seq))]];
+	    tclTRY assumption]
+    | Real((m,t) as c,_)->
+	if lookup (id,Some c) seq || m>0 then 
+	  tclFAIL 0 "already done" 
+	else
+	  tclTHENLIST 
+	    [generalize [mkApp(constr_of_reference id,[|t|])];
+	     intro; 
+	     tclSOLVE 
+	       [wrap 1 false tacrec 
+		  (deepen (record (id,Some c) seq))]]
+
+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 dummy_exists_tac dom  tacrec seq=
+	tclTHENS (cut dom) 
+	[tclTHENLIST
+	   [intro;
+	    (fun gls->
+	       split (Rawterm.ImplicitBindings 
+			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
+	    tclSOLVE [wrap 0 false tacrec (deepen seq)]];
+	 tclTRY assumption] 
+ 
+let right_instance_tac inst tacrec seq=
+  match inst with
+      Phantom _ ->anomaly "can't happen" 
+    | Real ((m,t),_) ->
+	if m>0 then tclFAIL 0 "not implemented ... yes"
+	else
+	tclTHEN (split (Rawterm.ImplicitBindings [t]))
+	(tclSOLVE [wrap 0 true tacrec (deepen seq)])
+
+let exists_tac insts tacrec seq gl=
+    tclFIRST 
+      (List.map (fun inst -> right_instance_tac inst tacrec seq) insts) gl
+
diff --git a/contrib/first-order/instances.mli b/contrib/first-order/instances.mli
new file mode 100644
index 000000000..b1d88280b
--- /dev/null
+++ b/contrib/first-order/instances.mli
@@ -0,0 +1,40 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Term
+open Tacmach
+open Names
+open Libnames
+open Rules
+  
+val give_right_instances : metavariable -> constr -> bool -> Formula.atoms -> 
+  Sequent.t -> Unify.instance list option
+
+val give_left_instances : Formula.left_formula list-> Sequent.t -> 
+  (Unify.instance*global_reference) list
+
+val collect_forall : Sequent.t -> Formula.left_formula list * Sequent.t
+
+val left_instance_tac : Unify.instance * global_reference -> seqtac
+
+val left_forall_tac : Formula.left_formula list -> seqtac
+
+val dummy_exists_tac : constr -> seqtac
+
+val right_instance_tac : Unify.instance -> seqtac
+
+val exists_tac : Unify.instance list -> seqtac
+	       
+
+
+
+
+
+
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 01ae688ad..c5c7319e8 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -19,7 +19,6 @@ open Reductionops
 open Declarations
 open Formula
 open Sequent
-open Unify
 open Libnames
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
@@ -193,64 +192,7 @@ let ll_forall_tac prod id tacrec seq=
 
 (* complicated stuff for instantiation with unification *)
 
-let rec collect_forall seq=
-  if is_empty_left seq then ([],seq) 
-  else
-    let hd,seq1=take_left seq in
-      (match hd.pat with 
-	   Lforall(_,_,_)-> 
-	     let (q,seq2)=collect_forall seq1 in
-	       ((hd::q),seq2)
-	 | _->[],seq)
-
-let left_instance_tac (inst,id) tacrec seq=
-  match inst with
-      Phantom dom->
-	if lookup id None seq then 
-	  tclFAIL 0 "already done"
-	else
-	  tclTHENS (cut dom) 
-	    [tclTHENLIST
-	       [intro;
-		(fun gls->generalize 
-		   [mkApp(constr_of_reference id,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
-		intro;
-		tclSOLVE [wrap 1 false tacrec 
-			    (deepen (record id None seq))]];
-	    tclTRY assumption]
-    | Real(t,_)->
-	if lookup id (Some t) seq then 
-	  tclFAIL 0 "already done" 
-	else
-	  tclTHENLIST 
-	    [generalize [mkApp(constr_of_reference id,[|t|])];
-	     intro; 
-	     tclSOLVE 
-	       [wrap 1 false tacrec 
-		  (deepen (record id (Some t) seq))]]
-
-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 dummy_exists_tac dom  tacrec seq=
-	tclTHENS (cut dom) 
-	[tclTHENLIST
-	   [intro;
-	    (fun gls->
-	       split (Rawterm.ImplicitBindings 
-			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
-	    tclSOLVE [wrap 0 false tacrec (deepen seq)]];
-	 tclTRY assumption] 
- 
-let right_instance_tac (t,_) tacrec seq=
-	tclTHEN (split (Rawterm.ImplicitBindings [t]))
-	(tclSOLVE [wrap 0 true tacrec (deepen seq)])
-
-let exists_tac insts tacrec seq gl=
-    tclFIRST 
-      (List.map (fun inst -> right_instance_tac inst tacrec seq) insts) gl
+(* moved to instances.ml *)
 
 (* special for compatibility with old Intuition *)
 
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index 045316263..10ffe863d 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -19,47 +19,37 @@ type lseqtac= global_reference -> seqtac
 
 val wrap : int -> bool -> seqtac
 
+val id_of_global: global_reference -> identifier
+
 val clear_global: global_reference -> tactic
 
 val axiom_tac : constr -> Sequent.t -> tactic
 
+val ll_atom_tac : constr -> lseqtac
+
 val evaluable_tac : evaluable_global_reference -> seqtac
 
 val left_evaluable_tac : evaluable_global_reference -> lseqtac
 
 val and_tac : seqtac
 
-val left_and_tac : inductive -> lseqtac
-
 val or_tac : seqtac
 
-val left_or_tac : inductive -> lseqtac
-
-val forall_tac : seqtac
-
-val collect_forall : Sequent.t -> Formula.left_formula list * Sequent.t
-
-val left_instance_tac : Unify.instance * global_reference -> seqtac
-
-val left_forall_tac : Formula.left_formula list -> seqtac
-
 val arrow_tac : seqtac
 
-val dummy_exists_tac : constr -> seqtac
+val left_and_tac : inductive -> lseqtac
 
-val right_instance_tac : constr * int -> seqtac
+val left_or_tac : inductive -> lseqtac
 
-val exists_tac : (constr * int) list -> seqtac
-	       
-val left_exists_tac : inductive -> lseqtac
+val left_false_tac : global_reference -> tactic
 
-val ll_arrow_tac : constr -> constr -> constr -> lseqtac
+val ll_ind_tac : inductive -> constr list -> lseqtac
 
-val ll_atom_tac : constr -> lseqtac
+val ll_arrow_tac : constr -> constr -> constr -> lseqtac
 
-val left_false_tac : global_reference -> tactic
+val forall_tac : seqtac
 
-val ll_ind_tac : inductive -> constr list -> lseqtac
+val left_exists_tac : inductive -> lseqtac
 
 val ll_forall_tac : types -> lseqtac
 
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 4ece7c8c5..91a8f1ddd 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -11,6 +11,7 @@
 open Term
 open Util
 open Formula
+open Unify
 open Tacmach
 open Names
 open Libnames
@@ -120,14 +121,17 @@ struct
   let compare=compare_constr
 end
 
+type h_item = global_reference * (int*constr) option
+
 module Hitem=
 struct 
-  type t=(global_reference * constr option)
+  type t = h_item
   let compare (id1,co1) (id2,co2)=
     (Pervasives.compare 
      =? (fun oc1 oc2 ->
 	   match oc1,oc2 with 
-	       Some c1,Some c2 -> OrderedConstr.compare c1 c2
+	       Some (m1,c1),Some (m2,c2) -> 
+		 ((-) =? OrderedConstr.compare) m1 m2 c1 c2
 	     | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
 end
 
@@ -163,9 +167,9 @@ type t=
 
 let deepen seq={seq with depth=seq.depth-1}
  
-let record id topt seq={seq with history=History.add (id,topt) seq.history}
+let record item seq={seq with history=History.add item seq.history}
 
-let lookup id topt seq=History.mem (id,topt) seq.history
+let lookup item seq=History.mem item seq.history
 
 let add_left (nam,t) seq internal gl=
   match build_left_entry nam t internal gl seq.cnt with
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
index 851396d45..79cf0d1ed 100644
--- a/contrib/first-order/sequent.mli
+++ b/contrib/first-order/sequent.mli
@@ -23,7 +23,9 @@ module OrderedConstr: Set.OrderedType with type t=constr
 
 module CM: Map.S with type key=constr
 
-module History: Set.S with type elt = global_reference * constr option
+type h_item = global_reference * (int*constr) option
+
+module History: Set.S with type elt = h_item
 
 val cm_add : constr -> global_reference -> global_reference list CM.t ->
   global_reference list CM.t
@@ -43,9 +45,9 @@ type t = {redexes:HP.t;
 
 val deepen: t -> t
 
-val record: global_reference -> constr option -> t -> t
+val record: h_item -> t -> t
 
-val lookup: global_reference -> constr option -> t -> bool
+val lookup: h_item -> t -> bool
 
 val add_left : global_reference * constr -> t -> bool -> 
   Proof_type.goal sigma -> t
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index b9c3a1a42..30ff1c811 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -10,17 +10,22 @@
 
 open Util
 open Formula 
-open Sequent
 open Tacmach
 open Term
 open Names
 open Termops
-open Pattern
 open Reductionops
 
 exception UFAIL of constr*constr
 
-let unif t1 t2= (* Martelli-Montanari style *)
+(* 
+   RIGID-only Martelli-Montanari style unification for CLOSED terms 
+   I repeat : t1 and t2 must NOT have ANY free deBruijn                        
+   sigma is kept normal with respect to itself but is lazily applied 
+   to the equation set. Raises UFAIL with a pair of  terms 
+*)
+
+let unif t1 t2= 
   let bige=Queue.create () 
   and sigma=ref [] in
   let bind i t=
@@ -83,9 +88,6 @@ let unif t1 t2= (* Martelli-Montanari style *)
 	(* this place is unreachable but needed for the sake of typing *)
     with Queue.Empty-> !sigma
 
-(* collect tries finds ground instantiations for Meta i*)
-let is_ground t=(Clenv.collect_metas t)=[]
-
 let is_head_meta t=match kind_of_term t with Meta _->true | _ ->false
 
 let value i t=
@@ -100,7 +102,7 @@ let value i t=
     vaux t
 	  
 type instance=
-    Real of (constr*int) (* instance*valeur heuristique*)
+    Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
   | Phantom of constr (* domaine de quantification *)
 
 let mk_rel_inst t=
@@ -118,97 +120,15 @@ let mk_rel_inst t=
 	       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 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
+  if is_head_meta t1 || is_head_meta t2 then None else
     try 
       let t=List.assoc i (unif t1 t2) in 
-	if is_ground t then Some (Real(t,value i t1))
-	else if is_head_meta t then Some (Phantom dom)
-	else None
+	if is_head_meta t then Some (Phantom dom)
+	else Some (Real(mk_rel_inst t,value i t1))
     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
-	    Phantom(d1),Phantom(d2)->
-	      (OrderedConstr.compare d1 d2)
-	  | Real(c1,n1),Real(c2,n2)->
-	      ((-) =? OrderedConstr.compare) n2 n1 c1 c2
-	  | Phantom(_),_-> 1
-	  | _,_-> -1
-
-module OrderedRightInstance=
-struct 
-  type t = constr*int
-  let compare (c1,n1) (c2,n2) = ((-) =? OrderedConstr.compare) n2 n1 c1 c2
-end
-
-module OrderedLeftInstance=
-struct
-  type t=instance * Libnames.global_reference
-  let compare (inst1,id1) (inst2,id2)=
-    (compare_instance =? Pervasives.compare) inst1 inst2 id1 id2
-    (* we want a __decreasing__ total order *)
-end
-  
-module RIS=Set.Make(OrderedRightInstance)
-module LIS=Set.Make(OrderedLeftInstance)
-
-let make_goal_atoms seq=
-  match seq.gl with
-      Atomic t->{negative=[];positive=[t]}
-    | Complex (_,_,l)->l 
-
-let make_left_atoms seq=
-    {negative=seq.latoms;positive=[]}
-
-let do_sequent setref triv add mkelt seq i dom atoms=
-  let flag=ref true in
-  let phref=ref triv in
-  let do_atoms a1 a2 =
-    let do_pair t1 t2 = 
-      match unif_atoms i dom t1 t2 with
-	  None->()
-	| Some (Phantom _) ->phref:=true
-	| Some c ->flag:=false;setref:=add (mkelt c) !setref in
-      List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive;
-      List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in
-    HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes;
-    do_atoms atoms (make_left_atoms seq);
-    do_atoms atoms (make_goal_atoms seq);
-    !flag && !phref 
- 
-let give_right_instances i dom triv atoms seq=
-  let setref=ref RIS.empty in
-  let inj=function
-       Real c->c
-     | _->anomaly "can't happen" in
-  if do_sequent setref triv RIS.add inj seq i dom atoms then
-    None
-  else
-    Some (RIS.elements !setref)
-
-let match_one_forall_hyp setref seq lf=
-  match lf.pat with 
-      Lforall(i,dom,triv)->
-	let inj x=(x,lf.id) in
-	  if do_sequent setref triv LIS.add inj seq i dom lf.atoms then
-	    setref:=LIS.add ((Phantom dom),lf.id) !setref 
-    | _ ->anomaly "can't happen" 
-
-let give_left_instances lfh seq=
-  let setref=ref LIS.empty in
-    List.iter (match_one_forall_hyp setref seq) lfh;
-    LIS.elements !setref
-
+	  
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
index 7effac207..013fc73cd 100644
--- a/contrib/first-order/unify.mli
+++ b/contrib/first-order/unify.mli
@@ -8,17 +8,14 @@
 
 (* $Id$ *)
 
-open Libnames
 open Term
 
+exception UFAIL of constr*constr
+
+val unif : constr -> constr -> (int*constr) list
+
 type instance=
-    Real of (constr*int) (* instance*valeur heuristique*)
-  | Phantom of constr (* domaine de quantification *)
+    Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
+  | Phantom of constr        (* domaine de quantification *)
 
 val unif_atoms : metavariable -> constr -> constr -> constr -> instance option
-  
-val give_right_instances : metavariable -> constr -> bool -> Formula.atoms -> 
-  Sequent.t -> (constr*int) list option
-
-val give_left_instances : Formula.left_formula list-> Sequent.t -> 
-  (instance*global_reference) list