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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(*
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
{
open Constrexpr
open Constrexpr_ops
open Stdarg
open Tacarg
open Extraargs
let (set_default_tactic, get_default_tactic, print_default_tactic) =
Tactic_option.declare_tactic_option "Program tactic"
let () =
(* Delay to recover the tactic imperatively *)
let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
snd (get_default_tactic ())
end in
Declare.Obls.default_tactic := tac
let with_tac f tac =
let env = Genintern.empty_glob_sign (Global.env ()) in
let tac = match tac with
| None -> None
| Some tac ->
let tac = Genarg.in_gen (Genarg.rawwit wit_ltac) tac in
let _, tac = Genintern.generic_intern env tac in
Some tac
in
f tac
(* We define new entries for programs, with the use of this module
* Subtac. These entries are named Subtac.<foo>
*)
module Tactic = Pltac
open Pcoq
let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig")
type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
Genarg.create_arg "withtac"
let withtac = Pcoq.create_generic_entry2 "withtac" (Genarg.rawwit wit_withtac)
}
GRAMMAR EXTEND Gram
GLOBAL: withtac;
withtac:
[ [ "with"; t = Tactic.tactic -> { Some t }
| -> { None } ] ]
;
Constr.closed_binder:
[[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> {
let typ = mkAppC (sigref loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in
[CLocalAssum ([id], default_binder_kind, typ)] }
] ];
END
{
open Declare.Obls
let obligation ~pm obl tac = with_tac (fun t -> obligation ~pm obl t) tac
let next_obligation ~pm obl tac = with_tac (fun t -> next_obligation ~pm obl t) tac
let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
}
VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program
| [ "Obligation" natural(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, Some name, Some t) tac }
| [ "Obligation" natural(num) "of" ident(name) withtac(tac) ] ->
{ obligation (num, Some name, None) tac }
| [ "Obligation" natural(num) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, None, Some t) tac }
| [ "Obligation" natural(num) withtac(tac) ] ->
{ obligation (num, None, None) tac }
| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
{ next_obligation (Some name) tac }
| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
END
VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "Obligation" natural(num) "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligation" natural(num) "with" tactic(t) ] ->
{ try_solve_obligation num None (Some (Tacinterp.interp t)) }
END
VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligations" "of" ident(name) ] ->
{ try_solve_obligations (Some name) None }
| [ "Solve" "Obligations" "with" tactic(t) ] ->
{ try_solve_obligations None (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligations" ] ->
{ try_solve_obligations None None }
END
VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "All" "Obligations" "with" tactic(t) ] ->
{ solve_all_obligations (Some (Tacinterp.interp t)) }
| [ "Solve" "All" "Obligations" ] ->
{ solve_all_obligations None }
END
VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Admit" "Obligations" "of" ident(name) ] -> { admit_obligations (Some name) }
| [ "Admit" "Obligations" ] -> { admit_obligations None }
END
VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
| #[ locality = Attributes.locality; ] [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
set_default_tactic
(Locality.make_section_locality locality)
(Tacintern.glob_tactic t);
}
END
{
open Pp
}
VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
| [ "Show" "Obligation" "Tactic" ] -> {
Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) }
END
VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program
| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) }
| [ "Obligations" ] -> { show_obligations None }
END
VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program
| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) }
| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) }
END
{
(* Declare a printer for the content of Program tactics *)
let () =
let printer env sigma _ _ _ = function
| None -> mt ()
| Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic env sigma tac
in
Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer
}
|
