Enhancement of the Ground tactic, addition of GTauto and GIntuition.

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

1 files changed, 144 insertions, 72 deletions

diff --git a/contrib/first-order/engine.ml4 b/contrib/first-order/engine.ml4
index 133fbe1229..26abbc63bb 100644
--- a/contrib/first-order/engine.ml4
+++ b/contrib/first-order/engine.ml4
@@ -17,100 +17,172 @@ open Term
 open Tacmach
 open Tactics
 open Tacticals
+open Libnames
 open Util
 
-let ground_tac ninst solver gl=
-  let metagen=newcnt () in
-  let rec toptac ninst seq gl=
+(* 
+   1- keep track of the instantiations and of ninst in the Sequent.t structure 
+   2- ordered instantiations
+*)
+
+let ground_tac solver startseq gl=
+  let rec toptac seq gl=
     match seq.gl with 
 	Atomic t->
-	  tclORELSE (axiom_tac t seq) (left_tac ninst seq []) gl
-      | Complex (pat,l)->
-	  match pat with
-	      Rand->and_tac seq (toptac ninst) metagen gl
-	    | Rforall->forall_tac seq (toptac ninst) metagen gl
-	    | Rarrow->arrow_tac seq (toptac ninst) metagen gl
-	    | _->
-		if not (is_empty_left seq) && rev_left seq then 
-		  left_tac ninst seq [] gl 
-		else 
-		  right_tac ninst seq pat l [] gl
-  and right_tac ninst seq pat atoms ctx gl=
+	  tclORELSE (axiom_tac t seq) (left_tac seq []) gl
+      | Complex (pat,t,l)->
+	  tclORELSE (axiom_tac t seq)
+	  (match pat with
+	       Rand->
+		 and_tac toptac seq
+	     | Rforall->
+		 forall_tac toptac seq
+	     | Rarrow->
+		 arrow_tac toptac seq
+	     | Revaluable egr->
+		 evaluable_tac egr toptac seq
+	     | _->
+		 if not (is_empty_left seq) && rev_left seq then 
+		   left_tac seq [] 
+		 else 
+		   right_tac seq pat l []) gl
+  and right_tac seq pat atoms ctx gl=
     let re_add s=re_add_left_list ctx s in
       match pat with
 	  Ror->
 	    tclORELSE
-	    (or_tac (re_add seq) (toptac ninst) metagen)
-	    (left_tac ninst seq ctx) gl
+	    (or_tac toptac (re_add seq))
+	    (left_tac seq ctx) gl
 	| Rexists(i,dom)->
 	    tclORELSE
-	    (if ninst=0 then tclFAIL 0 "max depth" else 
-	       exists_tac i dom atoms (re_add seq) (toptac (ninst-1)) metagen)
-	    (left_tac ninst seq ctx) gl
+	    (if seq.depth<=0 || not !qflag then 
+	       tclFAIL 0 "max depth" 
+	     else 
+	       exists_tac i dom atoms toptac (re_add seq))
+	    (left_tac seq ctx) gl
 	| _-> anomaly "unreachable place"
-  and left_tac ninst seq ctx gl=
+  and left_tac seq ctx gl=
     if is_empty_left seq then 
       solver gl (* put solver here *)
     else 
       let (hd,seq1)=take_left seq in 
       let re_add s=re_add_left_list ctx s in 
 	match hd.pat with
-	    Lfalse->left_false_tac hd.id gl
-	  | Land ind->left_and_tac ind hd.id seq1 (toptac ninst) metagen gl
-	  | Lor ind->left_or_tac ind hd.id seq1 (toptac ninst) metagen gl
+	    Lfalse->
+	      left_false_tac hd.id gl
+	  | Land ind->
+	      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)->
 	      tclORELSE
