]> matita.cs.unibo.it Git - helm.git/blob - cic_notation/cicNotationParser.expanded.ml
made executable again
[helm.git] / cic_notation / cicNotationParser.expanded.ml
1 (* *)(* Copyright (C) 2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 oopen Printf
27 mmodule Ast = CicNotationPtmmodule Env = CicNotationEnv
28 eexception Parse_error of Token.flocation * stringeexception Level_not_found of int
29 llet level1_pattern_grammar =
30   Grammar.gcreate CicNotationLexer.level1_pattern_lexerllet level2_ast_grammar = Grammar.gcreate CicNotationLexer.level2_ast_lexerllet level2_meta_grammar = Grammar.gcreate CicNotationLexer.level2_meta_lexer
31 llet min_precedence = 0llet max_precedence = 100
32 llet level1_pattern =
33   Grammar.Entry.create level1_pattern_grammar "level1_pattern"llet level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast"llet term = Grammar.Entry.create level2_ast_grammar "term"llet let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"llet level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
34 llet return_term loc term = ()
35 llet int_of_string s =
36   try Pervasives.int_of_string s with
37     Failure _ ->
38       failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
39 (** {2 Grammar extension} *)
40
41 llet gram_symbol s = Gramext.Stoken ("SYMBOL", s)llet gram_ident s = Gramext.Stoken ("IDENT", s)llet gram_number s = Gramext.Stoken ("NUMBER", s)llet gram_keyword s = Gramext.Stoken ("", s)llet gram_term = Gramext.Sself
42 llet gram_of_literal =
43   function
44     `Symbol s -> gram_symbol s
45   | `Keyword s -> gram_keyword s
46   | `Number s -> gram_number s
47 ttype binding =
48     NoBinding
49   | Binding of string * Env.value_type
50   | Env of (string * Env.value_type) list
51 llet make_action action bindings =
52   let rec aux (vl : CicNotationEnv.t) =
53     function
54       [] -> Gramext.action (fun (loc : Ast.location) -> action vl loc)
55     | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
56     | Binding (name, Env.TermType) :: tl ->
57         Gramext.action
58           (fun (v : Ast.term) ->
59              aux ((name, (Env.TermType, Env.TermValue v)) :: vl) tl)
60     | Binding (name, Env.StringType) :: tl ->
61         Gramext.action
62           (fun (v : string) ->
63              aux ((name, (Env.StringType, Env.StringValue v)) :: vl) tl)
64     | Binding (name, Env.NumType) :: tl ->
65         Gramext.action
66           (fun (v : string) ->
67              aux ((name, (Env.NumType, Env.NumValue v)) :: vl) tl)
68     | Binding (name, Env.OptType t) :: tl ->
69         Gramext.action
70           (fun (v : 'a option) ->
71              aux ((name, (Env.OptType t, Env.OptValue v)) :: vl) tl)
72     | Binding (name, Env.ListType t) :: tl ->
73         Gramext.action
74           (fun (v : 'a list) ->
75              aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
76     | Env _ :: tl ->
77         Gramext.action (fun (v : CicNotationEnv.t) -> aux (v @ vl) tl)
78   in
79   aux [] (List.rev bindings)
80 llet flatten_opt =
81   let rec aux acc =
82     function
83       [] -> List.rev acc
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
87   in
88   aux []
89   (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
90 llet extract_term_production pattern =
91   let rec aux =
92     function
93       Ast.AttributedTerm (_, t) -> aux t
94     | Ast.Literal l -> aux_literal l
95     | Ast.Layout l -> aux_layout l
96     | Ast.Magic m -> aux_magic m
97     | Ast.Variable v -> aux_variable v
98     | t -> prerr_endline (CicNotationPp.pp_term t); assert false
99   and aux_literal =
100     function
101       `Symbol s -> [NoBinding, gram_symbol s]
102     | `Keyword s -> [NoBinding, gram_keyword s]
103     | `Number s -> [NoBinding, gram_number s]
104   and aux_layout =
105     function
106       Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
107     | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
108     | Ast.Below (p1, p2) ->
109         aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
110     | Ast.Above (p1, p2) ->
111         aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
112     | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
113     | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
114     | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
115     | Ast.Root (p1, p2) ->
116         [NoBinding, gram_symbol "\\root"] @ aux p2 @
117           [NoBinding, gram_symbol "\\of"] @ aux p1
118     | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
119     | Ast.Break -> []
120     | Ast.Box (_, pl) -> List.flatten (List.map aux pl)
121     | Ast.Group pl -> List.flatten (List.map aux pl)
122   and aux_magic magic =
123     match magic with
124       Ast.Opt p ->
125         let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
126         let action (env_opt : CicNotationEnv.t option) (loc : Ast.location) =
127           match env_opt with
128             Some env -> List.map Env.opt_binding_some env
129           | None -> List.map Env.opt_binding_of_name p_names
130         in
131         [Env (List.map Env.opt_declaration p_names),
132          Gramext.srules
133            [[Gramext.Sopt (Gramext.srules [p_atoms, p_action])],
134             Gramext.action action]]
135     | Ast.List0 (p, _) | Ast.List1 (p, _) ->
136         let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
137         let action (env_list : CicNotationEnv.t list) (loc : Ast.location) =
138           CicNotationEnv.coalesce_env p_names env_list
139         in
140         let gram_of_list s =
141           match magic with
142             Ast.List0 (_, None) -> Gramext.Slist0 s
143           | Ast.List1 (_, None) -> Gramext.Slist1 s
144           | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
145           | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
146           | _ -> assert false
147         in
148         [Env (List.map Env.list_declaration p_names),
149          Gramext.srules
150            [[gram_of_list (Gramext.srules [p_atoms, p_action])],
151             Gramext.action action]]
152     | _ -> assert false
153   and aux_variable =
154     function
155       Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
156     | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
157     | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
158     | Ast.Ascription (p, s) -> assert false
159     | Ast.FreshVar _ -> assert false
160   and inner_pattern p =
161     let (p_bindings, p_atoms) = List.split (aux p) in
162     let p_names = flatten_opt p_bindings in
163     let action =
164       make_action (fun (env : CicNotationEnv.t) (loc : Ast.location) -> env)
165         p_bindings
166     in
167     p_bindings, p_atoms, p_names, action
168   in
169   aux pattern
170
171 let level_of precedence associativity =
172   if precedence < min_precedence || precedence > max_precedence then
173     raise (Level_not_found precedence);
174   let assoc_string =
175     match associativity with
176       Gramext.NonA -> "N"
177     | Gramext.LeftA -> "L"
178     | Gramext.RightA -> "R"
179   in
180   string_of_int precedence ^ assoc_string
181
182 type rule_id = Token.t Gramext.g_symbol list
183
184   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
185 let owned_keywords = Hashtbl.create 23
186
187 let extend level1_pattern ~precedence ~associativity action =
188   let (p_bindings, p_atoms) =
189     List.split (extract_term_production level1_pattern)
190   in
191   let level = level_of precedence associativity in
192   let p_names = flatten_opt p_bindings in
193   let _ =
194     Grammar.extend
195       [Grammar.Entry.obj (term : 'a Grammar.Entry.e),
196        Some (Gramext.Level level),
197        [None, Some associativity,
198         [p_atoms,
199          make_action
200            (fun (env : CicNotationEnv.t) (loc : Ast.location) ->
201               action env loc)
202            p_bindings]]]
203   in
204   let keywords = CicNotationUtil.keywords_of_term level1_pattern in
205   let rule_id = p_atoms in
206   List.iter CicNotationLexer.add_level2_ast_keyword keywords;
207   Hashtbl.add owned_keywords rule_id keywords;
208   rule_id
209
210 let delete rule_id =
211   let atoms = rule_id in
212   begin try
213     let keywords = Hashtbl.find owned_keywords rule_id in
214     List.iter CicNotationLexer.remove_level2_ast_keyword keywords
215   with
216     Not_found -> assert false
217   end;
218   Grammar.delete_rule term atoms
219
220 (** {2 Grammar} *)
221
222 let parse_level1_pattern_ref = ref (fun _ -> assert false)
223 let parse_level2_ast_ref = ref (fun _ -> assert false)
224 let parse_level2_meta_ref = ref (fun _ -> assert false)
225
226 let fold_cluster binder terms ty body =
227   List.fold_right (fun term body -> Ast.Binder (binder, (term, ty), body))
228     terms body  (* terms are names: either Ident or FreshVar *)
229
230 let fold_exists terms ty body =
231   List.fold_right
232     (fun term body ->
233        let lambda = Ast.Binder (`Lambda, (term, ty), body) in
234        Ast.Appl [Ast.Symbol ("exists", 0); lambda])
235     terms body
236
237 let fold_binder binder pt_names body =
238   List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body)
239     pt_names body
240
241 let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
242
243   (* create empty precedence level for "term" *)
244 let _ =
245   let dummy_action =
246     Gramext.action
247       (fun _ -> failwith "internal error, lexer generated a dummy token")
248   in
249   let dummy_prod = [[Gramext.Stoken ("DUMMY", "")], dummy_action] in
250   let mk_level_list first last =
251     let rec aux acc =
252       function
253         i when i < first -> acc
254       | i ->
255           aux
256             ((Some (string_of_int i ^ "N"), Some Gramext.NonA, dummy_prod) ::
257                (Some (string_of_int i ^ "L"), Some Gramext.LeftA,
258                 dummy_prod) ::
259                (Some (string_of_int i ^ "R"), Some Gramext.RightA,
260                 dummy_prod) ::
261                acc)
262             (i - 1)
263     in
264     aux [] last
265   in
266   Grammar.extend
267     [Grammar.Entry.obj (term : 'a Grammar.Entry.e), None,
268      mk_level_list min_precedence max_precedence]
269
270 (* {{{ Grammar for concrete syntax patterns, notation level 1 *)
271 let _ =
272   Grammar.extend
273     (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e) in
274      let grammar_entry_create s =
275        Grammar.Entry.create (Grammar.of_entry level1_pattern) s
276      in
277      let l1_pattern : 'l1_pattern Grammar.Entry.e =
278        grammar_entry_create "l1_pattern"
279      and literal : 'literal Grammar.Entry.e = grammar_entry_create "literal"
280      and sep : 'sep Grammar.Entry.e = grammar_entry_create "sep"
281      and l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e =
282        grammar_entry_create "l1_magic_pattern"
283      and l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e =
284        grammar_entry_create "l1_pattern_variable"
285      and l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e =
286        grammar_entry_create "l1_simple_pattern"
287      in
288      [Grammar.Entry.obj (level1_pattern : 'level1_pattern Grammar.Entry.e),
289       None,
290       [None, None,
291        [[Gramext.Snterm
292            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
293          Gramext.Stoken ("EOI", "")],
294         Gramext.action
295           (fun _ (p : 'l1_pattern)
296              (loc : Lexing.position * Lexing.position) ->
297              (CicNotationUtil.boxify p : 'level1_pattern))]];
298       Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
299       [None, None,
300        [[Gramext.Slist1
301            (Gramext.Snterm
302               (Grammar.Entry.obj
303                  (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)))],
304         Gramext.action
305           (fun (p : 'l1_simple_pattern list)
306              (loc : Lexing.position * Lexing.position) ->
307              (p : 'l1_pattern))]];
308       Grammar.Entry.obj (literal : 'literal Grammar.Entry.e), None,
309       [None, None,
310        [[Gramext.Stoken ("NUMBER", "")],
311         Gramext.action
312           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
313              (`Number n : 'literal));
314         [Gramext.Stoken ("QKEYWORD", "")],
315         Gramext.action
316           (fun (k : string) (loc : Lexing.position * Lexing.position) ->
317              (`Keyword k : 'literal));
318         [Gramext.Stoken ("SYMBOL", "")],
319         Gramext.action
320           (fun (s : string) (loc : Lexing.position * Lexing.position) ->
321              (`Symbol s : 'literal))]];
322       Grammar.Entry.obj (sep : 'sep Grammar.Entry.e), None,
323       [None, None,
324        [[Gramext.Stoken ("", "sep");
325          Gramext.Snterm
326            (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
327         Gramext.action
328           (fun (sep : 'literal) _ (loc : Lexing.position * Lexing.position) ->
329              (sep : 'sep))]];
330       Grammar.Entry.obj
331         (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e),
332       None,
333       [None, None,
334        [[Gramext.Stoken ("", "opt");
335          Gramext.Snterm
336            (Grammar.Entry.obj
337               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))],
338         Gramext.action
339           (fun (p : 'l1_simple_pattern) _
340              (loc : Lexing.position * Lexing.position) ->
341              (Ast.Opt p : 'l1_magic_pattern));
342         [Gramext.Stoken ("", "list1");
343          Gramext.Snterm
344            (Grammar.Entry.obj
345               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
346          Gramext.Sopt
347            (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
348         Gramext.action
349           (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
350              (loc : Lexing.position * Lexing.position) ->
351              (Ast.List1 (p, sep) : 'l1_magic_pattern));
352         [Gramext.Stoken ("", "list0");
353          Gramext.Snterm
354            (Grammar.Entry.obj
355               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
356          Gramext.Sopt
357            (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
358         Gramext.action
359           (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
360              (loc : Lexing.position * Lexing.position) ->
361              (Ast.List0 (p, sep) : 'l1_magic_pattern))]];
362       Grammar.Entry.obj
363         (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e),
364       None,
365       [None, None,
366        [[Gramext.Stoken ("", "ident"); Gramext.Stoken ("IDENT", "")],
367         Gramext.action
368           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
369              (Ast.IdentVar id : 'l1_pattern_variable));
370         [Gramext.Stoken ("", "number"); Gramext.Stoken ("IDENT", "")],
371         Gramext.action
372           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
373              (Ast.NumVar id : 'l1_pattern_variable));
374         [Gramext.Stoken ("", "term"); Gramext.Stoken ("IDENT", "")],
375         Gramext.action
376           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
377              (Ast.TermVar id : 'l1_pattern_variable))]];
378       Grammar.Entry.obj
379         (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e),
380       None,
381       [Some "layout", Some Gramext.LeftA,
382        [[Gramext.Stoken ("LPAREN", "");
383          Gramext.Snterm
384            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
385          Gramext.Stoken ("RPAREN", "")],
386         Gramext.action
387           (fun _ (p : 'l1_pattern) _
388              (loc : Lexing.position * Lexing.position) ->
389              (return_term loc (CicNotationUtil.group p) :
390               'l1_simple_pattern));
391         [Gramext.Stoken ("", "break")],
392         Gramext.action
393           (fun _ (loc : Lexing.position * Lexing.position) ->
394              (return_term loc (Ast.Layout Ast.Break) : 'l1_simple_pattern));
395         [Gramext.Stoken ("", "hovbox"); Gramext.Stoken ("LPAREN", "");
396          Gramext.Snterm
397            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
398          Gramext.Stoken ("RPAREN", "")],
399         Gramext.action
400           (fun _ (p : 'l1_pattern) _ _
401              (loc : Lexing.position * Lexing.position) ->
402              (return_term loc
403                 (Ast.Layout (Ast.Box ((Ast.HOV, false, false), p))) :
404               'l1_simple_pattern));
405         [Gramext.Stoken ("", "hvbox"); Gramext.Stoken ("LPAREN", "");
406          Gramext.Snterm
407            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
408          Gramext.Stoken ("RPAREN", "")],
409         Gramext.action
410           (fun _ (p : 'l1_pattern) _ _
411              (loc : Lexing.position * Lexing.position) ->
412              (return_term loc
413                 (Ast.Layout (Ast.Box ((Ast.HV, false, false), p))) :
414               'l1_simple_pattern));
415         [Gramext.Stoken ("", "vbox"); Gramext.Stoken ("LPAREN", "");
416          Gramext.Snterm
417            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
418          Gramext.Stoken ("RPAREN", "")],
419         Gramext.action
420           (fun _ (p : 'l1_pattern) _ _
421              (loc : Lexing.position * Lexing.position) ->
422              (return_term loc
423                 (Ast.Layout (Ast.Box ((Ast.V, false, false), p))) :
424               'l1_simple_pattern));
425         [Gramext.Stoken ("", "hbox"); Gramext.Stoken ("LPAREN", "");
426          Gramext.Snterm
427            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
428          Gramext.Stoken ("RPAREN", "")],
429         Gramext.action
430           (fun _ (p : 'l1_pattern) _ _
431              (loc : Lexing.position * Lexing.position) ->
432              (return_term loc
433                 (Ast.Layout (Ast.Box ((Ast.H, false, false), p))) :
434               'l1_simple_pattern));
435         [Gramext.Stoken ("SYMBOL", "\\root"); Gramext.Sself;
436          Gramext.Stoken ("SYMBOL", "\\of"); Gramext.Sself],
437         Gramext.action
438           (fun (arg : 'l1_simple_pattern) _ (index : 'l1_simple_pattern) _
439              (loc : Lexing.position * Lexing.position) ->
440              (return_term loc (Ast.Layout (Ast.Root (arg, index))) :
441               'l1_simple_pattern));
442         [Gramext.Stoken ("SYMBOL", "\\sqrt"); Gramext.Sself],
443         Gramext.action
444           (fun (p : 'l1_simple_pattern) _
445              (loc : Lexing.position * Lexing.position) ->
446              (return_term loc (Ast.Layout (Ast.Sqrt p)) :
447               'l1_simple_pattern));
448         [Gramext.Stoken ("SYMBOL", "\\frac"); Gramext.Sself; Gramext.Sself],
449         Gramext.action
450           (fun (p2 : 'l1_simple_pattern) (p1 : 'l1_simple_pattern) _
451              (loc : Lexing.position * Lexing.position) ->
452              (return_term loc (Ast.Layout (Ast.Frac (p1, p2))) :
453               'l1_simple_pattern));
454         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\atop"); Gramext.Sself],
455         Gramext.action
456           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
457              (loc : Lexing.position * Lexing.position) ->
458              (return_term loc (Ast.Layout (Ast.Atop (p1, p2))) :
459               'l1_simple_pattern));
460         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\over"); Gramext.Sself],
461         Gramext.action
462           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
463              (loc : Lexing.position * Lexing.position) ->
464              (return_term loc (Ast.Layout (Ast.Over (p1, p2))) :
465               'l1_simple_pattern));
466         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\above"); Gramext.Sself],
467         Gramext.action
468           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
469              (loc : Lexing.position * Lexing.position) ->
470              (return_term loc (Ast.Layout (Ast.Above (p1, p2))) :
471               'l1_simple_pattern));
472         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\below"); Gramext.Sself],
473         Gramext.action
474           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
475              (loc : Lexing.position * Lexing.position) ->
476              (return_term loc (Ast.Layout (Ast.Below (p1, p2))) :
477               'l1_simple_pattern));
478         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\sup"); Gramext.Sself],
479         Gramext.action
480           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
481              (loc : Lexing.position * Lexing.position) ->
482              (return_term loc (Ast.Layout (Ast.Sup (p1, p2))) :
483               'l1_simple_pattern));
484         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\sub"); Gramext.Sself],
485         Gramext.action
486           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
487              (loc : Lexing.position * Lexing.position) ->
488              (return_term loc (Ast.Layout (Ast.Sub (p1, p2))) :
489               'l1_simple_pattern))];
490        Some "simple", Some Gramext.NonA,
491        [[Gramext.Snterm
492            (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
493         Gramext.action
494           (fun (l : 'literal) (loc : Lexing.position * Lexing.position) ->
495              (return_term loc (Ast.Literal l) : 'l1_simple_pattern));
496         [Gramext.Snterm
497            (Grammar.Entry.obj
498               (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e))],
499         Gramext.action
500           (fun (v : 'l1_pattern_variable)
501              (loc : Lexing.position * Lexing.position) ->
502              (return_term loc (Ast.Variable v) : 'l1_simple_pattern));
503         [Gramext.Snterm
504            (Grammar.Entry.obj
505               (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e))],
506         Gramext.action
507           (fun (m : 'l1_magic_pattern)
508              (loc : Lexing.position * Lexing.position) ->
509              (return_term loc (Ast.Magic m) : 'l1_simple_pattern));
510         [Gramext.Stoken ("IDENT", "")],
511         Gramext.action
512           (fun (i : string) (loc : Lexing.position * Lexing.position) ->
513              (return_term loc (Ast.Variable (Ast.TermVar i)) :
514               'l1_simple_pattern))]]])
515 (* }}} *)
516
517 (* {{{ Grammar for ast magics, notation level 2 *)
518 let _ =
519   Grammar.extend
520     (let _ = (level2_meta : 'level2_meta Grammar.Entry.e) in
521      let grammar_entry_create s =
522        Grammar.Entry.create (Grammar.of_entry level2_meta) s
523      in
524      let l2_variable : 'l2_variable Grammar.Entry.e =
525        grammar_entry_create "l2_variable"
526      and l2_magic : 'l2_magic Grammar.Entry.e =
527        grammar_entry_create "l2_magic"
528      in
529      [Grammar.Entry.obj (l2_variable : 'l2_variable Grammar.Entry.e), None,
530       [None, None,
531        [[Gramext.Stoken ("IDENT", "")],
532         Gramext.action
533           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
534              (Ast.TermVar id : 'l2_variable));
535         [Gramext.Stoken ("", "anonymous")],
536         Gramext.action
537           (fun _ (loc : Lexing.position * Lexing.position) ->
538              (Ast.TermVar "_" : 'l2_variable));
539         [Gramext.Stoken ("", "fresh"); Gramext.Stoken ("IDENT", "")],
540         Gramext.action
541           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
542              (Ast.FreshVar id : 'l2_variable));
543         [Gramext.Stoken ("", "ident"); Gramext.Stoken ("IDENT", "")],
544         Gramext.action
545           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
546              (Ast.IdentVar id : 'l2_variable));
547         [Gramext.Stoken ("", "number"); Gramext.Stoken ("IDENT", "")],
548         Gramext.action
549           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
550              (Ast.NumVar id : 'l2_variable));
551         [Gramext.Stoken ("", "term"); Gramext.Stoken ("IDENT", "")],
552         Gramext.action
553           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
554              (Ast.TermVar id : 'l2_variable))]];
555       Grammar.Entry.obj (l2_magic : 'l2_magic Grammar.Entry.e), None,
556       [None, None,
557        [[Gramext.Stoken ("", "fail")],
558         Gramext.action
559           (fun _ (loc : Lexing.position * Lexing.position) ->
560              (Ast.Fail : 'l2_magic));
561         [Gramext.Stoken ("", "if");
562          Gramext.Snterm
563            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
564          Gramext.Stoken ("", "then");
565          Gramext.Snterm
566            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
567          Gramext.Stoken ("", "else");
568          Gramext.Snterm
569            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
570         Gramext.action
571           (fun (p_false : 'level2_meta) _ (p_true : 'level2_meta) _
572              (p_test : 'level2_meta) _
573              (loc : Lexing.position * Lexing.position) ->
574              (Ast.If (p_test, p_true, p_false) : 'l2_magic));
575         [Gramext.Stoken ("", "default");
576          Gramext.Snterm
577            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
578          Gramext.Snterm
579            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
580         Gramext.action
581           (fun (none : 'level2_meta) (some : 'level2_meta) _
582              (loc : Lexing.position * Lexing.position) ->
583              (Ast.Default (some, none) : 'l2_magic));
584         [Gramext.Stoken ("", "fold");
585          Gramext.srules
586            [[Gramext.Stoken ("", "right")],
587             Gramext.action
588               (fun _ (loc : Lexing.position * Lexing.position) ->
589                  (`Right : 'e__1));
590             [Gramext.Stoken ("", "left")],
591             Gramext.action
592               (fun _ (loc : Lexing.position * Lexing.position) ->
593                  (`Left : 'e__1))];
594          Gramext.Snterm
595            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
596          Gramext.Stoken ("", "rec"); Gramext.Stoken ("IDENT", "");
597          Gramext.Snterm
598            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
599         Gramext.action
600           (fun (recursive : 'level2_meta) (id : string) _
601              (base : 'level2_meta) (kind : 'e__1) _
602              (loc : Lexing.position * Lexing.position) ->
603              (Ast.Fold (kind, base, [id], recursive) : 'l2_magic))]];
604       Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e), None,
605       [None, None,
606        [[Gramext.Stoken ("UNPARSED_AST", "")],
607         Gramext.action
608           (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
609              (!parse_level2_ast_ref (Ulexing.from_utf8_string blob) :
610               'level2_meta));
611         [Gramext.Snterm
612            (Grammar.Entry.obj (l2_variable : 'l2_variable Grammar.Entry.e))],
613         Gramext.action
614           (fun (var : 'l2_variable)
615              (loc : Lexing.position * Lexing.position) ->
616              (Ast.Variable var : 'level2_meta));
617         [Gramext.Snterm
618            (Grammar.Entry.obj (l2_magic : 'l2_magic Grammar.Entry.e))],
619         Gramext.action
620           (fun (magic : 'l2_magic)
621              (loc : Lexing.position * Lexing.position) ->
622              (Ast.Magic magic : 'level2_meta))]]])
623 (* }}} *)
624
625 (* {{{ Grammar for ast patterns, notation level 2 *)
626 let _ =
627   Grammar.extend
628     (let _ = (level2_ast : 'level2_ast Grammar.Entry.e)
629      and _ = (term : 'term Grammar.Entry.e)
630      and _ = (let_defs : 'let_defs Grammar.Entry.e) in
631      let grammar_entry_create s =
632        Grammar.Entry.create (Grammar.of_entry level2_ast) s
633      in
634      let sort : 'sort Grammar.Entry.e = grammar_entry_create "sort"
635      and explicit_subst : 'explicit_subst Grammar.Entry.e =
636        grammar_entry_create "explicit_subst"
637      and meta_subst : 'meta_subst Grammar.Entry.e =
638        grammar_entry_create "meta_subst"
639      and meta_substs : 'meta_substs Grammar.Entry.e =
640        grammar_entry_create "meta_substs"
641      and possibly_typed_name : 'possibly_typed_name Grammar.Entry.e =
642        grammar_entry_create "possibly_typed_name"
643      and match_pattern : 'match_pattern Grammar.Entry.e =
644        grammar_entry_create "match_pattern"
645      and binder : 'binder Grammar.Entry.e = grammar_entry_create "binder"
646      and arg : 'arg Grammar.Entry.e = grammar_entry_create "arg"
647      and single_arg : 'single_arg Grammar.Entry.e =
648        grammar_entry_create "single_arg"
649      and induction_kind : 'induction_kind Grammar.Entry.e =
650        grammar_entry_create "induction_kind"
651      and binder_vars : 'binder_vars Grammar.Entry.e =
652        grammar_entry_create "binder_vars"
653      in
654      [Grammar.Entry.obj (level2_ast : 'level2_ast Grammar.Entry.e), None,
655       [None, None,
656        [[Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
657         Gramext.action
658           (fun (p : 'term) (loc : Lexing.position * Lexing.position) ->
659              (p : 'level2_ast))]];
660       Grammar.Entry.obj (sort : 'sort Grammar.Entry.e), None,
661       [None, None,
662        [[Gramext.Stoken ("", "CProp")],
663         Gramext.action
664           (fun _ (loc : Lexing.position * Lexing.position) ->
665              (`CProp : 'sort));
666         [Gramext.Stoken ("", "Type")],
667         Gramext.action
668           (fun _ (loc : Lexing.position * Lexing.position) ->
669              (`Type : 'sort));
670         [Gramext.Stoken ("", "Set")],
671         Gramext.action
672           (fun _ (loc : Lexing.position * Lexing.position) -> (`Set : 'sort));
673         [Gramext.Stoken ("", "Prop")],
674         Gramext.action
675           (fun _ (loc : Lexing.position * Lexing.position) ->
676              (`Prop : 'sort))]];
677       Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e),
678       None,
679       [None, None,
680        [[Gramext.Stoken ("SYMBOL", "\\subst"); Gramext.Stoken ("SYMBOL", "[");
681          Gramext.Slist1sep
682            (Gramext.srules
683               [[Gramext.Stoken ("IDENT", "");
684                 Gramext.Stoken ("SYMBOL", "≔");
685                 Gramext.Snterm
686                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
687                Gramext.action
688                  (fun (t : 'term) _ (i : string)
689                     (loc : Lexing.position * Lexing.position) ->
690                     (i, t : 'e__2))],
691             Gramext.Stoken ("SYMBOL", ";"));
692          Gramext.Stoken ("SYMBOL", "]")],
693         Gramext.action
694           (fun _ (substs : 'e__2 list) _ _
695              (loc : Lexing.position * Lexing.position) ->
696              (substs : 'explicit_subst))]];
697       Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None,
698       [None, None,
699        [[Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
700         Gramext.action
701           (fun (p : 'term) (loc : Lexing.position * Lexing.position) ->
702              (Some p : 'meta_subst));
703         [Gramext.Stoken ("SYMBOL", "_")],
704         Gramext.action
705           (fun (s : string) (loc : Lexing.position * Lexing.position) ->
706              (None : 'meta_subst))]];
707       Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e), None,
708       [None, None,
709        [[Gramext.Stoken ("SYMBOL", "[");
710          Gramext.Slist0
711            (Gramext.Snterm
712               (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e)));
713          Gramext.Stoken ("SYMBOL", "]")],
714         Gramext.action
715           (fun _ (substs : 'meta_subst list) _
716              (loc : Lexing.position * Lexing.position) ->
717              (substs : 'meta_substs))]];
718       Grammar.Entry.obj
719         (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e),
720       None,
721       [None, None,
722        [[Gramext.Snterm
723            (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e))],
724         Gramext.action
725           (fun (arg : 'single_arg)
726              (loc : Lexing.position * Lexing.position) ->
727              (arg, None : 'possibly_typed_name));
728         [Gramext.Stoken ("LPAREN", "");
729          Gramext.Snterm
730            (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e));
731          Gramext.Stoken ("SYMBOL", ":");
732          Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
733          Gramext.Stoken ("RPAREN", "")],
734         Gramext.action
735           (fun _ (typ : 'term) _ (id : 'single_arg) _
736              (loc : Lexing.position * Lexing.position) ->
737              (id, Some typ : 'possibly_typed_name))]];
738       Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e),
739       None,
740       [None, None,
741        [[Gramext.Stoken ("LPAREN", ""); Gramext.Stoken ("IDENT", "");
742          Gramext.Slist1
743            (Gramext.Snterm
744               (Grammar.Entry.obj
745                  (possibly_typed_name :
746                   'possibly_typed_name Grammar.Entry.e)));
747          Gramext.Stoken ("RPAREN", "")],
748         Gramext.action
749           (fun _ (vars : 'possibly_typed_name list) (id : string) _
750              (loc : Lexing.position * Lexing.position) ->
751              (id, None, vars : 'match_pattern));
752         [Gramext.Stoken ("IDENT", "")],
753         Gramext.action
754           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
755              (id, None, [] : 'match_pattern))]];
756       Grammar.Entry.obj (binder : 'binder Grammar.Entry.e), None,
757       [None, None,
758        [[Gramext.Stoken ("SYMBOL", "λ")],
759         Gramext.action
760           (fun _ (loc : Lexing.position * Lexing.position) ->
761              (`Lambda : 'binder));
762         [Gramext.Stoken ("SYMBOL", "∀")],
763         Gramext.action
764           (fun _ (loc : Lexing.position * Lexing.position) ->
765              (`Forall : 'binder));
766         [Gramext.Stoken ("SYMBOL", "Π")],
767         Gramext.action
768           (fun _ (loc : Lexing.position * Lexing.position) ->
769              (`Pi : 'binder))]];
770       Grammar.Entry.obj (arg : 'arg Grammar.Entry.e), None,
771       [None, None,
772        [[Gramext.Stoken ("UNPARSED_META", "")],
773         Gramext.action
774           (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
775              (let meta =
776                 !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
777               in
778               match meta with
779                 Ast.Variable (Ast.FreshVar _) -> [meta], None
780               | Ast.Variable (Ast.TermVar "_") ->
781                   [Ast.Ident ("_", None)], None
782               | _ -> failwith "Invalid bound name." :
783               'arg));
784         [Gramext.Stoken ("IDENT", "")],
785         Gramext.action
786           (fun (name : string) (loc : Lexing.position * Lexing.position) ->
787              ([Ast.Ident (name, None)], None : 'arg));
788         [Gramext.Stoken ("LPAREN", "");
789          Gramext.Slist1sep
790            (Gramext.Stoken ("IDENT", ""), Gramext.Stoken ("SYMBOL", ","));
791          Gramext.Stoken ("SYMBOL", ":");
792          Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
793          Gramext.Stoken ("RPAREN", "")],
794         Gramext.action
795           (fun _ (ty : 'term) _ (names : string list) _
796              (loc : Lexing.position * Lexing.position) ->
797              (List.map (fun n -> Ast.Ident (n, None)) names, Some ty :
798               'arg))]];
799       Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e), None,
800       [None, None,
801        [[Gramext.Stoken ("UNPARSED_META", "")],
802         Gramext.action
803           (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
804              (let meta =
805                 !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
806               in
807               match meta with
808                 Ast.Variable (Ast.FreshVar _) |
809                 Ast.Variable (Ast.IdentVar _) ->
810                   meta
811               | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
812               | _ -> failwith "Invalid index name." :
813               'single_arg));
814         [Gramext.Stoken ("IDENT", "")],
815         Gramext.action
816           (fun (name : string) (loc : Lexing.position * Lexing.position) ->
817              (Ast.Ident (name, None) : 'single_arg))]];
818       Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e),
819       None,
820       [None, None,
821        [[Gramext.Stoken ("", "corec")],
822         Gramext.action
823           (fun _ (loc : Lexing.position * Lexing.position) ->
824              (`CoInductive : 'induction_kind));
825         [Gramext.Stoken ("", "rec")],
826         Gramext.action
827           (fun _ (loc : Lexing.position * Lexing.position) ->
828              (`Inductive : 'induction_kind))]];
829       Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e), None,
830       [None, None,
831        [[Gramext.Slist1sep
832            (Gramext.srules
833               [[Gramext.Snterm
834                   (Grammar.Entry.obj
835                      (single_arg : 'single_arg Grammar.Entry.e));
836                 Gramext.Slist1
837                   (Gramext.Snterm
838                      (Grammar.Entry.obj (arg : 'arg Grammar.Entry.e)));
839                 Gramext.Sopt
840                   (Gramext.srules
841                      [[Gramext.Stoken ("", "on");
842                        Gramext.Snterm
843                          (Grammar.Entry.obj
844                             (single_arg : 'single_arg Grammar.Entry.e))],
845                       Gramext.action
846                         (fun (id : 'single_arg) _
847                            (loc : Lexing.position * Lexing.position) ->
848                            (id : 'e__3))]);
849                 Gramext.Sopt
850                   (Gramext.srules
851                      [[Gramext.Stoken ("SYMBOL", ":");
852                        Gramext.Snterm
853                          (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
854                       Gramext.action
855                         (fun (p : 'term) _
856                            (loc : Lexing.position * Lexing.position) ->
857                            (p : 'e__4))]);
858                 Gramext.Stoken ("SYMBOL", "≝");
859                 Gramext.Snterm
860                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
861                Gramext.action
862                  (fun (body : 'term) _ (ty : 'e__4 option)
863                     (index_name : 'e__3 option) (args : 'arg list)
864                     (name : 'single_arg)
865                     (loc : Lexing.position * Lexing.position) ->
866                     (let body = fold_binder `Lambda args body in
867                      let ty =
868                        match ty with
869                          None -> None
870                        | Some ty -> Some (fold_binder `Pi args ty)
871                      in
872                      let rec position_of name p =
873                        function
874                          [] -> None, p
875                        | n :: _ when n = name -> Some p, p
876                        | _ :: tl -> position_of name (p + 1) tl
877                      in
878                      let rec find_arg name n =
879                        function
880                          [] ->
881                            Ast.fail loc
882                              (sprintf "Argument %s not found"
883                                 (CicNotationPp.pp_term name))
884                        | (l, _) :: tl ->
885                            match position_of name 0 l with
886                              None, len -> find_arg name (n + len) tl
887                            | Some where, len -> n + where
888                      in
889                      let index =
890                        match index_name with
891                          None -> 0
892                        | Some index_name -> find_arg index_name 0 args
893                      in
894                      (name, ty), body, index :
895                      'e__5))],
896             Gramext.Stoken ("", "and"))],
897         Gramext.action
898           (fun (defs : 'e__5 list)
899              (loc : Lexing.position * Lexing.position) ->
900              (defs : 'let_defs))]];
901       Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e), None,
902       [None, None,
903        [[Gramext.Stoken ("LPAREN", "");
904          Gramext.srules
905            [[Gramext.Stoken ("SYMBOL", "_")],
906             Gramext.action
907               (fun _ (loc : Lexing.position * Lexing.position) ->
908                  ([Ast.Ident ("_", None)] : 'e__8));
909             [Gramext.Slist1sep
910                (Gramext.Snterm
911                   (Grammar.Entry.obj
912                      (single_arg : 'single_arg Grammar.Entry.e)),
913                 Gramext.Stoken ("SYMBOL", ","))],
914             Gramext.action
915               (fun (l : 'single_arg list)
916                  (loc : Lexing.position * Lexing.position) ->
917                  (l : 'e__8))];
918          Gramext.Sopt
919            (Gramext.srules
920               [[Gramext.Stoken ("SYMBOL", ":");
921                 Gramext.Snterm
922                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
923                Gramext.action
924                  (fun (t : 'term) _
925                     (loc : Lexing.position * Lexing.position) ->
926                     (t : 'e__9))]);
927          Gramext.Stoken ("RPAREN", "")],
928         Gramext.action
929           (fun _ (typ : 'e__9 option) (vars : 'e__8) _
930              (loc : Lexing.position * Lexing.position) ->
931              (vars, typ : 'binder_vars));
932         [Gramext.srules
933            [[Gramext.Stoken ("SYMBOL", "_")],
934             Gramext.action
935               (fun _ (loc : Lexing.position * Lexing.position) ->
936                  ([Ast.Ident ("_", None)] : 'e__6));
937             [Gramext.Slist1sep
938                (Gramext.Snterm
939                   (Grammar.Entry.obj
940                      (single_arg : 'single_arg Grammar.Entry.e)),
941                 Gramext.Stoken ("SYMBOL", ","))],
942             Gramext.action
943               (fun (l : 'single_arg list)
944                  (loc : Lexing.position * Lexing.position) ->
945                  (l : 'e__6))];
946          Gramext.Sopt
947            (Gramext.srules
948               [[Gramext.Stoken ("SYMBOL", ":");
949                 Gramext.Snterm
950                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
951                Gramext.action
952                  (fun (t : 'term) _
953                     (loc : Lexing.position * Lexing.position) ->
954                     (t : 'e__7))])],
955         Gramext.action
956           (fun (typ : 'e__7 option) (vars : 'e__6)
957              (loc : Lexing.position * Lexing.position) ->
958              (vars, typ : 'binder_vars))]];
959       Grammar.Entry.obj (term : 'term Grammar.Entry.e),
960       Some (Gramext.Level "10N"),
961       [None, None,
962        [[Gramext.Stoken ("", "let");
963          Gramext.Snterm
964            (Grammar.Entry.obj
965               (induction_kind : 'induction_kind Grammar.Entry.e));
966          Gramext.Snterm
967            (Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e));
968          Gramext.Stoken ("", "in"); Gramext.Sself],
969         Gramext.action
970           (fun (body : 'term) _ (defs : 'let_defs) (k : 'induction_kind) _
971              (loc : Lexing.position * Lexing.position) ->
972              (return_term loc (Ast.LetRec (k, defs, body)) : 'term));
973         [Gramext.Stoken ("", "let");
974          Gramext.Snterm
975            (Grammar.Entry.obj
976               (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e));
977          Gramext.Stoken ("SYMBOL", "≝"); Gramext.Sself;
978          Gramext.Stoken ("", "in"); Gramext.Sself],
979         Gramext.action
980           (fun (p2 : 'term) _ (p1 : 'term) _ (var : 'possibly_typed_name) _
981              (loc : Lexing.position * Lexing.position) ->
982              (return_term loc (Ast.LetIn (var, p1, p2)) : 'term))]];
983       Grammar.Entry.obj (term : 'term Grammar.Entry.e),
984       Some (Gramext.Level "20R"),
985       [None, None,
986        [[Gramext.Stoken ("SYMBOL", "∃");
987          Gramext.Snterm
988            (Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e));
989          Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
990         Gramext.action
991           (fun (body : 'term) _ (vars, typ : 'binder_vars) _
992              (loc : Lexing.position * Lexing.position) ->
993              (return_term loc (fold_exists vars typ body) : 'term));
994         [Gramext.Snterm
995            (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
996          Gramext.Snterm
997            (Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e));
998          Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
999         Gramext.action
1000           (fun (body : 'term) _ (vars, typ : 'binder_vars) (b : 'binder)
1001              (loc : Lexing.position * Lexing.position) ->
1002              (return_term loc (fold_cluster b vars typ body) : 'term))]];
1003       Grammar.Entry.obj (term : 'term Grammar.Entry.e),
1004       Some (Gramext.Level "70L"),
1005       [None, None,
1006        [[Gramext.Sself; Gramext.Sself],
1007         Gramext.action
1008           (fun (p2 : 'term) (p1 : 'term)
1009              (loc : Lexing.position * Lexing.position) ->
1010              (let rec aux =
1011                 function
1012                   Ast.Appl (hd :: tl) |
1013                   Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->
1014                     aux hd @ tl
1015                 | term -> [term]
1016               in
1017               return_term loc (Ast.Appl (aux p1 @ [p2])) :
1018               'term))]];
1019       Grammar.Entry.obj (term : 'term Grammar.Entry.e),
1020       Some (Gramext.Level "90N"),
1021       [None, None,
1022        [[Gramext.Stoken ("UNPARSED_META", "")],
1023         Gramext.action
1024           (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
1025              (!parse_level2_meta_ref (Ulexing.from_utf8_string blob) :
1026               'term));
1027         [Gramext.Stoken ("LPAREN", ""); Gramext.Sself;
1028          Gramext.Stoken ("RPAREN", "")],
1029         Gramext.action
1030           (fun _ (p : 'term) _ (loc : Lexing.position * Lexing.position) ->
1031              (p : 'term));
1032         [Gramext.Stoken ("LPAREN", ""); Gramext.Sself;
1033          Gramext.Stoken ("SYMBOL", ":"); Gramext.Sself;
1034          Gramext.Stoken ("RPAREN", "")],
1035         Gramext.action
1036           (fun _ (p2 : 'term) _ (p1 : 'term) _
1037              (loc : Lexing.position * Lexing.position) ->
1038              (return_term loc (Ast.Cast (p1, p2)) : 'term));
1039         [Gramext.Sopt
1040            (Gramext.srules
1041               [[Gramext.Stoken ("SYMBOL", "[");
1042                 Gramext.Snterm
1043                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
1044                 Gramext.Stoken ("SYMBOL", "]")],
1045                Gramext.action
1046                  (fun _ (ty : 'term) _
1047                     (loc : Lexing.position * Lexing.position) ->
1048                     (ty : 'e__10))]);
1049          Gramext.Stoken ("", "match"); Gramext.Sself;
1050          Gramext.Sopt
1051            (Gramext.srules
1052               [[Gramext.Stoken ("", "in"); Gramext.Stoken ("IDENT", "")],
1053                Gramext.action
1054                  (fun (id : string) _
1055                     (loc : Lexing.position * Lexing.position) ->
1056                     (id, None : 'e__11))]);
1057          Gramext.Stoken ("", "with"); Gramext.Stoken ("SYMBOL", "[");
1058          Gramext.Slist0sep
1059            (Gramext.srules
1060               [[Gramext.Snterm
1061                   (Grammar.Entry.obj
1062                      (match_pattern : 'match_pattern Grammar.Entry.e));
1063                 Gramext.Stoken ("SYMBOL", "⇒");
1064                 Gramext.Snterm
1065                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
1066                Gramext.action
1067                  (fun (rhs : 'term) _ (lhs : 'match_pattern)
1068                     (loc : Lexing.position * Lexing.position) ->
1069                     (lhs, rhs : 'e__12))],
1070             Gramext.Stoken ("SYMBOL", "|"));
1071          Gramext.Stoken ("SYMBOL", "]")],
1072         Gramext.action
1073           (fun _ (patterns : 'e__12 list) _ _ (indty_ident : 'e__11 option)
1074              (t : 'term) _ (outtyp : 'e__10 option)
1075              (loc : Lexing.position * Lexing.position) ->
1076              (return_term loc (Ast.Case (t, indty_ident, outtyp, patterns)) :
1077               'term));
1078         [Gramext.Snterm (Grammar.Entry.obj (sort : 'sort Grammar.Entry.e))],
1079         Gramext.action
1080           (fun (s : 'sort) (loc : Lexing.position * Lexing.position) ->
1081              (return_term loc (Ast.Sort s) : 'term));
1082         [Gramext.Stoken ("META", "");
1083          Gramext.Snterm
1084            (Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e))],
1085         Gramext.action
1086           (fun (s : 'meta_substs) (m : string)
1087              (loc : Lexing.position * Lexing.position) ->
1088              (return_term loc (Ast.Meta (int_of_string m, s)) : 'term));
1089         [Gramext.Stoken ("META", "")],
1090         Gramext.action
1091           (fun (m : string) (loc : Lexing.position * Lexing.position) ->
1092              (return_term loc (Ast.Meta (int_of_string m, [])) : 'term));
1093         [Gramext.Stoken ("PLACEHOLDER", "")],
1094         Gramext.action
1095           (fun _ (loc : Lexing.position * Lexing.position) ->
1096              (return_term loc Ast.UserInput : 'term));
1097         [Gramext.Stoken ("IMPLICIT", "")],
1098         Gramext.action
1099           (fun _ (loc : Lexing.position * Lexing.position) ->
1100              (return_term loc Ast.Implicit : 'term));
1101         [Gramext.Stoken ("NUMBER", "")],
1102         Gramext.action
1103           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
1104              (return_term loc (Ast.Num (n, 0)) : 'term));
1105         [Gramext.Stoken ("URI", "")],
1106         Gramext.action
1107           (fun (u : string) (loc : Lexing.position * Lexing.position) ->
1108              (return_term loc (Ast.Uri (u, None)) : 'term));
1109         [Gramext.Stoken ("CSYMBOL", "")],
1110         Gramext.action
1111           (fun (s : string) (loc : Lexing.position * Lexing.position) ->
1112              (return_term loc (Ast.Symbol (s, 0)) : 'term));
1113         [Gramext.Stoken ("IDENT", "");
1114          Gramext.Snterm
1115            (Grammar.Entry.obj
1116               (explicit_subst : 'explicit_subst Grammar.Entry.e))],
1117         Gramext.action
1118           (fun (s : 'explicit_subst) (id : string)
1119              (loc : Lexing.position * Lexing.position) ->
1120              (return_term loc (Ast.Ident (id, Some s)) : 'term));
1121         [Gramext.Stoken ("IDENT", "")],
1122         Gramext.action
1123           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
1124              (return_term loc (Ast.Ident (id, None)) : 'term))]]])
1125 (* }}} *)
1126
1127 (** {2 API implementation} *)
1128
1129 let exc_located_wrapper f =
1130   try f () with
1131     Stdpp.Exc_located (floc, Stream.Error msg) ->
1132       raise (Parse_error (floc, msg))
1133   | Stdpp.Exc_located (floc, exn) ->
1134       raise (Parse_error (floc, Printexc.to_string exn))
1135
1136 let parse_level1_pattern lexbuf =
1137   CicNotationLexer.set_lexbuf lexbuf;
1138   exc_located_wrapper
1139     (fun () -> Grammar.Entry.parse level1_pattern Stream.sempty)
1140
1141 let parse_level2_ast lexbuf =
1142   CicNotationLexer.set_lexbuf lexbuf;
1143   exc_located_wrapper (fun () -> Grammar.Entry.parse level2_ast Stream.sempty)
1144
1145 let parse_level2_meta lexbuf =
1146   CicNotationLexer.set_lexbuf lexbuf;
1147   exc_located_wrapper
1148     (fun () -> Grammar.Entry.parse level2_meta Stream.sempty)
1149
1150 let _ =
1151   parse_level1_pattern_ref := parse_level1_pattern;
1152   parse_level2_ast_ref := parse_level2_ast;
1153   parse_level2_meta_ref := parse_level2_meta
1154
1155 (** {2 Debugging} *)
1156
1157 let print_l2_pattern () =
1158   Grammar.print_entry Format.std_formatter (Grammar.Entry.obj term);
1159   Format.pp_print_flush Format.std_formatter ();
1160   flush stdout
1161
1162 (* vim:set encoding=utf8 foldmethod=marker: *)