From a6dd077a2b3e4d0c4395c2ee4cc2e1b6d10ab963 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 23 May 2005 15:23:38 +0000 Subject: [PATCH] added rule to generate camlp4 expansion of cicNotationParser.ml (in order to reverse engineer Grammar.extend usage ...) --- helm/ocaml/cic_notation/Makefile | 2 + .../cicNotationParser.expanded.ml | 849 ++++++++++++++++++ 2 files changed, 851 insertions(+) create mode 100644 helm/ocaml/cic_notation/cicNotationParser.expanded.ml diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index 6a43c4890..8a168568f 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -46,3 +46,5 @@ disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi $(OCAMLOPT) -c -rectypes $< +cicNotationParser.expanded.ml: cicNotationParser.ml + camlp4 -nolib '-I' '/usr/lib/ocaml/3.08.3/' '-I' '/home/zack/helm/ocaml/urimanager' '-I' '/usr/lib/ocaml/3.08.3/pcre' '-I' '/usr/lib/ocaml/3.08.3/' '-I' '/usr/lib/ocaml/3.08.3/netstring' '-I' '/usr/lib/ocaml/3.08.3/pxp-engine' '-I' '/usr/lib/ocaml/3.08.3/pxp-lex-utf8' '-I' '/usr/lib/ocaml/3.08.3/pxp-lex-iso88591' '-I' '/usr/lib/ocaml/3.08.3/pxp-lex-iso885915' '-I' '/usr/lib/ocaml/3.08.3/http' '-I' '/home/zacchiro/helm/ocaml/pxp' '-I' '/usr/lib/ocaml/3.08.3/zip' '-I' '/usr/lib/ocaml/3.08.3/expat' '-I' '/home/zacchiro/helm/ocaml/xml' '-I' '/home/zack/helm/ocaml/cic' '-I' '/usr/lib/ocaml/3.08.3/camlp4' '-I' '/home/zack/helm/ocaml/utf8_macros' '-I' '/usr/lib/ocaml/3.08.3/camlp4' '-I' '/usr/lib/ocaml/3.08.3/ulex' 'pa_o.cmo' 'pa_op.cmo' 'pr_o.cmo' 'pa_extend.cmo' 'pa_unicode_macro.cma' 'pa_ulex.cma' $< > $@ diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml new file mode 100644 index 000000000..bd42ea9cb --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml @@ -0,0 +1,849 @@ +(* *)(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +oopen Printf +eexception Parse_error of Token.flocation * string +llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer +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 notation = Grammar.Entry.create grammar "notation"(* level1 <-> level 2 *) +llet interpretation = Grammar.Entry.create grammar "interpretation"(* level2 <-> level 3 *) + +llet return_term loc term = () +llet loc_of_floc ({Lexing.pos_cnum = loc_begin}, {Lexing.pos_cnum = loc_end}) = + loc_begin, loc_end +llet fail floc msg = + let (x, y) = loc_of_floc floc in + failwith (sprintf "Error at characters %d - %d: %s" x y msg) +llet int_of_string s = + try Pervasives.int_of_string s with + Failure _ -> + failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s) +oopen CicNotationPt +llet boxify = + function + [a] -> a + | l -> Layout (Box (H, l)) +llet fold_binder binder pt_names body = + let fold_cluster binder names ty body = + List.fold_right + (fun name body -> Binder (binder, (Cic.Name name, ty), body)) names body + in + List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body) + pt_names body +llet return_term loc term = AttributedTerm (`Loc loc, term) +Elet _ = + Grammar.extend + (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e) + and _ = (level2_pattern : 'level2_pattern Grammar.Entry.e) + and _ = (level3_term : 'level3_term Grammar.Entry.e) + and _ = (notation : 'notation Grammar.Entry.e) + and _ = (interpretation : 'interpretation Grammar.Entry.e) in + let grammar_entry_create s = + Grammar.Entry.create (Grammar.of_entry level1_pattern) s + in + let l1_pattern : 'l1_pattern Grammar.Entry.e = + grammar_entry_create "l1_pattern" + and literal : 'literal Grammar.Entry.e = grammar_entry_create "literal" + and sep : 'sep Grammar.Entry.e = grammar_entry_create "sep" + and l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e = + grammar_entry_create "l1_magic_pattern" + and l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e = + grammar_entry_create "l1_pattern_variable" + and l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e = + grammar_entry_create "l1_simple_pattern" + and sort : 'sort Grammar.Entry.e = grammar_entry_create "sort" + and explicit_subst : 'explicit_subst Grammar.Entry.e = + grammar_entry_create "explicit_subst" + and meta_subst : 'meta_subst Grammar.Entry.e = + grammar_entry_create "meta_subst" + and possibly_typed_name : 'possibly_typed_name Grammar.Entry.e = + grammar_entry_create "possibly_typed_name" + and match_pattern : 'match_pattern Grammar.Entry.e = + grammar_entry_create "match_pattern" + and binder : 'binder Grammar.Entry.e = grammar_entry_create "binder" + and bound_names : 'bound_names Grammar.Entry.e = + grammar_entry_create "bound_names" + and induction_kind : 'induction_kind Grammar.Entry.e = + grammar_entry_create "induction_kind" + and let_defs : 'let_defs Grammar.Entry.e = + grammar_entry_create "let_defs" + and l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e = + grammar_entry_create "l2_pattern_variable" + and l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e = + grammar_entry_create "l2_magic_pattern" + and l2_pattern : 'l2_pattern Grammar.Entry.e = + grammar_entry_create "l2_pattern" + and argument : 'argument Grammar.Entry.e = + grammar_entry_create "argument" + and associativity : 'associativity Grammar.Entry.e = + grammar_entry_create "associativity" + and precedence : 'precedence Grammar.Entry.e = + grammar_entry_create "precedence" + in + [Grammar.Entry.obj (level1_pattern : 'level1_pattern Grammar.Entry.e), + None, + [None, None, + [[Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("EOI", "")], + Gramext.action + (fun _ (p : 'l1_pattern) + (loc : Lexing.position * Lexing.position) -> + (boxify p : 'level1_pattern))]]; + Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None, + [None, None, + [[Gramext.Slist0 + (Gramext.Snterm + (Grammar.Entry.obj + (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)))], + Gramext.action + (fun (p : 'l1_simple_pattern list) + (loc : Lexing.position * Lexing.position) -> + (p : 'l1_pattern))]]; + Grammar.Entry.obj (literal : 'literal Grammar.Entry.e), None, + [None, None, + [[Gramext.Stoken ("NUMBER", "")], + Gramext.action + (fun (n : string) (loc : Lexing.position * Lexing.position) -> + (`Number n : 'literal)); + [Gramext.Stoken ("KEYWORD", "")], + Gramext.action + (fun (k : string) (loc : Lexing.position * Lexing.position) -> + (`Keyword k : 'literal)); + [Gramext.Stoken ("SYMBOL", "")], + Gramext.action + (fun (s : string) (loc : Lexing.position * Lexing.position) -> + (`Symbol s : 'literal))]]; + Grammar.Entry.obj (sep : 'sep Grammar.Entry.e), None, + [None, None, + [[Gramext.Stoken ("SYMBOL", "\\SEP"); + Gramext.Snterm + (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))], + Gramext.action + (fun (sep : 'literal) _ (loc : Lexing.position * Lexing.position) -> + (sep : 'sep))]]; + Grammar.Entry.obj + (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e), + None, + [None, None, + [[Gramext.Stoken ("SYMBOL", "\\OPT"); + Gramext.Snterm + (Grammar.Entry.obj + (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))], + Gramext.action + (fun (p : 'l1_simple_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (Opt p : 'l1_magic_pattern)); + [Gramext.Stoken ("SYMBOL", "\\LIST1"); + Gramext.Snterm + (Grammar.Entry.obj + (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)); + Gramext.Sopt + (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))], + Gramext.action + (fun (sep : 'sep option) (p : 'l1_simple_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (List1 (p, sep) : 'l1_magic_pattern)); + [Gramext.Stoken ("SYMBOL", "\\LIST0"); + Gramext.Snterm + (Grammar.Entry.obj + (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)); + Gramext.Sopt + (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))], + Gramext.action + (fun (sep : 'sep option) (p : 'l1_simple_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (List0 (p, sep) : 'l1_magic_pattern))]]; + Grammar.Entry.obj + (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e), + None, + [None, None, + [[Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) _ (loc : Lexing.position * Lexing.position) -> + (IdentVar id : 'l1_pattern_variable)); + [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) _ (loc : Lexing.position * Lexing.position) -> + (NumVar id : 'l1_pattern_variable)); + [Gramext.Stoken ("SYMBOL", "\\TERM"); Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) _ (loc : Lexing.position * Lexing.position) -> + (TermVar id : 'l1_pattern_variable)); + [Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) (loc : Lexing.position * Lexing.position) -> + (TermVar id : 'l1_pattern_variable))]]; + Grammar.Entry.obj + (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e), + None, + [Some "layout", Some Gramext.LeftA, + [[Gramext.Stoken ("SYMBOL", "["); + Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "\\AS"); Gramext.Stoken ("IDENT", ""); + Gramext.Stoken ("SYMBOL", "]")], + Gramext.action + (fun _ (id : string) _ (p : 'l1_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc + (Variable (Ascription (Layout (Box (H, p)), id))) : + 'l1_simple_pattern)); + [Gramext.Stoken ("SYMBOL", "["); + Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "]")], + Gramext.action + (fun _ (p : 'l1_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern)); + [Gramext.Stoken ("SYMBOL", "\\BREAK")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout Break) : 'l1_simple_pattern)); + [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("SYMBOL", "["); + Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "]")], + Gramext.action + (fun _ (p : 'l1_pattern) _ _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Box (V, p))) : 'l1_simple_pattern)); + [Gramext.Stoken ("SYMBOL", "\\HBOX"); Gramext.Stoken ("SYMBOL", "["); + Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "]")], + Gramext.action + (fun _ (p : 'l1_pattern) _ _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern)); + [Gramext.Stoken ("SYMBOL", "\\ROOT"); + Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "\\OF"); Gramext.Sself], + Gramext.action + (fun (arg : 'l1_simple_pattern) _ (index : 'l1_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Root (arg, Layout (Box (H, index))))) : + 'l1_simple_pattern)); + [Gramext.Stoken ("SYMBOL", "\\SQRT"); Gramext.Sself], + Gramext.action + (fun (p : 'l1_simple_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Sqrt p)) : 'l1_simple_pattern)); + [Gramext.Stoken ("SYMBOL", "\\FRAC"); Gramext.Sself; Gramext.Sself], + Gramext.action + (fun (p2 : 'l1_simple_pattern) (p1 : 'l1_simple_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Frac (p1, p2))) : 'l1_simple_pattern)); + [Gramext.Stoken ("SYMBOL", "["); + Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "\\ATOP"); + Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "]")], + Gramext.action + (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Atop (boxify p1, boxify p2))) : + 'l1_simple_pattern)); + [Gramext.Stoken ("SYMBOL", "["); + Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "\\OVER"); + Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "]")], + Gramext.action + (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Frac (boxify p1, boxify p2))) : + 'l1_simple_pattern)); + [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself], + Gramext.action + (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Above (p1, p2))) : + 'l1_simple_pattern)); + [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\BELOW"); Gramext.Sself], + Gramext.action + (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Below (p1, p2))) : + 'l1_simple_pattern)); + [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUP"); Gramext.Sself], + Gramext.action + (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Sup (p1, p2))) : 'l1_simple_pattern)); + [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUB"); Gramext.Sself], + Gramext.action + (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Layout (Sub (p1, p2))) : 'l1_simple_pattern))]; + Some "simple", Some Gramext.NonA, + [[Gramext.Snterm + (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))], + Gramext.action + (fun (l : 'literal) (loc : Lexing.position * Lexing.position) -> + (return_term loc (Literal l) : 'l1_simple_pattern)); + [Gramext.Snterm + (Grammar.Entry.obj + (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e))], + Gramext.action + (fun (v : 'l1_pattern_variable) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Variable v) : 'l1_simple_pattern)); + [Gramext.Snterm + (Grammar.Entry.obj + (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e))], + Gramext.action + (fun (m : 'l1_magic_pattern) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Magic m) : 'l1_simple_pattern))]]; + Grammar.Entry.obj (level2_pattern : 'level2_pattern Grammar.Entry.e), + None, + [None, None, + [[Gramext.Snterm + (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))], + Gramext.action + (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) -> + (p : 'level2_pattern))]]; + Grammar.Entry.obj (sort : 'sort Grammar.Entry.e), None, + [None, None, + [[Gramext.Stoken ("SYMBOL", "\\TYPE")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (`Type : 'sort)); + [Gramext.Stoken ("SYMBOL", "\\SET")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> (`Set : 'sort)); + [Gramext.Stoken ("SYMBOL", "\\PROP")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (`Prop : 'sort))]]; + Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e), + None, [None, None, []]; + Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None, + [None, None, []]; + Grammar.Entry.obj + (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e), + None, + [None, None, + [[Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) (loc : Lexing.position * Lexing.position) -> + (Cic.Name id, None : 'possibly_typed_name)); + [Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", ""); + Gramext.Stoken ("SYMBOL", ":"); + Gramext.Snterm + (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", ")")], + Gramext.action + (fun _ (typ : 'l2_pattern) _ (id : string) _ + (loc : Lexing.position * Lexing.position) -> + (Cic.Name id, Some typ : 'possibly_typed_name))]]; + Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e), + None, + [None, None, + [[Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", ""); + Gramext.Slist1 + (Gramext.Snterm + (Grammar.Entry.obj + (possibly_typed_name : + 'possibly_typed_name Grammar.Entry.e))); + Gramext.Stoken ("SYMBOL", ")")], + Gramext.action + (fun _ (vars : 'possibly_typed_name list) (id : string) _ + (loc : Lexing.position * Lexing.position) -> + (id, vars : 'match_pattern)); + [Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) (loc : Lexing.position * Lexing.position) -> + (id, [] : 'match_pattern))]]; + Grammar.Entry.obj (binder : 'binder Grammar.Entry.e), None, + [None, None, + [[Gramext.Stoken ("SYMBOL", "λ")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (`Lambda : 'binder)); + [Gramext.Stoken ("SYMBOL", "∀")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (`Forall : 'binder)); + [Gramext.Stoken ("SYMBOL", "∃")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (`Exists : 'binder)); + [Gramext.Stoken ("SYMBOL", "Π")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (`Pi : 'binder))]]; + Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e), None, + [None, None, + [[Gramext.Slist1 + (Gramext.srules + [[Gramext.Stoken ("SYMBOL", "("); + Gramext.Slist1sep + (Gramext.Stoken ("IDENT", ""), + Gramext.Stoken ("SYMBOL", ",")); + Gramext.Sopt + (Gramext.srules + [[Gramext.Stoken ("SYMBOL", ":"); + Gramext.Snterm + (Grammar.Entry.obj + (l2_pattern : 'l2_pattern Grammar.Entry.e))], + Gramext.action + (fun (p : 'l2_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (p : 'e__2))]); + Gramext.Stoken ("SYMBOL", ")")], + Gramext.action + (fun _ (ty : 'e__2 option) (vars : string list) _ + (loc : Lexing.position * Lexing.position) -> + (vars, ty : 'e__3))])], + Gramext.action + (fun (clusters : 'e__3 list) + (loc : Lexing.position * Lexing.position) -> + (clusters : 'bound_names)); + [Gramext.Slist1sep + (Gramext.Stoken ("IDENT", ""), Gramext.Stoken ("SYMBOL", ",")); + Gramext.Sopt + (Gramext.srules + [[Gramext.Stoken ("SYMBOL", ":"); + Gramext.Snterm + (Grammar.Entry.obj + (l2_pattern : 'l2_pattern Grammar.Entry.e))], + Gramext.action + (fun (p : 'l2_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (p : 'e__1))])], + Gramext.action + (fun (ty : 'e__1 option) (vars : string list) + (loc : Lexing.position * Lexing.position) -> + ([vars, ty] : 'bound_names))]]; + Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e), + None, + [None, None, + [[Gramext.Stoken ("IDENT", "corec")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (`CoInductive : 'induction_kind)); + [Gramext.Stoken ("IDENT", "rec")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (`Inductive : 'induction_kind))]]; + Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e), None, + [None, None, + [[Gramext.Slist1sep + (Gramext.srules + [[Gramext.Stoken ("IDENT", ""); + Gramext.Snterm + (Grammar.Entry.obj + (bound_names : 'bound_names Grammar.Entry.e)); + Gramext.Sopt + (Gramext.srules + [[Gramext.Stoken ("IDENT", "on"); + Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) _ + (loc : Lexing.position * Lexing.position) -> + (id : 'e__4))]); + Gramext.Sopt + (Gramext.srules + [[Gramext.Stoken ("SYMBOL", ":"); + Gramext.Snterm + (Grammar.Entry.obj + (l2_pattern : 'l2_pattern Grammar.Entry.e))], + Gramext.action + (fun (p : 'l2_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (p : 'e__5))]); + Gramext.Stoken ("SYMBOL", "≝"); + Gramext.Snterm + (Grammar.Entry.obj + (l2_pattern : 'l2_pattern Grammar.Entry.e))], + Gramext.action + (fun (body : 'l2_pattern) _ (ty : 'e__5 option) + (index_name : 'e__4 option) (args : 'bound_names) + (name : string) + (loc : Lexing.position * Lexing.position) -> + (let body = fold_binder `Lambda args body in + let ty = + match ty with + None -> None + | Some ty -> Some (fold_binder `Pi args ty) + in + let rec position_of name p = + function + [] -> None, p + | n :: _ when n = name -> Some p, p + | _ :: tl -> position_of name (p + 1) tl + in + let rec find_arg name n = + function + [] -> fail loc (sprintf "Argument %s not found" name) + | (l, _) :: tl -> + match position_of name 0 l with + None, len -> find_arg name (n + len) tl + | Some where, len -> n + where + in + let index = + match index_name with + None -> 0 + | Some name -> find_arg name 0 args + in + (Cic.Name name, ty), body, index : + 'e__6))], + Gramext.Stoken ("IDENT", "and"))], + Gramext.action + (fun (defs : 'e__6 list) + (loc : Lexing.position * Lexing.position) -> + (defs : 'let_defs))]]; + Grammar.Entry.obj + (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e), + None, + [None, None, + [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) _ (loc : Lexing.position * Lexing.position) -> + (FreshVar id : 'l2_pattern_variable)); + [Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) _ (loc : Lexing.position * Lexing.position) -> + (IdentVar id : 'l2_pattern_variable)); + [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) _ (loc : Lexing.position * Lexing.position) -> + (NumVar id : 'l2_pattern_variable))]]; + Grammar.Entry.obj + (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e), + None, + [None, None, + [[Gramext.Stoken ("SYMBOL", "\\DEFAULT"); + Gramext.Snterm + (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e)); + Gramext.Snterm + (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))], + Gramext.action + (fun (none : 'l2_pattern) (some : 'l2_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (Default (some, none) : 'l2_magic_pattern)); + [Gramext.Stoken ("SYMBOL", "\\FOLD"); + Gramext.srules + [[Gramext.Stoken ("IDENT", "right")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (`Right : 'e__7)); + [Gramext.Stoken ("IDENT", "left")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (`Left : 'e__7))]; + Gramext.Snterm + (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "\\LAMBDA"); Gramext.Stoken ("IDENT", ""); + Gramext.Snterm + (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))], + Gramext.action + (fun (recursive : 'l2_pattern) (id : string) _ (base : 'l2_pattern) + (kind : 'e__7) _ (loc : Lexing.position * Lexing.position) -> + (Fold (kind, base, [id], recursive) : 'l2_magic_pattern))]]; + Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), None, + [Some "letin", Some Gramext.NonA, + [[Gramext.Stoken ("IDENT", "let"); + Gramext.Snterm + (Grammar.Entry.obj + (induction_kind : 'induction_kind Grammar.Entry.e)); + Gramext.Snterm + (Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e)); + Gramext.Stoken ("IDENT", "in"); Gramext.Sself], + Gramext.action + (fun (body : 'l2_pattern) _ (defs : 'let_defs) (k : 'induction_kind) + _ (loc : Lexing.position * Lexing.position) -> + (return_term loc (LetRec (k, defs, body)) : 'l2_pattern)); + [Gramext.Stoken ("IDENT", "let"); + Gramext.Snterm + (Grammar.Entry.obj + (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "≝"); Gramext.Sself; + Gramext.Stoken ("", "in"); Gramext.Sself], + Gramext.action + (fun (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _ + (var : 'possibly_typed_name) _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))]; + Some "binder", Some Gramext.RightA, + [[Gramext.Snterm + (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e)); + Gramext.Snterm + (Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "."); Gramext.Sself], + Gramext.action + (fun (body : 'l2_pattern) _ (names : 'bound_names) (b : 'binder) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (fold_binder b names body) : 'l2_pattern))]; + Some "extension", None, []; + Some "apply", Some Gramext.LeftA, + [[Gramext.Sself; Gramext.Sself], + Gramext.action + (fun (p2 : 'l2_pattern) (p1 : 'l2_pattern) + (loc : Lexing.position * Lexing.position) -> + (let rec aux = + function + Appl (hd :: tl) | AttributedTerm (_, Appl (hd :: tl)) -> + aux hd @ tl + | term -> [term] + in + return_term loc (Appl (aux p1 @ [p2])) : + 'l2_pattern))]; + Some "simple", Some Gramext.NonA, + [[Gramext.Snterm + (Grammar.Entry.obj + (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e))], + Gramext.action + (fun (m : 'l2_magic_pattern) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Magic m) : 'l2_pattern)); + [Gramext.Snterm + (Grammar.Entry.obj + (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e))], + Gramext.action + (fun (v : 'l2_pattern_variable) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Variable v) : 'l2_pattern)); + [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself; + Gramext.Stoken ("SYMBOL", ")")], + Gramext.action + (fun _ (p : 'l2_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (p : 'l2_pattern)); + [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself; + Gramext.Stoken ("SYMBOL", ":"); Gramext.Sself; + Gramext.Stoken ("SYMBOL", ")")], + Gramext.action + (fun _ (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Appl [Symbol ("cast", 0); p1; p2]) : + 'l2_pattern)); + [Gramext.Sopt + (Gramext.srules + [[Gramext.Stoken ("SYMBOL", "["); + Gramext.Snterm + (Grammar.Entry.obj + (l2_pattern : 'l2_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "]")], + Gramext.action + (fun _ (ty : 'l2_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (ty : 'e__8))]); + Gramext.Stoken ("IDENT", "match"); Gramext.Sself; + Gramext.Sopt + (Gramext.srules + [[Gramext.Stoken ("SYMBOL", ":"); Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) _ + (loc : Lexing.position * Lexing.position) -> + (id : 'e__9))]); + Gramext.Stoken ("IDENT", "with"); Gramext.Stoken ("SYMBOL", "["); + Gramext.Slist0sep + (Gramext.srules + [[Gramext.Snterm + (Grammar.Entry.obj + (match_pattern : 'match_pattern Grammar.Entry.e)); + Gramext.Stoken ("SYMBOL", "⇒"); + Gramext.Snterm + (Grammar.Entry.obj + (l2_pattern : 'l2_pattern Grammar.Entry.e))], + Gramext.action + (fun (rhs : 'l2_pattern) _ (lhs : 'match_pattern) + (loc : Lexing.position * Lexing.position) -> + (lhs, rhs : 'e__10))], + Gramext.Stoken ("SYMBOL", "|")); + Gramext.Stoken ("SYMBOL", "]")], + Gramext.action + (fun _ (patterns : 'e__10 list) _ _ (indty_ident : 'e__9 option) + (t : 'l2_pattern) _ (outtyp : 'e__8 option) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Case (t, indty_ident, outtyp, patterns)) : + 'l2_pattern)); + [Gramext.Stoken ("SYMBOL", "")], + Gramext.action + (fun (s : string) (loc : Lexing.position * Lexing.position) -> + (return_term loc (Symbol (s, 0)) : 'l2_pattern)); + [Gramext.Snterm (Grammar.Entry.obj (sort : 'sort Grammar.Entry.e))], + Gramext.action + (fun (s : 'sort) (loc : Lexing.position * Lexing.position) -> + (return_term loc (Sort s) : 'l2_pattern)); + [Gramext.Stoken ("META", ""); + Gramext.Snterm + (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e))], + Gramext.action + (fun (s : 'meta_subst) (m : string) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Meta (int_of_string m, s)) : 'l2_pattern)); + [Gramext.Stoken ("META", "")], + Gramext.action + (fun (m : string) (loc : Lexing.position * Lexing.position) -> + (return_term loc (Meta (int_of_string m, [])) : 'l2_pattern)); + [Gramext.Stoken ("IMPLICIT", "")], + Gramext.action + (fun _ (loc : Lexing.position * Lexing.position) -> + (return_term loc Implicit : 'l2_pattern)); + [Gramext.Stoken ("NUMBER", "")], + Gramext.action + (fun (n : string) (loc : Lexing.position * Lexing.position) -> + (return_term loc (Num (n, 0)) : 'l2_pattern)); + [Gramext.Stoken ("URI", "")], + Gramext.action + (fun (u : string) (loc : Lexing.position * Lexing.position) -> + (return_term loc (Uri (u, None)) : 'l2_pattern)); + [Gramext.Stoken ("IDENT", ""); + Gramext.Snterm + (Grammar.Entry.obj + (explicit_subst : 'explicit_subst Grammar.Entry.e))], + Gramext.action + (fun (s : 'explicit_subst) (id : string) + (loc : Lexing.position * Lexing.position) -> + (return_term loc (Ident (id, Some s)) : 'l2_pattern)); + [Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) (loc : Lexing.position * Lexing.position) -> + (return_term loc (Ident (id, None)) : 'l2_pattern))]]; + Grammar.Entry.obj (argument : 'argument Grammar.Entry.e), None, + [None, None, + [[Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("IDENT", ""); + Gramext.Stoken ("SYMBOL", "."); Gramext.Sself], + Gramext.action + (fun (a : 'argument) _ (id : string) _ + (loc : Lexing.position * Lexing.position) -> + (EtaArg (Some id, a) : 'argument)); + [Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("SYMBOL", "."); + Gramext.Sself], + Gramext.action + (fun (a : 'argument) _ _ + (loc : Lexing.position * Lexing.position) -> + (EtaArg (None, a) : 'argument)); + [Gramext.Stoken ("IDENT", "")], + Gramext.action + (fun (id : string) (loc : Lexing.position * Lexing.position) -> + (IdentArg id : 'argument))]]; + Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e), None, + [None, None, + [[Gramext.Stoken ("SYMBOL", "("); Gramext.Slist1 Gramext.Sself; + Gramext.Stoken ("SYMBOL", ")")], + Gramext.action + (fun _ (terms : 'level3_term list) _ + (loc : Lexing.position * Lexing.position) -> + (match terms with + [] -> assert false + | [term] -> term + | terms -> ApplPattern terms : + 'level3_term)); + [Gramext.Snterm + (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e))], + Gramext.action + (fun (a : 'argument) (loc : Lexing.position * Lexing.position) -> + (ArgPattern a : 'level3_term)); + [Gramext.Stoken ("URI", "")], + Gramext.action + (fun (u : string) (loc : Lexing.position * Lexing.position) -> + (UriPattern u : 'level3_term))]]; + Grammar.Entry.obj (associativity : 'associativity Grammar.Entry.e), + None, + [None, None, + [[Gramext.Stoken ("IDENT", "right"); + Gramext.Stoken ("IDENT", "associative")], + Gramext.action + (fun _ _ (loc : Lexing.position * Lexing.position) -> + (`Right : 'associativity)); + [Gramext.Stoken ("IDENT", "left"); + Gramext.Stoken ("IDENT", "associative")], + Gramext.action + (fun _ _ (loc : Lexing.position * Lexing.position) -> + (`Left : 'associativity))]]; + Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None, + [None, None, + [[Gramext.Stoken ("IDENT", "at"); + Gramext.Stoken ("IDENT", "precedence"); + Gramext.Stoken ("NUMBER", "")], + Gramext.action + (fun (n : string) _ _ (loc : Lexing.position * Lexing.position) -> + (n : 'precedence))]]; + Grammar.Entry.obj (notation : 'notation Grammar.Entry.e), None, + [None, None, + [[Gramext.Stoken ("IDENT", "notation"); + Gramext.Snterm + (Grammar.Entry.obj + (level1_pattern : 'level1_pattern Grammar.Entry.e)); + Gramext.Stoken ("IDENT", "for"); + Gramext.Snterm + (Grammar.Entry.obj + (level2_pattern : 'level2_pattern Grammar.Entry.e)); + Gramext.Sopt + (Gramext.Snterm + (Grammar.Entry.obj + (associativity : 'associativity Grammar.Entry.e))); + Gramext.Sopt + (Gramext.Snterm + (Grammar.Entry.obj + (precedence : 'precedence Grammar.Entry.e)))], + Gramext.action + (fun (prec : 'precedence option) (assoc : 'associativity option) + (p2 : 'level2_pattern) _ (p1 : 'level1_pattern) _ + (loc : Lexing.position * Lexing.position) -> + (() : 'notation))]]; + Grammar.Entry.obj (interpretation : 'interpretation Grammar.Entry.e), + None, + [None, None, + [[Gramext.Stoken ("IDENT", "interpretation"); + Gramext.Stoken ("SYMBOL", ""); + Gramext.Slist1 + (Gramext.Snterm + (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e))); + Gramext.Stoken ("IDENT", "as"); + Gramext.Snterm + (Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e))], + Gramext.action + (fun (t : 'level3_term) _ (args : 'argument list) (s : string) _ + (loc : Lexing.position * Lexing.position) -> + (() : 'interpretation))]]]) + +let exc_located_wrapper f = + try f () with + Stdpp.Exc_located (floc, Stream.Error msg) -> + raise (Parse_error (floc, msg)) + | Stdpp.Exc_located (floc, exn) -> + raise (Parse_error (floc, Printexc.to_string exn)) + +let parse_syntax_pattern stream = + exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream) + +let parse_ast_pattern stream = + exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream) + +let parse_interpretation stream = + exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream) + +(* vim:set encoding=utf8 foldmethod=marker: *) -- 2.39.2