-	      (if ninst=0 then tclFAIL 0 "max depth" else 
-		 left_forall_tac i dom hd.atoms hd.id (re_add seq)
-		   (toptac (ninst-1)) metagen)
-	      (left_tac ninst seq1 (hd::ctx)) gl
-	  | Lexists ->left_exists_tac hd.id seq1 (toptac ninst) metagen gl
-	  | LAatom a->
-	      tclORELSE
-	      (ll_atom_tac a hd.id (re_add seq1) (toptac ninst) metagen)
-	      (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
-	  | LAforall p ->	      
+	      (if seq.depth<=0 || not !qflag then 
+		 tclFAIL 0 "max depth" 
+	       else 
+		 left_forall_tac i dom hd.atoms hd.internal hd.id
+		    toptac (re_add seq))
+	      (left_tac seq1 (hd::ctx)) gl
+	  | Lexists ->
+	      if !qflag then
+		left_exists_tac hd.id toptac (re_add seq1) gl
+	      else (left_tac seq1 (hd::ctx)) gl
+	  | Levaluable egr->
+	      left_evaluable_tac egr hd.id toptac (re_add seq1) gl
+	  | LA (typ,lap)->
 	      tclORELSE
-	      (if ninst=0 then tclFAIL 0 "max depth" else 
-		 ll_forall_tac p hd.id (re_add seq1) 
-		   (toptac (ninst-1)) metagen)
-	      (left_tac ninst seq1 (hd::ctx)) gl
-	  | LAexists (ind,a,p,_) ->
-	      ll_ind_tac ind [a;p] hd.id seq1 (toptac ninst) metagen gl
-	  | LAarrow (a,b,c) ->	      
-	      tclORELSE
-	      (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
-
+	      (ll_atom_tac typ hd.id toptac (re_add seq1))
+	      (match lap with
+		   LLatom->
+		     (match seq1.gl with 
+			  Atomic t->
+			    (left_tac seq1 (hd::ctx))
+			| Complex (pat,_,atoms)->
+			    (right_tac seq1 pat atoms (hd::ctx))) 
+		 | LLfalse->
+		     ll_false_tac hd.id toptac (re_add seq1) 
+		 | 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))
+		 | LLexists (ind,a,p,_) ->
+		     if !qflag then
+		       ll_ind_tac ind [a;p] hd.id toptac (re_add seq1) 
+		     else
+		       left_tac seq1 (hd::ctx)
+		 | LLarrow (a,b,c) ->	      
+		     tclORELSE
+		     (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
+    wrap (List.length (pf_hyps gl)) true toptac (startseq gl) gl
+      
 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
+    
+let fail_solver=tclFAIL 0 "GroundTauto failed"
+		      
+let gen_ground_tac flag taco io l=
+  qflag:=flag;
+  let depth=
+    match io with 
+	Some i->i
+      | None-> !Auto.default_search_depth in
+  let solver= 
+    match taco with 
+	Some tac->tac
+      | None-> default_solver in
+  let startseq=create_with_ref_list l depth in
+    ground_tac solver startseq
+
+open Genarg
+open Pcoq
+open Pp
+
+type depth=int option
+
+let pr_depth _ _=function
+    None->mt ()
+  | Some i -> str " depth " ++ int i
+
+ARGUMENT EXTEND depth TYPED AS depth PRINTED BY pr_depth
+[ "depth" integer(i)]-> [ Some i]
+| [ ] -> [None]
+END 
+
+type with_reflist = global_reference list
+
+let pr_ref_list _ _=function
+    [] -> mt ()
+  | l -> prlist pr_reference l
 
 TACTIC EXTEND Ground
-   [ "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) ]
+   [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> 
+	 [ gen_ground_tac true (Some (snd t)) None l ]
+|   [ "Ground" tactic(t) "depth" integer(i) "with" ne_reference_list(l) ] -> 
+	 [ gen_ground_tac true (Some (snd t)) (Some i) l ]
+|   [ "Ground" tactic(t) "depth" integer(i) ] -> 
+	 [ gen_ground_tac true (Some (snd t)) (Some i) [] ]
+|   [ "Ground" tactic(t) ] -> 
+	 [ gen_ground_tac true (Some (snd t)) None [] ]
+|   [ "Ground" ] ->
+	 [ gen_ground_tac true None None [] ]
+END
+
+TACTIC EXTEND GTauto   
+  [ "GTauto" ] ->
+     [ gen_ground_tac false (Some fail_solver) (Some 0) [] ]   
+END
+
+TACTIC EXTEND GIntuition
+   ["GIntuition" tactic(t)] ->
+     [ gen_ground_tac false (Some(snd t)) None [] ]
+|  [ "GIntuition" ] ->
+     [ gen_ground_tac false None None [] ] 
 END
 
-