1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: egrammar.ml 11512 2008-10-27 12:28:36Z herbelin $ *)
23
(**************************************************************************)
25
* --- Note on the mapping of grammar productions to camlp4 actions ---
27
* Translation of environments: a production
28
* [ nt1(x1) ... nti(xi) ] -> act(x1..xi)
29
* is written (with camlp4 conventions):
30
* (fun vi -> .... (fun v1 -> act(v1 .. vi) )..)
31
* where v1..vi are the values generated by non-terminals nt1..nti.
32
* Since the actions are executed by substituting an environment,
33
* the make_*_action family build the following closure:
40
* (fun env -> gram_action .. env act)
47
(**********************************************************************)
48
(** Declare Notations grammar rules *)
51
| Term of Token.pattern
52
| NonTerm of constr_production_entry *
53
(Names.identifier * constr_production_entry) option
55
type 'a action_env = 'a list * 'a list list
57
let make_constr_action
58
(f : loc -> constr_expr action_env -> constr_expr) pil =
59
let rec make (env,envlist as fullenv : constr_expr action_env) = function
61
Gramext.action (fun loc -> f loc fullenv)
62
| None :: tl -> (* parse a non-binding item *)
63
Gramext.action (fun _ -> make fullenv tl)
64
| Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *)
65
Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
66
| Some (p, ETReference) :: tl -> (* non-terminal *)
67
Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
68
| Some (p, ETIdent) :: tl -> (* non-terminal *)
69
Gramext.action (fun (v:identifier) ->
70
make (CRef (Ident (dummy_loc,v)) :: env, envlist) tl)
71
| Some (p, ETBigint) :: tl -> (* non-terminal *)
72
Gramext.action (fun (v:Bigint.bigint) ->
73
make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
74
| Some (p, ETConstrList _) :: tl ->
75
Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
76
| Some (p, ETPattern) :: tl ->
77
failwith "Unexpected entry of type cases pattern" in
78
make ([],[]) (List.rev pil)
80
let make_cases_pattern_action
81
(f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
82
let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function
84
Gramext.action (fun loc -> f loc fullenv)
85
| None :: tl -> (* parse a non-binding item *)
86
Gramext.action (fun _ -> make fullenv tl)
87
| Some (p, ETConstr _) :: tl -> (* pattern non-terminal *)
88
Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
89
| Some (p, ETReference) :: tl -> (* non-terminal *)
90
Gramext.action (fun (v:reference) ->
91
make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
92
| Some (p, ETIdent) :: tl -> (* non-terminal *)
93
Gramext.action (fun (v:identifier) ->
95
(CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))::env, envlist) tl)
96
| Some (p, ETBigint) :: tl -> (* non-terminal *)
97
Gramext.action (fun (v:Bigint.bigint) ->
98
make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
99
| Some (p, ETConstrList _) :: tl ->
100
Gramext.action (fun (v:cases_pattern_expr list) ->
101
make (env, v :: envlist) tl)
102
| Some (p, (ETPattern | ETOther _)) :: tl ->
103
failwith "Unexpected entry of type cases pattern or other" in
104
make ([],[]) (List.rev pil)
106
let make_constr_prod_item univ assoc from forpat = function
107
| Term tok -> (Gramext.Stoken tok, None)
108
| NonTerm (nt, ovar) ->
109
let eobj = symbol_of_production assoc from forpat nt in
112
let prepare_empty_levels entry (pos,p4assoc,name,reinit) =
113
grammar_extend entry pos reinit [(name, p4assoc, [])]
115
let pure_sublevels level symbs =
116
map_succeed (function
117
| Gramext.Snterml (_,n) when Some (int_of_string n) <> level ->
122
let extend_constr (entry,level) (n,assoc) mkact forpat pt =
123
let univ = get_univ "constr" in
124
let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in
125
let (symbs,ntl) = List.split pil in
126
let pure_sublevels = pure_sublevels level symbs in
127
let needed_levels = register_empty_levels forpat pure_sublevels in
128
let pos,p4assoc,name,reinit = find_position forpat assoc level in
129
List.iter (prepare_empty_levels entry) needed_levels;
130
grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])]
132
let extend_constr_notation (n,assoc,ntn,rule) =
133
(* Add the notation in constr *)
134
let mkact loc env = CNotation (loc,ntn,env) in
135
let e = get_constr_entry false (ETConstr (n,())) in
136
extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule;
137
(* Add the notation in cases_pattern *)
138
let mkact loc env = CPatNotation (loc,ntn,env) in
139
let e = get_constr_entry true (ETConstr (n,())) in
140
extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
143
(**********************************************************************)
144
(** Making generic actions in type generic_argument *)
146
let make_generic_action
147
(f:loc -> ('b * raw_generic_argument) list -> 'a) pil =
148
let rec make env = function
150
Gramext.action (fun loc -> f loc env)
151
| None :: tl -> (* parse a non-binding item *)
152
Gramext.action (fun _ -> make env tl)
153
| Some (p, t) :: tl -> (* non-terminal *)
154
Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in
155
make [] (List.rev pil)
157
let make_rule univ f g pt =
158
let (symbs,ntl) = List.split (List.map g pt) in
159
let act = make_generic_action f ntl in
162
(**********************************************************************)
163
(** Grammar extensions declared at ML level *)
165
type grammar_tactic_production =
168
loc * (Gram.te Gramext.g_symbol * argument_type) * string option
170
let make_prod_item = function
171
| TacTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
172
| TacNonTerm (_,(nont,t), po) -> (nont, Option.map (fun p -> (p,t)) po)
174
(* Tactic grammar extensions *)
176
let tac_exts = ref []
177
let get_extend_tactic_grammars () = !tac_exts
179
let extend_tactic_grammar s gl =
180
tac_exts := (s,gl) :: !tac_exts;
181
let univ = get_univ "tactic" in
182
let mkact loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
183
let rules = List.map (make_rule univ mkact make_prod_item) gl in
184
Gram.extend Tactic.simple_tactic None [(None, None, List.rev rules)]
186
(* Vernac grammar extensions *)
188
let vernac_exts = ref []
189
let get_extend_vernac_grammars () = !vernac_exts
191
let extend_vernac_command_grammar s gl =
192
vernac_exts := (s,gl) :: !vernac_exts;
193
let univ = get_univ "vernac" in
194
let mkact loc l = VernacExtend (s,List.map snd l) in
195
let rules = List.map (make_rule univ mkact make_prod_item) gl in
196
Gram.extend Vernac_.command None [(None, None, List.rev rules)]
198
(**********************************************************************)
199
(** Grammar declaration for Tactic Notation (Coq level) *)
201
(* Interpretation of the grammar entry names *)
204
let t,n = repr_ident (id_of_string t) in
205
if s <> t or n = None then raise Not_found;
208
let rec interp_entry_name up_level s =
209
let l = String.length s in
210
if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
211
let t, g = interp_entry_name up_level (String.sub s 3 (l-8)) in
212
List1ArgType t, Gramext.Slist1 g
213
else if l > 5 & String.sub s (l-5) 5 = "_list" then
214
let t, g = interp_entry_name up_level (String.sub s 0 (l-5)) in
215
List0ArgType t, Gramext.Slist0 g
216
else if l > 4 & String.sub s (l-4) 4 = "_opt" then
217
let t, g = interp_entry_name up_level (String.sub s 0 (l-4)) in
218
OptArgType t, Gramext.Sopt g
220
let s = if s = "hyp" then "var" else s in
222
let i = find_index "tactic" s in
224
if up_level<>5 && i=up_level then Gramext.Sself else
225
if up_level<>5 && i=up_level-1 then Gramext.Snext else
226
Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i)
229
(* Qualified entries are no longer in use *)
230
try get_entry (get_univ "tactic") s
232
try get_entry (get_univ "prim") s
234
try get_entry (get_univ "constr") s
235
with _ -> error ("Unknown entry "^s^".")
237
let o = object_of_typed_entry e in
238
let t = type_of_typed_entry e in
239
t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)
241
let make_vprod_item n = function
242
| VTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
243
| VNonTerm (loc, nt, po) ->
244
let (etyp, e) = interp_entry_name n nt in
245
e, Option.map (fun p -> (p,etyp)) po
247
let get_tactic_entry n =
249
weaken_entry Tactic.simple_tactic, None
251
weaken_entry Tactic.binder_tactic, None
252
else if 1<=n && n<5 then
253
weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n))
255
error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
257
(* Declaration of the tactic grammar rule *)
259
let head_is_ident = function VTerm _::_ -> true | _ -> false
261
let add_tactic_entry (key,lev,prods,tac) =
262
let univ = get_univ "tactic" in
263
let entry, pos = get_tactic_entry lev in
264
let mkprod = make_vprod_item lev in
266
if lev = 0 then begin
267
if not (head_is_ident prods) then
268
error "Notation for simple tactic must start with an identifier.";
269
let mkact s tac loc l =
270
(TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in
271
make_rule univ (mkact key tac) mkprod prods
274
let mkact s tac loc l =
275
(TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in
276
make_rule univ (mkact key tac) mkprod prods in
277
synchronize_level_positions ();
278
grammar_extend entry pos None [(None, None, List.rev [rules])]
280
(**********************************************************************)
281
(** State of the grammar extensions *)
283
type notation_grammar =
284
int * Gramext.g_assoc option * notation * prod_item list
286
type all_grammar_command =
287
| Notation of Notation.level * notation_grammar
289
(string * int * grammar_production list *
290
(Names.dir_path * Tacexpr.glob_tactic_expr))
292
let (grammar_state : all_grammar_command list ref) = ref []
294
let extend_grammar gram =
296
| Notation (_,a) -> extend_constr_notation a
297
| TacticGrammar g -> add_tactic_entry g);
298
grammar_state := gram :: !grammar_state
300
let reset_extend_grammars_v8 () =
301
let te = List.rev !tac_exts in
302
let tv = List.rev !vernac_exts in
305
List.iter (fun (s,gl) -> print_string ("Resinstalling "^s); flush stdout; extend_tactic_grammar s gl) te;
306
List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv
308
let recover_notation_grammar ntn prec =
309
let l = map_succeed (function
310
| Notation (prec',(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> x
311
| _ -> failwith "") !grammar_state in
312
assert (List.length l = 1);
315
(* Summary functions: the state of the lexer is included in that of the parser.
316
Because the grammar affects the set of keywords when adding or removing
318
type frozen_t = all_grammar_command list * Lexer.frozen_t
320
let freeze () = (!grammar_state, Lexer.freeze ())
322
(* We compare the current state of the grammar and the state to unfreeze,
323
by computing the longest common suffixes *)
324
let factorize_grams l1 l2 =
325
if l1 == l2 then ([], [], l1) else list_share_tails l1 l2
327
let number_of_entries gcl =
330
| Notation _ -> n + 2 (* 1 for operconstr, 1 for pattern *)
331
| TacticGrammar _ -> n + 1)
334
let unfreeze (grams, lex) =
335
let (undo, redo, common) = factorize_grams !grammar_state grams in
336
let n = number_of_entries undo in
339
grammar_state := common;
341
List.iter extend_grammar (List.rev redo)
343
let init_grammar () =
344
remove_grammars (number_of_entries !grammar_state);
353
declare_summary "GRAMMAR_LEXER"
354
{ freeze_function = freeze;
355
unfreeze_function = unfreeze;
356
init_function = init;
357
survive_module = false;
358
survive_section = false }
added
removed
parsing/egrammar.ml
