*)
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 =
| 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
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
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))]];
+ (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))]];
[[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
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", "λ")],
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))]];
(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 =
let rec find_arg name n =
function
[] ->
- fail loc
+ Ast.fail loc
(sprintf "Argument %s not found"
(CicNotationPp.pp_term name))
| (l, _) :: 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
(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
(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
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} *)
| 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
projects / helm.git / commitdiff