*)
oopen Printf
-eexception Parse_error of Token.flocation * string
-llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer
-llet level1_pattern = Grammar.Entry.create grammar "level1_pattern"llet level2_pattern = Grammar.Entry.create grammar "level2_pattern"llet level3_term = Grammar.Entry.create grammar "level3_term"llet notation = Grammar.Entry.create grammar "notation"(* level1 <-> level 2 *)
-llet interpretation = Grammar.Entry.create grammar "interpretation"(* level2 <-> level 3 *)
-
+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 loc_of_floc ({Lexing.pos_cnum = loc_begin}, {Lexing.pos_cnum = loc_end}) =
- loc_begin, loc_end
-llet fail floc msg =
- let (x, y) = loc_of_floc floc in
- failwith (sprintf "Error at characters %d - %d: %s" x y msg)
llet int_of_string s =
try Pervasives.int_of_string s with
Failure _ ->
failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
-oopen CicNotationPt
-llet boxify =
+(** {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
- [a] -> a
- | l -> Layout (Box (H, l))
-llet fold_binder binder pt_names body =
- let fold_cluster binder names ty body =
- List.fold_right
- (fun name body -> Binder (binder, (Cic.Name name, ty), body)) names body
+ `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
-llet return_term loc term = AttributedTerm (`Loc loc, term)
-Elet _ =
+
+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
- (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e)
- and _ = (level2_pattern : 'level2_pattern Grammar.Entry.e)
- and _ = (level3_term : 'level3_term Grammar.Entry.e)
- and _ = (notation : 'notation Grammar.Entry.e)
- and _ = (interpretation : 'interpretation Grammar.Entry.e) in
+ [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
grammar_entry_create "l1_pattern_variable"
and l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e =
grammar_entry_create "l1_simple_pattern"
- and sort : 'sort Grammar.Entry.e = grammar_entry_create "sort"
- and explicit_subst : 'explicit_subst Grammar.Entry.e =
- grammar_entry_create "explicit_subst"
- and meta_subst : 'meta_subst Grammar.Entry.e =
- grammar_entry_create "meta_subst"
- and possibly_typed_name : 'possibly_typed_name Grammar.Entry.e =
- grammar_entry_create "possibly_typed_name"
- and match_pattern : 'match_pattern Grammar.Entry.e =
- grammar_entry_create "match_pattern"
- and binder : 'binder Grammar.Entry.e = grammar_entry_create "binder"
- and bound_names : 'bound_names Grammar.Entry.e =
- grammar_entry_create "bound_names"
- and induction_kind : 'induction_kind Grammar.Entry.e =
- grammar_entry_create "induction_kind"
- and let_defs : 'let_defs Grammar.Entry.e =
- grammar_entry_create "let_defs"
- and l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e =
- grammar_entry_create "l2_pattern_variable"
- and l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e =
- grammar_entry_create "l2_magic_pattern"
- and l2_pattern : 'l2_pattern Grammar.Entry.e =
- grammar_entry_create "l2_pattern"
- and argument : 'argument Grammar.Entry.e =
- grammar_entry_create "argument"
- and associativity : 'associativity Grammar.Entry.e =
- grammar_entry_create "associativity"
- and precedence : 'precedence Grammar.Entry.e =
- grammar_entry_create "precedence"
in
[Grammar.Entry.obj (level1_pattern : 'level1_pattern Grammar.Entry.e),
None,
Gramext.action
(fun _ (p : 'l1_pattern)
(loc : Lexing.position * Lexing.position) ->
- (boxify p : 'level1_pattern))]];
+ (CicNotationUtil.boxify p : 'level1_pattern))]];
Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
[None, None,
- [[Gramext.Slist0
+ [[Gramext.Slist1
(Gramext.Snterm
(Grammar.Entry.obj
(l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)))],
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));
(`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
(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));
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));
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));
- [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.Stoken ("SYMBOL", "[");
+ [[Gramext.Stoken ("LPAREN", "");
Gramext.Snterm
(Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "\\AS"); Gramext.Stoken ("IDENT", "");
- Gramext.Stoken ("SYMBOL", "]")],
+ Gramext.Stoken ("RPAREN", "")],
Gramext.action
- (fun _ (id : string) _ (p : 'l1_pattern) _
+ (fun _ (p : 'l1_pattern) _
(loc : Lexing.position * Lexing.position) ->
- (return_term loc
- (Variable (Ascription (Layout (Box (H, p)), id))) :
+ (return_term loc (CicNotationUtil.group p) :
'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "[");
+ [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 ("SYMBOL", "]")],
+ Gramext.Stoken ("RPAREN", "")],
Gramext.action
- (fun _ (p : 'l1_pattern) _
+ (fun _ (p : 'l1_pattern) _ _
(loc : Lexing.position * Lexing.position) ->
- (return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "\\BREAK")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Layout Break) : 'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("SYMBOL", "[");
+ (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 ("SYMBOL", "]")],
+ 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 ("SYMBOL", "[");
+ (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 ("SYMBOL", "]")],
+ 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");
+ (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 ("SYMBOL", "\\OF"); Gramext.Sself],
+ Gramext.Stoken ("RPAREN", "")],
Gramext.action
- (fun (arg : 'l1_simple_pattern) _ (index : 'l1_pattern) _
+ (fun _ (p : 'l1_pattern) _ _
(loc : Lexing.position * Lexing.position) ->
- (return_term loc (Layout (Root (arg, Layout (Box (H, index))))) :
+ (return_term loc
+ (Ast.Layout (Ast.Box ((Ast.H, false, false), p))) :
'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "\\SQRT"); Gramext.Sself],
+ [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 (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.Stoken ("SYMBOL", "[");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "\\ATOP");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "]")],
+ (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_pattern) _ (p1 : 'l1_pattern) _
+ (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
(loc : Lexing.position * Lexing.position) ->
- (return_term loc (Layout (Atop (boxify p1, boxify p2))) :
+ (return_term loc (Ast.Layout (Ast.Atop (p1, p2))) :
'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "[");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "\\OVER");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "]")],
+ [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\over"); Gramext.Sself],
Gramext.action
- (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
+ (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
(loc : Lexing.position * Lexing.position) ->
- (return_term loc (Layout (Frac (boxify p1, boxify p2))) :
+ (return_term loc (Ast.Layout (Ast.Over (p1, p2))) :
'l1_simple_pattern));
- [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself],
+ [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))]];
- Grammar.Entry.obj (level2_pattern : 'level2_pattern Grammar.Entry.e),
- None,
+ (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.Snterm
- (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+ [[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 (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) ->
- (p : 'level2_pattern))]];
+ (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))]];
Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e),
- None, [None, None, []];
+ 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, []];
+ [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.Stoken ("IDENT", "")],
+ [[Gramext.Snterm
+ (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e))],
Gramext.action
- (fun (id : string) (loc : Lexing.position * Lexing.position) ->
- (Cic.Name id, None : 'possibly_typed_name));
- [Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
- Gramext.Stoken ("SYMBOL", ":");
+ (fun (arg : 'single_arg)
+ (loc : Lexing.position * Lexing.position) ->
+ (arg, None : 'possibly_typed_name));
+ [Gramext.Stoken ("LPAREN", "");
Gramext.Snterm
- (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", ")")],
+ (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 : 'l2_pattern) _ (id : string) _
+ (fun _ (typ : 'term) _ (id : 'single_arg) _
(loc : Lexing.position * Lexing.position) ->
- (Cic.Name id, Some typ : 'possibly_typed_name))]];
+ (id, Some typ : 'possibly_typed_name))]];
Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e),
None,
[None, None,
- [[Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
+ [[Gramext.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", "λ")],
Gramext.action
(fun _ (loc : Lexing.position * Lexing.position) ->
(`Forall : 'binder));
- [Gramext.Stoken ("SYMBOL", "∃")],
- Gramext.action
- (fun _ (loc : Lexing.position * Lexing.position) ->
- (`Exists : 'binder));
[Gramext.Stoken ("SYMBOL", "Π")],
Gramext.action
(fun _ (loc : Lexing.position * Lexing.position) ->
(`Pi : 'binder))]];
- Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e), None,
+ Grammar.Entry.obj (arg : 'arg Grammar.Entry.e), None,
[None, None,
- [[Gramext.Slist1
- (Gramext.srules
- [[Gramext.Stoken ("SYMBOL", "(");
- Gramext.Slist1sep
- (Gramext.Stoken ("IDENT", ""),
- Gramext.Stoken ("SYMBOL", ","));
- Gramext.Sopt
- (Gramext.srules
- [[Gramext.Stoken ("SYMBOL", ":");
- Gramext.Snterm
- (Grammar.Entry.obj
- (l2_pattern : 'l2_pattern Grammar.Entry.e))],
- Gramext.action
- (fun (p : 'l2_pattern) _
- (loc : Lexing.position * Lexing.position) ->
- (p : 'e__2))]);
- Gramext.Stoken ("SYMBOL", ")")],
- Gramext.action
- (fun _ (ty : 'e__2 option) (vars : string list) _
- (loc : Lexing.position * Lexing.position) ->
- (vars, ty : 'e__3))])],
+ [[Gramext.Stoken ("UNPARSED_META", "")],
Gramext.action
- (fun (clusters : 'e__3 list)
- (loc : Lexing.position * Lexing.position) ->
- (clusters : 'bound_names));
- [Gramext.Slist1sep
+ (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.Sopt
- (Gramext.srules
- [[Gramext.Stoken ("SYMBOL", ":");
- Gramext.Snterm
- (Grammar.Entry.obj
- (l2_pattern : 'l2_pattern Grammar.Entry.e))],
- Gramext.action
- (fun (p : 'l2_pattern) _
- (loc : Lexing.position * Lexing.position) ->
- (p : 'e__1))])],
+ Gramext.Stoken ("SYMBOL", ":");
+ Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
+ Gramext.Stoken ("RPAREN", "")],
Gramext.action
- (fun (ty : 'e__1 option) (vars : string list)
+ (fun _ (ty : 'term) _ (names : string list) _
(loc : Lexing.position * Lexing.position) ->
- ([vars, ty] : 'bound_names))]];
+ (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 ("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))]];
[None, None,
[[Gramext.Slist1sep
(Gramext.srules
- [[Gramext.Stoken ("IDENT", "");
- Gramext.Snterm
+ [[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 ("IDENT", "")],
+ [[Gramext.Stoken ("", "on");
+ Gramext.Snterm
+ (Grammar.Entry.obj
+ (single_arg : 'single_arg Grammar.Entry.e))],
Gramext.action
- (fun (id : string) _
+ (fun (id : 'single_arg) _
(loc : Lexing.position * Lexing.position) ->
- (id : 'e__4))]);
+ (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__5))]);
+ (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__5 option)
- (index_name : 'e__4 option) (args : 'bound_names)
- (name : string)
+ (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 =
in
let rec find_arg name n =
function
- [] -> fail loc (sprintf "Argument %s not found" name)
+ [] ->
+ 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
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
- (Cic.Name name, ty), body, index :
- 'e__6))],
- Gramext.Stoken ("IDENT", "and"))],
+ (name, ty), body, index :
+ 'e__5))],
+ Gramext.Stoken ("", "and"))],
Gramext.action
- (fun (defs : 'e__6 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,
+ Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e), None,
[None, None,
- [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (FreshVar id : 'l2_pattern_variable));
- [Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (IdentVar id : 'l2_pattern_variable));
- [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (NumVar id : 'l2_pattern_variable))]];
- Grammar.Entry.obj
- (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e),
- None,
- [None, None,
- [[Gramext.Stoken ("SYMBOL", "\\DEFAULT");
- Gramext.Snterm
- (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
- Gramext.Snterm
- (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
- Gramext.action
- (fun (none : 'l2_pattern) (some : 'l2_pattern) _
- (loc : Lexing.position * Lexing.position) ->
- (Default (some, none) : 'l2_magic_pattern));
- [Gramext.Stoken ("SYMBOL", "\\FOLD");
+ [[Gramext.Stoken ("LPAREN", "");
Gramext.srules
- [[Gramext.Stoken ("IDENT", "right")],
+ [[Gramext.Stoken ("SYMBOL", "_")],
Gramext.action
(fun _ (loc : Lexing.position * Lexing.position) ->
- (`Right : 'e__7));
- [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__7))];
- Gramext.Snterm
- (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "\\LAMBDA"); Gramext.Stoken ("IDENT", "");
- Gramext.Snterm
- (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
- Gramext.action
- (fun (recursive : 'l2_pattern) (id : string) _ (base : 'l2_pattern)
- (kind : 'e__7) _ (loc : Lexing.position * Lexing.position) ->
- (Fold (kind, base, [id], recursive) : 'l2_magic_pattern))]];
- Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), None,
- [Some "letin", Some Gramext.NonA,
- [[Gramext.Stoken ("IDENT", "let");
+ ([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 ("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))];
- Some "binder", 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))];
- Some "extension", None, [];
- Some "apply", 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))];
- Some "simple", Some Gramext.NonA,
- [[Gramext.Snterm
- (Grammar.Entry.obj
- (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e))],
- Gramext.action
- (fun (m : 'l2_magic_pattern)
- (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Magic m) : 'l2_pattern));
- [Gramext.Snterm
- (Grammar.Entry.obj
- (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e))],
+ 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__8))]);
- 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__9))]);
- Gramext.Stoken ("IDENT", "with"); Gramext.Stoken ("SYMBOL", "[");
+ (id, None : 'e__11))]);
+ Gramext.Stoken ("", "with"); Gramext.Stoken ("SYMBOL", "[");
Gramext.Slist0sep
(Gramext.srules
[[Gramext.Snterm
(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__10))],
+ (lhs, rhs : 'e__12))],
Gramext.Stoken ("SYMBOL", "|"));
Gramext.Stoken ("SYMBOL", "]")],
Gramext.action
- (fun _ (patterns : 'e__10 list) _ _ (indty_ident : 'e__9 option)
- (t : 'l2_pattern) _ (outtyp : 'e__8 option)
+ (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));
- [Gramext.Stoken ("SYMBOL", "")],
- Gramext.action
- (fun (s : string) (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Symbol (s, 0)) : '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_subst : 'meta_subst Grammar.Entry.e))],
+ (Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e))],
Gramext.action
- (fun (s : 'meta_subst) (m : string)
+ (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
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", "right");
- Gramext.Stoken ("IDENT", "associative")],
- Gramext.action
- (fun _ _ (loc : Lexing.position * Lexing.position) ->
- (`Right : 'associativity));
- [Gramext.Stoken ("IDENT", "left");
- Gramext.Stoken ("IDENT", "associative")],
- Gramext.action
- (fun _ _ (loc : Lexing.position * Lexing.position) ->
- (`Left : 'associativity))]];
- Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("IDENT", "at");
- Gramext.Stoken ("IDENT", "precedence");
- Gramext.Stoken ("NUMBER", "")],
- Gramext.action
- (fun (n : string) _ _ (loc : Lexing.position * Lexing.position) ->
- (n : 'precedence))]];
- Grammar.Entry.obj (notation : 'notation Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("IDENT", "notation");
- Gramext.Snterm
- (Grammar.Entry.obj
- (level1_pattern : 'level1_pattern Grammar.Entry.e));
- Gramext.Stoken ("IDENT", "for");
- Gramext.Snterm
- (Grammar.Entry.obj
- (level2_pattern : 'level2_pattern Grammar.Entry.e));
- Gramext.Sopt
- (Gramext.Snterm
- (Grammar.Entry.obj
- (associativity : 'associativity Grammar.Entry.e)));
- Gramext.Sopt
- (Gramext.Snterm
- (Grammar.Entry.obj
- (precedence : 'precedence Grammar.Entry.e)))],
- Gramext.action
- (fun (prec : 'precedence option) (assoc : 'associativity option)
- (p2 : 'level2_pattern) _ (p1 : 'level1_pattern) _
- (loc : Lexing.position * Lexing.position) ->
- (() : 'notation))]];
- Grammar.Entry.obj (interpretation : 'interpretation Grammar.Entry.e),
- None,
- [None, None,
- [[Gramext.Stoken ("IDENT", "interpretation");
- Gramext.Stoken ("SYMBOL", "");
- Gramext.Slist1
- (Gramext.Snterm
- (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e)));
- Gramext.Stoken ("IDENT", "as");
- Gramext.Snterm
- (Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e))],
- Gramext.action
- (fun (t : 'level3_term) _ (args : 'argument list) (s : string) _
- (loc : Lexing.position * Lexing.position) ->
- (() : 'interpretation))]]])
+ (return_term loc (Ast.Ident (id, None)) : 'term))]]])
+(* }}} *)
+
+(** {2 API implementation} *)
let exc_located_wrapper f =
try f () with
| 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_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
-let parse_ast_pattern stream =
- exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream)
+(** {2 Debugging} *)
-let parse_interpretation stream =
- exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream)
+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: *)