--- /dev/null
+(* *)(* 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: *)
projects / helm.git / commitdiff