-
Notifications
You must be signed in to change notification settings - Fork 631
/
tac2env.ml
334 lines (262 loc) · 9.21 KB
/
tac2env.ml
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
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
(************************************************************************)
(* * 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 Util
open Names
open Libnames
open Tac2expr
open Tac2ffi
type global_data = {
gdata_expr : glb_tacexpr;
gdata_type : type_scheme;
gdata_mutable : bool;
gdata_deprecation : Deprecation.t option;
}
type constructor_data = {
cdata_prms : int;
cdata_type : type_constant;
cdata_args : int glb_typexpr list;
cdata_indx : int option;
}
type projection_data = {
pdata_prms : int;
pdata_type : type_constant;
pdata_ptyp : int glb_typexpr;
pdata_mutb : bool;
pdata_indx : int;
}
type alias_data = {
alias_body : raw_tacexpr;
alias_depr : Deprecation.t option;
}
type ltac_state = {
ltac_tactics : global_data KNmap.t;
ltac_constructors : constructor_data KNmap.t;
ltac_projections : projection_data KNmap.t;
ltac_types : glb_quant_typedef KNmap.t;
ltac_aliases : alias_data KNmap.t;
}
let empty_state = {
ltac_tactics = KNmap.empty;
ltac_constructors = KNmap.empty;
ltac_projections = KNmap.empty;
ltac_types = KNmap.empty;
ltac_aliases = KNmap.empty;
}
let ltac_state = Summary.ref empty_state ~name:"ltac2-state"
let ltac_notations = Summary.ref KNmap.empty ~stage:Summary.Stage.Synterp ~name:"ltac2-notations"
let define_global kn e =
let state = !ltac_state in
ltac_state := { state with ltac_tactics = KNmap.add kn e state.ltac_tactics }
let interp_global kn =
let data = KNmap.find kn ltac_state.contents.ltac_tactics in
data
let globals () = (!ltac_state).ltac_tactics
let define_constructor kn t =
let state = !ltac_state in
ltac_state := { state with ltac_constructors = KNmap.add kn t state.ltac_constructors }
let interp_constructor kn = KNmap.find kn ltac_state.contents.ltac_constructors
let define_projection kn t =
let state = !ltac_state in
ltac_state := { state with ltac_projections = KNmap.add kn t state.ltac_projections }
let interp_projection kn = KNmap.find kn ltac_state.contents.ltac_projections
let define_type kn e =
let state = !ltac_state in
ltac_state := { state with ltac_types = KNmap.add kn e state.ltac_types }
let interp_type kn = KNmap.find kn ltac_state.contents.ltac_types
let define_alias ?deprecation kn tac =
let state = !ltac_state in
let data = { alias_body = tac; alias_depr = deprecation } in
ltac_state := { state with ltac_aliases = KNmap.add kn data state.ltac_aliases }
let interp_alias kn = KNmap.find kn ltac_state.contents.ltac_aliases
let define_notation kn tac =
ltac_notations := KNmap.add kn tac !ltac_notations
let interp_notation kn = KNmap.find kn !ltac_notations
module ML =
struct
type t = ml_tactic_name
let compare n1 n2 =
let c = String.compare n1.mltac_plugin n2.mltac_plugin in
if Int.equal c 0 then String.compare n1.mltac_tactic n2.mltac_tactic
else c
end
module MLMap = Map.Make(ML)
let primitive_map = ref MLMap.empty
let define_primitive name f =
let f = match f with
| ValCls f -> ValCls (annotate_closure (FrPrim name) f)
| _ -> f
in
primitive_map := MLMap.add name f !primitive_map
let interp_primitive name = MLMap.find name !primitive_map
(** Name management *)
module FullPath =
struct
type t = full_path
let equal = eq_full_path
let to_string = string_of_path
let repr sp =
let dir,id = repr_path sp in
id, (DirPath.repr dir)
end
type tacref = Tac2expr.tacref =
| TacConstant of ltac_constant
| TacAlias of ltac_alias
module TacRef =
struct
type t = tacref
let compare r1 r2 = match r1, r2 with
| TacConstant c1, TacConstant c2 -> KerName.compare c1 c2
| TacAlias c1, TacAlias c2 -> KerName.compare c1 c2
| TacConstant _, TacAlias _ -> -1
| TacAlias _, TacConstant _ -> 1
let equal r1 r2 = compare r1 r2 == 0
end
module KnTab = Nametab.Make(FullPath)(KerName)
module RfTab = Nametab.Make(FullPath)(TacRef)
module RfMap = Map.Make(TacRef)
type nametab = {
tab_ltac : RfTab.t;
tab_ltac_rev : full_path RfMap.t;
tab_cstr : KnTab.t;
tab_cstr_rev : full_path KNmap.t;
tab_type : KnTab.t;
tab_type_rev : full_path KNmap.t;
tab_proj : KnTab.t;
tab_proj_rev : full_path KNmap.t;
}
let empty_nametab = {
tab_ltac = RfTab.empty;
tab_ltac_rev = RfMap.empty;
tab_cstr = KnTab.empty;
tab_cstr_rev = KNmap.empty;
tab_type = KnTab.empty;
tab_type_rev = KNmap.empty;
tab_proj = KnTab.empty;
tab_proj_rev = KNmap.empty;
}
let nametab = Summary.ref empty_nametab ~name:"ltac2-nametab"
let push_ltac vis sp kn =
let tab = !nametab in
let tab_ltac = RfTab.push vis sp kn tab.tab_ltac in
let tab_ltac_rev = RfMap.add kn sp tab.tab_ltac_rev in
nametab := { tab with tab_ltac; tab_ltac_rev }
let locate_ltac qid =
let tab = !nametab in
RfTab.locate qid tab.tab_ltac
let locate_extended_all_ltac qid =
let tab = !nametab in
RfTab.find_prefixes qid tab.tab_ltac
let path_of_ltac kn = RfMap.find kn (!nametab).tab_ltac_rev
let shortest_qualid_of_ltac kn =
let tab = !nametab in
let sp = RfMap.find kn tab.tab_ltac_rev in
RfTab.shortest_qualid Id.Set.empty sp tab.tab_ltac
let push_constructor vis sp kn =
let tab = !nametab in
let tab_cstr = KnTab.push vis sp kn tab.tab_cstr in
let tab_cstr_rev = KNmap.add kn sp tab.tab_cstr_rev in
nametab := { tab with tab_cstr; tab_cstr_rev }
let locate_constructor qid =
let tab = !nametab in
KnTab.locate qid tab.tab_cstr
let locate_extended_all_constructor qid =
let tab = !nametab in
KnTab.find_prefixes qid tab.tab_cstr
let path_of_constructor kn = KNmap.find kn (!nametab).tab_cstr_rev
let shortest_qualid_of_constructor kn =
let tab = !nametab in
let sp = KNmap.find kn tab.tab_cstr_rev in
KnTab.shortest_qualid Id.Set.empty sp tab.tab_cstr
let push_type vis sp kn =
let tab = !nametab in
let tab_type = KnTab.push vis sp kn tab.tab_type in
let tab_type_rev = KNmap.add kn sp tab.tab_type_rev in
nametab := { tab with tab_type; tab_type_rev }
let locate_type qid =
let tab = !nametab in
KnTab.locate qid tab.tab_type
let locate_extended_all_type qid =
let tab = !nametab in
KnTab.find_prefixes qid tab.tab_type
let shortest_qualid_of_type ?loc kn =
let tab = !nametab in
let sp = KNmap.find kn tab.tab_type_rev in
KnTab.shortest_qualid ?loc Id.Set.empty sp tab.tab_type
let push_projection vis sp kn =
let tab = !nametab in
let tab_proj = KnTab.push vis sp kn tab.tab_proj in
let tab_proj_rev = KNmap.add kn sp tab.tab_proj_rev in
nametab := { tab with tab_proj; tab_proj_rev }
let locate_projection qid =
let tab = !nametab in
KnTab.locate qid tab.tab_proj
let locate_extended_all_projection qid =
let tab = !nametab in
KnTab.find_prefixes qid tab.tab_proj
let shortest_qualid_of_projection kn =
let tab = !nametab in
let sp = KNmap.find kn tab.tab_proj_rev in
KnTab.shortest_qualid Id.Set.empty sp tab.tab_proj
type 'a or_glb_tacexpr =
| GlbVal of 'a
| GlbTacexpr of glb_tacexpr
type environment = {
env_ist : valexpr Id.Map.t;
}
type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r glb_typexpr
type ('a, 'b) ml_object = {
ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
ml_subst : Mod_subst.substitution -> 'b -> 'b;
ml_interp : environment -> 'b -> valexpr Proofview.tactic;
ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
}
module MLTypeObj =
struct
type ('a, 'b) t = ('a, 'b) ml_object
end
module MLType = Tac2dyn.ArgMap(MLTypeObj)
let ml_object_table = ref MLType.empty
let define_ml_object t tpe =
ml_object_table := MLType.add t (MLType.Pack tpe) !ml_object_table
let interp_ml_object t =
try
let MLType.Pack ans = MLType.find t !ml_object_table in
ans
with Not_found ->
CErrors.anomaly Pp.(str "Unknown object type " ++ str (Tac2dyn.Arg.repr t))
(** Absolute paths *)
let coq_prefix =
MPfile (DirPath.make (List.map Id.of_string ["Init"; "Ltac2"]))
let std_prefix =
MPfile (DirPath.make (List.map Id.of_string ["Std"; "Ltac2"]))
let ltac1_prefix =
MPfile (DirPath.make (List.map Id.of_string ["Ltac1"; "Ltac2"]))
(** Generic arguments *)
let wit_ltac2in1 = Genarg.make0 "ltac2in1"
let wit_ltac2in1_val = Genarg.make0 "ltac2in1val"
let wit_ltac2_constr = Genarg.make0 "ltac2:in-constr"
let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation"
let wit_ltac2_val = Genarg.make0 "ltac2:value"
let () = Geninterp.register_val0 wit_ltac2in1 None
let () = Geninterp.register_val0 wit_ltac2in1_val None
let () = Geninterp.register_val0 wit_ltac2_constr None
let () = Geninterp.register_val0 wit_ltac2_quotation None
let is_constructor_id id =
let id = Id.to_string id in
assert (String.length id > 0);
match id with
| "true" | "false" -> true (* built-in constructors *)
| _ ->
match id.[0] with
| 'A'..'Z' -> true
| _ -> false
let is_constructor qid =
let (_, id) = repr_qualid qid in
is_constructor_id id