Ground update

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

5 files changed, 58 insertions, 33 deletions

diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 1715658dca..5026671847 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -20,6 +20,8 @@ open Libnames
 
 let qflag=ref true
 
+let red_flags=ref Closure.betaiotazeta
+
 let (=?) f g i1 i2 j1 j2=
   let c=f i1 i2 in
     if c=0 then g j1 j2 else c
@@ -63,18 +65,13 @@ let ind_hyps nevar ind largs=
       fst (Sign.decompose_prod_assum t2) in
     Array.init lp myhyps
 
-let match_with_evaluable gl t=
-  let env=pf_env gl in
-  let hd=       
-    match kind_of_term t with
-	App (head,_) -> head
-      | _ -> t in
-    match kind_of_term hd with
-	Const cst->
-	  if Environ.evaluable_constant cst env 
-	  then Some (EvalConstRef cst,t)
-	  else None
-      | _-> None
+let special_nf gl=
+  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> Closure.norm_val infos (Closure.inject t))
+
+let special_whd gl=
+  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
 
 type kind_of_formula=
     Arrow of constr*constr
@@ -86,8 +83,8 @@ type kind_of_formula=
   | Atom of constr
       
 let rec kind_of_formula gl term =
-  let normalize t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t in 
-  let cciterm=whd_betaiotazeta term in
+  let normalize=special_nf gl in
+  let cciterm=special_whd gl term in
     match match_with_imp_term cciterm with
 	Some (a,b)-> Arrow(a,(pop b))
       |_->
@@ -119,14 +116,7 @@ let rec kind_of_formula gl term =
 		| _ ->  
 		    match match_with_sigma_type cciterm with
 			Some (i,l)-> Exists((destInd i),l)
-		      |_-> 
-			 match match_with_evaluable gl cciterm with 
-			     Some (ec,t)->	  
-			       let nt=Tacred.unfoldn [[1],ec] 
-					(pf_env gl)
-					(Refiner.sig_sig gl) t in
-				 kind_of_formula gl nt
-			   | None ->Atom (normalize cciterm)
+		      |_-> Atom (normalize cciterm)
   
 type atoms = {positive:constr list;negative:constr list}
 
@@ -140,7 +130,7 @@ let build_atoms gl metagen side cciterm =
   let trivial =ref false
   and positive=ref []
   and negative=ref [] in
-  let normalize t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t in 
+  let normalize=special_nf gl in 
   let rec build_rec env polarity cciterm=
     match kind_of_formula gl cciterm with
 	False(_,_)->if not polarity then trivial:=true
@@ -225,7 +215,7 @@ type t={id:global_reference;
 	atoms:atoms}
     
 let build_formula side nam typ gl metagen=
-  let normalize t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t in
+  let normalize = special_nf gl in
     try 
       let m=meta_succ(metagen false) in
       let trivial,atoms=
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index 140358523f..9e027e2403 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -14,6 +14,8 @@ open Libnames
 
 val qflag : bool ref
 
+val red_flags: Closure.RedFlags.reds ref
+
 val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 
   'a -> 'a -> 'b -> 'b -> int
   
@@ -28,9 +30,6 @@ val construct_nhyps : inductive -> int array
 
 val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array
 
-val match_with_evaluable : Proof_type.goal Tacmach.sigma ->
-  constr -> (evaluable_global_reference * constr) option
-
 type atoms = {positive:constr list;negative:constr list}
 
 type side = Hyp | Concl | Hint
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index d46a4a5295..06d3872251 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -16,8 +16,34 @@ open Term
 open Tacmach
 open Tactics
 open Tacticals
-      
+open Libnames
+
+let old_search=ref !Auto.searchtable 
+
+(* I use this solution as a means to know whether hints have changed, 
+but this prevents the GC from collecting the previous table, 
+resulting in some limited space wasting*)
+
+let update_flags ()=
+  if not ( !Auto.searchtable == !old_search ) then
+    begin
+      old_search:=!Auto.searchtable;
+      let predref=ref Names.KNpred.empty in
+      let f p_a_t = 
+	match p_a_t.Auto.code with
+	    Auto.Unfold_nth (ConstRef kn)->
+	      predref:=Names.KNpred.add kn !predref
+	  | _ ->() in
+      let g _ l=List.iter f l in
+      let h _ hdb=Auto.Hint_db.iter g hdb in
+	Util.Stringmap.iter h !Auto.searchtable;
+	red_flags:=
+	Closure.RedFlags.red_add_transparent 
+	  Closure.betaiotazeta (Names.Idpred.full,!predref)
+    end
+
 let ground_tac solver startseq gl=
+  update_flags ();
   let rec toptac skipped seq gl=
     if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
     then Pp.msgnl (Proof_trees.pr_goal (sig_it gl));
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 4e57bd3caf..1dc72eecb8 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -109,6 +109,8 @@ let mk_open_instance id gl m t=
   let var_id=
     if id==dummy_id then dummy_bvid else
       let typ=pf_type_of gl (constr_of_reference id) in
+	(* since we know we will get a product, 
+	   reduction is not too expensive *)
       let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
 	match nam with 
 	    Name id -> id
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index e68b4bf4a5..7ab2003e35 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -530,18 +530,26 @@ let rec tclFIRST = function
   | [] -> tclFAIL_s "No applicable tactic."
   |  t::rest -> tclORELSE0 t (tclFIRST rest)
 
-let ite_gen tcal tac_if continue tac_else=
+let ite_gen tcal tac_if continue tac_else gl=
   let success=ref false in
   let tac_if0 gl=
     let result=tac_if gl in
       success:=true;result in
-  let tac_else0 gl=
+  let tac_else0 e gl=
     if !success then 
-      tclFAIL_s "failure in THEN branch" gl 
+      raise e 
     else 
       tac_else gl in
-    tclORELSE0 (tcal tac_if0 continue)  (tac_else0)  
-    
+    try 
+      tcal tac_if0 continue gl
+    with
+      | e when catchable_exception e -> tac_else0 e gl
+      | (FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))) as e ->
+	  tac_else0 e gl
+      | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
+      | Stdpp.Exc_located (s,FailError (lvl,s')) ->
+	  raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
+	
 (* Try the first tactic and, if it succeeds, continue with 
    the second one, and if it fails, use the third one *)