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 oopen CicNotationEnvoopen CicNotationPt
28 eexception Parse_error of Token.flocation * stringeexception Level_not_found of int
29 llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer
30 llet min_precedence = 0llet max_precedence = 100llet default_precedence = 50
31 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 *)
32 llet interpretation = Grammar.Entry.create grammar "interpretation"(* level2 <-> level 3 *)
33 llet phrase = Grammar.Entry.create grammar "phrase"
34 llet return_term loc term = ()
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)
42 (** {2 Grammar extension} *)
44 llet symbol s = Gramext.Stoken ("SYMBOL", s)llet ident s = Gramext.Stoken ("IDENT", s)llet number s = Gramext.Stoken ("NUMBER", s)llet term = Gramext.Sself
45 llet g_symbol_of_literal =
48 | `Keyword s -> ident s
49 | `Number s -> number s
52 | Binding of string * value_type
53 | Env of (string * value_type) list
54 llet make_action action bindings =
55 let rec aux (vl : env_type) =
57 [] -> Gramext.action (fun (loc : location) -> action vl loc)
58 | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
59 | Binding (name, TermType) :: tl ->
61 (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl)
62 | Binding (name, StringType) :: tl ->
65 aux ((name, (StringType, StringValue v)) :: vl) tl)
66 | Binding (name, NumType) :: tl ->
68 (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
69 | Binding (name, OptType t) :: tl ->
71 (fun (v : 'a option) ->
72 aux ((name, (OptType t, OptValue v)) :: vl) tl)
73 | Binding (name, ListType t) :: tl ->
76 aux ((name, (ListType t, ListValue v)) :: vl) tl)
77 | Env _ :: tl -> Gramext.action (fun (v : env_type) -> aux (v @ vl) tl)
79 aux [] (List.rev bindings)
84 | NoBinding :: tl -> aux acc tl
85 | Env names :: tl -> aux (List.rev names @ acc) tl
86 | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
90 (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
91 let extract_term_production pattern =
94 AttributedTerm (_, t) -> aux t
95 | Literal l -> aux_literal l
96 | Layout l -> aux_layout l
97 | Magic m -> aux_magic m
98 | Variable v -> aux_variable v
99 | t -> prerr_endline (CicNotationPp.pp_term t); assert false
102 `Symbol s -> [NoBinding, symbol s]
103 | `Keyword s -> [NoBinding, ident s]
104 | `Number s -> [NoBinding, number s]
107 Sub (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUB"] @ aux p2
108 | Sup (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUP"] @ aux p2
109 | Below (p1, p2) -> aux p1 @ [NoBinding, symbol "\\BELOW"] @ aux p2
110 | Above (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ABOVE"] @ aux p2
111 | Frac (p1, p2) -> aux p1 @ [NoBinding, symbol "\\FRAC"] @ aux p2
112 | Atop (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ATOP"] @ aux p2
113 | Over (p1, p2) -> aux p1 @ [NoBinding, symbol "\\OVER"] @ aux p2
115 [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"] @
117 | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
119 | Box (_, pl) -> List.flatten (List.map aux pl)
120 and aux_magic magic =
123 let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
124 let action (env_opt : env_type option) (loc : location) =
126 Some env -> List.map opt_binding_some env
127 | None -> List.map opt_binding_of_name p_names
129 [Env (List.map opt_declaration p_names),
131 [[Gramext.Sopt (Gramext.srules [p_atoms, p_action])],
132 Gramext.action action]]
133 | List0 (p, _) | List1 (p, _) ->
134 let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
135 let env0 = List.map list_binding_of_name p_names in
136 let grow_env_entry env n v =
137 prerr_endline "grow_env_entry";
140 n', (ty, ListValue vl) as entry ->
141 if n' = n then n', (ty, ListValue (v :: vl)) else entry
145 let grow_env env_i env =
146 prerr_endline "grow_env";
147 List.fold_left (fun env (n, (_, v)) -> grow_env_entry env n v) env
150 let action (env_list : env_type list) (loc : location) =
151 prerr_endline "list action"; List.fold_right grow_env env_list env0
155 List0 (_, None) -> Gramext.Slist0 s
156 | List1 (_, None) -> Gramext.Slist1 s
157 | List0 (_, Some l) -> Gramext.Slist0sep (s, g_symbol_of_literal l)
158 | List1 (_, Some l) -> Gramext.Slist1sep (s, g_symbol_of_literal l)
161 [Env (List.map list_declaration p_names),
163 [[g_symbol (Gramext.srules [p_atoms, p_action])],
164 Gramext.action action]]
168 NumVar s -> [Binding (s, NumType), number ""]
169 | TermVar s -> [Binding (s, TermType), term]
170 | IdentVar s -> [Binding (s, StringType), ident ""]
171 | Ascription (p, s) -> assert false
172 | FreshVar _ -> assert false
173 and inner_pattern p =
174 let (p_bindings, p_atoms) = List.split (aux p) in
175 let p_names = flatten_opt p_bindings in
178 ("inner names: " ^ String.concat " " (List.map fst p_names))
182 (fun (env : env_type) (loc : location) ->
183 prerr_endline "inner action"; env)
186 p_bindings, p_atoms, p_names, action
190 let level_of_int precedence =
191 if precedence < min_precedence || precedence > max_precedence then
192 raise (Level_not_found precedence);
193 string_of_int precedence
195 type rule_id = Token.t Gramext.g_symbol list
197 let extend level1_pattern ?(precedence = default_precedence) =
198 fun ?associativity action ->
199 let (p_bindings, p_atoms) =
200 List.split (extract_term_production level1_pattern)
202 let level = level_of_int precedence in
203 let p_names = flatten_opt p_bindings in
205 prerr_endline (string_of_int (List.length p_bindings));
207 [Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e),
208 Some (Gramext.Level level),
209 [None, associativity,
212 (fun (env : env_type) (loc : location) -> action env loc)
217 let delete atoms = Grammar.delete_rule l2_pattern atoms
224 | l -> Layout (Box (H, l))
226 let fold_binder binder pt_names body =
227 let fold_cluster binder terms ty body =
228 List.fold_right (fun term body -> Binder (binder, (term, ty), body)) terms
231 List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body)
234 let return_term loc term = AttributedTerm (`Loc loc, term)
237 let mk_level_list first last =
240 i when i < first -> acc
241 | i -> aux ((Some (string_of_int i), None, []) :: acc) (i - 1)
246 [Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e), None,
247 mk_level_list min_precedence max_precedence]
251 (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e)
252 and _ = (level2_pattern : 'level2_pattern Grammar.Entry.e)
253 and _ = (level3_term : 'level3_term Grammar.Entry.e)
254 and _ = (l2_pattern : 'l2_pattern Grammar.Entry.e)
255 and _ = (notation : 'notation Grammar.Entry.e)
256 and _ = (interpretation : 'interpretation Grammar.Entry.e)
257 and _ = (phrase : 'phrase Grammar.Entry.e) in
258 let grammar_entry_create s =
259 Grammar.Entry.create (Grammar.of_entry level1_pattern) s
261 let l1_pattern : 'l1_pattern Grammar.Entry.e =
262 grammar_entry_create "l1_pattern"
263 and literal : 'literal Grammar.Entry.e = grammar_entry_create "literal"
264 and sep : 'sep Grammar.Entry.e = grammar_entry_create "sep"
265 and l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e =
266 grammar_entry_create "l1_magic_pattern"
267 and l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e =
268 grammar_entry_create "l1_pattern_variable"
269 and l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e =
270 grammar_entry_create "l1_simple_pattern"
271 and sort : 'sort Grammar.Entry.e = grammar_entry_create "sort"
272 and explicit_subst : 'explicit_subst Grammar.Entry.e =
273 grammar_entry_create "explicit_subst"
274 and meta_subst : 'meta_subst Grammar.Entry.e =
275 grammar_entry_create "meta_subst"
276 and meta_substs : 'meta_substs Grammar.Entry.e =
277 grammar_entry_create "meta_substs"
278 and possibly_typed_name : 'possibly_typed_name Grammar.Entry.e =
279 grammar_entry_create "possibly_typed_name"
280 and match_pattern : 'match_pattern Grammar.Entry.e =
281 grammar_entry_create "match_pattern"
282 and binder : 'binder Grammar.Entry.e = grammar_entry_create "binder"
283 and bound_name : 'bound_name Grammar.Entry.e =
284 grammar_entry_create "bound_name"
285 and bound_names : 'bound_names Grammar.Entry.e =
286 grammar_entry_create "bound_names"
287 and induction_kind : 'induction_kind Grammar.Entry.e =
288 grammar_entry_create "induction_kind"
289 and let_defs : 'let_defs Grammar.Entry.e =
290 grammar_entry_create "let_defs"
291 and l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e =
292 grammar_entry_create "l2_pattern_variable"
293 and l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e =
294 grammar_entry_create "l2_magic_pattern"
295 and argument : 'argument Grammar.Entry.e =
296 grammar_entry_create "argument"
297 and associativity : 'associativity Grammar.Entry.e =
298 grammar_entry_create "associativity"
299 and precedence : 'precedence Grammar.Entry.e =
300 grammar_entry_create "precedence"
302 [Grammar.Entry.obj (level1_pattern : 'level1_pattern Grammar.Entry.e),
307 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))],
309 (fun (p : 'l1_simple_pattern)
310 (loc : Lexing.position * Lexing.position) ->
311 (p : 'level1_pattern))]];
312 Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
317 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)))],
319 (fun (p : 'l1_simple_pattern list)
320 (loc : Lexing.position * Lexing.position) ->
321 (p : 'l1_pattern))]];
322 Grammar.Entry.obj (literal : 'literal Grammar.Entry.e), None,
324 [[Gramext.Stoken ("NUMBER", "")],
326 (fun (n : string) (loc : Lexing.position * Lexing.position) ->
327 (`Number n : 'literal));
328 [Gramext.Stoken ("KEYWORD", "")],
330 (fun (k : string) (loc : Lexing.position * Lexing.position) ->
331 (`Keyword k : 'literal));
332 [Gramext.Stoken ("SYMBOL", "")],
334 (fun (s : string) (loc : Lexing.position * Lexing.position) ->
335 (`Symbol s : 'literal))]];
336 Grammar.Entry.obj (sep : 'sep Grammar.Entry.e), None,
338 [[Gramext.Stoken ("SYMBOL", "\\SEP");
340 (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
342 (fun (sep : 'literal) _ (loc : Lexing.position * Lexing.position) ->
345 (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e),
348 [[Gramext.Stoken ("SYMBOL", "\\OPT");
351 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))],
353 (fun (p : 'l1_simple_pattern) _
354 (loc : Lexing.position * Lexing.position) ->
355 (Opt p : 'l1_magic_pattern));
356 [Gramext.Stoken ("SYMBOL", "\\LIST1");
359 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
361 (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
363 (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
364 (loc : Lexing.position * Lexing.position) ->
365 (List1 (p, sep) : 'l1_magic_pattern));
366 [Gramext.Stoken ("SYMBOL", "\\LIST0");
369 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
371 (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
373 (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
374 (loc : Lexing.position * Lexing.position) ->
375 (List0 (p, sep) : 'l1_magic_pattern))]];
377 (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e),
380 [[Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")],
382 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
383 (IdentVar id : 'l1_pattern_variable));
384 [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")],
386 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
387 (NumVar id : 'l1_pattern_variable));
388 [Gramext.Stoken ("SYMBOL", "\\TERM"); Gramext.Stoken ("IDENT", "")],
390 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
391 (TermVar id : 'l1_pattern_variable))]];
393 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e),
395 [Some "layout", Some Gramext.LeftA,
396 [[Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\AS");
397 Gramext.Stoken ("IDENT", "")],
399 (fun (id : string) _ (p : 'l1_simple_pattern)
400 (loc : Lexing.position * Lexing.position) ->
401 (return_term loc (Variable (Ascription (p, id))) :
402 'l1_simple_pattern));
403 [Gramext.Stoken ("DELIM", "\\[");
405 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
406 Gramext.Stoken ("DELIM", "\\]")],
408 (fun _ (p : 'l1_pattern) _
409 (loc : Lexing.position * Lexing.position) ->
410 (return_term loc (boxify p) : 'l1_simple_pattern));
411 [Gramext.Stoken ("SYMBOL", "\\BREAK")],
413 (fun _ (loc : Lexing.position * Lexing.position) ->
414 (return_term loc (Layout Break) : 'l1_simple_pattern));
415 [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("DELIM", "\\[");
417 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
418 Gramext.Stoken ("DELIM", "\\]")],
420 (fun _ (p : 'l1_pattern) _ _
421 (loc : Lexing.position * Lexing.position) ->
422 (return_term loc (Layout (Box (V, p))) : 'l1_simple_pattern));
423 [Gramext.Stoken ("SYMBOL", "\\HBOX"); Gramext.Stoken ("DELIM", "\\[");
425 (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
426 Gramext.Stoken ("DELIM", "\\]")],
428 (fun _ (p : 'l1_pattern) _ _
429 (loc : Lexing.position * Lexing.position) ->
430 (return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern));
431 [Gramext.Stoken ("SYMBOL", "\\ROOT"); Gramext.Sself;
432 Gramext.Stoken ("SYMBOL", "\\OF"); Gramext.Sself],
434 (fun (arg : 'l1_simple_pattern) _ (index : 'l1_simple_pattern) _
435 (loc : Lexing.position * Lexing.position) ->
436 (return_term loc (Layout (Root (arg, index))) :
437 'l1_simple_pattern));
438 [Gramext.Stoken ("SYMBOL", "\\SQRT"); Gramext.Sself],
440 (fun (p : 'l1_simple_pattern) _
441 (loc : Lexing.position * Lexing.position) ->
442 (return_term loc (Layout (Sqrt p)) : 'l1_simple_pattern));
443 [Gramext.Stoken ("SYMBOL", "\\FRAC"); Gramext.Sself; Gramext.Sself],
445 (fun (p2 : 'l1_simple_pattern) (p1 : 'l1_simple_pattern) _
446 (loc : Lexing.position * Lexing.position) ->
447 (return_term loc (Layout (Frac (p1, p2))) : 'l1_simple_pattern));
448 [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ATOP"); Gramext.Sself],
450 (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
451 (loc : Lexing.position * Lexing.position) ->
452 (return_term loc (Layout (Atop (p1, p2))) : 'l1_simple_pattern));
453 [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\OVER"); Gramext.Sself],
455 (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
456 (loc : Lexing.position * Lexing.position) ->
457 (return_term loc (Layout (Over (p1, p2))) : 'l1_simple_pattern));
458 [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself],
460 (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
461 (loc : Lexing.position * Lexing.position) ->
462 (return_term loc (Layout (Above (p1, p2))) :
463 'l1_simple_pattern));
464 [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\BELOW"); Gramext.Sself],
466 (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
467 (loc : Lexing.position * Lexing.position) ->
468 (return_term loc (Layout (Below (p1, p2))) :
469 'l1_simple_pattern));
470 [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUP"); Gramext.Sself],
472 (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
473 (loc : Lexing.position * Lexing.position) ->
474 (return_term loc (Layout (Sup (p1, p2))) : 'l1_simple_pattern));
475 [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUB"); Gramext.Sself],
477 (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
478 (loc : Lexing.position * Lexing.position) ->
479 (return_term loc (Layout (Sub (p1, p2))) : 'l1_simple_pattern))];
480 Some "simple", Some Gramext.NonA,
482 (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
484 (fun (l : 'literal) (loc : Lexing.position * Lexing.position) ->
485 (return_term loc (Literal l) : 'l1_simple_pattern));
488 (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e))],
490 (fun (v : 'l1_pattern_variable)
491 (loc : Lexing.position * Lexing.position) ->
492 (return_term loc (Variable v) : 'l1_simple_pattern));
495 (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e))],
497 (fun (m : 'l1_magic_pattern)
498 (loc : Lexing.position * Lexing.position) ->
499 (return_term loc (Magic m) : 'l1_simple_pattern));
500 [Gramext.Stoken ("IDENT", "")],
502 (fun (i : string) (loc : Lexing.position * Lexing.position) ->
503 (return_term loc (Ident (i, None)) : 'l1_simple_pattern))]];
504 Grammar.Entry.obj (level2_pattern : 'level2_pattern Grammar.Entry.e),
508 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
510 (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) ->
511 (p : 'level2_pattern))]];
512 Grammar.Entry.obj (sort : 'sort Grammar.Entry.e), None,
514 [[Gramext.Stoken ("SYMBOL", "\\TYPE")],
516 (fun _ (loc : Lexing.position * Lexing.position) ->
518 [Gramext.Stoken ("SYMBOL", "\\SET")],
520 (fun _ (loc : Lexing.position * Lexing.position) -> (`Set : 'sort));
521 [Gramext.Stoken ("SYMBOL", "\\PROP")],
523 (fun _ (loc : Lexing.position * Lexing.position) ->
525 Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e),
528 [[Gramext.Stoken ("SYMBOL", "\\subst"); Gramext.Stoken ("SYMBOL", "[");
531 [[Gramext.Stoken ("IDENT", "");
532 Gramext.Stoken ("SYMBOL", "≔");
535 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
537 (fun (t : 'l2_pattern) _ (i : string)
538 (loc : Lexing.position * Lexing.position) ->
540 Gramext.Stoken ("SYMBOL", ";"));
541 Gramext.Stoken ("SYMBOL", "]")],
543 (fun _ (substs : 'e__1 list) _ _
544 (loc : Lexing.position * Lexing.position) ->
545 (substs : 'explicit_subst))]];
546 Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None,
549 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
551 (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) ->
552 (Some p : 'meta_subst));
553 [Gramext.Stoken ("SYMBOL", "_")],
555 (fun (s : string) (loc : Lexing.position * Lexing.position) ->
556 (None : 'meta_subst))]];
557 Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e), None,
559 [[Gramext.Stoken ("SYMBOL", "[");
562 (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e)));
563 Gramext.Stoken ("SYMBOL", "]")],
565 (fun _ (substs : 'meta_subst list) _
566 (loc : Lexing.position * Lexing.position) ->
567 (substs : 'meta_substs))]];
569 (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e),
573 (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e))],
575 (fun (id : 'bound_name) (loc : Lexing.position * Lexing.position) ->
576 (id, None : 'possibly_typed_name));
577 [Gramext.Stoken ("SYMBOL", "(");
579 (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e));
580 Gramext.Stoken ("SYMBOL", ":");
582 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
583 Gramext.Stoken ("SYMBOL", ")")],
585 (fun _ (typ : 'l2_pattern) _ (id : 'bound_name) _
586 (loc : Lexing.position * Lexing.position) ->
587 (id, Some typ : 'possibly_typed_name))]];
588 Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e),
591 [[Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
595 (possibly_typed_name :
596 'possibly_typed_name Grammar.Entry.e)));
597 Gramext.Stoken ("SYMBOL", ")")],
599 (fun _ (vars : 'possibly_typed_name list) (id : string) _
600 (loc : Lexing.position * Lexing.position) ->
601 (id, vars : 'match_pattern));
602 [Gramext.Stoken ("IDENT", "")],
604 (fun (id : string) (loc : Lexing.position * Lexing.position) ->
605 (id, [] : 'match_pattern))]];
606 Grammar.Entry.obj (binder : 'binder Grammar.Entry.e), None,
608 [[Gramext.Stoken ("SYMBOL", "λ")],
610 (fun _ (loc : Lexing.position * Lexing.position) ->
611 (`Lambda : 'binder));
612 [Gramext.Stoken ("SYMBOL", "∀")],
614 (fun _ (loc : Lexing.position * Lexing.position) ->
615 (`Forall : 'binder));
616 [Gramext.Stoken ("SYMBOL", "∃")],
618 (fun _ (loc : Lexing.position * Lexing.position) ->
619 (`Exists : 'binder));
620 [Gramext.Stoken ("SYMBOL", "Π")],
622 (fun _ (loc : Lexing.position * Lexing.position) ->
624 Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e), None,
626 [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")],
628 (fun (i : string) _ (loc : Lexing.position * Lexing.position) ->
629 (Variable (FreshVar i) : 'bound_name));
630 [Gramext.Stoken ("IDENT", "")],
632 (fun (i : string) (loc : Lexing.position * Lexing.position) ->
633 (Ident (i, None) : 'bound_name))]];
634 Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e), None,
638 [[Gramext.Stoken ("SYMBOL", "(");
642 (bound_name : 'bound_name Grammar.Entry.e)),
643 Gramext.Stoken ("SYMBOL", ","));
646 [[Gramext.Stoken ("SYMBOL", ":");
649 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
651 (fun (p : 'l2_pattern) _
652 (loc : Lexing.position * Lexing.position) ->
654 Gramext.Stoken ("SYMBOL", ")")],
656 (fun _ (ty : 'e__3 option) (vars : 'bound_name list) _
657 (loc : Lexing.position * Lexing.position) ->
658 (vars, ty : 'e__4))])],
660 (fun (clusters : 'e__4 list)
661 (loc : Lexing.position * Lexing.position) ->
662 (clusters : 'bound_names));
665 (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e)),
666 Gramext.Stoken ("SYMBOL", ","));
669 [[Gramext.Stoken ("SYMBOL", ":");
672 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
674 (fun (p : 'l2_pattern) _
675 (loc : Lexing.position * Lexing.position) ->
678 (fun (ty : 'e__2 option) (vars : 'bound_name list)
679 (loc : Lexing.position * Lexing.position) ->
680 ([vars, ty] : 'bound_names))]];
681 Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e),
684 [[Gramext.Stoken ("IDENT", "corec")],
686 (fun _ (loc : Lexing.position * Lexing.position) ->
687 (`CoInductive : 'induction_kind));
688 [Gramext.Stoken ("IDENT", "rec")],
690 (fun _ (loc : Lexing.position * Lexing.position) ->
691 (`Inductive : 'induction_kind))]];
692 Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e), None,
698 (bound_name : 'bound_name Grammar.Entry.e));
701 (bound_names : 'bound_names Grammar.Entry.e));
704 [[Gramext.Stoken ("IDENT", "on");
707 (bound_name : 'bound_name Grammar.Entry.e))],
709 (fun (id : 'bound_name) _
710 (loc : Lexing.position * Lexing.position) ->
714 [[Gramext.Stoken ("SYMBOL", ":");
717 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
719 (fun (p : 'l2_pattern) _
720 (loc : Lexing.position * Lexing.position) ->
722 Gramext.Stoken ("SYMBOL", "≝");
725 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
727 (fun (body : 'l2_pattern) _ (ty : 'e__6 option)
728 (index_name : 'e__5 option) (args : 'bound_names)
730 (loc : Lexing.position * Lexing.position) ->
731 (let body = fold_binder `Lambda args body in
735 | Some ty -> Some (fold_binder `Pi args ty)
737 let rec position_of name p =
740 | n :: _ when n = name -> Some p, p
741 | _ :: tl -> position_of name (p + 1) tl
743 let rec find_arg name n =
747 (sprintf "Argument %s not found"
748 (CicNotationPp.pp_term name))
750 match position_of name 0 l with
751 None, len -> find_arg name (n + len) tl
752 | Some where, len -> n + where
755 match index_name with
757 | Some name -> find_arg name 0 args
759 (name, ty), body, index :
761 Gramext.Stoken ("IDENT", "and"))],
763 (fun (defs : 'e__7 list)
764 (loc : Lexing.position * Lexing.position) ->
765 (defs : 'let_defs))]];
767 (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e),
770 [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")],
772 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
773 (FreshVar id : 'l2_pattern_variable));
774 [Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")],
776 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
777 (IdentVar id : 'l2_pattern_variable));
778 [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")],
780 (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
781 (NumVar id : 'l2_pattern_variable))]];
783 (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e),
786 [[Gramext.Stoken ("SYMBOL", "\\DEFAULT");
787 Gramext.Stoken ("DELIM", "\\[");
789 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
790 Gramext.Stoken ("DELIM", "\\]"); Gramext.Stoken ("DELIM", "\\[");
792 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
793 Gramext.Stoken ("DELIM", "\\]")],
795 (fun _ (none : 'l2_pattern) _ _ (some : 'l2_pattern) _ _
796 (loc : Lexing.position * Lexing.position) ->
797 (Default (some, none) : 'l2_magic_pattern));
798 [Gramext.Stoken ("SYMBOL", "\\FOLD");
800 [[Gramext.Stoken ("IDENT", "right")],
802 (fun _ (loc : Lexing.position * Lexing.position) ->
804 [Gramext.Stoken ("IDENT", "left")],
806 (fun _ (loc : Lexing.position * Lexing.position) ->
808 Gramext.Stoken ("DELIM", "\\[");
810 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
811 Gramext.Stoken ("DELIM", "\\]");
812 Gramext.Stoken ("SYMBOL", "\\LAMBDA"); Gramext.Stoken ("IDENT", "");
813 Gramext.Stoken ("DELIM", "\\[");
815 (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
816 Gramext.Stoken ("DELIM", "\\]")],
818 (fun _ (recursive : 'l2_pattern) _ (id : string) _ _
819 (base : 'l2_pattern) _ (kind : 'e__8) _
820 (loc : Lexing.position * Lexing.position) ->
821 (Fold (kind, base, [id], recursive) : 'l2_magic_pattern))]];
822 Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
823 Some (Gramext.Level "10"),
824 [Some "10", Some Gramext.NonA,
825 [[Gramext.Stoken ("IDENT", "let");
828 (induction_kind : 'induction_kind Grammar.Entry.e));
830 (Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e));
831 Gramext.Stoken ("IDENT", "in"); Gramext.Sself],
833 (fun (body : 'l2_pattern) _ (defs : 'let_defs) (k : 'induction_kind)
834 _ (loc : Lexing.position * Lexing.position) ->
835 (return_term loc (LetRec (k, defs, body)) : 'l2_pattern));
836 [Gramext.Stoken ("IDENT", "let");
839 (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e));
840 Gramext.Stoken ("SYMBOL", "≝"); Gramext.Sself;
841 Gramext.Stoken ("", "in"); Gramext.Sself],
843 (fun (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _
844 (var : 'possibly_typed_name) _
845 (loc : Lexing.position * Lexing.position) ->
846 (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))]];
847 Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
848 Some (Gramext.Level "20"),
849 [Some "20", Some Gramext.RightA,
851 (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
853 (Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e));
854 Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
856 (fun (body : 'l2_pattern) _ (names : 'bound_names) (b : 'binder)
857 (loc : Lexing.position * Lexing.position) ->
858 (return_term loc (fold_binder b names body) : 'l2_pattern))]];
859 Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
860 Some (Gramext.Level "70"),
861 [Some "70", Some Gramext.LeftA,
862 [[Gramext.Sself; Gramext.Sself],
864 (fun (p2 : 'l2_pattern) (p1 : 'l2_pattern)
865 (loc : Lexing.position * Lexing.position) ->
868 Appl (hd :: tl) | AttributedTerm (_, Appl (hd :: tl)) ->
872 return_term loc (Appl (aux p1 @ [p2])) :
874 Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
875 Some (Gramext.Level "90"),
876 [Some "90", Some Gramext.NonA,
879 (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e))],
881 (fun (m : 'l2_magic_pattern)
882 (loc : Lexing.position * Lexing.position) ->
883 (return_term loc (Magic m) : 'l2_pattern));
886 (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e))],
888 (fun (v : 'l2_pattern_variable)
889 (loc : Lexing.position * Lexing.position) ->
890 (return_term loc (Variable v) : 'l2_pattern));
891 [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself;
892 Gramext.Stoken ("SYMBOL", ")")],
894 (fun _ (p : 'l2_pattern) _
895 (loc : Lexing.position * Lexing.position) ->
897 [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself;
898 Gramext.Stoken ("SYMBOL", ":"); Gramext.Sself;
899 Gramext.Stoken ("SYMBOL", ")")],
901 (fun _ (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _
902 (loc : Lexing.position * Lexing.position) ->
903 (return_term loc (Appl [Symbol ("cast", 0); p1; p2]) :
907 [[Gramext.Stoken ("SYMBOL", "[");
910 (l2_pattern : 'l2_pattern Grammar.Entry.e));
911 Gramext.Stoken ("SYMBOL", "]")],
913 (fun _ (ty : 'l2_pattern) _
914 (loc : Lexing.position * Lexing.position) ->
916 Gramext.Stoken ("IDENT", "match"); Gramext.Sself;
919 [[Gramext.Stoken ("SYMBOL", ":"); Gramext.Stoken ("IDENT", "")],
922 (loc : Lexing.position * Lexing.position) ->
924 Gramext.Stoken ("IDENT", "with"); Gramext.Stoken ("SYMBOL", "[");
929 (match_pattern : 'match_pattern Grammar.Entry.e));
930 Gramext.Stoken ("SYMBOL", "⇒");
933 (l2_pattern : 'l2_pattern Grammar.Entry.e))],
935 (fun (rhs : 'l2_pattern) _ (lhs : 'match_pattern)
936 (loc : Lexing.position * Lexing.position) ->
937 (lhs, rhs : 'e__11))],
938 Gramext.Stoken ("SYMBOL", "|"));
939 Gramext.Stoken ("SYMBOL", "]")],
941 (fun _ (patterns : 'e__11 list) _ _ (indty_ident : 'e__10 option)
942 (t : 'l2_pattern) _ (outtyp : 'e__9 option)
943 (loc : Lexing.position * Lexing.position) ->
944 (return_term loc (Case (t, indty_ident, outtyp, patterns)) :
946 [Gramext.Snterm (Grammar.Entry.obj (sort : 'sort Grammar.Entry.e))],
948 (fun (s : 'sort) (loc : Lexing.position * Lexing.position) ->
949 (return_term loc (Sort s) : 'l2_pattern));
950 [Gramext.Stoken ("META", "");
952 (Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e))],
954 (fun (s : 'meta_substs) (m : string)
955 (loc : Lexing.position * Lexing.position) ->
956 (return_term loc (Meta (int_of_string m, s)) : 'l2_pattern));
957 [Gramext.Stoken ("META", "")],
959 (fun (m : string) (loc : Lexing.position * Lexing.position) ->
960 (return_term loc (Meta (int_of_string m, [])) : 'l2_pattern));
961 [Gramext.Stoken ("IMPLICIT", "")],
963 (fun _ (loc : Lexing.position * Lexing.position) ->
964 (return_term loc Implicit : 'l2_pattern));
965 [Gramext.Stoken ("NUMBER", "")],
967 (fun (n : string) (loc : Lexing.position * Lexing.position) ->
968 (return_term loc (Num (n, 0)) : 'l2_pattern));
969 [Gramext.Stoken ("URI", "")],
971 (fun (u : string) (loc : Lexing.position * Lexing.position) ->
972 (return_term loc (Uri (u, None)) : 'l2_pattern));
973 [Gramext.Stoken ("IDENT", "");
976 (explicit_subst : 'explicit_subst Grammar.Entry.e))],
978 (fun (s : 'explicit_subst) (id : string)
979 (loc : Lexing.position * Lexing.position) ->
980 (return_term loc (Ident (id, Some s)) : 'l2_pattern));
981 [Gramext.Stoken ("IDENT", "")],
983 (fun (id : string) (loc : Lexing.position * Lexing.position) ->
984 (return_term loc (Ident (id, None)) : 'l2_pattern))]];
985 Grammar.Entry.obj (argument : 'argument Grammar.Entry.e), None,
987 [[Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("IDENT", "");
988 Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
990 (fun (a : 'argument) _ (id : string) _
991 (loc : Lexing.position * Lexing.position) ->
992 (EtaArg (Some id, a) : 'argument));
993 [Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("SYMBOL", ".");
996 (fun (a : 'argument) _ _
997 (loc : Lexing.position * Lexing.position) ->
998 (EtaArg (None, a) : 'argument));
999 [Gramext.Stoken ("IDENT", "")],
1001 (fun (id : string) (loc : Lexing.position * Lexing.position) ->
1002 (IdentArg id : 'argument))]];
1003 Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e), None,
1005 [[Gramext.Stoken ("SYMBOL", "("); Gramext.Slist1 Gramext.Sself;
1006 Gramext.Stoken ("SYMBOL", ")")],
1008 (fun _ (terms : 'level3_term list) _
1009 (loc : Lexing.position * Lexing.position) ->
1013 | terms -> ApplPattern terms :
1016 (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e))],
1018 (fun (a : 'argument) (loc : Lexing.position * Lexing.position) ->
1019 (ArgPattern a : 'level3_term));
1020 [Gramext.Stoken ("URI", "")],
1022 (fun (u : string) (loc : Lexing.position * Lexing.position) ->
1023 (UriPattern u : 'level3_term))]];
1024 Grammar.Entry.obj (associativity : 'associativity Grammar.Entry.e),
1027 [[Gramext.Stoken ("IDENT", "non");
1028 Gramext.Stoken ("IDENT", "associative")],
1030 (fun _ _ (loc : Lexing.position * Lexing.position) ->
1031 (Gramext.NonA : 'associativity));
1032 [Gramext.Stoken ("IDENT", "right");
1033 Gramext.Stoken ("IDENT", "associative")],
1035 (fun _ _ (loc : Lexing.position * Lexing.position) ->
1036 (Gramext.RightA : 'associativity));
1037 [Gramext.Stoken ("IDENT", "left");
1038 Gramext.Stoken ("IDENT", "associative")],
1040 (fun _ _ (loc : Lexing.position * Lexing.position) ->
1041 (Gramext.LeftA : 'associativity))]];
1042 Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None,
1044 [[Gramext.Stoken ("IDENT", "with");
1045 Gramext.Stoken ("IDENT", "precedence");
1046 Gramext.Stoken ("NUMBER", "")],
1048 (fun (n : string) _ _ (loc : Lexing.position * Lexing.position) ->
1049 (int_of_string n : 'precedence))]];
1050 Grammar.Entry.obj (notation : 'notation Grammar.Entry.e), None,
1052 [[Gramext.Stoken ("IDENT", "notation");
1055 (level1_pattern : 'level1_pattern Grammar.Entry.e));
1059 (associativity : 'associativity Grammar.Entry.e)));
1062 (Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e)));
1063 Gramext.Stoken ("IDENT", "for");
1066 (level2_pattern : 'level2_pattern Grammar.Entry.e))],
1068 (fun (p2 : 'level2_pattern) _ (prec : 'precedence option)
1069 (assoc : 'associativity option) (p1 : 'level1_pattern) _
1070 (loc : Lexing.position * Lexing.position) ->
1071 (p1, assoc, prec, p2 : 'notation))]];
1072 Grammar.Entry.obj (interpretation : 'interpretation Grammar.Entry.e),
1075 [[Gramext.Stoken ("IDENT", "interpretation");
1076 Gramext.Stoken ("SYMBOL", "");
1079 (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e)));
1080 Gramext.Stoken ("IDENT", "as");
1082 (Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e))],
1084 (fun (t : 'level3_term) _ (args : 'argument list) (s : string) _
1085 (loc : Lexing.position * Lexing.position) ->
1086 (() : 'interpretation))]];
1087 Grammar.Entry.obj (phrase : 'phrase Grammar.Entry.e), None,
1090 (Grammar.Entry.obj (notation : 'notation Grammar.Entry.e));
1091 Gramext.Stoken ("SYMBOL", ".")],
1093 (fun _ (l1, assoc, prec, l2 : 'notation)
1094 (loc : Lexing.position * Lexing.position) ->
1095 (Notation (l1, assoc, prec, l2) : 'phrase));
1096 [Gramext.Stoken ("IDENT", "print");
1099 (level2_pattern : 'level2_pattern Grammar.Entry.e));
1100 Gramext.Stoken ("SYMBOL", ".")],
1102 (fun _ (p2 : 'level2_pattern) _
1103 (loc : Lexing.position * Lexing.position) ->
1104 (Print p2 : 'phrase))]]])
1106 (** {2 API implementation} *)
1108 let exc_located_wrapper f =
1110 Stdpp.Exc_located (floc, Stream.Error msg) ->
1111 raise (Parse_error (floc, msg))
1112 | Stdpp.Exc_located (floc, exn) ->
1113 raise (Parse_error (floc, Printexc.to_string exn))
1115 let parse_syntax_pattern stream =
1116 exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
1117 let parse_ast_pattern stream =
1118 exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream)
1119 let parse_interpretation stream =
1120 exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream)
1121 let parse_phrase stream =
1122 exc_located_wrapper (fun () -> Grammar.Entry.parse phrase stream)
1124 (** {2 Debugging} *)
1126 let print_l2_pattern () =
1127 Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern);
1128 Format.pp_print_flush Format.std_formatter ();
1131 (* vim:set encoding=utf8 foldmethod=marker: *)