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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4deps: "grammar/grammar.cma" i*)
open Formula
open Sequent
open Ground
open Goptions
open Tacticals
open Tacinterp
open Libnames
open Constrarg
open Stdarg
open Pcoq.Prim
DECLARE PLUGIN "ground_plugin"
(* declaring search depth as a global option *)
let ground_depth=ref 3
let _=
let gdopt=
{ optsync=true;
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 congruence_depth=ref 100
let _=
let gdopt=
{ optsync=true;
optdepr=false;
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 (Loc.ghost, 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
| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
set_default_solver
(Locality.make_section_locality (Locality.LocalityFixme.consume ()))
(Tacintern.glob_tactic t) ]
END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
| [ "Print" "Firstorder" "Solver" ] -> [
Feedback.msg_info
(Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
END
let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
let gen_ground_tac flag taco ids bases gl=
let backup= !qflag in
try
qflag:=flag;
let solver=
match taco with
Some tac-> tac
| None-> snd (default_solver ()) in
let startseq gl=
let seq=empty_seq !ground_depth in
let seq,gl = extend_with_ref_list ids seq gl in
extend_with_auto_hints bases seq gl in
let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in
qflag:=backup;result
with reraise -> qflag:=backup;raise reraise
(* 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=
onAllHypsAndConcl
(function
None->unfold_in_concl (Lazy.force defined_connectives)
| Some id->
unfold_in_hyp (Lazy.force defined_connectives)
(Tacexpr.InHypType id)) *)
open Pp
open Genarg
open Ppconstr
open Printer
let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l
let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
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_TYPED AS reference_list
RAW_PRINTED BY pr_firstorder_using_raw
GLOB_TYPED AS reference_list
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) ] ->
[ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ]
| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
[ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ]
| [ "firstorder" tactic_opt(t) firstorder_using(l)
"with" ne_preident_list(l') ] ->
[ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ]
END
TACTIC EXTEND gintuition
[ "gintuition" tactic_opt(t) ] ->
[ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ]
END
open Proofview.Notations
open Cc_plugin
open Decl_mode_plugin
let default_declarative_automation =
Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
Tacticals.New.tclORELSE
(Tacticals.New.tclORELSE (Auto.h_trivial [] None)
(Cctac.congruence_tac !congruence_depth []))
(Proofview.V82.tactic (gen_ground_tac true
(Some (Tacticals.New.tclTHEN
(snd (default_solver ()))
(Cctac.congruence_tac !congruence_depth [])))
[] []))
let () =
Decl_proof_instr.register_automation_tac default_declarative_automation
|
