From: Stefano Zacchiroli Date: Wed, 21 Sep 2005 14:38:27 +0000 (+0000) Subject: rebuilt X-Git-Tag: LAST_BEFORE_NEW~66 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fa8d47ad95242f20e1c106f36e2dc83001b18b43;p=helm.git rebuilt --- diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml index 5c73d2b4c..9d0b57940 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml @@ -24,57 +24,57 @@ *) oopen Printf -oopen CicNotationEnvoopen CicNotationPt +mmodule Ast = CicNotationPtmmodule Env = CicNotationEnv eexception Parse_error of Token.flocation * stringeexception Level_not_found of int -llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer -llet min_precedence = 0llet max_precedence = 100llet default_precedence = 50 -llet level1_pattern = Grammar.Entry.create grammar "level1_pattern"llet level2_pattern = Grammar.Entry.create grammar "level2_pattern"llet level3_term = Grammar.Entry.create grammar "level3_term"llet l2_pattern = Grammar.Entry.create grammar "l2_pattern"llet notation = Grammar.Entry.create grammar "notation"(* level1 <-> level 2 *) -llet interpretation = Grammar.Entry.create grammar "interpretation"(* level2 <-> level 3 *) -llet phrase = Grammar.Entry.create grammar "phrase" +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 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) (** {2 Grammar extension} *) -llet symbol s = Gramext.Stoken ("SYMBOL", s)llet ident s = Gramext.Stoken ("IDENT", s)llet number s = Gramext.Stoken ("NUMBER", s)llet term = Gramext.Sself -llet g_symbol_of_literal = +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 -> symbol s - | `Keyword s -> ident s - | `Number s -> number s + `Symbol s -> gram_symbol s + | `Keyword s -> gram_keyword s + | `Number s -> gram_number s ttype binding = NoBinding - | Binding of string * value_type - | Env of (string * value_type) list + | Binding of string * Env.value_type + | Env of (string * Env.value_type) list llet make_action action bindings = - let rec aux (vl : env_type) = + let rec aux (vl : CicNotationEnv.t) = function - [] -> Gramext.action (fun (loc : location) -> action vl loc) + [] -> Gramext.action (fun (loc : Ast.location) -> action vl loc) | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl) - | Binding (name, TermType) :: tl -> + | Binding (name, Env.TermType) :: tl -> Gramext.action - (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl) - | Binding (name, StringType) :: tl -> + (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, (StringType, StringValue v)) :: vl) tl) - | Binding (name, NumType) :: tl -> + aux ((name, (Env.StringType, Env.StringValue v)) :: vl) tl) + | Binding (name, Env.NumType) :: tl -> Gramext.action - (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl) - | Binding (name, OptType t) :: tl -> + (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, (OptType t, OptValue v)) :: vl) tl) - | Binding (name, ListType t) :: tl -> + aux ((name, (Env.OptType t, Env.OptValue v)) :: vl) tl) + | Binding (name, Env.ListType t) :: tl -> Gramext.action (fun (v : 'a list) -> - aux ((name, (ListType t, ListValue v)) :: vl) tl) - | Env _ :: tl -> Gramext.action (fun (v : env_type) -> aux (v @ vl) tl) + 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 = @@ -86,169 +86,191 @@ llet flatten_opt = | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl in aux [] - (* given a level 1 pattern computes the new RHS of "term" grammar entry *) -let extract_term_production pattern = +llet extract_term_production pattern = let rec aux = function - AttributedTerm (_, t) -> aux t - | Literal l -> aux_literal l - | Layout l -> aux_layout l - | Magic m -> aux_magic m - | Variable v -> aux_variable v - | t -> - prerr_endline (CicNotationPp.pp_term t); - assert false + 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, symbol s] - | `Keyword s -> [NoBinding, ident s] - | `Number s -> [NoBinding, number s] + `Symbol s -> [NoBinding, gram_symbol s] + | `Keyword s -> [NoBinding, gram_keyword s] + | `Number s -> [NoBinding, gram_number s] and aux_layout = function - Sub (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUB"] @ aux p2 - | Sup (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUP"] @ aux p2 - | Below (p1, p2) -> aux p1 @ [NoBinding, symbol "\\BELOW"] @ aux p2 - | Above (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ABOVE"] @ aux p2 - | Frac (p1, p2) -> aux p1 @ [NoBinding, symbol "\\FRAC"] @ aux p2 - | Atop (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ATOP"] @ aux p2 - | Over (p1, p2) -> aux p1 @ [NoBinding, symbol "\\OVER"] @ aux p2 - | Root (p1, p2) -> - [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"] @ - aux p1 - | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p -(* | Break -> [] *) - | Box (_, pl) -> List.flatten (List.map aux pl) + 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 - Opt p -> + Ast.Opt p -> let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in - let action (env_opt : env_type option) (loc : location) = + let action (env_opt : CicNotationEnv.t option) (loc : Ast.location) = match env_opt with - Some env -> List.map opt_binding_some env - | None -> List.map opt_binding_of_name p_names + Some env -> List.map Env.opt_binding_some env + | None -> List.map Env.opt_binding_of_name p_names in - [Env (List.map opt_declaration p_names), + [Env (List.map Env.opt_declaration p_names), Gramext.srules [[Gramext.Sopt (Gramext.srules [p_atoms, p_action])], Gramext.action action]] - | List0 (p, _) | List1 (p, _) -> + | Ast.List0 (p, _) | Ast.List1 (p, _) -> let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in - let env0 = List.map list_binding_of_name p_names in - let grow_env_entry env n v = - List.map - (function - n', (ty, ListValue vl) as entry -> - if n' = n then n', (ty, ListValue (v :: vl)) else entry - | _ -> assert false) - env - in - let grow_env env_i env = - List.fold_left (fun env (n, (_, v)) -> grow_env_entry env n v) env - env_i + let action (env_list : CicNotationEnv.t list) (loc : Ast.location) = + CicNotationEnv.coalesce_env p_names env_list in - let action (env_list : env_type list) (loc : location) = - List.fold_right grow_env env_list env0 - in - let g_symbol s = + let gram_of_list s = match magic with - List0 (_, None) -> Gramext.Slist0 s - | List1 (_, None) -> Gramext.Slist1 s - | List0 (_, Some l) -> Gramext.Slist0sep (s, g_symbol_of_literal l) - | List1 (_, Some l) -> Gramext.Slist1sep (s, g_symbol_of_literal l) + 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 list_declaration p_names), + [Env (List.map Env.list_declaration p_names), Gramext.srules - [[g_symbol (Gramext.srules [p_atoms, p_action])], + [[gram_of_list (Gramext.srules [p_atoms, p_action])], Gramext.action action]] | _ -> assert false and aux_variable = function - NumVar s -> [Binding (s, NumType), number ""] - | TermVar s -> [Binding (s, TermType), term] - | IdentVar s -> [Binding (s, StringType), ident ""] - | Ascription (p, s) -> assert false - | FreshVar _ -> assert false + 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 : env_type) (loc : location) -> env) + 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_int precedence = +let level_of precedence associativity = if precedence < min_precedence || precedence > max_precedence then raise (Level_not_found precedence); - string_of_int 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 -let extend level1_pattern ?(precedence = default_precedence) = - fun ?associativity action -> - let (p_bindings, p_atoms) = - List.split (extract_term_production level1_pattern) - in - let level = level_of_int precedence in - let p_names = flatten_opt p_bindings in - let _ = - Grammar.extend - [Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e), - Some (Gramext.Level level), - [None, associativity, - [p_atoms, - make_action - (fun (env : env_type) (loc : location) -> action env loc) - p_bindings]]] - in - p_atoms + (* 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 atoms = Grammar.delete_rule l2_pattern atoms +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 boxify = - function - [a] -> a - | l -> Layout (Box (H, l)) +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 = - let fold_cluster binder terms ty body = - List.fold_right (fun term body -> Binder (binder, (term, ty), body)) terms - body - in List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body) pt_names body -let return_term loc term = AttributedTerm (`Loc loc, term) +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), None, []) :: acc) (i - 1) + | 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 (l2_pattern : 'a Grammar.Entry.e), None, + [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) - and _ = (level2_pattern : 'level2_pattern Grammar.Entry.e) - and _ = (level3_term : 'level3_term Grammar.Entry.e) - and _ = (l2_pattern : 'l2_pattern Grammar.Entry.e) - and _ = (notation : 'notation Grammar.Entry.e) - and _ = (interpretation : 'interpretation Grammar.Entry.e) - and _ = (phrase : 'phrase Grammar.Entry.e) in + (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e) in let grammar_entry_create s = Grammar.Entry.create (Grammar.of_entry level1_pattern) s in @@ -262,47 +284,17 @@ let _ = 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 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 bound_name : 'bound_name Grammar.Entry.e = - grammar_entry_create "bound_name" - 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 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_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))], + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("EOI", "")], Gramext.action - (fun (p : 'l1_simple_pattern) + (fun _ (p : 'l1_pattern) (loc : Lexing.position * Lexing.position) -> - (p : 'level1_pattern))]]; + (CicNotationUtil.boxify p : 'level1_pattern))]]; Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None, [None, None, [[Gramext.Slist1 @@ -319,7 +311,7 @@ let _ = Gramext.action (fun (n : string) (loc : Lexing.position * Lexing.position) -> (`Number n : 'literal)); - [Gramext.Stoken ("KEYWORD", "")], + [Gramext.Stoken ("QKEYWORD", "")], Gramext.action (fun (k : string) (loc : Lexing.position * Lexing.position) -> (`Keyword k : 'literal)); @@ -329,7 +321,7 @@ let _ = (`Symbol s : 'literal))]]; Grammar.Entry.obj (sep : 'sep Grammar.Entry.e), None, [None, None, - [[Gramext.Stoken ("SYMBOL", "\\SEP"); + [[Gramext.Stoken ("", "sep"); Gramext.Snterm (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))], Gramext.action @@ -339,15 +331,15 @@ let _ = (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e), None, [None, None, - [[Gramext.Stoken ("SYMBOL", "\\OPT"); + [[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) -> - (Opt p : 'l1_magic_pattern)); - [Gramext.Stoken ("SYMBOL", "\\LIST1"); + (Ast.Opt p : 'l1_magic_pattern)); + [Gramext.Stoken ("", "list1"); Gramext.Snterm (Grammar.Entry.obj (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)); @@ -356,8 +348,8 @@ let _ = 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"); + (Ast.List1 (p, sep) : 'l1_magic_pattern)); + [Gramext.Stoken ("", "list0"); Gramext.Snterm (Grammar.Entry.obj (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)); @@ -366,153 +358,319 @@ let _ = Gramext.action (fun (sep : 'sep option) (p : 'l1_simple_pattern) _ (loc : Lexing.position * Lexing.position) -> - (List0 (p, sep) : 'l1_magic_pattern))]]; + (Ast.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.Stoken ("", "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", "")], + (Ast.IdentVar id : 'l1_pattern_variable)); + [Gramext.Stoken ("", "number"); 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", "")], + (Ast.NumVar id : 'l1_pattern_variable)); + [Gramext.Stoken ("", "term"); Gramext.Stoken ("IDENT", "")], Gramext.action (fun (id : string) _ (loc : Lexing.position * Lexing.position) -> - (TermVar id : 'l1_pattern_variable))]]; + (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.Sself; Gramext.Stoken ("SYMBOL", "\\AS"); - Gramext.Stoken ("IDENT", "")], + [[Gramext.Stoken ("LPAREN", ""); + Gramext.Snterm + (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e)); + Gramext.Stoken ("RPAREN", "")], Gramext.action - (fun (id : string) _ (p : 'l1_simple_pattern) + (fun _ (p : 'l1_pattern) _ (loc : Lexing.position * Lexing.position) -> - (return_term loc (Variable (Ascription (p, id))) : + (return_term loc (CicNotationUtil.group p) : 'l1_simple_pattern)); - [Gramext.Stoken ("DELIM", "\\["); + [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 ("DELIM", "\\]")], + Gramext.Stoken ("RPAREN", "")], Gramext.action - (fun _ (p : 'l1_pattern) _ + (fun _ (p : 'l1_pattern) _ _ (loc : Lexing.position * Lexing.position) -> - (return_term loc (boxify p) : 'l1_simple_pattern)); - [Gramext.Stoken ("SYMBOL", "\\BREAK")], + (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 _ (loc : Lexing.position * Lexing.position) -> - (return_term loc (Layout Break) : 'l1_simple_pattern)); - [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("DELIM", "\\["); + (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 ("DELIM", "\\]")], + Gramext.Stoken ("RPAREN", "")], 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 ("DELIM", "\\["); + (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 ("DELIM", "\\]")], + Gramext.Stoken ("RPAREN", "")], 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.Sself; - Gramext.Stoken ("SYMBOL", "\\OF"); Gramext.Sself], + (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 (Layout (Root (arg, index))) : + (return_term loc (Ast.Layout (Ast.Root (arg, index))) : 'l1_simple_pattern)); - [Gramext.Stoken ("SYMBOL", "\\SQRT"); Gramext.Sself], + [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], + (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 (Layout (Frac (p1, p2))) : 'l1_simple_pattern)); - [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ATOP"); Gramext.Sself], + (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 (Layout (Atop (p1, p2))) : 'l1_simple_pattern)); - [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\OVER"); Gramext.Sself], + (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 (Layout (Over (p1, p2))) : 'l1_simple_pattern)); - [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself], + (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 (Layout (Above (p1, p2))) : + (return_term loc (Ast.Layout (Ast.Above (p1, p2))) : 'l1_simple_pattern)); - [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\BELOW"); Gramext.Sself], + [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))) : + (return_term loc (Ast.Layout (Ast.Below (p1, p2))) : 'l1_simple_pattern)); - [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUP"); Gramext.Sself], + [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], + (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 (Layout (Sub (p1, p2))) : 'l1_simple_pattern))]; + (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 (Literal l) : 'l1_simple_pattern)); + (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 (Variable v) : 'l1_simple_pattern)); + (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 (Magic m) : 'l1_simple_pattern)); + (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 (Ident (i, None)) : 'l1_simple_pattern))]]; - Grammar.Entry.obj (level2_pattern : 'level2_pattern Grammar.Entry.e), - None, + (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.Snterm - (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))], + [[Gramext.Stoken ("IDENT", "")], Gramext.action - (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) -> - (p : 'level2_pattern))]]; + (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 ("SYMBOL", "\\TYPE")], + [[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 ("SYMBOL", "\\SET")], + [Gramext.Stoken ("", "Set")], Gramext.action (fun _ (loc : Lexing.position * Lexing.position) -> (`Set : 'sort)); - [Gramext.Stoken ("SYMBOL", "\\PROP")], + [Gramext.Stoken ("", "Prop")], Gramext.action (fun _ (loc : Lexing.position * Lexing.position) -> (`Prop : 'sort))]]; @@ -525,24 +683,22 @@ let _ = [[Gramext.Stoken ("IDENT", ""); Gramext.Stoken ("SYMBOL", "≔"); Gramext.Snterm - (Grammar.Entry.obj - (l2_pattern : 'l2_pattern Grammar.Entry.e))], + (Grammar.Entry.obj (term : 'term Grammar.Entry.e))], Gramext.action - (fun (t : 'l2_pattern) _ (i : string) + (fun (t : 'term) _ (i : string) (loc : Lexing.position * Lexing.position) -> - (i, t : 'e__1))], + (i, t : 'e__2))], Gramext.Stoken ("SYMBOL", ";")); Gramext.Stoken ("SYMBOL", "]")], Gramext.action - (fun _ (substs : 'e__1 list) _ _ + (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 (l2_pattern : 'l2_pattern Grammar.Entry.e))], + [[Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e))], Gramext.action - (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) -> + (fun (p : 'term) (loc : Lexing.position * Lexing.position) -> (Some p : 'meta_subst)); [Gramext.Stoken ("SYMBOL", "_")], Gramext.action @@ -564,39 +720,39 @@ let _ = None, [None, None, [[Gramext.Snterm - (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e))], + (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e))], Gramext.action - (fun (id : 'bound_name) (loc : Lexing.position * Lexing.position) -> - (id, None : 'possibly_typed_name)); - [Gramext.Stoken ("SYMBOL", "("); + (fun (arg : 'single_arg) + (loc : Lexing.position * Lexing.position) -> + (arg, None : 'possibly_typed_name)); + [Gramext.Stoken ("LPAREN", ""); Gramext.Snterm - (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e)); + (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e)); Gramext.Stoken ("SYMBOL", ":"); - Gramext.Snterm - (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e)); - Gramext.Stoken ("SYMBOL", ")")], + Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e)); + Gramext.Stoken ("RPAREN", "")], Gramext.action - (fun _ (typ : 'l2_pattern) _ (id : 'bound_name) _ + (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 ("SYMBOL", "("); Gramext.Stoken ("IDENT", ""); + [[Gramext.Stoken ("LPAREN", ""); Gramext.Stoken ("IDENT", ""); Gramext.Slist1 (Gramext.Snterm (Grammar.Entry.obj (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e))); - Gramext.Stoken ("SYMBOL", ")")], + Gramext.Stoken ("RPAREN", "")], Gramext.action (fun _ (vars : 'possibly_typed_name list) (id : string) _ (loc : Lexing.position * Lexing.position) -> - (id, vars : 'match_pattern)); + (id, None, vars : 'match_pattern)); [Gramext.Stoken ("IDENT", "")], Gramext.action (fun (id : string) (loc : Lexing.position * Lexing.position) -> - (id, [] : 'match_pattern))]]; + (id, None, [] : 'match_pattern))]]; Grammar.Entry.obj (binder : 'binder Grammar.Entry.e), None, [None, None, [[Gramext.Stoken ("SYMBOL", "λ")], @@ -607,79 +763,66 @@ let _ = 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_name : 'bound_name Grammar.Entry.e), None, + Grammar.Entry.obj (arg : 'arg Grammar.Entry.e), None, [None, None, - [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")], + [[Gramext.Stoken ("UNPARSED_META", "")], Gramext.action - (fun (i : string) _ (loc : Lexing.position * Lexing.position) -> - (Variable (FreshVar i) : 'bound_name)); + (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 (i : string) (loc : Lexing.position * Lexing.position) -> - (Ident (i, None) : 'bound_name))]]; - Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e), None, - [None, None, - [[Gramext.Slist1 - (Gramext.srules - [[Gramext.Stoken ("SYMBOL", "("); - Gramext.Slist1sep - (Gramext.Snterm - (Grammar.Entry.obj - (bound_name : 'bound_name Grammar.Entry.e)), - 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__3))]); - Gramext.Stoken ("SYMBOL", ")")], - Gramext.action - (fun _ (ty : 'e__3 option) (vars : 'bound_name list) _ - (loc : Lexing.position * Lexing.position) -> - (vars, ty : 'e__4))])], + (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 (clusters : 'e__4 list) + (fun _ (ty : 'term) _ (names : string list) _ (loc : Lexing.position * Lexing.position) -> - (clusters : 'bound_names)); - [Gramext.Slist1sep - (Gramext.Snterm - (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e)), - 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))])], + (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 (ty : 'e__2 option) (vars : 'bound_name list) - (loc : Lexing.position * Lexing.position) -> - ([vars, ty] : 'bound_names))]]; + (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 ("IDENT", "corec")], + [[Gramext.Stoken ("", "corec")], Gramext.action (fun _ (loc : Lexing.position * Lexing.position) -> (`CoInductive : 'induction_kind)); - [Gramext.Stoken ("IDENT", "rec")], + [Gramext.Stoken ("", "rec")], Gramext.action (fun _ (loc : Lexing.position * Lexing.position) -> (`Inductive : 'induction_kind))]]; @@ -689,38 +832,36 @@ let _ = (Gramext.srules [[Gramext.Snterm (Grammar.Entry.obj - (bound_name : 'bound_name Grammar.Entry.e)); - Gramext.Snterm - (Grammar.Entry.obj - (bound_names : 'bound_names Grammar.Entry.e)); + (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 ("IDENT", "on"); + [[Gramext.Stoken ("", "on"); Gramext.Snterm (Grammar.Entry.obj - (bound_name : 'bound_name Grammar.Entry.e))], + (single_arg : 'single_arg Grammar.Entry.e))], Gramext.action - (fun (id : 'bound_name) _ + (fun (id : 'single_arg) _ (loc : Lexing.position * Lexing.position) -> - (id : 'e__5))]); + (id : 'e__3))]); Gramext.Sopt (Gramext.srules [[Gramext.Stoken ("SYMBOL", ":"); Gramext.Snterm - (Grammar.Entry.obj - (l2_pattern : 'l2_pattern Grammar.Entry.e))], + (Grammar.Entry.obj (term : 'term Grammar.Entry.e))], Gramext.action - (fun (p : 'l2_pattern) _ + (fun (p : 'term) _ (loc : Lexing.position * Lexing.position) -> - (p : 'e__6))]); + (p : 'e__4))]); Gramext.Stoken ("SYMBOL", "≝"); Gramext.Snterm - (Grammar.Entry.obj - (l2_pattern : 'l2_pattern Grammar.Entry.e))], + (Grammar.Entry.obj (term : 'term Grammar.Entry.e))], Gramext.action - (fun (body : 'l2_pattern) _ (ty : 'e__6 option) - (index_name : 'e__5 option) (args : 'bound_names) - (name : 'bound_name) + (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 = @@ -737,7 +878,7 @@ let _ = let rec find_arg name n = function [] -> - fail loc + Ast.fail loc (sprintf "Argument %s not found" (CicNotationPp.pp_term name)) | (l, _) :: tl -> @@ -748,174 +889,172 @@ let _ = let index = match index_name with None -> 0 - | Some name -> find_arg name 0 args + | Some index_name -> find_arg index_name 0 args in (name, ty), body, index : - 'e__7))], - Gramext.Stoken ("IDENT", "and"))], + 'e__5))], + Gramext.Stoken ("", "and"))], Gramext.action - (fun (defs : 'e__7 list) + (fun (defs : 'e__5 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, + Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e), None, [None, None, - [[Gramext.Stoken ("SYMBOL", "\\DEFAULT"); - Gramext.Stoken ("DELIM", "\\["); - Gramext.Snterm - (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e)); - Gramext.Stoken ("DELIM", "\\]"); Gramext.Stoken ("DELIM", "\\["); - Gramext.Snterm - (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e)); - Gramext.Stoken ("DELIM", "\\]")], - 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.Stoken ("LPAREN", ""); Gramext.srules - [[Gramext.Stoken ("IDENT", "right")], + [[Gramext.Stoken ("SYMBOL", "_")], Gramext.action (fun _ (loc : Lexing.position * Lexing.position) -> - (`Right : 'e__8)); - [Gramext.Stoken ("IDENT", "left")], + ([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) -> - (`Left : 'e__8))]; - Gramext.Stoken ("DELIM", "\\["); - Gramext.Snterm - (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e)); - Gramext.Stoken ("DELIM", "\\]"); - Gramext.Stoken ("SYMBOL", "\\LAMBDA"); Gramext.Stoken ("IDENT", ""); - Gramext.Stoken ("DELIM", "\\["); - Gramext.Snterm - (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e)); - Gramext.Stoken ("DELIM", "\\]")], + ([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 _ (recursive : 'l2_pattern) _ (id : string) _ _ - (base : 'l2_pattern) _ (kind : 'e__8) _ + (fun (typ : 'e__7 option) (vars : 'e__6) (loc : Lexing.position * Lexing.position) -> - (Fold (kind, base, [id], recursive) : 'l2_magic_pattern))]]; - Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), - Some (Gramext.Level "10"), - [Some "10", Some Gramext.NonA, - [[Gramext.Stoken ("IDENT", "let"); + (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 ("IDENT", "in"); Gramext.Sself], + Gramext.Stoken ("", "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"); + (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 : 'l2_pattern) _ (p1 : 'l2_pattern) _ - (var : 'possibly_typed_name) _ + (fun (p2 : 'term) _ (p1 : 'term) _ (var : 'possibly_typed_name) _ (loc : Lexing.position * Lexing.position) -> - (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))]]; - Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), - Some (Gramext.Level "20"), - [Some "20", Some Gramext.RightA, - [[Gramext.Snterm + (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 (bound_names : 'bound_names Grammar.Entry.e)); + (Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e)); Gramext.Stoken ("SYMBOL", "."); Gramext.Sself], Gramext.action - (fun (body : 'l2_pattern) _ (names : 'bound_names) (b : 'binder) + (fun (body : 'term) _ (vars, typ : 'binder_vars) (b : 'binder) (loc : Lexing.position * Lexing.position) -> - (return_term loc (fold_binder b names body) : 'l2_pattern))]]; - Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), - Some (Gramext.Level "70"), - [Some "70", Some Gramext.LeftA, + (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 : 'l2_pattern) (p1 : 'l2_pattern) + (fun (p2 : 'term) (p1 : 'term) (loc : Lexing.position * Lexing.position) -> (let rec aux = function - Appl (hd :: tl) | AttributedTerm (_, Appl (hd :: tl)) -> + Ast.Appl (hd :: tl) | + Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) -> aux hd @ tl | term -> [term] in - return_term loc (Appl (aux p1 @ [p2])) : - 'l2_pattern))]]; - Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), - Some (Gramext.Level "90"), - [Some "90", 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))], + 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 (v : 'l2_pattern_variable) - (loc : Lexing.position * Lexing.position) -> - (return_term loc (Variable v) : 'l2_pattern)); - [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself; - Gramext.Stoken ("SYMBOL", ")")], + (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 : 'l2_pattern) _ - (loc : Lexing.position * Lexing.position) -> - (p : 'l2_pattern)); - [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself; + (fun _ (p : 'term) _ (loc : Lexing.position * Lexing.position) -> + (p : 'term)); + [Gramext.Stoken ("LPAREN", ""); Gramext.Sself; Gramext.Stoken ("SYMBOL", ":"); Gramext.Sself; - Gramext.Stoken ("SYMBOL", ")")], + Gramext.Stoken ("RPAREN", "")], Gramext.action - (fun _ (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _ + (fun _ (p2 : 'term) _ (p1 : 'term) _ (loc : Lexing.position * Lexing.position) -> - (return_term loc (Appl [Symbol ("cast", 0); p1; p2]) : - 'l2_pattern)); + (return_term loc (Ast.Cast (p1, p2)) : 'term)); [Gramext.Sopt (Gramext.srules [[Gramext.Stoken ("SYMBOL", "["); Gramext.Snterm - (Grammar.Entry.obj - (l2_pattern : 'l2_pattern Grammar.Entry.e)); + (Grammar.Entry.obj (term : 'term Grammar.Entry.e)); Gramext.Stoken ("SYMBOL", "]")], Gramext.action - (fun _ (ty : 'l2_pattern) _ + (fun _ (ty : 'term) _ (loc : Lexing.position * Lexing.position) -> - (ty : 'e__9))]); - Gramext.Stoken ("IDENT", "match"); Gramext.Sself; + (ty : 'e__10))]); + Gramext.Stoken ("", "match"); Gramext.Sself; Gramext.Sopt (Gramext.srules - [[Gramext.Stoken ("SYMBOL", ":"); Gramext.Stoken ("IDENT", "")], + [[Gramext.Stoken ("", "in"); Gramext.Stoken ("IDENT", "")], Gramext.action (fun (id : string) _ (loc : Lexing.position * Lexing.position) -> - (id : 'e__10))]); - Gramext.Stoken ("IDENT", "with"); Gramext.Stoken ("SYMBOL", "["); + (id, None : 'e__11))]); + Gramext.Stoken ("", "with"); Gramext.Stoken ("SYMBOL", "["); Gramext.Slist0sep (Gramext.srules [[Gramext.Snterm @@ -923,47 +1062,54 @@ let _ = (match_pattern : 'match_pattern Grammar.Entry.e)); Gramext.Stoken ("SYMBOL", "⇒"); Gramext.Snterm - (Grammar.Entry.obj - (l2_pattern : 'l2_pattern Grammar.Entry.e))], + (Grammar.Entry.obj (term : 'term Grammar.Entry.e))], Gramext.action - (fun (rhs : 'l2_pattern) _ (lhs : 'match_pattern) + (fun (rhs : 'term) _ (lhs : 'match_pattern) (loc : Lexing.position * Lexing.position) -> - (lhs, rhs : 'e__11))], + (lhs, rhs : 'e__12))], Gramext.Stoken ("SYMBOL", "|")); Gramext.Stoken ("SYMBOL", "]")], Gramext.action - (fun _ (patterns : 'e__11 list) _ _ (indty_ident : 'e__10 option) - (t : 'l2_pattern) _ (outtyp : 'e__9 option) + (fun _ (patterns : 'e__12 list) _ _ (indty_ident : 'e__11 option) + (t : 'term) _ (outtyp : 'e__10 option) (loc : Lexing.position * Lexing.position) -> - (return_term loc (Case (t, indty_ident, outtyp, patterns)) : - 'l2_pattern)); + (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 (Sort s) : 'l2_pattern)); + (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 (Meta (int_of_string m, s)) : 'l2_pattern)); + (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 (Meta (int_of_string m, [])) : 'l2_pattern)); + (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 Implicit : 'l2_pattern)); + (return_term loc Ast.Implicit : 'term)); [Gramext.Stoken ("NUMBER", "")], Gramext.action (fun (n : string) (loc : Lexing.position * Lexing.position) -> - (return_term loc (Num (n, 0)) : 'l2_pattern)); + (return_term loc (Ast.Num (n, 0)) : 'term)); [Gramext.Stoken ("URI", "")], Gramext.action (fun (u : string) (loc : Lexing.position * Lexing.position) -> - (return_term loc (Uri (u, None)) : 'l2_pattern)); + (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 @@ -971,131 +1117,12 @@ let _ = Gramext.action (fun (s : 'explicit_subst) (id : string) (loc : Lexing.position * Lexing.position) -> - (return_term loc (Ident (id, Some s)) : 'l2_pattern)); + (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 (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", "non"); - Gramext.Stoken ("IDENT", "associative")], - Gramext.action - (fun _ _ (loc : Lexing.position * Lexing.position) -> - (Gramext.NonA : 'associativity)); - [Gramext.Stoken ("IDENT", "right"); - Gramext.Stoken ("IDENT", "associative")], - Gramext.action - (fun _ _ (loc : Lexing.position * Lexing.position) -> - (Gramext.RightA : 'associativity)); - [Gramext.Stoken ("IDENT", "left"); - Gramext.Stoken ("IDENT", "associative")], - Gramext.action - (fun _ _ (loc : Lexing.position * Lexing.position) -> - (Gramext.LeftA : 'associativity))]]; - Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None, - [None, None, - [[Gramext.Stoken ("IDENT", "with"); - Gramext.Stoken ("IDENT", "precedence"); - Gramext.Stoken ("NUMBER", "")], - Gramext.action - (fun (n : string) _ _ (loc : Lexing.position * Lexing.position) -> - (int_of_string 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.Sopt - (Gramext.Snterm - (Grammar.Entry.obj - (associativity : 'associativity Grammar.Entry.e))); - Gramext.Sopt - (Gramext.Snterm - (Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e))); - Gramext.Stoken ("IDENT", "for"); - Gramext.Snterm - (Grammar.Entry.obj - (level2_pattern : 'level2_pattern Grammar.Entry.e))], - Gramext.action - (fun (p2 : 'level2_pattern) _ (prec : 'precedence option) - (assoc : 'associativity option) (p1 : 'level1_pattern) _ - (loc : Lexing.position * Lexing.position) -> - (p1, assoc, prec, p2 : '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))]]; - Grammar.Entry.obj (phrase : 'phrase Grammar.Entry.e), None, - [None, None, - [[Gramext.Snterm - (Grammar.Entry.obj (notation : 'notation Grammar.Entry.e)); - Gramext.Stoken ("SYMBOL", ".")], - Gramext.action - (fun _ (l1, assoc, prec, l2 : 'notation) - (loc : Lexing.position * Lexing.position) -> - (Notation (l1, assoc, prec, l2) : 'phrase)); - [Gramext.Stoken ("IDENT", "print"); - Gramext.Snterm - (Grammar.Entry.obj - (level2_pattern : 'level2_pattern Grammar.Entry.e)); - Gramext.Stoken ("SYMBOL", ".")], - Gramext.action - (fun _ (p2 : 'level2_pattern) _ - (loc : Lexing.position * Lexing.position) -> - (Print p2 : 'phrase))]]]) + (return_term loc (Ast.Ident (id, None)) : 'term))]]]) +(* }}} *) (** {2 API implementation} *) @@ -1106,19 +1133,29 @@ let exc_located_wrapper f = | 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) -let parse_phrase stream = - exc_located_wrapper (fun () -> Grammar.Entry.parse phrase stream) +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 l2_pattern); + Grammar.print_entry Format.std_formatter (Grammar.Entry.obj term); Format.pp_print_flush Format.std_formatter (); flush stdout