1 (* *)(* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
27 eexception Parse_error of Token.flocation * stringeexception Level_not_found of int
28 llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer
29 llet level1_pattern = Grammar.Entry.create grammar "level1_pattern"llet level2_pattern = Grammar.Entry.create grammar "level2_pattern"llet level3_term = Grammar.Entry.create grammar "level3_term"llet l2_pattern = Grammar.Entry.create grammar "l2_pattern"llet notation = Grammar.Entry.create grammar "notation"(* level1 <-> level 2 *)
30 llet interpretation = Grammar.Entry.create grammar "interpretation"(* level2 <-> level 3 *)
32 llet return_term loc term = ()
33 llet loc_of_floc ({Lexing.pos_cnum = loc_begin}, {Lexing.pos_cnum = loc_end}) =
36 let (x, y) = loc_of_floc floc in
37 failwith (sprintf "Error at characters %d - %d: %s" x y msg)
38 llet int_of_string s =
39 try Pervasives.int_of_string s with
41 failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
46 | l -> Layout (Box (H, l))
47 llet fold_binder binder pt_names body =
48 let fold_cluster binder names ty body =
50 (fun name body -> Binder (binder, (Cic.Name name, ty), body)) names body
52 List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body)
54 llet return_term loc term = AttributedTerm (`Loc loc, term)
57 (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e)
58 and _ = (level2_pattern : 'level2_pattern Grammar.Entry.e)
59 and _ = (level3_term : 'level3_term Grammar.Entry.e)
60 and _ = (l2_pattern : 'l2_pattern Grammar.Entry.e)
61 and _ = (notation : 'notation Grammar.Entry.e)
62 and _ = (interpretation : 'interpretation Grammar.Entry.e) in
63 let grammar_entry_create s =
64 Grammar.Entry.create (Grammar.of_entry level1_pattern) s
66 let l1_pattern : 'l1_pattern Grammar.Entry.e =
67 grammar_entry_create "l1_pattern"
68 and literal : 'literal Grammar.Entry.e = grammar_entry_create "literal"
69 and sep : 'sep Grammar.Entry.e = grammar_entry_create "sep"
70 and l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e =
71 grammar_entry_create "l1_magic_pattern"
72 and l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e =
73 grammar_entry_create "l1_pattern_variable"
74 and l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e =
75 grammar_entry_create "l1_simple_pattern"
76 and sort : 'sort Grammar.Entry.e = grammar_entry_create "sort"
77 and explicit_subst : 'explicit_subst Grammar.Entry.e =
78 grammar_entry_create "explicit_subst"
79 and meta_subst : 'meta_subst Grammar.Entry.e =
80 grammar_entry_create "meta_subst"
81 and possibly_typed_name : 'possibly_typed_name Grammar.Entry.e =
82 grammar_entry_create "possibly_typed_name"
83 and match_pattern : 'match_pattern Grammar.Entry.e =
84 grammar_entry_create "match_pattern"
85 and binder : 'binder Grammar.Entry.e = grammar_entry_create "binder"
86 and bound_names : 'bound_names Grammar.Entry.e =
87 grammar_entry_create "bound_names"
88 and induction_kind : 'induction_kind Grammar.Entry.e =
89 grammar_entry_create "induction_kind"
90 and let_defs : 'let_defs Grammar.Entry.e =
91 grammar_entry_create "let_defs"
92 and l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e =
93 grammar_entry_create "l2_pattern_variable"
94 and l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e =
95 grammar_entry_create "l2_magic_pattern"
96 and argument : 'argument Grammar.Entry.e =
97 grammar_entry_create "argument"
98 and associativity : 'associativity Grammar.Entry.e =
99 grammar_entry_create "associativity"
100 and precedence : 'precedence Grammar.Entry.e =
101 grammar_entry_create "precedence"
103 [Grammar.Entry.obj (level1_pattern : 'level1_pattern Grammar.Entry.e),
107 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
108 Gramext.Stoken ("EOI", "")],
110 (fun _ (p : 'l1_pattern)
111 (loc : Lexing.position * Lexing.position) ->
112 (boxify p : 'level1_pattern))]];
113 Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
118 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)))],
120 (fun (p : 'l1_simple_pattern list)
121 (loc : Lexing.position * Lexing.position) ->
122 (p : 'l1_pattern))]];
123 Grammar.Entry.obj (literal : 'literal Grammar.Entry.e), None,
125 [[Gramext.Stoken ("NUMBER", "")],
127 (fun (n : string) (loc : Lexing.position * Lexing.position) ->
128 (`Number n : 'literal));
129 [Gramext.Stoken ("KEYWORD", "")],
131 (fun (k : string) (loc : Lexing.position * Lexing.position) ->
132 (`Keyword k : 'literal));
133 [Gramext.Stoken ("SYMBOL", "")],
135 (fun (s : string) (loc : Lexing.position * Lexing.position) ->
136 (`Symbol s : 'literal))]];
137 Grammar.Entry.obj (sep : 'sep Grammar.Entry.e), None,
139 [[Gramext.Stoken ("SYMBOL", "\\SEP");
141 (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
143 (fun (sep : 'literal) _ (loc : Lexing.position * Lexing.position) ->
146 (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e),
149 [[Gramext.Stoken ("SYMBOL", "\\OPT");
152 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))],
154 (fun (p : 'l1_simple_pattern) _
155 (loc : Lexing.position * Lexing.position) ->
156 (Opt p : 'l1_magic_pattern));
157 [Gramext.Stoken ("SYMBOL", "\\LIST1");
160 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
162 (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
164 (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
165 (loc : Lexing.position * Lexing.position) ->
166 (List1 (p, sep) : 'l1_magic_pattern));
167 [Gramext.Stoken ("SYMBOL", "\\LIST0");
170 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
172 (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
174 (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
175 (loc : Lexing.position * Lexing.position) ->
176 (List0 (p, sep) : 'l1_magic_pattern))]];
178 (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e),
181 [[Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")],
183 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
184 (IdentVar id : 'l1_pattern_variable));
185 [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")],
187 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
188 (NumVar id : 'l1_pattern_variable));
189 [Gramext.Stoken ("SYMBOL", "\\TERM"); Gramext.Stoken ("IDENT", "")],
191 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
192 (TermVar id : 'l1_pattern_variable));
193 [Gramext.Stoken ("IDENT", "")],
195 (fun (id : string) (loc : Lexing.position * Lexing.position) ->
196 (TermVar id : 'l1_pattern_variable))]];
198 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e),
200 [Some "layout", Some Gramext.LeftA,
201 [[Gramext.Stoken ("SYMBOL", "[");
203 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
204 Gramext.Stoken ("SYMBOL", "\\AS"); Gramext.Stoken ("IDENT", "");
205 Gramext.Stoken ("SYMBOL", "]")],
207 (fun _ (id : string) _ (p : 'l1_pattern) _
208 (loc : Lexing.position * Lexing.position) ->
210 (Variable (Ascription (Layout (Box (H, p)), id))) :
211 'l1_simple_pattern));
212 [Gramext.Stoken ("SYMBOL", "[");
214 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
215 Gramext.Stoken ("SYMBOL", "]")],
217 (fun _ (p : 'l1_pattern) _
218 (loc : Lexing.position * Lexing.position) ->
219 (return_term loc (boxify p) : 'l1_simple_pattern));
220 [Gramext.Stoken ("SYMBOL", "\\BREAK")],
222 (fun _ (loc : Lexing.position * Lexing.position) ->
223 (return_term loc (Layout Break) : 'l1_simple_pattern));
224 [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("SYMBOL", "[");
226 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
227 Gramext.Stoken ("SYMBOL", "]")],
229 (fun _ (p : 'l1_pattern) _ _
230 (loc : Lexing.position * Lexing.position) ->
231 (return_term loc (Layout (Box (V, p))) : 'l1_simple_pattern));
232 [Gramext.Stoken ("SYMBOL", "\\HBOX"); Gramext.Stoken ("SYMBOL", "[");
234 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
235 Gramext.Stoken ("SYMBOL", "]")],
237 (fun _ (p : 'l1_pattern) _ _
238 (loc : Lexing.position * Lexing.position) ->
239 (return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern));
240 [Gramext.Stoken ("SYMBOL", "\\ROOT");
242 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
243 Gramext.Stoken ("SYMBOL", "\\OF"); Gramext.Sself],
245 (fun (arg : 'l1_simple_pattern) _ (index : 'l1_pattern) _
246 (loc : Lexing.position * Lexing.position) ->
247 (return_term loc (Layout (Root (arg, Layout (Box (H, index))))) :
248 'l1_simple_pattern));
249 [Gramext.Stoken ("SYMBOL", "\\SQRT"); Gramext.Sself],
251 (fun (p : 'l1_simple_pattern) _
252 (loc : Lexing.position * Lexing.position) ->
253 (return_term loc (Layout (Sqrt p)) : 'l1_simple_pattern));
254 [Gramext.Stoken ("SYMBOL", "\\FRAC"); Gramext.Sself; Gramext.Sself],
256 (fun (p2 : 'l1_simple_pattern) (p1 : 'l1_simple_pattern) _
257 (loc : Lexing.position * Lexing.position) ->
258 (return_term loc (Layout (Frac (p1, p2))) : 'l1_simple_pattern));
259 [Gramext.Stoken ("SYMBOL", "[");
261 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
262 Gramext.Stoken ("SYMBOL", "\\ATOP");
264 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
265 Gramext.Stoken ("SYMBOL", "]")],
267 (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
268 (loc : Lexing.position * Lexing.position) ->
269 (return_term loc (Layout (Atop (boxify p1, boxify p2))) :
270 'l1_simple_pattern));
271 [Gramext.Stoken ("SYMBOL", "[");
273 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
274 Gramext.Stoken ("SYMBOL", "\\OVER");
276 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
277 Gramext.Stoken ("SYMBOL", "]")],
279 (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
280 (loc : Lexing.position * Lexing.position) ->
281 (return_term loc (Layout (Over (boxify p1, boxify p2))) :
282 'l1_simple_pattern));
283 [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself],
285 (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
286 (loc : Lexing.position * Lexing.position) ->
287 (return_term loc (Layout (Above (p1, p2))) :
288 'l1_simple_pattern));
289 [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\BELOW"); Gramext.Sself],
291 (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
292 (loc : Lexing.position * Lexing.position) ->
293 (return_term loc (Layout (Below (p1, p2))) :
294 'l1_simple_pattern));
295 [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUP"); Gramext.Sself],
297 (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
298 (loc : Lexing.position * Lexing.position) ->
299 (return_term loc (Layout (Sup (p1, p2))) : 'l1_simple_pattern));
300 [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUB"); Gramext.Sself],
302 (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
303 (loc : Lexing.position * Lexing.position) ->
304 (return_term loc (Layout (Sub (p1, p2))) : 'l1_simple_pattern))];
305 Some "simple", Some Gramext.NonA,
307 (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
309 (fun (l : 'literal) (loc : Lexing.position * Lexing.position) ->
310 (return_term loc (Literal l) : 'l1_simple_pattern));
313 (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e))],
315 (fun (v : 'l1_pattern_variable)
316 (loc : Lexing.position * Lexing.position) ->
317 (return_term loc (Variable v) : 'l1_simple_pattern));
320 (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e))],
322 (fun (m : 'l1_magic_pattern)
323 (loc : Lexing.position * Lexing.position) ->
324 (return_term loc (Magic m) : 'l1_simple_pattern))]];
325 Grammar.Entry.obj (level2_pattern : 'level2_pattern Grammar.Entry.e),
329 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
331 (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) ->
332 (p : 'level2_pattern))]];
333 Grammar.Entry.obj (sort : 'sort Grammar.Entry.e), None,
335 [[Gramext.Stoken ("SYMBOL", "\\TYPE")],
337 (fun _ (loc : Lexing.position * Lexing.position) ->
339 [Gramext.Stoken ("SYMBOL", "\\SET")],
341 (fun _ (loc : Lexing.position * Lexing.position) -> (`Set : 'sort));
342 [Gramext.Stoken ("SYMBOL", "\\PROP")],
344 (fun _ (loc : Lexing.position * Lexing.position) ->
346 Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e),
347 None, [None, None, []];
348 Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None,
351 (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e),
354 [[Gramext.Stoken ("IDENT", "")],
356 (fun (id : string) (loc : Lexing.position * Lexing.position) ->
357 (Cic.Name id, None : 'possibly_typed_name));
358 [Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
359 Gramext.Stoken ("SYMBOL", ":");
361 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
362 Gramext.Stoken ("SYMBOL", ")")],
364 (fun _ (typ : 'l2_pattern) _ (id : string) _
365 (loc : Lexing.position * Lexing.position) ->
366 (Cic.Name id, Some typ : 'possibly_typed_name))]];
367 Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e),
370 [[Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
374 (possibly_typed_name :
375 'possibly_typed_name Grammar.Entry.e)));
376 Gramext.Stoken ("SYMBOL", ")")],
378 (fun _ (vars : 'possibly_typed_name list) (id : string) _
379 (loc : Lexing.position * Lexing.position) ->
380 (id, vars : 'match_pattern));
381 [Gramext.Stoken ("IDENT", "")],
383 (fun (id : string) (loc : Lexing.position * Lexing.position) ->
384 (id, [] : 'match_pattern))]];
385 Grammar.Entry.obj (binder : 'binder Grammar.Entry.e), None,
387 [[Gramext.Stoken ("SYMBOL", "λ")],
389 (fun _ (loc : Lexing.position * Lexing.position) ->
390 (`Lambda : 'binder));
391 [Gramext.Stoken ("SYMBOL", "∀")],
393 (fun _ (loc : Lexing.position * Lexing.position) ->
394 (`Forall : 'binder));
395 [Gramext.Stoken ("SYMBOL", "∃")],
397 (fun _ (loc : Lexing.position * Lexing.position) ->
398 (`Exists : 'binder));
399 [Gramext.Stoken ("SYMBOL", "Π")],
401 (fun _ (loc : Lexing.position * Lexing.position) ->
403 Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e), None,
407 [[Gramext.Stoken ("SYMBOL", "(");
409 (Gramext.Stoken ("IDENT", ""),
410 Gramext.Stoken ("SYMBOL", ","));
413 [[Gramext.Stoken ("SYMBOL", ":");
416 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
418 (fun (p : 'l2_pattern) _
419 (loc : Lexing.position * Lexing.position) ->
421 Gramext.Stoken ("SYMBOL", ")")],
423 (fun _ (ty : 'e__2 option) (vars : string list) _
424 (loc : Lexing.position * Lexing.position) ->
425 (vars, ty : 'e__3))])],
427 (fun (clusters : 'e__3 list)
428 (loc : Lexing.position * Lexing.position) ->
429 (clusters : 'bound_names));
431 (Gramext.Stoken ("IDENT", ""), Gramext.Stoken ("SYMBOL", ","));
434 [[Gramext.Stoken ("SYMBOL", ":");
437 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
439 (fun (p : 'l2_pattern) _
440 (loc : Lexing.position * Lexing.position) ->
443 (fun (ty : 'e__1 option) (vars : string list)
444 (loc : Lexing.position * Lexing.position) ->
445 ([vars, ty] : 'bound_names))]];
446 Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e),
449 [[Gramext.Stoken ("IDENT", "corec")],
451 (fun _ (loc : Lexing.position * Lexing.position) ->
452 (`CoInductive : 'induction_kind));
453 [Gramext.Stoken ("IDENT", "rec")],
455 (fun _ (loc : Lexing.position * Lexing.position) ->
456 (`Inductive : 'induction_kind))]];
457 Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e), None,
461 [[Gramext.Stoken ("IDENT", "");
464 (bound_names : 'bound_names Grammar.Entry.e));
467 [[Gramext.Stoken ("IDENT", "on");
468 Gramext.Stoken ("IDENT", "")],
471 (loc : Lexing.position * Lexing.position) ->
475 [[Gramext.Stoken ("SYMBOL", ":");
478 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
480 (fun (p : 'l2_pattern) _
481 (loc : Lexing.position * Lexing.position) ->
483 Gramext.Stoken ("SYMBOL", "≝");
486 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
488 (fun (body : 'l2_pattern) _ (ty : 'e__5 option)
489 (index_name : 'e__4 option) (args : 'bound_names)
491 (loc : Lexing.position * Lexing.position) ->
492 (let body = fold_binder `Lambda args body in
496 | Some ty -> Some (fold_binder `Pi args ty)
498 let rec position_of name p =
501 | n :: _ when n = name -> Some p, p
502 | _ :: tl -> position_of name (p + 1) tl
504 let rec find_arg name n =
506 [] -> fail loc (sprintf "Argument %s not found" name)
508 match position_of name 0 l with
509 None, len -> find_arg name (n + len) tl
510 | Some where, len -> n + where
513 match index_name with
515 | Some name -> find_arg name 0 args
517 (Cic.Name name, ty), body, index :
519 Gramext.Stoken ("IDENT", "and"))],
521 (fun (defs : 'e__6 list)
522 (loc : Lexing.position * Lexing.position) ->
523 (defs : 'let_defs))]];
525 (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e),
528 [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")],
530 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
531 (FreshVar id : 'l2_pattern_variable));
532 [Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")],
534 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
535 (IdentVar id : 'l2_pattern_variable));
536 [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")],
538 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
539 (NumVar id : 'l2_pattern_variable))]];
541 (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e),
544 [[Gramext.Stoken ("SYMBOL", "\\DEFAULT");
546 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
548 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
550 (fun (none : 'l2_pattern) (some : 'l2_pattern) _
551 (loc : Lexing.position * Lexing.position) ->
552 (Default (some, none) : 'l2_magic_pattern));
553 [Gramext.Stoken ("SYMBOL", "\\FOLD");
555 [[Gramext.Stoken ("IDENT", "right")],
557 (fun _ (loc : Lexing.position * Lexing.position) ->
559 [Gramext.Stoken ("IDENT", "left")],
561 (fun _ (loc : Lexing.position * Lexing.position) ->
564 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
565 Gramext.Stoken ("SYMBOL", "\\LAMBDA"); Gramext.Stoken ("IDENT", "");
567 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
569 (fun (recursive : 'l2_pattern) (id : string) _ (base : 'l2_pattern)
570 (kind : 'e__7) _ (loc : Lexing.position * Lexing.position) ->
571 (Fold (kind, base, [id], recursive) : 'l2_magic_pattern))]];
572 Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), None,
574 Some "10", Some Gramext.NonA,
575 [[Gramext.Stoken ("IDENT", "let");
578 (induction_kind : 'induction_kind Grammar.Entry.e));
580 (Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e));
581 Gramext.Stoken ("IDENT", "in"); Gramext.Sself],
583 (fun (body : 'l2_pattern) _ (defs : 'let_defs) (k : 'induction_kind)
584 _ (loc : Lexing.position * Lexing.position) ->
585 (return_term loc (LetRec (k, defs, body)) : 'l2_pattern));
586 [Gramext.Stoken ("IDENT", "let");
589 (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e));
590 Gramext.Stoken ("SYMBOL", "≝"); Gramext.Sself;
591 Gramext.Stoken ("", "in"); Gramext.Sself],
593 (fun (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _
594 (var : 'possibly_typed_name) _
595 (loc : Lexing.position * Lexing.position) ->
596 (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))];
597 Some "20", Some Gramext.RightA,
599 (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
601 (Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e));
602 Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
604 (fun (body : 'l2_pattern) _ (names : 'bound_names) (b : 'binder)
605 (loc : Lexing.position * Lexing.position) ->
606 (return_term loc (fold_binder b names body) : 'l2_pattern))];
607 Some "30", None, []; Some "40", None, []; Some "50", None, [];
609 Some "70", Some Gramext.LeftA,
610 [[Gramext.Sself; Gramext.Sself],
612 (fun (p2 : 'l2_pattern) (p1 : 'l2_pattern)
613 (loc : Lexing.position * Lexing.position) ->
616 Appl (hd :: tl) | AttributedTerm (_, Appl (hd :: tl)) ->
620 return_term loc (Appl (aux p1 @ [p2])) :
623 Some "90", Some Gramext.NonA,
626 (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e))],
628 (fun (m : 'l2_magic_pattern)
629 (loc : Lexing.position * Lexing.position) ->
630 (return_term loc (Magic m) : 'l2_pattern));
633 (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e))],
635 (fun (v : 'l2_pattern_variable)
636 (loc : Lexing.position * Lexing.position) ->
637 (return_term loc (Variable v) : 'l2_pattern));
638 [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself;
639 Gramext.Stoken ("SYMBOL", ")")],
641 (fun _ (p : 'l2_pattern) _
642 (loc : Lexing.position * Lexing.position) ->
644 [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself;
645 Gramext.Stoken ("SYMBOL", ":"); Gramext.Sself;
646 Gramext.Stoken ("SYMBOL", ")")],
648 (fun _ (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _
649 (loc : Lexing.position * Lexing.position) ->
650 (return_term loc (Appl [Symbol ("cast", 0); p1; p2]) :
654 [[Gramext.Stoken ("SYMBOL", "[");
657 (l2_pattern : 'l2_pattern Grammar.Entry.e));
658 Gramext.Stoken ("SYMBOL", "]")],
660 (fun _ (ty : 'l2_pattern) _
661 (loc : Lexing.position * Lexing.position) ->
663 Gramext.Stoken ("IDENT", "match"); Gramext.Sself;
666 [[Gramext.Stoken ("SYMBOL", ":"); Gramext.Stoken ("IDENT", "")],
669 (loc : Lexing.position * Lexing.position) ->
671 Gramext.Stoken ("IDENT", "with"); Gramext.Stoken ("SYMBOL", "[");
676 (match_pattern : 'match_pattern Grammar.Entry.e));
677 Gramext.Stoken ("SYMBOL", "⇒");
680 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
682 (fun (rhs : 'l2_pattern) _ (lhs : 'match_pattern)
683 (loc : Lexing.position * Lexing.position) ->
684 (lhs, rhs : 'e__10))],
685 Gramext.Stoken ("SYMBOL", "|"));
686 Gramext.Stoken ("SYMBOL", "]")],
688 (fun _ (patterns : 'e__10 list) _ _ (indty_ident : 'e__9 option)
689 (t : 'l2_pattern) _ (outtyp : 'e__8 option)
690 (loc : Lexing.position * Lexing.position) ->
691 (return_term loc (Case (t, indty_ident, outtyp, patterns)) :
693 [Gramext.Stoken ("SYMBOL", "")],
695 (fun (s : string) (loc : Lexing.position * Lexing.position) ->
696 (return_term loc (Symbol (s, 0)) : 'l2_pattern));
697 [Gramext.Snterm (Grammar.Entry.obj (sort : 'sort Grammar.Entry.e))],
699 (fun (s : 'sort) (loc : Lexing.position * Lexing.position) ->
700 (return_term loc (Sort s) : 'l2_pattern));
701 [Gramext.Stoken ("META", "");
703 (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e))],
705 (fun (s : 'meta_subst) (m : string)
706 (loc : Lexing.position * Lexing.position) ->
707 (return_term loc (Meta (int_of_string m, s)) : 'l2_pattern));
708 [Gramext.Stoken ("META", "")],
710 (fun (m : string) (loc : Lexing.position * Lexing.position) ->
711 (return_term loc (Meta (int_of_string m, [])) : 'l2_pattern));
712 [Gramext.Stoken ("IMPLICIT", "")],
714 (fun _ (loc : Lexing.position * Lexing.position) ->
715 (return_term loc Implicit : 'l2_pattern));
716 [Gramext.Stoken ("NUMBER", "")],
718 (fun (n : string) (loc : Lexing.position * Lexing.position) ->
719 (prerr_endline "number"; return_term loc (Num (n, 0)) :
721 [Gramext.Stoken ("URI", "")],
723 (fun (u : string) (loc : Lexing.position * Lexing.position) ->
724 (return_term loc (Uri (u, None)) : 'l2_pattern));
725 [Gramext.Stoken ("IDENT", "");
728 (explicit_subst : 'explicit_subst Grammar.Entry.e))],
730 (fun (s : 'explicit_subst) (id : string)
731 (loc : Lexing.position * Lexing.position) ->
732 (return_term loc (Ident (id, Some s)) : 'l2_pattern));
733 [Gramext.Stoken ("IDENT", "")],
735 (fun (id : string) (loc : Lexing.position * Lexing.position) ->
736 (return_term loc (Ident (id, None)) : 'l2_pattern))];
737 Some "100", None, []];
738 Grammar.Entry.obj (argument : 'argument Grammar.Entry.e), None,
740 [[Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("IDENT", "");
741 Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
743 (fun (a : 'argument) _ (id : string) _
744 (loc : Lexing.position * Lexing.position) ->
745 (EtaArg (Some id, a) : 'argument));
746 [Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("SYMBOL", ".");
749 (fun (a : 'argument) _ _
750 (loc : Lexing.position * Lexing.position) ->
751 (EtaArg (None, a) : 'argument));
752 [Gramext.Stoken ("IDENT", "")],
754 (fun (id : string) (loc : Lexing.position * Lexing.position) ->
755 (IdentArg id : 'argument))]];
756 Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e), None,
758 [[Gramext.Stoken ("SYMBOL", "("); Gramext.Slist1 Gramext.Sself;
759 Gramext.Stoken ("SYMBOL", ")")],
761 (fun _ (terms : 'level3_term list) _
762 (loc : Lexing.position * Lexing.position) ->
766 | terms -> ApplPattern terms :
769 (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e))],
771 (fun (a : 'argument) (loc : Lexing.position * Lexing.position) ->
772 (ArgPattern a : 'level3_term));
773 [Gramext.Stoken ("URI", "")],
775 (fun (u : string) (loc : Lexing.position * Lexing.position) ->
776 (UriPattern u : 'level3_term))]];
777 Grammar.Entry.obj (associativity : 'associativity Grammar.Entry.e),
780 [[Gramext.Stoken ("IDENT", "right");
781 Gramext.Stoken ("IDENT", "associative")],
783 (fun _ _ (loc : Lexing.position * Lexing.position) ->
784 (`Right : 'associativity));
785 [Gramext.Stoken ("IDENT", "left");
786 Gramext.Stoken ("IDENT", "associative")],
788 (fun _ _ (loc : Lexing.position * Lexing.position) ->
789 (`Left : 'associativity))]];
790 Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None,
792 [[Gramext.Stoken ("IDENT", "at");
793 Gramext.Stoken ("IDENT", "precedence");
794 Gramext.Stoken ("NUMBER", "")],
796 (fun (n : string) _ _ (loc : Lexing.position * Lexing.position) ->
797 (n : 'precedence))]];
798 Grammar.Entry.obj (notation : 'notation Grammar.Entry.e), None,
800 [[Gramext.Stoken ("IDENT", "notation");
803 (level1_pattern : 'level1_pattern Grammar.Entry.e));
804 Gramext.Stoken ("IDENT", "for");
807 (level2_pattern : 'level2_pattern Grammar.Entry.e));
811 (associativity : 'associativity Grammar.Entry.e)));
815 (precedence : 'precedence Grammar.Entry.e)))],
817 (fun (prec : 'precedence option) (assoc : 'associativity option)
818 (p2 : 'level2_pattern) _ (p1 : 'level1_pattern) _
819 (loc : Lexing.position * Lexing.position) ->
821 Grammar.Entry.obj (interpretation : 'interpretation Grammar.Entry.e),
824 [[Gramext.Stoken ("IDENT", "interpretation");
825 Gramext.Stoken ("SYMBOL", "");
828 (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e)));
829 Gramext.Stoken ("IDENT", "as");
831 (Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e))],
833 (fun (t : 'level3_term) _ (args : 'argument list) (s : string) _
834 (loc : Lexing.position * Lexing.position) ->
835 (() : 'interpretation))]]])
837 let exc_located_wrapper f =
839 Stdpp.Exc_located (floc, Stream.Error msg) ->
840 raise (Parse_error (floc, msg))
841 | Stdpp.Exc_located (floc, exn) ->
842 raise (Parse_error (floc, Printexc.to_string exn))
844 let parse_syntax_pattern stream =
845 exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
847 let parse_ast_pattern stream =
848 exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream)
850 let parse_interpretation stream =
851 exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream)
853 (** {2 Grammar extension} *)
855 type associativity_kind = [ `Left | `Right | `None ]
857 let symbol s = Gramext.Stoken ("SYMBOL", s)
858 let ident s = Gramext.Stoken ("IDENT", s)
859 let number s = Gramext.Stoken ("NUMBER", s)
860 let term = Gramext.Sself
862 type env_type = (string * (value_type * value)) list
864 let make_action action =
865 let rec aux (vl : env_type) =
869 prerr_endline "make_action";
870 Gramext.action (fun (loc : location) -> action vl loc)
871 | None :: tl -> Gramext.action (fun _ -> aux vl tl)
872 | Some (name, TermType) :: tl ->
874 (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl)
875 | Some (name, StringType) :: tl ->
878 aux ((name, (StringType, StringValue v)) :: vl) tl)
879 | Some (name, NumType) :: tl ->
881 (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
882 | Some (name, OptType t) :: tl ->
884 (fun (v : 'a option) ->
885 aux ((name, (OptType t, OptValue v)) :: vl) tl)
886 | Some (name, ListType t) :: tl ->
888 (fun (v : 'a list) ->
889 aux ((name, (ListType t, ListValue v)) :: vl) tl)
897 | None :: tl -> aux acc tl
898 | Some hd :: tl -> aux (hd :: acc) tl
902 (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
903 let extract_term_production pattern =
906 Literal l -> aux_literal l
907 | Layout l -> aux_layout l
908 | Magic m -> aux_magic m
909 | Variable v -> aux_variable v
913 `Symbol s -> [None, symbol s]
914 | `Keyword s -> [None, ident s]
915 | `Number s -> [None, number s]
918 Sub (p1, p2) -> aux p1 @ [None, symbol "\\SUB"] @ aux p2
919 | Sup (p1, p2) -> aux p1 @ [None, symbol "\\SUP"] @ aux p2
920 | Below (p1, p2) -> aux p1 @ [None, symbol "\\BELOW"] @ aux p2
921 | Above (p1, p2) -> aux p1 @ [None, symbol "\\ABOVE"] @ aux p2
922 | Frac (p1, p2) -> aux p1 @ [None, symbol "\\FRAC"] @ aux p2
923 | Atop (p1, p2) -> aux p1 @ [None, symbol "\\ATOP"] @ aux p2
924 | Over (p1, p2) -> aux p1 @ [None, symbol "\\OVER"] @ aux p2
926 [None, symbol "\\ROOT"] @ aux p2 @ [None, symbol "\\OF"] @ aux p1
927 | Sqrt p -> [None, symbol "\\SQRT"] @ aux p
929 | Box (_, pl) -> List.flatten (List.map aux pl)
933 let (p_bindings, p_atoms) = List.split (aux p) in
934 let p_names = flatten_opt p_bindings in
940 make_action (fun (env : env_type) (loc : location) -> env)
943 (fun (env_opt : env_type option) (loc : location) ->
947 (fun (name, (typ, v)) ->
948 name, (OptType typ, OptValue (Some v)))
952 (fun (name, typ) -> name, (OptType typ, OptValue None))
957 NumVar s -> [Some (s, NumType), number ""]
958 | TermVar s -> [Some (s, TermType), term]
959 | IdentVar s -> [Some (s, StringType), ident ""]
960 | Ascription (p, s) -> assert false
961 | FreshVar _ -> assert false
965 let level_of_int precedence =
966 if precedence mod 10 <> 0 || precedence < 0 || precedence > 100 then
967 raise (Level_not_found precedence);
968 string_of_int precedence
970 type rule_id = Token.t Gramext.g_symbol list
972 let extend level1_pattern ?(precedence = 0) =
973 fun ?associativity action ->
974 let (p_bindings, p_atoms) =
975 List.split (extract_term_production level1_pattern)
977 let level = level_of_int precedence in
978 let p_names = flatten_opt p_bindings in
979 let entry = Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e) in
981 prerr_endline (string_of_int (List.length p_bindings));
983 [entry, Some (Gramext.Level level),
984 [Some level, associativity,
987 (fun (env : env_type) (loc : location) -> action env loc)
992 let delete atoms = Grammar.delete_rule l2_pattern atoms
994 let print_l2_pattern () =
995 Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern);
996 Format.pp_print_flush Format.std_formatter ();
999 (* vim:set encoding=utf8 foldmethod=marker: *)