Untersuchungsergebnis.mlg Download desLex {Lex[90] Coq[123] Abap[149]}zum Wurzelverzeichnis wechseln
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
{
open Ltac_plugin
open Formula
open Sequent
open Ground
open Goptions
open Tacmach.New
open Tacticals.New
open Tacinterp
open Stdarg
open Tacarg
open Attributes
open Pcoq.Prim
}
DECLARE PLUGIN "ground_plugin"
(* declaring search depth as a global option *)
{
let ground_depth=ref 3
let ()=
let gdopt=
{ optdepr=false;
optname="Firstorder Depth";
optkey=["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 ()=
let congruence_depth=ref 100 in
let gdopt=
{ optdepr=true; (* noop *)
optname="Congruence Depth";
optkey=["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_intuition_tac =
let tac _ _ = Auto.h_auto None [] None in
let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
Tacenv.register_ml_tactic name [| tac |];
Tacexpr.TacML (CAst.make (entry, []))
let (set_default_solver, default_solver, print_default_solver) =
Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
}
VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
| #[ locality; ] [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
set_default_solver
(Locality.make_section_locality locality)
(Tacintern.glob_tactic t)
}
END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
| [ "Print" "Firstorder" "Solver" ] -> {
Feedback.msg_notice
(Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) }
END
{
let gen_ground_tac flag taco ids bases =
let backup= !qflag in
Proofview.tclOR begin
Proofview.Goal.enter begin fun gl ->
qflag:=flag;
let solver=
match taco with
Some tac-> tac
| None-> snd (default_solver ()) in
let startseq k =
Proofview.Goal.enter begin fun gl ->
let seq=empty_seq !ground_depth in
let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
end
in
let result=ground_tac solver startseq in
qflag := backup;
result
end
end
(fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e)
(* special for compatibility with Intuition
let constant str = Coqlib.get_constr str
let defined_connectives=lazy
[[],EvalConstRef (destConst (constant "core.not.type"));
[],EvalConstRef (destConst (constant "core.iff.type"))]
let normalize_evaluables=
onAllHypsAndConcl
(function
None->unfold_in_concl (Lazy.force defined_connectives)
| Some id->
unfold_in_hyp (Lazy.force defined_connectives)
(Tacexpr.InHypType id)) *)
open Ppconstr
open Printer
let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid
let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (Pputils.pr_or_var (fun x -> pr_global (snd x)))
let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
let warn_deprecated_syntax =
CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
(fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator")
}
ARGUMENT EXTEND firstorder_using
TYPED AS reference list
PRINTED BY { pr_firstorder_using_typed }
RAW_PRINTED BY { pr_firstorder_using_raw }
GLOB_PRINTED BY { pr_firstorder_using_glob }
| [ "using" reference(a) ] -> { [a] }
| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> { a::l }
| [ "using" reference(a) reference(b) reference_list(l) ] -> {
warn_deprecated_syntax ();
a::b::l
}
| [ ] -> { [] }
END
TACTIC EXTEND firstorder
| [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
{ gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] }
| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
{ gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l }
| [ "firstorder" tactic_opt(t) firstorder_using(l)
"with" ne_preident_list(l') ] ->
{ gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' }
END
TACTIC EXTEND gintuition
| [ "gintuition" tactic_opt(t) ] ->
{ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] }
END
[ zur Elbe Produktseite wechseln0.108Quellennavigators
]
