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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Pp
open Util
open Extend
open Pcoq
open Topconstr
open Ast
open Genarg
open Libnames
open Nameops
(* State of the grammar extensions *)
type all_grammar_command =
| Notation of
(int * Gramext.g_assoc option * notation * prod_item list *
int list option)
| Grammar of grammar_command
| TacticGrammar of
(string * (string * grammar_production list) *
(Names.dir_path * Tacexpr.raw_tactic_expr))
list
let subst_all_grammar_command subst = function
| Notation _ -> anomaly "Notation not in GRAMMAR summary"
| Grammar gc -> Grammar (subst_grammar_command subst gc)
| TacticGrammar g -> TacticGrammar g (* TODO ... *)
let (grammar_state : all_grammar_command list ref) = ref []
(**************************************************************************)
(* Interpretation of the right hand side of grammar rules *)
(* When reporting errors, we add the name of the grammar rule that failed *)
let specify_name name e =
match e with
| UserError(lab,strm) ->
UserError(lab, (str"during interpretation of grammar rule " ++
str name ++ str"," ++ spc () ++ strm))
| Anomaly(lab,strm) ->
Anomaly(lab, (str"during interpretation of grammar rule " ++
str name ++ str"," ++ spc () ++ strm))
| Failure s ->
Failure("during interpretation of grammar rule "^name^", "^s)
| e -> e
(* Translation of environments: a production
* [ nt1(x1) ... nti(xi) ] -> act(x1..xi)
* is written (with camlp4 conventions):
* (fun vi -> .... (fun v1 -> act(v1 .. vi) )..)
* where v1..vi are the values generated by non-terminals nt1..nti.
* Since the actions are executed by substituting an environment,
* make_act builds the following closure:
*
* ((fun env ->
* (fun vi ->
* (fun env -> ...
*
* (fun v1 ->
* (fun env -> gram_action .. env act)
* ((x1,v1)::env))
* ...)
* ((xi,vi)::env)))
* [])
*)
open Names
type 'a action_env = (identifier * 'a) list
let make_act (f : loc -> constr_expr action_env -> constr_expr) pil =
let rec make (env : constr_expr action_env) = function
| [] ->
Gramext.action (fun loc -> f loc env)
| None :: tl -> (* parse a non-binding item *)
Gramext.action (fun _ -> make env tl)
| Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *)
Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl)
| Some (p, ETReference) :: tl -> (* non-terminal *)
Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl)
| Some (p, ETIdent) :: tl -> (* non-terminal *)
Gramext.action (fun (v:identifier) ->
make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
| Some (p, ETBigint) :: tl -> (* non-terminal *)
Gramext.action (fun (v:Bignat.bigint) ->
make ((p,CNumeral (dummy_loc,v)) :: env) tl)
| Some (p, ETPattern) :: tl ->
failwith "Unexpected entry of type cases pattern" in
make [] (List.rev pil)
let make_act_in_cases_pattern (* For Notations *)
(f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
let rec make (env : cases_pattern_expr action_env) = function
| [] ->
Gramext.action (fun loc -> f loc env)
| None :: tl -> (* parse a non-binding item *)
Gramext.action (fun _ -> make env tl)
| Some (p, ETConstr _) :: tl -> (* pattern non-terminal *)
Gramext.action (fun (v:cases_pattern_expr) -> make ((p,v) :: env) tl)
| Some (p, ETReference) :: tl -> (* non-terminal *)
Gramext.action (fun (v:reference) ->
make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
| Some (p, ETIdent) :: tl -> (* non-terminal *)
Gramext.action (fun (v:identifier) ->
make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl)
| Some (p, ETBigint) :: tl -> (* non-terminal *)
Gramext.action (fun (v:Bignat.bigint) ->
make ((p,CPatNumeral (dummy_loc,v)) :: env) tl)
| Some (p, (ETPattern | ETOther _)) :: tl ->
failwith "Unexpected entry of type cases pattern or other" in
make [] (List.rev pil)
let make_cases_pattern_act (* For Grammar *)
(f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
let rec make (env : cases_pattern_expr action_env) = function
| [] ->
Gramext.action (fun loc -> f loc env)
| None :: tl -> (* parse a non-binding item *)
Gramext.action (fun _ -> make env tl)
| Some (p, ETPattern) :: tl -> (* non-terminal *)
Gramext.action (fun v -> make ((p,v) :: env) tl)
| Some (p, ETReference) :: tl -> (* non-terminal *)
Gramext.action (fun v -> make ((p,CPatAtom(dummy_loc,Some v)) :: env)
tl)
| Some (p, ETBigint) :: tl -> (* non-terminal *)
Gramext.action (fun v -> make ((p,CPatNumeral(dummy_loc,v)) :: env) tl)
| Some (p, (ETIdent | ETConstr _ | ETOther _)) :: tl ->
error "ident and constr entry not admitted in patterns cases syntax extensions" in
make [] (List.rev pil)
(* Grammar extension command. Rules are assumed correct.
* Type-checking of grammar rules is done during the translation of
* ast to the type grammar_command. We only check that the existing
* entries have the type assumed in the grammar command (these types
* annotations are added when type-checking the command, function
* Extend.of_ast) *)
let rec build_prod_item univ assoc fromlevel pat = function
| ProdList0 s -> Gramext.Slist0 (build_prod_item univ assoc fromlevel pat s)
| ProdList1 s -> Gramext.Slist1 (build_prod_item univ assoc fromlevel pat s)
| ProdOpt s -> Gramext.Sopt (build_prod_item univ assoc fromlevel pat s)
| ProdPrimitive typ -> symbol_of_production assoc fromlevel pat typ
let symbol_of_prod_item univ assoc from forpat = function
| Term tok -> (Gramext.Stoken tok, None)
| NonTerm (nt, ovar) ->
let eobj = build_prod_item univ assoc from forpat nt in
(eobj, ovar)
let coerce_to_id = function
| CRef (Ident (_,id)) -> id
| c ->
user_err_loc (constr_loc c, "subst_rawconstr",
str"This expression should be a simple identifier")
let coerce_to_ref = function
| CRef r -> r
| c ->
user_err_loc (constr_loc c, "subst_rawconstr",
str"This expression should be a simple reference")
let subst_ref loc subst id =
try coerce_to_ref (List.assoc id subst) with Not_found -> Ident (loc,id)
let subst_pat_id loc subst id =
try List.assoc id subst
with Not_found -> CPatAtom (loc,Some (Ident (loc,id)))
let subst_id subst id =
try coerce_to_id (List.assoc id subst) with Not_found -> id
(*
let subst_cases_pattern_expr a loc subs =
let rec subst = function
| CPatAlias (_,p,x) -> CPatAlias (loc,subst p,x)
(* No subst in compound pattern ? *)
| CPatCstr (_,ref,pl) -> CPatCstr (loc,ref,List.map subst pl)
| CPatAtom (_,Some (Ident (_,id))) -> subst_pat_id loc subs id
| CPatAtom (_,x) -> CPatAtom (loc,x)
| CPatNotation (_,ntn,l) -> CPatNotation
| CPatNumeral (_,n) -> CPatNumeral (loc,n)
| CPatDelimiters (_,key,p) -> CPatDelimiters (loc,key,subst p)
in subst a
*)
let subst_constr_expr a loc subs =
let rec subst = function
| CRef (Ident (_,id)) ->
(try List.assoc id subs with Not_found -> CRef (Ident (loc,id)))
(* Temporary: no robust treatment of substituted binders *)
| CLambdaN (_,[],c) -> subst c
| CLambdaN (_,([],t)::bl,c) -> subst (CLambdaN (loc,bl,c))
| CLambdaN (_,((_,na)::bl,t)::bll,c) ->
let na = name_app (subst_id subs) na in
CLambdaN (loc,[[loc,na],subst t], subst (CLambdaN (loc,(bl,t)::bll,c)))
| CProdN (_,[],c) -> subst c
| CProdN (_,([],t)::bl,c) -> subst (CProdN (loc,bl,c))
| CProdN (_,((_,na)::bl,t)::bll,c) ->
let na = name_app (subst_id subs) na in
CProdN (loc,[[loc,na],subst t], subst (CProdN (loc,(bl,t)::bll,c)))
| CLetIn (_,(_,na),b,c) ->
let na = name_app (subst_id subs) na in
CLetIn (loc,(loc,na),subst b,subst c)
| CArrow (_,a,b) -> CArrow (loc,subst a,subst b)
| CAppExpl (_,(p,Ident (_,id)),l) ->
CAppExpl (loc,(p,subst_ref loc subs id),List.map subst l)
| CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l)
| CApp (_,(p,a),l) ->
CApp (loc,(p,subst a),List.map (fun (a,i) -> (subst a,i)) l)
| CCast (_,a,b) -> CCast (loc,subst a,subst b)
| CNotation (_,n,l) -> CNotation (loc,n,List.map subst l)
| CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
| CNumeral _ | CDynamic _ | CRef _ as x -> x
| CCases (_,(po,rtntypo),a,bl) ->
(* TODO: apply g on the binding variables in pat... *)
let bl = List.map (fun (_,pat,rhs) -> (loc,pat,subst rhs)) bl in
CCases (loc,(option_app subst po,option_app subst rtntypo),
List.map (fun (tm,x) -> subst tm,x) a,bl)
| COrderedCase (_,s,po,a,bl) ->
COrderedCase (loc,s,option_app subst po,subst a,List.map subst bl)
| CLetTuple (_,nal,(na,po),a,b) ->
let na = option_app (name_app (subst_id subs)) na in
let nal = List.map (name_app (subst_id subs)) nal in
CLetTuple (loc,nal,(na,option_app subst po),subst a,subst b)
| CIf (_,c,(na,po),b1,b2) ->
let na = option_app (name_app (subst_id subs)) na in
CIf (loc,subst c,(na,option_app subst po),subst b1,subst b2)
| CFix (_,id,dl) ->
CFix (loc,id,List.map (fun (id,n,on, t,d) -> (id,n, on,subst t,subst d)) dl)
| CCoFix (_,id,dl) ->
CCoFix (loc,id,List.map (fun (id,t,d) -> (id,subst t,subst d)) dl)
in subst a
let make_rule univ assoc etyp rule =
let pil = List.map (symbol_of_prod_item univ assoc etyp false) rule.gr_production in
let (symbs,ntl) = List.split pil in
let act = match etyp with
| ETPattern ->
(* Ugly *)
let f loc env = match rule.gr_action, env with
| CRef (Ident(_,p)), [p',a] when p=p' -> a
| CDelimiters (_,s,CRef (Ident(_,p))), [p',a] when p=p' ->
CPatDelimiters (loc,s,a)
| _ -> error "Unable to handle this grammar extension of pattern" in
make_cases_pattern_act f ntl
| ETIdent | ETBigint | ETReference -> error "Cannot extend"
| ETConstr _ | ETOther _ ->
make_act (subst_constr_expr rule.gr_action) ntl in
(symbs, act)
(* Rules of a level are entered in reverse order, so that the first rules
are applied before the last ones *)
let extend_entry univ (te, etyp, pos, name, ass, p4ass, rls) =
let rules = List.rev (List.map (make_rule univ ass etyp) rls) in
grammar_extend te pos [(name, p4ass, rules)]
(* Defines new entries. If the entry already exists, check its type *)
let define_entry univ {ge_name=typ; gl_assoc=ass; gl_rules=rls} =
let e,lev,keepassoc = get_constr_entry false typ in
let pos,p4ass,name = find_position false keepassoc ass lev in
(e,typ,pos,name,ass,p4ass,rls)
(* Add a bunch of grammar rules. Does not check if it is well formed *)
let extend_grammar_rules gram =
let univ = get_univ gram.gc_univ in
let tl = List.map (define_entry univ) gram.gc_entries in
List.iter (extend_entry univ) tl
(* Add a grammar rules for tactics *)
type grammar_tactic_production =
| TacTerm of string
| TacNonTerm of loc * (Gram.te Gramext.g_symbol * argument_type) * string option
let make_prod_item = function
| TacTerm s -> (Gramext.Stoken (Extend.terminal s), None)
| TacNonTerm (_,(nont,t), po) ->
(nont, option_app (fun p -> (p,t)) po)
let make_gen_act f pil =
let rec make env = function
| [] ->
Gramext.action (fun loc -> f loc env)
| None :: tl -> (* parse a non-binding item *)
Gramext.action (fun _ -> make env tl)
| Some (p, t) :: tl -> (* non-terminal *)
Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in
make [] (List.rev pil)
let extend_constr entry (n,assoc,pos,p4assoc,name) make_act (forpat,pt) =
let univ = get_univ "constr" in
let pil = List.map (symbol_of_prod_item univ assoc n forpat) pt in
let (symbs,ntl) = List.split pil in
let act = make_act ntl in
grammar_extend entry pos [(name, p4assoc, [symbs, act])]
let extend_constr_notation (n,assoc,ntn,rule,permut) =
let mkact =
match permut with
None -> (fun loc env -> CNotation (loc,ntn,List.map snd env))
| Some p -> (fun loc env ->
CNotation (loc,ntn,List.map (fun i -> snd (List.nth env i)) p)) in
let (e,level,keepassoc) = get_constr_entry false (ETConstr (n,())) in
let pos,p4assoc,name = find_position false keepassoc assoc level in
extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name)
(make_act mkact) (false,rule);
if not !Options.v7 then
let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
let (e,level,keepassoc) = get_constr_entry true (ETConstr (n,())) in
let pos,p4assoc,name = find_position true keepassoc assoc level in
extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name)
(make_act_in_cases_pattern mkact) (true,rule)
(* These grammars are not a removable *)
let make_rule univ f g (s,pt) =
let hd = Gramext.Stoken ("IDENT", s) in
let pil = (hd,None) :: List.map g pt in
let (symbs,ntl) = List.split pil in
let act = make_gen_act f ntl in
(symbs, act)
let tac_exts = ref []
let get_extend_tactic_grammars () = !tac_exts
let extend_tactic_grammar s gl =
tac_exts := (s,gl) :: !tac_exts;
let univ = get_univ "tactic" in
let make_act loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
let rules = List.map (make_rule univ make_act make_prod_item) gl in
Gram.extend Tactic.simple_tactic None [(None, None, List.rev rules)]
let vernac_exts = ref []
let get_extend_vernac_grammars () = !vernac_exts
let extend_vernac_command_grammar s gl =
vernac_exts := (s,gl) :: !vernac_exts;
let univ = get_univ "vernac" in
let make_act loc l = Vernacexpr.VernacExtend (s,List.map snd l) in
let rules = List.map (make_rule univ make_act make_prod_item) gl in
Gram.extend Vernac_.command None [(None, None, List.rev rules)]
let rec interp_entry_name u s =
let l = String.length s in
if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
let t, g = interp_entry_name u (String.sub s 3 (l-8)) in
List1ArgType t, Gramext.Slist1 g
else if l > 5 & String.sub s (l-5) 5 = "_list" then
let t, g = interp_entry_name u (String.sub s 0 (l-5)) in
List0ArgType t, Gramext.Slist0 g
else if l > 4 & String.sub s (l-4) 4 = "_opt" then
let t, g = interp_entry_name u (String.sub s 0 (l-4)) in
OptArgType t, Gramext.Sopt g
else
let e = get_entry (get_univ u) s in
let o = object_of_typed_entry e in
let t = type_of_typed_entry e in
t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)
let qualified_nterm current_univ = function
| NtQual (univ, en) -> (univ, en)
| NtShort en -> (current_univ, en)
let make_vprod_item univ = function
| VTerm s -> (Gramext.Stoken (Extend.terminal s), None)
| VNonTerm (loc, nt, po) ->
let (u,nt) = qualified_nterm univ nt in
let (etyp, e) = interp_entry_name u nt in
e, option_app (fun p -> (p,etyp)) po
let add_tactic_entries gl =
let univ = get_univ "tactic" in
let make_act s tac loc l = Tacexpr.TacAlias (loc,s,l,tac) in
let f (s,l,tac) =
make_rule univ (make_act s tac) (make_vprod_item "tactic") l in
let rules = List.map f gl in
let _ = find_position true true None None (* to synchronise with remove *) in
grammar_extend Tactic.simple_tactic None [(None, None, List.rev rules)]
let extend_grammar gram =
(match gram with
| Notation a -> extend_constr_notation a
| Grammar g -> extend_grammar_rules g
| TacticGrammar l -> add_tactic_entries l);
grammar_state := gram :: !grammar_state
let reset_extend_grammars_v8 () =
let te = List.rev !tac_exts in
let tv = List.rev !vernac_exts in
tac_exts := [];
vernac_exts := [];
List.iter (fun (s,gl) -> extend_tactic_grammar s gl) te;
List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv
(* Summary functions: the state of the lexer is included in that of the parser.
Because the grammar affects the set of keywords when adding or removing
grammar rules. *)
type frozen_t = all_grammar_command list * Lexer.frozen_t
let freeze () = (!grammar_state, Lexer.freeze ())
(* We compare the current state of the grammar and the state to unfreeze,
by computing the longest common suffixes *)
let factorize_grams l1 l2 =
if l1 == l2 then ([], [], l1) else list_share_tails l1 l2
let number_of_entries gcl =
List.fold_left
(fun n -> function
| Notation _ ->
if !Options.v7 then n + 1
else n + 2 (* 1 for operconstr, 1 for pattern *)
| Grammar gc ->
n + (List.length gc.gc_entries)
| TacticGrammar _ -> n + 1)
0 gcl
let unfreeze (grams, lex) =
let (undo, redo, common) = factorize_grams !grammar_state grams in
let n = number_of_entries undo in
remove_grammars n;
remove_levels n;
grammar_state := common;
Lexer.unfreeze lex;
List.iter extend_grammar (List.rev redo)
let init_grammar () =
remove_grammars (number_of_entries !grammar_state);
grammar_state := []
let init () =
init_grammar ()
open Summary
let _ =
declare_summary "GRAMMAR_LEXER"
{ freeze_function = freeze;
unfreeze_function = unfreeze;
init_function = init;
survive_module = false;
survive_section = false }
|