diff options
Diffstat (limited to 'contrib/first-order/g_ground.ml4')
-rw-r--r-- | contrib/first-order/g_ground.ml4 | 103 |
1 files changed, 103 insertions, 0 deletions
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 new file mode 100644 index 00000000..f85f2171 --- /dev/null +++ b/contrib/first-order/g_ground.ml4 @@ -0,0 +1,103 @@ +(************************************************************************) +(* 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,v 1.10.2.1 2004/07/16 19:30:10 herbelin Exp $ *) + +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 5 + +let _= + let gdopt= + { optsync=true; + optname="Firstorder Depth"; + optkey=SecondaryTable("Firstorder","Depth"); + optread=(fun ()->Some !ground_depth); + optwrite= + (function + None->ground_depth:=5 + | Some i->ground_depth:=(max i 0))} + in + declare_int_option gdopt + +let default_solver=(Tacinterp.interp <:tactic<auto with *>>) + +let fail_solver=tclFAIL 0 "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) "with" ne_reference_list(l) ] -> + [ gen_ground_tac true (option_app eval_tactic t) (Ids l) ] +| [ "Firstorder" tactic_opt(t) "using" ne_preident_list(l) ] -> + [ gen_ground_tac true (option_app eval_tactic t) (Bases l) ] +| [ "Firstorder" tactic_opt(t) ] -> + [ gen_ground_tac true (option_app eval_tactic t) Void ] +END + +(* Obsolete since V8.0 +TACTIC EXTEND GTauto + [ "GTauto" ] -> + [ gen_ground_tac false (Some fail_solver) Void ] +END +*) + +TACTIC EXTEND GIntuition + [ "GIntuition" tactic_opt(t) ] -> + [ gen_ground_tac false (option_app eval_tactic t) Void ] +END |