Source file egramcoq.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
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
open Util
open CErrors
open Names
open Libnames
open Constrexpr
open Extend
open Notationextern
open Notation_gram
open Pcoq
let constr_level = string_of_int
let default_levels =
[200,Gramlib.Gramext.RightA,false;
100,Gramlib.Gramext.RightA,false;
99,Gramlib.Gramext.RightA,true;
90,Gramlib.Gramext.RightA,true;
10,Gramlib.Gramext.LeftA,false;
9,Gramlib.Gramext.RightA,false;
8,Gramlib.Gramext.RightA,true;
1,Gramlib.Gramext.LeftA,false;
0,Gramlib.Gramext.RightA,false]
let default_pattern_levels =
[200,Gramlib.Gramext.RightA,true;
100,Gramlib.Gramext.RightA,false;
99,Gramlib.Gramext.RightA,true;
90,Gramlib.Gramext.RightA,true;
10,Gramlib.Gramext.LeftA,false;
1,Gramlib.Gramext.LeftA,false;
0,Gramlib.Gramext.RightA,false]
let default_constr_levels = (default_levels, default_pattern_levels)
let find_levels levels = function
| InConstrEntry -> levels, String.Map.find "constr" levels
| InCustomEntry s ->
try levels, String.Map.find s levels
with Not_found ->
String.Map.add s ([],[]) levels, ([],[])
let save_levels levels custom lev =
let s = match custom with InConstrEntry -> "constr" | InCustomEntry s -> s in
String.Map.add s lev levels
let admissible_assoc = function
| Gramlib.Gramext.LeftA, Some (Gramlib.Gramext.RightA | Gramlib.Gramext.NonA) -> false
| Gramlib.Gramext.RightA, Some Gramlib.Gramext.LeftA -> false
| _ -> true
let create_assoc = function
| None -> Gramlib.Gramext.RightA
| Some a -> a
exception NotationLevelMismatch
of entry_level * Gramlib.Gramext.g_assoc * Gramlib.Gramext.g_assoc
let () = CErrors.register_handler (function
| NotationLevelMismatch (p, current, expected) ->
Some Pp.(str "Level " ++ int p ++ str " is already declared to have " ++
Gramlib.Gramext.pr_assoc current ++
str " while it is now expected to have " ++
Gramlib.Gramext.pr_assoc expected ++ str ".")
| _ -> None)
let error_level_assoc p current expected =
raise @@ NotationLevelMismatch (p, current, expected)
type position = NewFirst | NewAfter of int | ReuseFirst | ReuseLevel of int
let create_pos = function
| None -> NewFirst
| Some lev -> NewAfter lev
let find_position_gen current ensure assoc lev =
match lev with
| None ->
current, (ReuseFirst, None, None, None)
| Some n ->
let after = ref None in
let init = ref None in
let rec add_level q = function
| (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
| (p,a,reinit)::l when Int.equal p n ->
if reinit then
let a' = create_assoc assoc in
(init := Some (a', q); (p,a',false)::l)
else if admissible_assoc (a,assoc) then
raise_notrace Exit
else
error_level_assoc p a (Option.get assoc)
| l -> after := q; (n,create_assoc assoc,ensure)::l
in
try
let updated = add_level None current in
let assoc = create_assoc assoc in
begin match !init with
| None ->
updated, (create_pos !after, Some assoc, Some (constr_level n), None)
| _ ->
updated, (ReuseLevel n, None, None, !init)
end
with
Exit ->
current, (ReuseLevel n, None, None, None)
let rec list_mem_assoc_triple x = function
| [] -> false
| (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l
let register_empty_levels accu forpat levels =
let rec filter accu = function
| [] -> ([], accu)
| (where,n) :: rem ->
let rem, accu = filter accu rem in
let accu, (clev, plev) = find_levels accu where in
let levels = if forpat then plev else clev in
if not (list_mem_assoc_triple n levels) then
let nlev, ans = find_position_gen levels true None (Some n) in
let nlev = if forpat then (clev, nlev) else (nlev, plev) in
(where, ans) :: rem, save_levels accu where nlev
else rem, accu
in
let (l,accu) = filter accu levels in
List.rev l, accu
let find_position accu custom forpat assoc level =
let accu, (clev, plev) = find_levels accu custom in
let levels = if forpat then plev else clev in
let nlev, ans = find_position_gen levels false assoc level in
let nlev = if forpat then (clev, nlev) else (nlev, plev) in
(ans, save_levels accu custom nlev)
(** Declare Notations grammar rules *)
let camlp5_assoc =
let open Gramlib.Gramext in function
| Some NonA | Some RightA -> RightA
| None | Some LeftA -> LeftA
let assoc_eq al ar =
let open Gramlib.Gramext in
match al, ar with
| NonA, NonA
| RightA, RightA
| LeftA, LeftA -> true
| _, _ -> false
(** [adjust_level assoc from prod] where [assoc] and [from] are the name
and associativity of the level where to add the rule; the meaning of
the result is
DefaultLevel = entry name
NextLevel = NEXT
NumLevel n = constr LEVEL n *)
let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with
| (NumLevel n,_) when not (notation_entry_eq custom custom') -> NumLevel n
| (DefaultLevel,InternalProd) ->
if notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel
| (DefaultLevel,BorderProd _) when not (notation_entry_eq custom custom') ->
if notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel
| (NumLevel n,BorderProd (_,None)) -> NumLevel n
| (DefaultLevel,BorderProd (_,None)) -> assert false
| ((NumLevel _ | DefaultLevel),BorderProd (Right,Some (NonA|LeftA))) -> NextLevel
| (NumLevel n,BorderProd (Right,Some RightA)) -> NumLevel n
| (DefaultLevel,BorderProd (Right,Some RightA)) -> NumLevel from
| ((NumLevel _ | DefaultLevel),BorderProd (Left,Some NonA)) -> DefaultLevel
| ((NumLevel _ | DefaultLevel),BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
DefaultLevel
| (NumLevel n,BorderProd (Left,Some LeftA)) -> NumLevel n
| ((NumLevel _ | DefaultLevel),BorderProd (Left,Some _)) -> NextLevel
| (NextLevel,_) -> assert (notation_entry_eq custom custom'); NextLevel
| (NumLevel n,InternalProd) ->
if from = n + 1 then NextLevel else NumLevel n
type _ target =
| ForConstr : constr_expr target
| ForPattern : cases_pattern_expr target
type prod_info = production_level * production_position
type (_, _) entry =
| TTIdent : ('self, lident) entry
| TTName : ('self, lname) entry
| TTGlobal : ('self, qualid) entry
| TTBigint : ('self, string) entry
| TTBinder : bool -> ('self, kinded_cases_pattern_expr) entry
| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : notation_entry * prod_info * (bool * string) list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry
| TTOpenBinderList : ('self, local_binder_expr list) entry
| TTClosedBinderListPure : (bool * string) list -> ('self, local_binder_expr list list) entry
| TTClosedBinderListOther : ('self, 'a) entry * (bool * string) list -> ('self, 'a list) entry
type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
let constr_custom_entry : (string, Constrexpr.constr_expr) entry_command =
create_entry_command "constr" { eext_fun = (fun s st -> [s], st); eext_eq = (==) }
let pattern_custom_entry : (string, Constrexpr.cases_pattern_expr) entry_command =
create_entry_command "pattern" { eext_fun = (fun s st -> [s], st); eext_eq = (==) }
let custom_entry_locality = Summary.ref ~name:"LOCAL-CUSTOM-ENTRY" String.Set.empty
(** If the entry is present then local *)
let create_custom_entry ~local s =
if List.mem s ["constr";"pattern";"ident";"global";"binder";"bigint"] then
user_err Pp.(quote (str s) ++ str " is a reserved entry name.");
let sc = "custom:"^s in
let sp = "custom_pattern:"^s in
let _ = extend_entry_command constr_custom_entry sc in
let _ = extend_entry_command pattern_custom_entry sp in
let () = if local then custom_entry_locality := String.Set.add s !custom_entry_locality in
()
let find_custom_entry s =
let sc = "custom:"^s in
let sp = "custom_pattern:"^s in
try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp)
with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
let exists_custom_entry s = match find_custom_entry s with
| _ -> true
| exception _ -> false
let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality
let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int option =
fun custom forpat level ->
match custom with
| InCustomEntry s ->
(let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
match forpat with
| ForConstr -> entry_for_constr, Some level
| ForPattern -> entry_for_patttern, Some level)
| InConstrEntry ->
match forpat with
| ForConstr ->
if level = 200 then Constr.binder_constr, None
else Constr.term, Some level
| ForPattern -> Constr.pattern, Some level
let target_entry : type s. notation_entry -> s target -> s Entry.t = function
| InConstrEntry ->
(function
| ForConstr -> Constr.term
| ForPattern -> Constr.pattern)
| InCustomEntry s ->
let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
function
| ForConstr -> entry_for_constr
| ForPattern -> entry_for_patttern
let is_self custom (custom',from) e = notation_entry_eq custom custom' && match e with
| (NumLevel n, BorderProd (Right, _ )) -> false
| (NumLevel n, BorderProd (Left, _)) -> Int.equal from n
| _ -> false
let is_binder_level custom (custom',from) e = match e with
| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) ->
custom = InConstrEntry && custom' = InConstrEntry && from = 200
| _ -> false
let make_pattern (keyword,s) =
if keyword then TPattern (Tok.PKEYWORD s) else
match NumTok.Unsigned.parse_string s with
| Some n -> TPattern (Tok.PNUMBER (Some n))
| None -> TPattern (Tok.PIDENT (Some s))
let make_sep_rules tkl =
Pcoq.Symbol.tokens (List.map make_pattern tkl)
type ('s, 'a) mayrec_symbol =
| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol
| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol
let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
if is_binder_level custom from p
then
MayRecNo (Pcoq.Symbol.nterml (target_entry custom forpat) "200")
else if is_self custom from p then MayRecMay Pcoq.Symbol.self
else
let g = target_entry custom forpat in
let lev = adjust_level custom assoc from p in
begin match lev with
| DefaultLevel -> MayRecNo (Pcoq.Symbol.nterm g)
| NextLevel -> MayRecMay Pcoq.Symbol.next
| NumLevel lev -> MayRecNo (Pcoq.Symbol.nterml g (string_of_int lev))
end
let rec symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
| TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
| TTConstrList (s, typ', [], forpat) ->
begin match symbol_of_target s typ' assoc from forpat with
| MayRecNo s -> MayRecNo (Pcoq.Symbol.list1 s)
| MayRecMay s -> MayRecMay (Pcoq.Symbol.list1 s) end
| TTConstrList (s, typ', tkl, forpat) ->
begin match symbol_of_target s typ' assoc from forpat with
| MayRecNo s -> MayRecNo (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false)
| MayRecMay s -> MayRecMay (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false) end
| TTPattern p -> MayRecNo (Pcoq.Symbol.nterml Constr.pattern (string_of_int p))
| TTOpenBinderList -> MayRecNo (Pcoq.Symbol.nterm Constr.open_binders)
| TTClosedBinderListPure [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder))
| TTClosedBinderListPure tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
| TTClosedBinderListOther (typ,[]) ->
begin match symbol_of_entry assoc from typ with
| MayRecNo s -> MayRecNo (Pcoq.Symbol.list1 s)
| MayRecMay s -> MayRecMay (Pcoq.Symbol.list1 s) end
| TTClosedBinderListOther (typ,tkl) ->
begin match symbol_of_entry assoc from typ with
| MayRecNo s -> MayRecNo (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false)
| MayRecMay s -> MayRecMay (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false) end
| TTIdent -> MayRecNo (Pcoq.Symbol.nterm Prim.identref)
| TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name)
| TTBinder true -> MayRecNo (Pcoq.Symbol.nterm Constr.one_open_binder)
| TTBinder false -> MayRecNo (Pcoq.Symbol.nterm Constr.one_closed_binder)
| TTBigint -> MayRecNo (Pcoq.Symbol.nterm Prim.bignat)
| TTGlobal -> MayRecNo (Pcoq.Symbol.nterm Constr.global)
let rec interp_entry forpat e = match e with
| ETProdIdent -> TTAny TTIdent
| ETProdName -> TTAny TTName
| ETProdGlobal -> TTAny TTGlobal
| ETProdBigint -> TTAny TTBigint
| ETProdOneBinder o -> TTAny (TTBinder o)
| ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
| ETProdPattern p -> TTAny (TTPattern p)
| ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
| ETProdBinderList (ETBinderClosed (None, tkl)) -> TTAny (TTClosedBinderListPure tkl)
| ETProdBinderList (ETBinderClosed (Some e, tkl)) ->
let TTAny e = interp_entry forpat e in TTAny (TTClosedBinderListOther (e, tkl))
let cases_pattern_expr_of_id { CAst.loc; v = id } =
CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with
| Anonymous -> CPatAtom None
| Name id -> CPatAtom (Some (qualid_of_ident ?loc id))
type 'r env = {
constrs : 'r list;
constrlists : 'r list list;
binders : kinded_cases_pattern_expr list;
binderlists : local_binder_expr list list;
}
let push_constr subst v = { subst with constrs = v :: subst.constrs }
let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v ->
match e with
| TTConstr _ -> push_constr subst v
| TTIdent ->
begin match forpat with
| ForConstr -> { subst with binders = (cases_pattern_expr_of_id v, Glob_term.Explicit) :: subst.binders }
| ForPattern -> push_constr subst (cases_pattern_expr_of_id v)
end
| TTName ->
begin match forpat with
| ForConstr -> { subst with binders = (cases_pattern_expr_of_name v, Glob_term.Explicit) :: subst.binders }
| ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
end
| TTPattern _ ->
begin match forpat with
| ForConstr -> { subst with binders = (v, Glob_term.Explicit) :: subst.binders }
| ForPattern -> push_constr subst v
end
| TTBinder o -> { subst with binders = v :: subst.binders }
| TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists }
| TTClosedBinderListPure _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
| TTClosedBinderListOther (TTIdent, _) -> { subst with binderlists = List.map (fun a -> CLocalPattern (cases_pattern_expr_of_id a)) v :: subst.binderlists }
| TTClosedBinderListOther (TTName, _) -> { subst with binderlists = List.map (fun a -> CLocalPattern (cases_pattern_expr_of_name a)) v :: subst.binderlists }
| TTClosedBinderListOther (TTPattern _, _) -> { subst with binderlists = List.map (fun a -> CLocalPattern a) v :: subst.binderlists }
| TTClosedBinderListOther _ -> user_err (Pp.str "Invalid binder list entry.")
| TTBigint ->
begin match forpat with
| ForConstr -> push_constr subst (CAst.make @@ CPrim (Number (NumTok.Signed.of_int_string v)))
| ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Number (NumTok.Signed.of_int_string v)))
end
| TTGlobal ->
begin match forpat with
| ForConstr -> push_constr subst (CAst.make @@ CRef (v, None))
| ForPattern -> push_constr subst (CAst.make @@ CPatAtom (Some v))
end
| TTConstrList _ -> { subst with constrlists = v :: subst.constrlists }
type (_, _) ty_symbol =
| TyTerm : 'a Tok.p -> ('s, 'a) ty_symbol
| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) mayrec_symbol * bool -> ('s, 'a) ty_symbol
type ('self, _, 'r) ty_rule =
| TyStop : ('self, 'r, 'r) ty_rule
| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule
| TyMark : int * bool * int * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule
type 'r gen_eval = Loc.t -> 'r env -> 'r
let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> a = function
| TyStop ->
fun f env loc -> f loc env
| TyNext (rem, TyTerm _) ->
fun f env _ -> ty_eval rem f env
| TyNext (rem, TyNonTerm (_, _, _, false)) ->
fun f env _ -> ty_eval rem f env
| TyNext (rem, TyNonTerm (forpat, e, _, true)) ->
fun f env v ->
ty_eval rem f (push_item forpat e env v)
| TyMark (n, b, p, rem) ->
fun f env ->
let heads, constrs = List.chop n env.constrs in
let constrlists, constrs =
if b then
let constrlist = List.hd env.constrlists in
let constrlist, tail = List.chop (List.length constrlist - p) constrlist in
(heads @ constrlist) :: List.tl env.constrlists, tail @ constrs
else
let constrlist, tail = List.chop (n - p) heads in
constrlist :: env.constrlists, tail @ constrs
in
ty_eval rem f { env with constrs; constrlists; }
type ('s, 'a, 'r) mayrec_rule =
| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) Rule.t -> ('s, 'a, 'r) mayrec_rule
| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) Rule.t -> ('s, 'a, 'r) mayrec_rule
let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function
| TyStop -> MayRecRNo Rule.stop
| TyMark (_, _, _, r) -> ty_erase r
| TyNext (rem, TyTerm tok) ->
begin match ty_erase rem with
| MayRecRNo rem -> MayRecRMay (Rule.next rem (Symbol.token tok))
| MayRecRMay rem -> MayRecRMay (Rule.next rem (Symbol.token tok)) end
| TyNext (rem, TyNonTerm (_, _, s, _)) ->
begin match ty_erase rem, s with
| MayRecRNo rem, MayRecNo s -> MayRecRMay (Rule.next rem s)
| MayRecRNo rem, MayRecMay s -> MayRecRMay (Rule.next rem s)
| MayRecRMay rem, MayRecNo s -> MayRecRMay (Rule.next rem s)
| MayRecRMay rem, MayRecMay s -> MayRecRMay (Rule.next rem s) end
type ('self, 'r) any_ty_rule =
| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
let make_ty_rule assoc from forpat prods =
let rec make_ty_rule = function
| [] -> AnyTyRule TyStop
| GramConstrTerminal (kw,s) :: rem ->
let AnyTyRule r = make_ty_rule rem in
let TPattern tk = make_pattern (kw,s) in
AnyTyRule (TyNext (r, TyTerm tk))
| GramConstrNonTerminal (e, var) :: rem ->
let AnyTyRule r = make_ty_rule rem in
let TTAny e = interp_entry forpat e in
let s = symbol_of_entry assoc from e in
let bind = match var with None -> false | Some _ -> true in
AnyTyRule (TyNext (r, TyNonTerm (forpat, e, s, bind)))
| GramConstrListMark (n, b, p) :: rem ->
let AnyTyRule r = make_ty_rule rem in
AnyTyRule (TyMark (n, b, p, r))
in
make_ty_rule (List.rev prods)
let target_to_bool : type r. r target -> bool = function
| ForConstr -> false
| ForPattern -> true
let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
let empty = match pos with
| ReuseFirst -> Pcoq.Reuse (None, [])
| ReuseLevel n -> Pcoq.Reuse (Some (constr_level n), [])
| NewFirst -> Pcoq.Fresh (Gramlib.Gramext.First, [(name, p4assoc, [])])
| NewAfter n -> Pcoq.Fresh (Gramlib.Gramext.After (constr_level n), [(name, p4assoc, [])])
in
match reinit with
| None ->
ExtendRule (target_entry where forpat, empty)
| Some (assoc, pos) ->
let pos = match pos with None -> Gramlib.Gramext.First | Some n -> Gramlib.Gramext.After (constr_level n) in
let reinit = (assoc, pos) in
ExtendRuleReinit (target_entry where forpat, reinit, empty)
let different_levels (custom,opt_level) (custom',string_level) =
match opt_level with
| None -> true
| Some level -> not (notation_entry_eq custom custom') || level <> int_of_string string_level
let rec pure_sublevels' assoc from forpat level = function
| [] -> []
| GramConstrNonTerminal (e,_) :: rem ->
let rem = pure_sublevels' assoc from forpat level rem in
let push where p rem =
match symbol_of_target where p assoc from forpat with
| MayRecNo sym ->
(match Pcoq.level_of_nonterm sym with
| None -> rem
| Some i ->
if different_levels (fst from,level) (where,i) then
(where,int_of_string i) :: rem
else rem)
| _ -> rem in
(match e with
| ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
| ETProdConstr (s,p) -> push s p rem
| _ -> rem)
| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' assoc from forpat level rem
let make_act : type r. r target -> _ -> r gen_eval = function
| ForConstr -> fun notation loc env ->
let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in
CAst.make ~loc @@ CNotation (None, notation, env)
| ForPattern -> fun notation loc env ->
let env = (env.constrs, env.constrlists) in
CAst.make ~loc @@ CPatNotation (None, notation, env, [])
let extend_constr state forpat ng =
let custom,n,_ = ng.notgram_level in
let assoc = ng.notgram_assoc in
let (entry, level) = interp_constr_entry_key custom forpat n in
let fold (accu, state) pt =
let AnyTyRule r = make_ty_rule assoc (custom,n) forpat pt in
let pure_sublevels = pure_sublevels' assoc (custom,n) forpat level pt in
let isforpat = target_to_bool forpat in
let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
let (pos,p4assoc,name,reinit), state = find_position state custom isforpat assoc level in
let empty_rules = List.map (prepare_empty_levels forpat) needed_levels in
let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in
let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
let rule =
let r = match ty_erase r with
| MayRecRNo symbs -> Pcoq.Production.make symbs act
| MayRecRMay symbs -> Pcoq.Production.make symbs act
in
let rule = name, p4assoc, [r] in
match pos with
| NewFirst -> Pcoq.Fresh (Gramlib.Gramext.First, [rule])
| NewAfter n -> Pcoq.Fresh (Gramlib.Gramext.After (constr_level n), [rule])
| ReuseFirst -> Pcoq.Reuse (None, [r])
| ReuseLevel n -> Pcoq.Reuse (Some (constr_level n), [r])
in
let r = match reinit with
| None ->
ExtendRule (entry, rule)
| Some (assoc, pos) ->
let pos = match pos with None -> Gramlib.Gramext.First | Some n -> Gramlib.Gramext.After (constr_level n) in
let reinit = (assoc, pos) in
ExtendRuleReinit (entry, reinit, rule)
in
(accu @ empty_rules @ [r], state)
in
List.fold_left fold ([], state) ng.notgram_prods
let constr_levels = GramState.field ()
let is_disjunctive_pattern_rule ng =
String.is_sub "( _ | " (snd ng.notgram_notation) 0
let warn_disj_pattern_notation =
let open Pp in
let pp ng = str "Use of " ++ Notation.pr_notation ng.notgram_notation ++
str " Notation is deprecated as it is inconsistent with pattern syntax." in
CWarnings.create ~name:"disj-pattern-notation" ~category:CWarnings.CoreCategories.syntax ~default:CWarnings.Disabled pp
let extend_constr_notation ng state =
let levels = match GramState.get state constr_levels with
| None -> String.Map.add "constr" default_constr_levels String.Map.empty
| Some lev -> lev
in
let (r, levels) = extend_constr levels ForConstr ng in
let (r', levels) =
if is_disjunctive_pattern_rule ng then begin
warn_disj_pattern_notation ng;
([], levels)
end else extend_constr levels ForPattern ng in
let state = GramState.set state constr_levels levels in
(r @ r', state)
let constr_grammar : one_notation_grammar grammar_command =
create_grammar_command "Notation" { gext_fun = extend_constr_notation; gext_eq = (==) }
let extend_constr_grammar ntn = extend_grammar_command constr_grammar ntn