-
Notifications
You must be signed in to change notification settings - Fork 632
/
tac2quote.ml
557 lines (490 loc) · 19.9 KB
/
tac2quote.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
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
(************************************************************************)
(* * 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 Pp
open Names
open Util
open CAst
open Tac2dyn
open Tac2expr
open Tac2qexpr
(** Generic arguments *)
let wit_pattern = Arg.create "pattern"
let wit_reference = Arg.create "reference"
let wit_ident = Arg.create "ident"
let wit_constr = Arg.create "constr"
let wit_open_constr = Arg.create "open_constr"
let wit_preterm = Arg.create "preterm"
let wit_ltac1 = Arg.create "ltac1"
let wit_ltac1val = Arg.create "ltac1val"
(** Syntactic quoting of expressions. *)
let prefix_gen n =
MPfile (DirPath.make (List.map Id.of_string [n; "Ltac2"]))
let control_prefix = prefix_gen "Control"
let pattern_prefix = prefix_gen "Pattern"
let array_prefix = prefix_gen "Array"
let format_prefix = MPdot (prefix_gen "Message", Label.make "Format")
let kername prefix n = KerName.make prefix (Label.of_id (Id.of_string_soft n))
let std_core n = kername Tac2env.std_prefix n
let coq_core n = kername Tac2env.coq_prefix n
let control_core n = kername control_prefix n
let pattern_core n = kername pattern_prefix n
let global_ref ?loc kn =
CAst.make ?loc @@ CTacRef (AbsKn (TacConstant kn))
let constructor ?loc kn args =
let cst = CAst.make ?loc @@ CTacCst (AbsKn (Other kn)) in
if List.is_empty args then cst
else CAst.make ?loc @@ CTacApp (cst, args)
let std_constructor ?loc name args =
constructor ?loc (std_core name) args
let std_proj ?loc name =
AbsKn (std_core name)
let thunk e =
let t_unit = coq_core "unit" in
let loc = e.loc in
let ty = CAst.make?loc @@ CTypRef (AbsKn (Other t_unit), []) in
let pat = CAst.make ?loc @@ CPatVar (Anonymous) in
let pat = CAst.make ?loc @@ CPatCnv (pat, ty) in
CAst.make ?loc @@ CTacFun ([pat], e)
let of_pair f g {loc;v=(e1, e2)} =
CAst.make ?loc @@ CTacApp (CAst.make ?loc @@ CTacCst (AbsKn (Tuple 2)), [f e1; g e2])
let of_tuple ?loc el = match el with
| [] ->
CAst.make ?loc @@ CTacCst (AbsKn (Tuple 0))
| [e] -> e
| el ->
let len = List.length el in
CAst.make ?loc @@ CTacApp (CAst.make ?loc @@ CTacCst (AbsKn (Tuple len)), el)
let of_string {loc;v=n} =
CAst.make ?loc @@ CTacAtm (AtmStr n)
let of_int {loc;v=n} =
CAst.make ?loc @@ CTacAtm (AtmInt n)
let of_option ?loc f opt = match opt with
| None -> constructor ?loc (coq_core "None") []
| Some e -> constructor ?loc (coq_core "Some") [f e]
let inj_wit ?loc wit x =
CAst.make ?loc @@ CTacExt (wit, x)
let of_variable {loc;v=id} =
let qid = Libnames.qualid_of_ident ?loc id in
if Tac2env.is_constructor qid then
CErrors.user_err ?loc (str "Invalid identifier" ++ spc () ++ Id.print id ++
spc () ++ str "classifying as an Ltac2 constructor")
else CAst.make ?loc @@ CTacRef (RelId qid)
let of_anti f = function
| QExpr x -> f x
| QAnti id -> of_variable id
let of_ident {loc;v=id} = inj_wit ?loc wit_ident id
let quote_constr ?delimiters c =
let loc = Constrexpr_ops.constr_loc c in
Option.cata
(List.fold_left (fun c d ->
CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c))
c)
c delimiters
let of_constr ?delimiters c =
let loc = Constrexpr_ops.constr_loc c in
let c = quote_constr ?delimiters c in
inj_wit ?loc wit_constr c
let of_open_constr ?delimiters c =
let loc = Constrexpr_ops.constr_loc c in
let c = quote_constr ?delimiters c in
inj_wit ?loc wit_open_constr c
let of_preterm ?delimiters c =
let loc = Constrexpr_ops.constr_loc c in
let c = quote_constr ?delimiters c in
inj_wit ?loc wit_preterm c
let of_bool ?loc b =
let c = if b then coq_core "true" else coq_core "false" in
constructor ?loc c []
let rec of_list ?loc f = function
| [] -> constructor (coq_core "[]") []
| e :: l ->
constructor ?loc (coq_core "::") [f e; of_list ?loc f l]
let array_of_list ?loc l =
let of_list = global_ref ?loc (kername array_prefix "of_list") in
CAst.make ?loc @@ CTacApp (of_list, [l])
let of_qhyp {loc;v=h} = match h with
| QAnonHyp n -> std_constructor ?loc "AnonHyp" [of_int n]
| QNamedHyp id -> std_constructor ?loc "NamedHyp" [of_ident id]
let of_bindings {loc;v=b} = match b with
| QNoBindings ->
std_constructor ?loc "NoBindings" []
| QImplicitBindings tl ->
std_constructor ?loc "ImplicitBindings" [of_list ?loc of_open_constr tl]
| QExplicitBindings tl ->
let map e = of_pair (fun q -> of_anti of_qhyp q) of_open_constr e in
std_constructor ?loc "ExplicitBindings" [of_list ?loc map tl]
let of_constr_with_bindings c = of_pair of_open_constr of_bindings c
let rec of_intro_pattern {loc;v=pat} = match pat with
| QIntroForthcoming b ->
std_constructor ?loc "IntroForthcoming" [of_bool b]
| QIntroNaming iname ->
std_constructor ?loc "IntroNaming" [of_intro_pattern_naming iname]
| QIntroAction iact ->
std_constructor ?loc "IntroAction" [of_intro_pattern_action iact]
and of_intro_pattern_naming {loc;v=pat} = match pat with
| QIntroIdentifier id ->
std_constructor ?loc "IntroIdentifier" [of_anti of_ident id]
| QIntroFresh id ->
std_constructor ?loc "IntroFresh" [of_anti of_ident id]
| QIntroAnonymous ->
std_constructor ?loc "IntroAnonymous" []
and of_intro_pattern_action {loc;v=pat} = match pat with
| QIntroWildcard ->
std_constructor ?loc "IntroWildcard" []
| QIntroOrAndPattern pat ->
std_constructor ?loc "IntroOrAndPattern" [of_or_and_intro_pattern pat]
| QIntroInjection il ->
std_constructor ?loc "IntroInjection" [of_intro_patterns il]
| QIntroRewrite b ->
std_constructor ?loc "IntroRewrite" [of_bool ?loc b]
and of_or_and_intro_pattern {loc;v=pat} = match pat with
| QIntroOrPattern ill ->
std_constructor ?loc "IntroOrPattern" [of_list ?loc of_intro_patterns ill]
| QIntroAndPattern il ->
std_constructor ?loc "IntroAndPattern" [of_intro_patterns il]
and of_intro_patterns {loc;v=l} =
of_list ?loc of_intro_pattern l
let of_hyp_location_flag ?loc = function
| Locus.InHyp -> std_constructor ?loc "InHyp" []
| Locus.InHypTypeOnly -> std_constructor ?loc "InHypTypeOnly" []
| Locus.InHypValueOnly -> std_constructor ?loc "InHypValueOnly" []
let of_occurrences {loc;v=occ} = match occ with
| QAllOccurrences -> std_constructor ?loc "AllOccurrences" []
| QAllOccurrencesBut occs ->
let map occ = of_anti of_int occ in
let occs = of_list ?loc map occs in
std_constructor ?loc "AllOccurrencesBut" [occs]
| QNoOccurrences -> std_constructor ?loc "NoOccurrences" []
| QOnlyOccurrences occs ->
let map occ = of_anti of_int occ in
let occs = of_list ?loc map occs in
std_constructor ?loc "OnlyOccurrences" [occs]
let of_hyp_location ?loc ((occs, id), flag) =
of_tuple ?loc [
of_anti of_ident id;
of_occurrences occs;
of_hyp_location_flag ?loc flag;
]
let of_clause {loc;v=cl} =
let hyps = of_option ?loc (fun l -> of_list ?loc of_hyp_location l) cl.q_onhyps in
let concl = of_occurrences cl.q_concl_occs in
CAst.make ?loc @@ CTacRec (None, [
std_proj "on_hyps", hyps;
std_proj "on_concl", concl;
])
let of_destruction_arg {loc;v=arg} = match arg with
| QElimOnConstr c ->
let arg = thunk (of_constr_with_bindings c) in
std_constructor ?loc "ElimOnConstr" [arg]
| QElimOnIdent id -> std_constructor ?loc "ElimOnIdent" [of_ident id]
| QElimOnAnonHyp n -> std_constructor ?loc "ElimOnAnonHyp" [of_int n]
let of_induction_clause {loc;v=cl} =
let arg = of_destruction_arg cl.indcl_arg in
let eqn = of_option ?loc of_intro_pattern_naming cl.indcl_eqn in
let as_ = of_option ?loc of_or_and_intro_pattern cl.indcl_as in
let in_ = of_option ?loc of_clause cl.indcl_in in
CAst.make ?loc @@ CTacRec (None, [
std_proj "indcl_arg", arg;
std_proj "indcl_eqn", eqn;
std_proj "indcl_as", as_;
std_proj "indcl_in", in_;
])
let check_pattern_id ?loc id =
if Tac2env.is_constructor (Libnames.qualid_of_ident id) then
CErrors.user_err ?loc (str "Invalid pattern binding name " ++ Id.print id)
let pattern_vars pat =
let rec aux () accu pat = match pat.CAst.v with
| Constrexpr.CPatVar id
| Constrexpr.CEvar ({CAst.v=id}, []) ->
let loc = pat.CAst.loc in
let () = check_pattern_id ?loc id in
Id.Map.add id loc accu
| _ ->
Constrexpr_ops.fold_constr_expr_with_binders (fun _ () -> ()) aux () accu pat
in
aux () Id.Map.empty pat
let abstract_vars loc ?typ vars tac =
let get_name na = match na.CAst.v with
| Name id -> Some (CAst.make ?loc:na.CAst.loc id)
| Anonymous -> None
in
let def = List.find_map get_name vars in
let na, tac = match def with
| None -> (Anonymous, tac)
| Some id0 ->
(* Trick: in order not to shadow a variable nor to choose an arbitrary
name, we reuse one which is going to be shadowed by the matched
variables anyways. *)
let build_bindings (n, accu) { CAst.loc; CAst.v = na } = match na with
| Anonymous -> (n + 1, accu)
| Name _ ->
let get = global_ref ?loc (kername array_prefix "get") in
let args = [of_variable id0; of_int CAst.(make ?loc n)] in
let e = CAst.make ?loc @@ CTacApp (get, args) in
let accu = (CAst.make ?loc @@ CPatVar na, e) :: accu in
(n + 1, accu)
in
let (_, bnd) = List.fold_left build_bindings (0, []) vars in
let tac = CAst.make ?loc @@ CTacLet (false, bnd, tac) in
(Name id0.CAst.v, tac)
in
let pat = CAst.make ?loc @@ CPatVar na in
let pat = match typ with
| None -> pat
| Some typ ->
let t_array = coq_core "array" in
let typ = CAst.make ?loc @@ CTypRef (AbsKn (Other t_array), [typ]) in
CAst.make ?loc @@ CPatCnv (pat, typ)
in
CAst.make ?loc @@ CTacFun ([pat], tac)
let of_pattern p =
inj_wit ?loc:p.CAst.loc wit_pattern p
let of_conversion {loc;v=c} = match c with
| QConvert c ->
let pat = of_option ?loc of_pattern None in
let c = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar Anonymous], of_constr c) in
of_tuple ?loc [pat; c]
| QConvertWith (pat, c) ->
let vars = pattern_vars pat in
let pat = of_option ?loc of_pattern (Some pat) in
let c = of_constr c in
(* Order is critical here *)
let vars = List.map (fun (id, loc) -> CAst.make ?loc (Name id)) (Id.Map.bindings vars) in
let c = abstract_vars loc vars c in
of_tuple [pat; c]
let of_repeat {loc;v=r} = match r with
| QPrecisely n -> std_constructor ?loc "Precisely" [of_int n]
| QUpTo n -> std_constructor ?loc "UpTo" [of_int n]
| QRepeatStar -> std_constructor ?loc "RepeatStar" []
| QRepeatPlus -> std_constructor ?loc "RepeatPlus" []
let of_orient loc b =
if b then std_constructor ?loc "LTR" []
else std_constructor ?loc "RTL" []
let of_rewriting {loc;v=rew} =
let orient =
let {loc;v=orient} = rew.rew_orient in
of_option ?loc (fun b -> of_orient loc b) orient
in
let repeat = of_repeat rew.rew_repeat in
let equatn = thunk (of_constr_with_bindings rew.rew_equatn) in
CAst.make ?loc @@ CTacRec (None, [
std_proj "rew_orient", orient;
std_proj "rew_repeat", repeat;
std_proj "rew_equatn", equatn;
])
let of_hyp ?loc id =
let hyp = global_ref ?loc (control_core "hyp") in
CAst.make ?loc @@ CTacApp (hyp, [of_ident id])
let of_exact_hyp ?loc id =
let refine = global_ref ?loc (control_core "refine") in
CAst.make ?loc @@ CTacApp (refine, [thunk (of_hyp ?loc id)])
let of_exact_var ?loc id =
let refine = global_ref ?loc (control_core "refine") in
CAst.make ?loc @@ CTacApp (refine, [thunk (of_variable id)])
let of_dispatch tacs =
let loc = tacs.loc in
let default = function
| Some e -> thunk e
| None -> thunk (CAst.make ?loc @@ CTacCst (AbsKn (Tuple 0)))
in
let map e = of_pair default (fun l -> of_list ?loc default l) (CAst.make ?loc e) in
of_pair (fun l -> of_list ?loc default l) (fun r -> of_option ?loc map r) tacs
let make_red_flag l =
let open Genredexpr in
let rec add_flag red = function
| [] -> red
| {v=flag} :: lf ->
let red = match flag with
| QBeta -> { red with rBeta = true }
| QMatch -> { red with rMatch = true }
| QFix -> { red with rFix = true }
| QCofix -> { red with rCofix = true }
| QZeta -> { red with rZeta = true }
| QConst {loc;v=l} ->
if red.rDelta then
CErrors.user_err ?loc Pp.(str
"Cannot set both constants to unfold and constants not to unfold");
{ red with rConst = red.rConst @ l }
| QDeltaBut {loc;v=l} ->
if red.rConst <> [] && not red.rDelta then
CErrors.user_err ?loc Pp.(str
"Cannot set both constants to unfold and constants not to unfold");
{ red with rConst = red.rConst @ l; rDelta = true }
| QIota ->
{ red with rMatch = true; rFix = true; rCofix = true }
in
add_flag red lf
in
add_flag
{rBeta = false; rMatch = false; rFix = false; rCofix = false;
rZeta = false; rDelta = false; rConst = []}
l
let of_reference r =
let of_ref ref =
inj_wit ?loc:ref.loc wit_reference ref
in
of_anti of_ref r
let of_strategy_flag {loc;v=flag} =
let open Genredexpr in
let flag = make_red_flag flag in
CAst.make ?loc @@ CTacRec (None, [
std_proj "rBeta", of_bool ?loc flag.rBeta;
std_proj "rMatch", of_bool ?loc flag.rMatch;
std_proj "rFix", of_bool ?loc flag.rFix;
std_proj "rCofix", of_bool ?loc flag.rCofix;
std_proj "rZeta", of_bool ?loc flag.rZeta;
std_proj "rDelta", of_bool ?loc flag.rDelta;
std_proj "rConst", of_list ?loc of_reference flag.rConst;
])
let of_hintdb {loc;v=hdb} = match hdb with
| QHintAll -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) None
| QHintDbs ids -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) (Some ids)
let extract_name ?loc oid = match oid with
| None -> Anonymous
| Some id ->
let () = check_pattern_id ?loc id in
Name id
(** For every branch in the matching, generate a corresponding term of type
[(match_kind * pattern * (context -> constr array -> 'a))]
where the function binds the names from the pattern to the contents of the
constr array. *)
let of_constr_matching {loc;v=m} =
let map {loc;v=({loc=ploc;v=pat}, tac)} =
let (knd, pat, na) = match pat with
| QConstrMatchPattern pat ->
let knd = constructor ?loc (pattern_core "MatchPattern") [] in
(knd, pat, Anonymous)
| QConstrMatchContext (id, pat) ->
let na = extract_name ?loc id in
let knd = constructor ?loc (pattern_core "MatchContext") [] in
(knd, pat, na)
in
let vars = pattern_vars pat in
(* Order of elements is crucial here! *)
let vars = Id.Map.bindings vars in
let vars = List.map (fun (id, loc) -> CAst.make ?loc (Name id)) vars in
(* Annotate the bound array variable with constr type *)
let typ =
let t_constr = coq_core "constr" in
CAst.make ?loc @@ CTypRef (AbsKn (Other t_constr), [])
in
let e = abstract_vars loc ~typ vars tac in
let e = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar na], e) in
let pat = inj_wit ?loc:ploc wit_pattern pat in
of_tuple [knd; pat; e]
in
let e = of_list ?loc map m in
let tykn = pattern_core "constr_matching" in
let ty = CAst.make ?loc (CTypRef (AbsKn (Other tykn),[CAst.make ?loc (CTypVar Anonymous)])) in
CAst.make ?loc (CTacCnv (e, ty))
(** From the patterns and the body of the branch, generate:
- a goal pattern: (constr_match list * constr_match)
- a branch function (ident array -> context array -> constr array -> context -> 'a)
*)
let of_goal_matching {loc;v=gm} =
let mk_pat {loc;v=p} = match p with
| QConstrMatchPattern pat ->
let knd = constructor ?loc (pattern_core "MatchPattern") [] in
(CAst.make ?loc Anonymous, pat, knd)
| QConstrMatchContext (id, pat) ->
let na = extract_name ?loc id in
let knd = constructor ?loc (pattern_core "MatchContext") [] in
(CAst.make ?loc na, pat, knd)
in
let mk_gpat {loc;v=p} =
let concl_pat = p.q_goal_match_concl in
let hyps_pats = p.q_goal_match_hyps in
let (concl_ctx, concl_pat, concl_knd) = mk_pat concl_pat in
let vars = pattern_vars concl_pat in
let map accu (na, bod, pat) = match bod with
| None ->
let (ctx, pat, knd) = mk_pat pat in
let vars = pattern_vars pat in
(Id.Map.fold Id.Map.add vars accu, (na, None, (ctx, knd, pat)))
| Some bod ->
let bctx, bpat, bknd = mk_pat bod in
let (ctx, pat, knd) = mk_pat pat in
let bvars = pattern_vars bpat in
let vars = pattern_vars pat in
let accu = Id.Map.fold Id.Map.add bvars accu in
let accu = Id.Map.fold Id.Map.add vars accu in
(accu, (na, Some ((bctx, bknd, bpat)), (ctx, knd, pat)))
in
let (vars, hyps_pats) = List.fold_left_map map vars hyps_pats in
let concl = of_tuple [concl_knd; of_pattern concl_pat] in
let of_hyp_pat (_, bpat, (_, knd, pat)) =
let bpat = Option.map (fun (_, a, b) -> (a, b)) bpat in
let of_mpat (a, b) = of_tuple [a; of_pattern b] in
of_tuple [of_option of_mpat bpat; of_mpat (knd, pat)]
in
let r = of_tuple [
of_list ?loc of_hyp_pat hyps_pats;
concl]
in
let hyps = List.map (fun (na, _, _) -> na) hyps_pats in
let hbctx = CList.filter_map (fun (_, b, _) -> Option.map pi1 b) hyps_pats in
let hctx = CList.map (fun (_, _, (na, _, _)) -> na) hyps_pats in
(* Order of elements is crucial here! *)
let vars = Id.Map.bindings vars in
let subst = List.map (fun (id, loc) -> CAst.make ?loc (Name id)) vars in
(r, hyps, hbctx, hctx, subst, concl_ctx)
in
let map {loc;v=(pat, tac)} =
let (pat, hyps, hbctx, hctx, subst, cctx) = mk_gpat pat in
let tac = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar cctx.CAst.v], tac) in
let tac = abstract_vars loc subst tac in
let tac = abstract_vars loc hctx tac in
let tac = abstract_vars loc hbctx tac in
let tac = abstract_vars loc hyps tac in
of_tuple ?loc [pat; tac]
in
let e = of_list ?loc map gm in
let tykn = pattern_core "goal_matching" in
let ty = CAst.make ?loc (CTypRef (AbsKn (Other tykn),[CAst.make ?loc (CTypVar Anonymous)])) in
CAst.make ?loc (CTacCnv (e, ty))
let of_move_location {loc;v=mv} = match mv with
| QMoveAfter id -> std_constructor ?loc "MoveAfter" [of_anti of_ident id]
| QMoveBefore id -> std_constructor ?loc "MoveBefore" [of_anti of_ident id]
| QMoveFirst -> std_constructor ?loc "MoveFirst" []
| QMoveLast -> std_constructor ?loc "MoveLast" []
let of_pose p =
of_pair (fun id -> of_option (fun id -> of_anti of_ident id) id) of_open_constr p
let of_assertion {loc;v=ast} = match ast with
| QAssertType (ipat, c, tac) ->
let ipat = of_option of_intro_pattern ipat in
let c = of_constr c in
let tac = of_option thunk tac in
std_constructor ?loc "AssertType" [ipat; c; tac]
| QAssertValue (id, c) ->
let id = of_anti of_ident id in
let c = of_constr c in
std_constructor ?loc "AssertValue" [id; c]
let of_format accu = function
| Tac2print.FmtString ->
CAst.make @@ CTacApp (global_ref (kername format_prefix "string"), [accu])
| Tac2print.FmtInt ->
CAst.make @@ CTacApp (global_ref (kername format_prefix "int"), [accu])
| Tac2print.FmtConstr ->
CAst.make @@ CTacApp (global_ref (kername format_prefix "constr"), [accu])
| Tac2print.FmtIdent ->
CAst.make @@ CTacApp (global_ref (kername format_prefix "ident"), [accu])
| Tac2print.FmtLiteral lit ->
let s = of_string (CAst.make lit) in
CAst.make @@ CTacApp (global_ref (kername format_prefix "literal"), [s; accu])
| Tac2print.FmtAlpha ->
CAst.make @@ CTacApp (global_ref (kername format_prefix "alpha"), [accu])
let of_format { v = fmt; loc } =
let fmt =
try Tac2print.parse_format fmt
with Tac2print.InvalidFormat ->
CErrors.user_err ?loc (str "Invalid format")
in
let stop = global_ref (kername format_prefix "stop") in
List.fold_left of_format stop fmt