diff options
Diffstat (limited to 'contrib/firstorder/g_ground.ml4')
-rw-r--r-- | contrib/firstorder/g_ground.ml4 | 128 |
1 files changed, 0 insertions, 128 deletions
diff --git a/contrib/firstorder/g_ground.ml4 b/contrib/firstorder/g_ground.ml4 deleted file mode 100644 index f7b0a546..00000000 --- a/contrib/firstorder/g_ground.ml4 +++ /dev/null @@ -1,128 +0,0 @@ -(************************************************************************) -(* 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 - |