+++ /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
-mmodule Ast = CicNotationPtmmodule Env = CicNotationEnv
-eexception Parse_error of Token.flocation * stringeexception Level_not_found of int
-llet level1_pattern_grammar =
- Grammar.gcreate CicNotationLexer.level1_pattern_lexerllet level2_ast_grammar = Grammar.gcreate CicNotationLexer.level2_ast_lexerllet level2_meta_grammar = Grammar.gcreate CicNotationLexer.level2_meta_lexer
-llet min_precedence = 0llet max_precedence = 100
-llet level1_pattern =
- 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"
-llet return_term loc term = ()
-llet int_of_string s =
- try Pervasives.int_of_string s with
- Failure _ ->
- failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
-(** {2 Grammar extension} *)
-
-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
-llet gram_of_literal =
- function
- `Symbol s -> gram_symbol s
- | `Keyword s -> gram_keyword s
- | `Number s -> gram_number s
-ttype binding =
- NoBinding
- | Binding of string * Env.value_type
- | Env of (string * Env.value_type) list
-llet make_action action bindings =
- let rec aux (vl : CicNotationEnv.t) =
- function
- [] -> Gramext.action (fun (loc : Ast.location) -> action vl loc)
- | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
- | Binding (name, Env.TermType) :: tl ->
- Gramext.action
- (fun (v : Ast.term) ->
- aux ((name, (Env.TermType, Env.TermValue v)) :: vl) tl)
- | Binding (name, Env.StringType) :: tl ->
- Gramext.action
- (fun (v : string) ->
- aux ((name, (Env.StringType, Env.StringValue v)) :: vl) tl)
- | Binding (name, Env.NumType) :: tl ->
- Gramext.action
- (fun (v : string) ->
- aux ((name, (Env.NumType, Env.NumValue v)) :: vl) tl)
- | Binding (name, Env.OptType t) :: tl ->
- Gramext.action
- (fun (v : 'a option) ->
- aux ((name, (Env.OptType t, Env.OptValue v)) :: vl) tl)
- | Binding (name, Env.ListType t) :: tl ->
- Gramext.action
- (fun (v : 'a list) ->
- aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
- | Env _ :: tl ->
- Gramext.action (fun (v : CicNotationEnv.t) -> aux (v @ vl) tl)
- in
- aux [] (List.rev bindings)
-llet flatten_opt =
- let rec aux acc =
- function
- [] -> List.rev acc
- | NoBinding :: tl -> aux acc tl
- | Env names :: tl -> aux (List.rev names @ acc) tl
- | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
- in
- aux []
- (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
-llet extract_term_production pattern =
- let rec aux =
- function
- Ast.AttributedTerm (_, t) -> aux t
- | Ast.Literal l -> aux_literal l
- | Ast.Layout l -> aux_layout l
- | Ast.Magic m -> aux_magic m
- | Ast.Variable v -> aux_variable v
- | t -> prerr_endline (CicNotationPp.pp_term t); assert false
- and aux_literal =
- function
- `Symbol s -> [NoBinding, gram_symbol s]
- | `Keyword s -> [NoBinding, gram_keyword s]
- | `Number s -> [NoBinding, gram_number s]
- and aux_layout =
- function
- Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
- | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
- | Ast.Below (p1, p2) ->
- aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
- | Ast.Above (p1, p2) ->
- aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
- | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
- | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
- | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
- | Ast.Root (p1, p2) ->
- [NoBinding, gram_symbol "\\root"] @ aux p2 @
- [NoBinding, gram_symbol "\\of"] @ aux p1
- | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
- | Ast.Break -> []
- | Ast.Box (_, pl) -> List.flatten (List.map aux pl)
- | Ast.Group pl -> List.flatten (List.map aux pl)
- and aux_magic magic =
- match magic with
- Ast.Opt p ->
- let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
- let action (env_opt : CicNotationEnv.t option) (loc : Ast.location) =
- match env_opt with
- Some env -> List.map Env.opt_binding_some env
- | None -> List.map Env.opt_binding_of_name p_names
- in
- [Env (List.map Env.opt_declaration p_names),
- Gramext.srules
- [[Gramext.Sopt (Gramext.srules [p_atoms, p_action])],
- Gramext.action action]]
- | Ast.List0 (p, _) | Ast.List1 (p, _) ->
- let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
- let action (env_list : CicNotationEnv.t list) (loc : Ast.location) =
- CicNotationEnv.coalesce_env p_names env_list
- in
- let gram_of_list s =
- match magic with
- Ast.List0 (_, None) -> Gramext.Slist0 s
- | Ast.List1 (_, None) -> Gramext.Slist1 s
- | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
- | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
- | _ -> assert false
- in
- [Env (List.map Env.list_declaration p_names),
- Gramext.srules
- [[gram_of_list (Gramext.srules [p_atoms, p_action])],
- Gramext.action action]]
- | _ -> assert false
- and aux_variable =
- function
- Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
- | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
- | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
- | Ast.Ascription (p, s) -> assert false
- | Ast.FreshVar _ -> assert false
- and inner_pattern p =
- let (p_bindings, p_atoms) = List.split (aux p) in
- let p_names = flatten_opt p_bindings in
- let action =
- make_action (fun (env : CicNotationEnv.t) (loc : Ast.location) -> env)
- p_bindings
- in
- p_bindings, p_atoms, p_names, action
- in
- aux pattern
-
-let level_of precedence associativity =
- if precedence < min_precedence || precedence > max_precedence then
- raise (Level_not_found precedence);
- let assoc_string =
- match associativity with
- Gramext.NonA -> "N"
- | Gramext.LeftA -> "L"
- | Gramext.RightA -> "R"
- in
- string_of_int precedence ^ assoc_string
-
-type rule_id = Token.t Gramext.g_symbol list
-
- (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
-let owned_keywords = Hashtbl.create 23
-
-let extend level1_pattern ~precedence ~associativity action =
- let (p_bindings, p_atoms) =
- List.split (extract_term_production level1_pattern)
- in
- let level = level_of precedence associativity in
- let p_names = flatten_opt p_bindings in
- let _ =
- Grammar.extend
- [Grammar.Entry.obj (term : 'a Grammar.Entry.e),
- Some (Gramext.Level level),
- [None, Some associativity,
- [p_atoms,
- make_action
- (fun (env : CicNotationEnv.t) (loc : Ast.location) ->
- action env loc)
- p_bindings]]]
- in
- let keywords = CicNotationUtil.keywords_of_term level1_pattern in
- let rule_id = p_atoms in
- List.iter CicNotationLexer.add_level2_ast_keyword keywords;
- Hashtbl.add owned_keywords rule_id keywords;
- rule_id
-
-let delete rule_id =
- let atoms = rule_id in
- begin try
- let keywords = Hashtbl.find owned_keywords rule_id in
- List.iter CicNotationLexer.remove_level2_ast_keyword keywords
- with
- Not_found -> assert false
- end;
- Grammar.delete_rule term atoms
-
-(** {2 Grammar} *)
-
-let parse_level1_pattern_ref = ref (fun _ -> assert false)
-let parse_level2_ast_ref = ref (fun _ -> assert false)
-let parse_level2_meta_ref = ref (fun _ -> assert false)
-
-let fold_cluster binder terms ty body =
- List.fold_right (fun term body -> Ast.Binder (binder, (term, ty), body))
- terms body (* terms are names: either Ident or FreshVar *)
-
-let fold_exists terms ty body =
- List.fold_right
- (fun term body ->
- let lambda = Ast.Binder (`Lambda, (term, ty), body) in
- Ast.Appl [Ast.Symbol ("exists", 0); lambda])
- terms body
-
-let fold_binder binder pt_names body =
- List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body)
- pt_names body
-
-let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
-
- (* create empty precedence level for "term" *)
-let _ =
- let dummy_action =
- Gramext.action
- (fun _ -> failwith "internal error, lexer generated a dummy token")
- in
- let dummy_prod = [[Gramext.Stoken ("DUMMY", "")], dummy_action] in
- let mk_level_list first last =
- let rec aux acc =
- function
- i when i < first -> acc
- | i ->
- aux
- ((Some (string_of_int i ^ "N"), Some Gramext.NonA, dummy_prod) ::
- (Some (string_of_int i ^ "L"), Some Gramext.LeftA,
- dummy_prod) ::
- (Some (string_of_int i ^ "R"), Some Gramext.RightA,
- dummy_prod) ::
- acc)
- (i - 1)
- in
- aux [] last
- in
- Grammar.extend
- [Grammar.Entry.obj (term : 'a Grammar.Entry.e), None,
- mk_level_list min_precedence max_precedence]
-
-(* {{{ Grammar for concrete syntax patterns, notation level 1 *)
-let _ =
- Grammar.extend
- (let _ = (level1_pattern : 'level1_pattern 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"
- 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) ->
- (CicNotationUtil.boxify p : 'level1_pattern))]];
- Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Slist1
- (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 ("QKEYWORD", "")],
- 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 ("", "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 ("", "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) ->
- (Ast.Opt p : 'l1_magic_pattern));
- [Gramext.Stoken ("", "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) ->
- (Ast.List1 (p, sep) : 'l1_magic_pattern));
- [Gramext.Stoken ("", "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) ->
- (Ast.List0 (p, sep) : 'l1_magic_pattern))]];
- Grammar.Entry.obj
- (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e),
- None,
- [None, None,
- [[Gramext.Stoken ("", "ident"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (Ast.IdentVar id : 'l1_pattern_variable));
- [Gramext.Stoken ("", "number"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (Ast.NumVar id : 'l1_pattern_variable));
- [Gramext.Stoken ("", "term"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (Ast.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 ("LPAREN", "");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (p : 'l1_pattern) _
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (CicNotationUtil.group p) :
- 'l1_simple_pattern));
- [Gramext.Stoken ("", "break")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Layout Ast.Break) : 'l1_simple_pattern));
- [Gramext.Stoken ("", "hovbox"); Gramext.Stoken ("LPAREN", "");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (p : 'l1_pattern) _ _
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc
- (Ast.Layout (Ast.Box ((Ast.HOV, false, false), p))) :
- 'l1_simple_pattern));
- [Gramext.Stoken ("", "hvbox"); Gramext.Stoken ("LPAREN", "");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (p : 'l1_pattern) _ _
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc
- (Ast.Layout (Ast.Box ((Ast.HV, false, false), p))) :
- 'l1_simple_pattern));
- [Gramext.Stoken ("", "vbox"); Gramext.Stoken ("LPAREN", "");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (p : 'l1_pattern) _ _
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc
- (Ast.Layout (Ast.Box ((Ast.V, false, false), p))) :
- 'l1_simple_pattern));
- [Gramext.Stoken ("", "hbox"); Gramext.Stoken ("LPAREN", "");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (p : 'l1_pattern) _ _
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc
- (Ast.Layout (Ast.Box ((Ast.H, false, false), p))) :
- 'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "\\root"); Gramext.Sself;
- Gramext.Stoken ("SYMBOL", "\\of"); Gramext.Sself],
- Gramext.action
- (fun (arg : 'l1_simple_pattern) _ (index : 'l1_simple_pattern) _
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Layout (Ast.Root (arg, 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 (Ast.Layout (Ast.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 (Ast.Layout (Ast.Frac (p1, p2))) :
- 'l1_simple_pattern));
- [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\atop"); Gramext.Sself],
- Gramext.action
- (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Layout (Ast.Atop (p1, p2))) :
- 'l1_simple_pattern));
- [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\over"); Gramext.Sself],
- Gramext.action
- (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Layout (Ast.Over (p1, 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 (Ast.Layout (Ast.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 (Ast.Layout (Ast.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 (Ast.Layout (Ast.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 (Ast.Layout (Ast.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 (Ast.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 (Ast.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 (Ast.Magic m) : 'l1_simple_pattern));
- [Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (i : string) (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Variable (Ast.TermVar i)) :
- 'l1_simple_pattern))]]])
-(* }}} *)
-
-(* {{{ Grammar for ast magics, notation level 2 *)
-let _ =
- Grammar.extend
- (let _ = (level2_meta : 'level2_meta Grammar.Entry.e) in
- let grammar_entry_create s =
- Grammar.Entry.create (Grammar.of_entry level2_meta) s
- in
- let l2_variable : 'l2_variable Grammar.Entry.e =
- grammar_entry_create "l2_variable"
- and l2_magic : 'l2_magic Grammar.Entry.e =
- grammar_entry_create "l2_magic"
- in
- [Grammar.Entry.obj (l2_variable : 'l2_variable Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) (loc : Lexing.position * Lexing.position) ->
- (Ast.TermVar id : 'l2_variable));
- [Gramext.Stoken ("", "anonymous")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (Ast.TermVar "_" : 'l2_variable));
- [Gramext.Stoken ("", "fresh"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (Ast.FreshVar id : 'l2_variable));
- [Gramext.Stoken ("", "ident"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (Ast.IdentVar id : 'l2_variable));
- [Gramext.Stoken ("", "number"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (Ast.NumVar id : 'l2_variable));
- [Gramext.Stoken ("", "term"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (Ast.TermVar id : 'l2_variable))]];
- Grammar.Entry.obj (l2_magic : 'l2_magic Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("", "fail")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (Ast.Fail : 'l2_magic));
- [Gramext.Stoken ("", "if");
- Gramext.Snterm
- (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
- Gramext.Stoken ("", "then");
- Gramext.Snterm
- (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
- Gramext.Stoken ("", "else");
- Gramext.Snterm
- (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
- Gramext.action
- (fun (p_false : 'level2_meta) _ (p_true : 'level2_meta) _
- (p_test : 'level2_meta) _
- (loc : Lexing.position * Lexing.position) ->
- (Ast.If (p_test, p_true, p_false) : 'l2_magic));
- [Gramext.Stoken ("", "default");
- Gramext.Snterm
- (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
- Gramext.Snterm
- (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
- Gramext.action
- (fun (none : 'level2_meta) (some : 'level2_meta) _
- (loc : Lexing.position * Lexing.position) ->
- (Ast.Default (some, none) : 'l2_magic));
- [Gramext.Stoken ("", "fold");
- Gramext.srules
- [[Gramext.Stoken ("", "right")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (`Right : 'e__1));
- [Gramext.Stoken ("", "left")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (`Left : 'e__1))];
- Gramext.Snterm
- (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
- Gramext.Stoken ("", "rec"); Gramext.Stoken ("IDENT", "");
- Gramext.Snterm
- (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
- Gramext.action
- (fun (recursive : 'level2_meta) (id : string) _
- (base : 'level2_meta) (kind : 'e__1) _
- (loc : Lexing.position * Lexing.position) ->
- (Ast.Fold (kind, base, [id], recursive) : 'l2_magic))]];
- Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("UNPARSED_AST", "")],
- Gramext.action
- (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
- (!parse_level2_ast_ref (Ulexing.from_utf8_string blob) :
- 'level2_meta));
- [Gramext.Snterm
- (Grammar.Entry.obj (l2_variable : 'l2_variable Grammar.Entry.e))],
- Gramext.action
- (fun (var : 'l2_variable)
- (loc : Lexing.position * Lexing.position) ->
- (Ast.Variable var : 'level2_meta));
- [Gramext.Snterm
- (Grammar.Entry.obj (l2_magic : 'l2_magic Grammar.Entry.e))],
- Gramext.action
- (fun (magic : 'l2_magic)
- (loc : Lexing.position * Lexing.position) ->
- (Ast.Magic magic : 'level2_meta))]]])
-(* }}} *)
-
-(* {{{ Grammar for ast patterns, notation level 2 *)
-let _ =
- Grammar.extend
- (let _ = (level2_ast : 'level2_ast Grammar.Entry.e)
- and _ = (term : 'term Grammar.Entry.e)
- and _ = (let_defs : 'let_defs Grammar.Entry.e) in
- let grammar_entry_create s =
- Grammar.Entry.create (Grammar.of_entry level2_ast) s
- in
- let 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 meta_substs : 'meta_substs Grammar.Entry.e =
- grammar_entry_create "meta_substs"
- 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 arg : 'arg Grammar.Entry.e = grammar_entry_create "arg"
- and single_arg : 'single_arg Grammar.Entry.e =
- grammar_entry_create "single_arg"
- and induction_kind : 'induction_kind Grammar.Entry.e =
- grammar_entry_create "induction_kind"
- and binder_vars : 'binder_vars Grammar.Entry.e =
- grammar_entry_create "binder_vars"
- in
- [Grammar.Entry.obj (level2_ast : 'level2_ast Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
- Gramext.action
- (fun (p : 'term) (loc : Lexing.position * Lexing.position) ->
- (p : 'level2_ast))]];
- Grammar.Entry.obj (sort : 'sort Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("", "CProp")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (`CProp : 'sort));
- [Gramext.Stoken ("", "Type")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (`Type : 'sort));
- [Gramext.Stoken ("", "Set")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) -> (`Set : 'sort));
- [Gramext.Stoken ("", "Prop")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (`Prop : 'sort))]];
- Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e),
- None,
- [None, None,
- [[Gramext.Stoken ("SYMBOL", "\\subst"); Gramext.Stoken ("SYMBOL", "[");
- Gramext.Slist1sep
- (Gramext.srules
- [[Gramext.Stoken ("IDENT", "");
- Gramext.Stoken ("SYMBOL", "≔");
- Gramext.Snterm
- (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
- Gramext.action
- (fun (t : 'term) _ (i : string)
- (loc : Lexing.position * Lexing.position) ->
- (i, t : 'e__2))],
- Gramext.Stoken ("SYMBOL", ";"));
- Gramext.Stoken ("SYMBOL", "]")],
- Gramext.action
- (fun _ (substs : 'e__2 list) _ _
- (loc : Lexing.position * Lexing.position) ->
- (substs : 'explicit_subst))]];
- Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
- Gramext.action
- (fun (p : 'term) (loc : Lexing.position * Lexing.position) ->
- (Some p : 'meta_subst));
- [Gramext.Stoken ("SYMBOL", "_")],
- Gramext.action
- (fun (s : string) (loc : Lexing.position * Lexing.position) ->
- (None : 'meta_subst))]];
- Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("SYMBOL", "[");
- Gramext.Slist0
- (Gramext.Snterm
- (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e)));
- Gramext.Stoken ("SYMBOL", "]")],
- Gramext.action
- (fun _ (substs : 'meta_subst list) _
- (loc : Lexing.position * Lexing.position) ->
- (substs : 'meta_substs))]];
- Grammar.Entry.obj
- (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e),
- None,
- [None, None,
- [[Gramext.Snterm
- (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e))],
- Gramext.action
- (fun (arg : 'single_arg)
- (loc : Lexing.position * Lexing.position) ->
- (arg, None : 'possibly_typed_name));
- [Gramext.Stoken ("LPAREN", "");
- Gramext.Snterm
- (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", ":");
- Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (typ : 'term) _ (id : 'single_arg) _
- (loc : Lexing.position * Lexing.position) ->
- (id, Some typ : 'possibly_typed_name))]];
- Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e),
- None,
- [None, None,
- [[Gramext.Stoken ("LPAREN", ""); Gramext.Stoken ("IDENT", "");
- Gramext.Slist1
- (Gramext.Snterm
- (Grammar.Entry.obj
- (possibly_typed_name :
- 'possibly_typed_name Grammar.Entry.e)));
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (vars : 'possibly_typed_name list) (id : string) _
- (loc : Lexing.position * Lexing.position) ->
- (id, None, vars : 'match_pattern));
- [Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) (loc : Lexing.position * Lexing.position) ->
- (id, None, [] : '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) ->
- (`Pi : 'binder))]];
- Grammar.Entry.obj (arg : 'arg Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("UNPARSED_META", "")],
- Gramext.action
- (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
- (let meta =
- !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
- in
- match meta with
- Ast.Variable (Ast.FreshVar _) -> [meta], None
- | Ast.Variable (Ast.TermVar "_") ->
- [Ast.Ident ("_", None)], None
- | _ -> failwith "Invalid bound name." :
- 'arg));
- [Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (name : string) (loc : Lexing.position * Lexing.position) ->
- ([Ast.Ident (name, None)], None : 'arg));
- [Gramext.Stoken ("LPAREN", "");
- Gramext.Slist1sep
- (Gramext.Stoken ("IDENT", ""), Gramext.Stoken ("SYMBOL", ","));
- Gramext.Stoken ("SYMBOL", ":");
- Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (ty : 'term) _ (names : string list) _
- (loc : Lexing.position * Lexing.position) ->
- (List.map (fun n -> Ast.Ident (n, None)) names, Some ty :
- 'arg))]];
- Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("UNPARSED_META", "")],
- Gramext.action
- (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
- (let meta =
- !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
- in
- match meta with
- Ast.Variable (Ast.FreshVar _) |
- Ast.Variable (Ast.IdentVar _) ->
- meta
- | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
- | _ -> failwith "Invalid index name." :
- 'single_arg));
- [Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (name : string) (loc : Lexing.position * Lexing.position) ->
- (Ast.Ident (name, None) : 'single_arg))]];
- Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e),
- None,
- [None, None,
- [[Gramext.Stoken ("", "corec")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (`CoInductive : 'induction_kind));
- [Gramext.Stoken ("", "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.Snterm
- (Grammar.Entry.obj
- (single_arg : 'single_arg Grammar.Entry.e));
- Gramext.Slist1
- (Gramext.Snterm
- (Grammar.Entry.obj (arg : 'arg Grammar.Entry.e)));
- Gramext.Sopt
- (Gramext.srules
- [[Gramext.Stoken ("", "on");
- Gramext.Snterm
- (Grammar.Entry.obj
- (single_arg : 'single_arg Grammar.Entry.e))],
- Gramext.action
- (fun (id : 'single_arg) _
- (loc : Lexing.position * Lexing.position) ->
- (id : 'e__3))]);
- Gramext.Sopt
- (Gramext.srules
- [[Gramext.Stoken ("SYMBOL", ":");
- Gramext.Snterm
- (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
- Gramext.action
- (fun (p : 'term) _
- (loc : Lexing.position * Lexing.position) ->
- (p : 'e__4))]);
- Gramext.Stoken ("SYMBOL", "≝");
- Gramext.Snterm
- (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
- Gramext.action
- (fun (body : 'term) _ (ty : 'e__4 option)
- (index_name : 'e__3 option) (args : 'arg list)
- (name : 'single_arg)
- (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
- [] ->
- Ast.fail loc
- (sprintf "Argument %s not found"
- (CicNotationPp.pp_term 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 index_name -> find_arg index_name 0 args
- in
- (name, ty), body, index :
- 'e__5))],
- Gramext.Stoken ("", "and"))],
- Gramext.action
- (fun (defs : 'e__5 list)
- (loc : Lexing.position * Lexing.position) ->
- (defs : 'let_defs))]];
- Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("LPAREN", "");
- Gramext.srules
- [[Gramext.Stoken ("SYMBOL", "_")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- ([Ast.Ident ("_", None)] : 'e__8));
- [Gramext.Slist1sep
- (Gramext.Snterm
- (Grammar.Entry.obj
- (single_arg : 'single_arg Grammar.Entry.e)),
- Gramext.Stoken ("SYMBOL", ","))],
- Gramext.action
- (fun (l : 'single_arg list)
- (loc : Lexing.position * Lexing.position) ->
- (l : 'e__8))];
- Gramext.Sopt
- (Gramext.srules
- [[Gramext.Stoken ("SYMBOL", ":");
- Gramext.Snterm
- (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
- Gramext.action
- (fun (t : 'term) _
- (loc : Lexing.position * Lexing.position) ->
- (t : 'e__9))]);
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (typ : 'e__9 option) (vars : 'e__8) _
- (loc : Lexing.position * Lexing.position) ->
- (vars, typ : 'binder_vars));
- [Gramext.srules
- [[Gramext.Stoken ("SYMBOL", "_")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- ([Ast.Ident ("_", None)] : 'e__6));
- [Gramext.Slist1sep
- (Gramext.Snterm
- (Grammar.Entry.obj
- (single_arg : 'single_arg Grammar.Entry.e)),
- Gramext.Stoken ("SYMBOL", ","))],
- Gramext.action
- (fun (l : 'single_arg list)
- (loc : Lexing.position * Lexing.position) ->
- (l : 'e__6))];
- Gramext.Sopt
- (Gramext.srules
- [[Gramext.Stoken ("SYMBOL", ":");
- Gramext.Snterm
- (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
- Gramext.action
- (fun (t : 'term) _
- (loc : Lexing.position * Lexing.position) ->
- (t : 'e__7))])],
- Gramext.action
- (fun (typ : 'e__7 option) (vars : 'e__6)
- (loc : Lexing.position * Lexing.position) ->
- (vars, typ : 'binder_vars))]];
- Grammar.Entry.obj (term : 'term Grammar.Entry.e),
- Some (Gramext.Level "10N"),
- [None, None,
- [[Gramext.Stoken ("", "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 ("", "in"); Gramext.Sself],
- Gramext.action
- (fun (body : 'term) _ (defs : 'let_defs) (k : 'induction_kind) _
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.LetRec (k, defs, body)) : 'term));
- [Gramext.Stoken ("", "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 : 'term) _ (p1 : 'term) _ (var : 'possibly_typed_name) _
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.LetIn (var, p1, p2)) : 'term))]];
- Grammar.Entry.obj (term : 'term Grammar.Entry.e),
- Some (Gramext.Level "20R"),
- [None, None,
- [[Gramext.Stoken ("SYMBOL", "∃");
- Gramext.Snterm
- (Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
- Gramext.action
- (fun (body : 'term) _ (vars, typ : 'binder_vars) _
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (fold_exists vars typ body) : 'term));
- [Gramext.Snterm
- (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
- Gramext.Snterm
- (Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
- Gramext.action
- (fun (body : 'term) _ (vars, typ : 'binder_vars) (b : 'binder)
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (fold_cluster b vars typ body) : 'term))]];
- Grammar.Entry.obj (term : 'term Grammar.Entry.e),
- Some (Gramext.Level "70L"),
- [None, None,
- [[Gramext.Sself; Gramext.Sself],
- Gramext.action
- (fun (p2 : 'term) (p1 : 'term)
- (loc : Lexing.position * Lexing.position) ->
- (let rec aux =
- function
- Ast.Appl (hd :: tl) |
- Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->
- aux hd @ tl
- | term -> [term]
- in
- return_term loc (Ast.Appl (aux p1 @ [p2])) :
- 'term))]];
- Grammar.Entry.obj (term : 'term Grammar.Entry.e),
- Some (Gramext.Level "90N"),
- [None, None,
- [[Gramext.Stoken ("UNPARSED_META", "")],
- Gramext.action
- (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
- (!parse_level2_meta_ref (Ulexing.from_utf8_string blob) :
- 'term));
- [Gramext.Stoken ("LPAREN", ""); Gramext.Sself;
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (p : 'term) _ (loc : Lexing.position * Lexing.position) ->
- (p : 'term));
- [Gramext.Stoken ("LPAREN", ""); Gramext.Sself;
- Gramext.Stoken ("SYMBOL", ":"); Gramext.Sself;
- Gramext.Stoken ("RPAREN", "")],
- Gramext.action
- (fun _ (p2 : 'term) _ (p1 : 'term) _
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Cast (p1, p2)) : 'term));
- [Gramext.Sopt
- (Gramext.srules
- [[Gramext.Stoken ("SYMBOL", "[");
- Gramext.Snterm
- (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "]")],
- Gramext.action
- (fun _ (ty : 'term) _
- (loc : Lexing.position * Lexing.position) ->
- (ty : 'e__10))]);
- Gramext.Stoken ("", "match"); Gramext.Sself;
- Gramext.Sopt
- (Gramext.srules
- [[Gramext.Stoken ("", "in"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _
- (loc : Lexing.position * Lexing.position) ->
- (id, None : 'e__11))]);
- Gramext.Stoken ("", "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 (term : 'term Grammar.Entry.e))],
- Gramext.action
- (fun (rhs : 'term) _ (lhs : 'match_pattern)
- (loc : Lexing.position * Lexing.position) ->
- (lhs, rhs : 'e__12))],
- Gramext.Stoken ("SYMBOL", "|"));
- Gramext.Stoken ("SYMBOL", "]")],
- Gramext.action
- (fun _ (patterns : 'e__12 list) _ _ (indty_ident : 'e__11 option)
- (t : 'term) _ (outtyp : 'e__10 option)
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Case (t, indty_ident, outtyp, patterns)) :
- 'term));
- [Gramext.Snterm (Grammar.Entry.obj (sort : 'sort Grammar.Entry.e))],
- Gramext.action
- (fun (s : 'sort) (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Sort s) : 'term));
- [Gramext.Stoken ("META", "");
- Gramext.Snterm
- (Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e))],
- Gramext.action
- (fun (s : 'meta_substs) (m : string)
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Meta (int_of_string m, s)) : 'term));
- [Gramext.Stoken ("META", "")],
- Gramext.action
- (fun (m : string) (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Meta (int_of_string m, [])) : 'term));
- [Gramext.Stoken ("PLACEHOLDER", "")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (return_term loc Ast.UserInput : 'term));
- [Gramext.Stoken ("IMPLICIT", "")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (return_term loc Ast.Implicit : 'term));
- [Gramext.Stoken ("NUMBER", "")],
- Gramext.action
- (fun (n : string) (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Num (n, 0)) : 'term));
- [Gramext.Stoken ("URI", "")],
- Gramext.action
- (fun (u : string) (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Uri (u, None)) : 'term));
- [Gramext.Stoken ("CSYMBOL", "")],
- Gramext.action
- (fun (s : string) (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Symbol (s, 0)) : 'term));
- [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 (Ast.Ident (id, Some s)) : 'term));
- [Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ast.Ident (id, None)) : 'term))]]])
-(* }}} *)
-
-(** {2 API implementation} *)
-
-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_level1_pattern lexbuf =
- CicNotationLexer.set_lexbuf lexbuf;
- exc_located_wrapper
- (fun () -> Grammar.Entry.parse level1_pattern Stream.sempty)
-
-let parse_level2_ast lexbuf =
- CicNotationLexer.set_lexbuf lexbuf;
- exc_located_wrapper (fun () -> Grammar.Entry.parse level2_ast Stream.sempty)
-
-let parse_level2_meta lexbuf =
- CicNotationLexer.set_lexbuf lexbuf;
- exc_located_wrapper
- (fun () -> Grammar.Entry.parse level2_meta Stream.sempty)
-
-let _ =
- parse_level1_pattern_ref := parse_level1_pattern;
- parse_level2_ast_ref := parse_level2_ast;
- parse_level2_meta_ref := parse_level2_meta
-
-(** {2 Debugging} *)
-
-let print_l2_pattern () =
- Grammar.print_entry Format.std_formatter (Grammar.Entry.obj term);
- Format.pp_print_flush Format.std_formatter ();
- flush stdout
-
-(* vim:set encoding=utf8 foldmethod=marker: *)
projects / helm.git / blobdiff