Ground update + some bugfix

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

7 files changed, 127 insertions, 155 deletions

diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 3b387d73ae..dea7c552e7 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -118,47 +118,68 @@ let rec kind_of_formula gl term =
 			 match match_with_evaluable gl cciterm with 
 			     Some (ec,t)->Evaluable (ec,t)
 			   | None ->Atom cciterm
-			       
-let build_atoms gl metagen=
+  
+type atoms = {positive:constr list;negative:constr list}
+
+let no_atoms = (false,{positive=[];negative=[]})
+
+let build_atoms gl metagen polarity cciterm =
+  let trivial =ref false
+  and positive=ref []
+  and negative=ref [] in
+  let pfenv=lazy (pf_env gl) in
   let rec build_rec env polarity cciterm =
     match kind_of_formula gl cciterm with
-	False->[]
+	False->if not polarity then trivial:=true
       | Arrow (a,b)->
-	  (build_rec env (not polarity) a)@
-	  (build_rec env polarity b)
+	  build_rec env (not polarity) a;
+	  build_rec env polarity b
       | And(i,l) | Or(i,l)->
 	  let v = ind_hyps 0 i l in
-	  let g i accu (_,_,t) =
-	    (build_rec env polarity (lift i t))@accu in
-	  let f l accu =
-	    list_fold_left_i g (1-(List.length l)) accu l in
-	    Array.fold_right f v [] 
+	  let g i _ (_,_,t) =
+	    build_rec env polarity (lift i t) in
+	  let f l =
+	    list_fold_left_i g (1-(List.length l)) () l in
+	    if polarity && (* we have a constant constructor *)
+	      array_exists (function []->true|_->false) v 
+	    then trivial:=true;
+	    Array.iter f v 
       | Exists(i,l)->
 	  let var=mkMeta (metagen true) in
 	  let v =(ind_hyps 1 i l).(0) in
-	  let g i accu (_,_,t) =
-	    (build_rec (var::env) polarity (lift i t))@accu in
-	    list_fold_left_i g (2-(List.length l)) [] v
+	  let g i _ (_,_,t) =
+	    build_rec (var::env) polarity (lift i t) in
+	    list_fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
 	  let var=mkMeta (metagen true) in
 	    build_rec (var::env) polarity b
       | Atom t->
-	  [polarity,(substnl env 0 cciterm)]
+	  let unsigned=substnl env 0 t in
+	    if polarity then 
+	      positive:= unsigned :: !positive 
+	    else 
+	      negative:= unsigned :: !negative
       | Evaluable(ec,t)->
-	  let nt=Tacred.unfoldn [[1],ec] (pf_env gl) (Refiner.sig_sig gl) t in
+	  let nt=Tacred.unfoldn [[1],ec] (Lazy.force pfenv) 
+		   (Refiner.sig_sig gl) t in
 	    build_rec env polarity nt
-  in build_rec []
+  in 
+    build_rec [] polarity cciterm;
+    (!trivial,
+     {positive= !positive;
+      negative= !negative})
+
        
 type right_pattern =
     Rand
   | Ror 
   | Rforall
-  | Rexists of metavariable*constr
+  | Rexists of metavariable*constr*bool
   | Rarrow
   | Revaluable of evaluable_global_reference
       
 type right_formula =
-    Complex of right_pattern*constr*((bool*constr) list)
+    Complex of right_pattern*constr*atoms
   | Atomic of constr
       
 type left_arrow_pattern=
@@ -175,7 +196,7 @@ type left_pattern=
     Lfalse    
   | Land of inductive
   | Lor of inductive 
-  | Lforall of metavariable*constr
+  | Lforall of metavariable*constr*bool
   | Lexists of inductive
   | Levaluable of evaluable_global_reference
   | LA of constr*left_arrow_pattern
@@ -183,11 +204,16 @@ type left_pattern=
 type left_formula={id:global_reference;
 		   constr:constr;
 		   pat:left_pattern;
-		   atoms:(bool*constr) list;
+		   atoms:atoms;
 		   internal:bool}
     
 let build_left_entry nam typ internal gl metagen=
   try 
+    let m=meta_succ(metagen false) in
+    let trivial,atoms=
+      if !qflag then 
+	build_atoms gl metagen false typ 
+      else no_atoms in
     let pattern=
       match kind_of_formula gl typ with
 	  False        ->  Lfalse
