1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq 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 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 =
declare_nat_option_and_ref ~depr:false ~key:["Firstorder";"Depth"] ~value:3
let default_intuition_tac =
let tac _ _ = Auto.h_auto None [] (Some []) 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) sigma 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
}
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 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
|
