Columbo aufrufen.mlg Download desUnknown {[0] [0] [0]}Datei anzeigen
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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 Sequent
open Ground
open Goptions
open Tacmach
open Tacticals
open Tacinterp
open Stdarg
open Tacarg
open Procq.Prim
}
DECLARE PLUGIN "rocq-runtime.plugins.firstorder"
(* declaring search depth as a global option *)
{
let { Goptions.get = ground_depth } =
declare_nat_option_and_ref
~key:["Firstorder";"Depth"]
~value:3
()
let (set_default_solver, default_solver, print_default_solver) =
Tactic_option.declare_tactic_option "Firstorder default solver"
}
VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
| #[ locality = Tactic_option.tac_option_locality; ] [ "Set" "Firstorder" "Solver" generic_tactic(t) ] -> {
set_default_solver
locality
(Gentactic.intern (Global.env()) 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 ist taco ids bases =
let flags = Ground.get_flags () in
Proofview.tclOR begin
Proofview.Goal.enter begin fun gl ->
let solver=
match taco with
| Some tac -> tactic_of_value ist tac
| None-> 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 ~flags (pf_env gl) (project gl) ids seq in
let seq, sigma = extend_with_auto_hints ~flags (pf_env gl) sigma bases seq in
tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
end
in
let () =
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
then
Feedback.msg_debug (Printer.Debug.pr_goal gl)
in
let result=ground_tac ~flags solver startseq in
result
end
end
(fun (e, info) -> Proofview.tclZERO ~info e)
(* special for compatibility with Intuition
let constant str = Rocqlib.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
}
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" ne_reference_list_sep(l,",") ] -> { l }
| [ ] -> { [] }
END
TACTIC EXTEND firstorder
| [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
{ gen_ground_tac ist t l [] }
| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
{ gen_ground_tac ist t [] l }
| [ "firstorder" tactic_opt(t) firstorder_using(l)
"with" ne_preident_list(l') ] ->
{ gen_ground_tac ist t l l' }
END
[ 0.113Quellennavigators
]