@@ -195,7 +221,8 @@ let build_left_entry nam typ internal gl metagen=
 	| And(i,_)         ->  Land i
 	| Or(i,_)          ->  Lor i
 	| Exists (ind,_) ->  Lexists ind 
-	| Forall (d,_) -> let m=meta_succ(metagen false) in Lforall(m,d)
+	| Forall (d,_) -> 
+	    Lforall(m,d,trivial)
 	| Evaluable (egc,_) ->Levaluable egc 
 	| Arrow (a,b) ->LA (a, 
 			    match kind_of_formula gl a with
@@ -206,20 +233,21 @@ let build_left_entry nam typ internal gl metagen=
 			      | Arrow(a,c)-> LLarrow(a,c,b)
 			      | Exists(i,l)->LLexists(i,l)
 			      | Forall(_,_)->LLforall a
-			      | Evaluable (egc,_)-> LLevaluable egc) in    
-    let l=
-      if !qflag then 
-	build_atoms gl metagen false typ 
-      else [] in
+			      | Evaluable (egc,_)-> LLevaluable egc) in
       Left {id=nam;
 	    constr=typ;
 	    pat=pattern;
-	    atoms=l;
+	    atoms=atoms;
 	    internal=internal}
   with Is_atom a-> Right a
     
 let build_right_entry typ gl metagen=
   try
+    let m=meta_succ(metagen false) in 
+    let trivial,atoms=
+      if !qflag then 
+	build_atoms gl metagen true typ
+      else no_atoms in
     let pattern=
       match kind_of_formula gl typ with
 	  False        -> raise (Is_atom typ)
@@ -227,16 +255,11 @@ let build_right_entry typ gl metagen=
 	| And(_,_)        -> Rand
 	| Or(_,_)         -> Ror
 	| Exists (i,l) -> 
-	    let m=meta_succ(metagen false) in 
 	    let (_,_,d)=list_last (ind_hyps 0 i l).(0) in
-	      Rexists(m,d)
+	      Rexists(m,d,trivial)
 	| Forall (_,a) -> Rforall 
 	| Arrow (a,b) -> Rarrow 
 	| Evaluable (egc,_)->Revaluable egc in
-    let l=
-      if !qflag then 
-	build_atoms gl metagen true typ
-      else [] in
-      Complex(pattern,typ,l)
+      Complex(pattern,typ,atoms)
   with Is_atom a-> Atomic a
 
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index c71c7fce2f..b2c4e2499e 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -43,20 +43,22 @@ type kind_of_formula=
 
 val kind_of_formula : Proof_type.goal Tacmach.sigma -> 
   constr -> kind_of_formula
+
+type atoms = {positive:constr list;negative:constr list}
 			
 val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> 
-  bool -> constr -> (bool*constr) list
+  bool -> constr -> bool * atoms
 
 type right_pattern =
     Rand
   | Ror 
   | Rforall
-  | Rexists of metavariable*constr
+  | Rexists of metavariable*constr*bool
   | Rarrow
   | Revaluable of Names.evaluable_global_reference
     
 type right_formula =
-    Complex of right_pattern*constr*((bool*constr) list)
+    Complex of right_pattern*constr*atoms
   | Atomic of constr
       
 type left_arrow_pattern=
@@ -73,7 +75,7 @@ type left_pattern=
     Lfalse    
   | Land of inductive
   | Lor of inductive 
-  | Lforall of metavariable*constr
+  | Lforall of metavariable*constr*bool
   | Lexists of inductive
   | Levaluable of Names.evaluable_global_reference
   | LA of constr*left_arrow_pattern
@@ -81,7 +83,7 @@ type left_pattern=
 type left_formula={id:global_reference;
 		   constr:constr;
 		   pat:left_pattern;
-		   atoms:(bool*constr) list;
+		   atoms:atoms;
 		   internal:bool}
 
 (*exception Is_atom of constr*)
@@ -92,5 +94,3 @@ val build_left_entry :
 
 val build_right_entry : types -> Proof_type.goal Tacmach.sigma -> 
   counter -> right_formula
