1 files changed, 128 insertions, 0 deletions
diff --git a/contrib/firstorder/g_ground.ml4 b/contrib/firstorder/g_ground.ml4
new file mode 100644
index 00000000..f7b0a546
--- /dev/null
+++ b/contrib/firstorder/g_ground.ml4
@@ -0,0 +1,128 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma"  i*)
+
+(* $Id: g_ground.ml4 10346 2007-12-05 21:11:19Z aspiwack $ *)
+
+open Formula
+open Sequent
+open Ground
+open Goptions
+open Tactics
+open Tacticals
+open Tacinterp
+open Term
+open Names
+open Util
+open Libnames
+
+(* declaring search depth as a global option *)
+
+let ground_depth=ref 3
+
+let _=
+  let gdopt=
+    { optsync=true;
+      optname="Firstorder Depth";
+      optkey=SecondaryTable("Firstorder","Depth"); 
+      optread=(fun ()->Some !ground_depth); 
+      optwrite=
+   (function 
+	None->ground_depth:=3
+      |	Some i->ground_depth:=(max i 0))}
+  in
+    declare_int_option gdopt
+
+let congruence_depth=ref 100
+
+let _=
+  let gdopt=
+    { optsync=true;
+      optname="Congruence Depth";
+      optkey=SecondaryTable("Congruence","Depth"); 
+      optread=(fun ()->Some !congruence_depth); 
+      optwrite=
+   (function 
+	None->congruence_depth:=0
+      |	Some i->congruence_depth:=(max i 0))}
+  in
+    declare_int_option gdopt
+
+let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
+
+let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
+		      
+type external_env=
+    Ids of global_reference list
+  | Bases of Auto.hint_db_name list
+  | Void
+
+let gen_ground_tac flag taco ext gl=
+  let backup= !qflag in
+    try
+      qflag:=flag;
+      let solver= 
+	match taco with 
+	    Some tac-> tac
+	  | None-> default_solver in
+      let startseq=
+	match ext with
+	    Void -> (fun gl -> empty_seq !ground_depth)
+	  | Ids l-> create_with_ref_list l !ground_depth
+	  | Bases l-> create_with_auto_hints l !ground_depth in
+      let result=ground_tac solver startseq gl in 
+	qflag:=backup;result
+    with e ->qflag:=backup;raise e
+      
+(* special for compatibility with Intuition 
+
+let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
+
+let defined_connectives=lazy
+  [[],EvalConstRef (destConst (constant "not"));
+   [],EvalConstRef (destConst (constant "iff"))]
+
+let normalize_evaluables=
+  onAllClauses
+    (function 
+	 None->unfold_in_concl (Lazy.force defined_connectives)
+       | Some id-> 
+	   unfold_in_hyp (Lazy.force defined_connectives) 
+	   (Tacexpr.InHypType id)) *)
+
+TACTIC EXTEND firstorder
+    [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] -> 
+      [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ]
+|   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> 
+      [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ]
+|   [ "firstorder" tactic_opt(t) ] -> 
+      [ gen_ground_tac true (Option.map eval_tactic t) Void ]
+END
+
+TACTIC EXTEND gintuition
+  [ "gintuition" tactic_opt(t) ] ->
+     [ gen_ground_tac false (Option.map eval_tactic t) Void ]
+END
+
+
+let default_declarative_automation gls = 
+  tclORELSE
+    (tclORELSE (Auto.h_trivial [] None) 
+    (Cctac.congruence_tac !congruence_depth []))
+    (gen_ground_tac true 
+       (Some (tclTHEN
+		default_solver
+		(Cctac.congruence_tac !congruence_depth [])))
+       Void) gls
+
+
+
+let () = 
+  Decl_proof_instr.register_automation_tac default_declarative_automation
+