-
-
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4
index ce2ba22fff..78887715a0 100644
--- a/contrib/first-order/ground.ml4
+++ b/contrib/first-order/ground.ml4
@@ -24,6 +24,8 @@ open Goptions
 (* declaring search depth as a global option *)
 
 let ground_depth=ref 5
+
+let set_qflag b= qflag:=b
 		   
 let _=
   let gdopt=
@@ -70,12 +72,13 @@ let ground_tac solver startseq gl=
 		   tclORELSE
 		   (or_tac toptac (re_add seq))
 		   (left_tac seq ctx) gl
-	       | Rexists(i,dom)->
+	       | Rexists(i,dom,triv)->
 		   let cont_tac=left_tac seq ctx in
 		     if seq.depth<=0 || not !qflag then 
 		       cont_tac gl
 		     else 
-		       (match Unify.give_right_instances i dom atoms seq with
+		       (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 ->
@@ -96,7 +99,7 @@ let ground_tac solver startseq gl=
 	      left_and_tac ind hd.id toptac (re_add seq1) gl
 	  | Lor ind->
 	      left_or_tac ind hd.id toptac (re_add seq1) gl
-	  | Lforall (i,dom)->
+	  | Lforall (_,_,_)->
 	      let (lfp,seq2)=collect_forall seq in
 		tclORELSE
 		  (if seq.depth<=0 || not !qflag then 
@@ -122,11 +125,11 @@ let ground_tac solver startseq gl=
 		     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) 
@@ -145,19 +148,18 @@ let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
     
 let fail_solver=tclFAIL 0 "GroundTauto failed"
 		      
-let gen_ground_tac flag taco l=
+let gen_ground_tac flag taco l gl=
   let backup= !qflag in
     try
-      qflag:=flag;
+      set_qflag flag;
       let solver= 
 	match taco with 
 	    Some tac->tac
 	  | None-> default_solver in
       let startseq=create_with_ref_list l !ground_depth in
-      let result=
-	ground_tac solver startseq
-      in qflag:=backup;result
-    with e -> qflag:=backup;raise e
+      let result=ground_tac solver startseq gl in 
+	set_qflag backup;result
+    with e -> set_qflag backup;raise e
 	   
 open Genarg
 open Pcoq
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 1af4db1bce..4c8c8f9b3d 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -105,7 +105,7 @@ let rec collect_forall seq=
   else
     let hd,seq1=take_left seq in
       (match hd.pat with 
-	   Lforall(i,dom)-> 
+	   Lforall(_,_,_)-> 
 	     let (q,seq2)=collect_forall seq1 in
 	       ((hd::q),seq2)
 	 | _->[],seq)
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index bd24d38f5e..4587a3ddff 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -24,7 +24,7 @@ let priority = function (* pure heuristics, <=0 for non reversible *)
       Lfalse             ->1000
     | Land _             ->  90
     | Lor _              ->  40
-    | Lforall (_,_)      -> -30 (* must stay at lowest priority *)
+    | Lforall (_,_,_)      -> -30 (* must stay at lowest priority *)
     | Lexists _           ->  60
     | Levaluable _       -> 100
     | LA(_,lap) ->
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index e5ac4134f5..1172d4cbec 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -100,7 +100,7 @@ let value i t=
     vaux t
 	  
 type instance=
-    Real of constr*int (* instance*valeur heuristique*)
+    Real of (constr*int) (* instance*valeur heuristique*)
   | Phantom of constr (* domaine de quantification *)
  	  
 let unif_atoms i dom t1 t2=
@@ -139,104 +139,51 @@ end
   
 module RIS=Set.Make(OrderedRightInstance)
 module LIS=Set.Make(OrderedLeftInstance)
-  
-(* le premier argument est une sous formule a instancier *)
-
-let match_atom_with_latoms i dom (pol,atom) latoms accu=
-  if pol then 
-    let f latom accu=
-      match unif_atoms i dom atom latom with
-	  None->accu
-	| Some (Phantom _) ->(true,snd accu)
-	| Some (Real(t,i)) ->(false,RIS.add (t,i) (snd accu)) in
-      List.fold_right f latoms accu
-  else accu 
-
-let match_atom_with_hyp_atoms i dom (pol,atom) lf accu=
-  let f (b,hatom) accu=
-    if b=pol then accu else
-      match unif_atoms i dom atom hatom with
-	  None->accu
-	| Some (Phantom _) ->(true,snd accu)
-	| Some (Real(t,i))->(false,RIS.add (t,i) (snd accu)) in
-    List.fold_right f lf.atoms accu
-
-let match_atom_with_goal i dom (pol,atom) glatoms accu=
-  let f (b,glatom) accu=
-    if b=pol then accu else
-      match unif_atoms i dom atom glatom with
-	  None->accu
-	| Some (Phantom _) ->(true,snd accu)
-	| Some (Real(t,i)) ->(false,RIS.add (t,i) (snd accu)) in
-    List.fold_right f glatoms accu
-
-let give_right_instances i dom ratoms seq=
-  let f ratom accu=
-    let accu1= match_atom_with_goal i dom ratom ratoms accu in
-    let accu2=
-      match_atom_with_latoms i dom ratom seq.latoms accu1 in
-      HP.fold (match_atom_with_hyp_atoms i dom ratom) seq.redexes accu2 in
-  let (b,accu0)=List.fold_right f ratoms (false,RIS.empty) in
-    if b & RIS.is_empty accu0 then 
-      None
-    else
-      Some (RIS.elements accu0)
-
-(*left*) 
-	  
-let match_named_atom_with_latoms id i dom (pol,atom) latoms accu=
-  if pol then 
-    let f latom accu=
-      match unif_atoms i dom atom latom with
-	  None->accu
-	| Some (Phantom _) ->(true,snd accu)
-	| Some inst ->(false,LIS.add (inst,id) (snd accu)) in
-      List.fold_right f latoms accu
-  else accu 
-
-let match_named_atom_with_hyp_atoms id i dom (pol,atom) lf accu=
-  let f (b,hatom) accu=
-    if b=pol then accu else
-      match unif_atoms i dom atom hatom with
-	  None->accu
-	| Some (Phantom _) ->(true,snd accu)
-	| Some inst->(false,LIS.add (inst,id) (snd accu)) in
-    List.fold_right f lf.atoms accu
-
-let match_named_atom_with_goal id i dom (pol,atom) gl accu=
-  match gl with 
-      Atomic t->
-	if pol then accu else
-	  (match unif_atoms i dom atom t with
-	       None->accu
-	     | Some (Phantom _) ->(true,snd accu)
-	     | Some inst ->(false,LIS.add (inst,id) (snd accu)))
-    | Complex (_,_,glatoms)->
-	let f (b,glatom) accu=
-	  if b=pol then accu else
-	    match unif_atoms i dom atom glatom with
-		None->accu
-	      | Some (Phantom _) ->(true,snd accu)
-	      | Some inst ->(false,LIS.add (inst,id) (snd accu)) in
-	  List.fold_right f glatoms accu
 
-let match_one_forall_hyp seq lf accu=
+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)->
-	let f latom accu=
-	  let accu1=match_named_atom_with_goal lf.id i dom latom seq.gl accu in
-	  let accu2=
-	    match_named_atom_with_latoms lf.id i dom latom seq.latoms accu1 in
-	    HP.fold (match_named_atom_with_hyp_atoms lf.id i dom latom) 
-	      seq.redexes accu2 in
-	let (b,accu0)=List.fold_right f lf.atoms (false,LIS.empty) in
-	  if b & LIS.is_empty accu0 then 
-	    LIS.add (Phantom dom,lf.id) accu
-	  else
-	    LIS.union accu0 accu
+      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=
-  LIS.elements (List.fold_right (match_one_forall_hyp seq) lfh LIS.empty)
+  let setref=ref LIS.empty in
+    List.iter (match_one_forall_hyp setref seq) lfh;
+    LIS.elements !setref
 
-(* TODO: match with goal *)
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
index 90d3cb3f99..7effac2079 100644
--- a/contrib/first-order/unify.mli
+++ b/contrib/first-order/unify.mli
@@ -12,12 +12,12 @@ open Libnames
 open Term
 
 type instance=
-    Real of constr*int (* instance*valeur heuristique*)
+    Real of (constr*int) (* instance*valeur heuristique*)
   | Phantom of constr (* domaine de quantification *)
 
 val unif_atoms : metavariable -> constr -> constr -> constr -> instance option
   
-val give_right_instances : metavariable -> constr -> (bool * constr) list -> 
+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 ->