From a27b20cd9c35409c634fcf82ccbf183ce237e703 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Jul 2015 17:30:46 -0700 Subject: [PATCH] feat(frontends/lean/notation_cmd): allow local notation to override reserved notation closes #712 --- src/frontends/lean/notation_cmd.cpp | 110 ++++++++++++++++++---------- tests/lean/712.lean | 30 ++++++++ tests/lean/712.lean.expected.out | 8 ++ 3 files changed, 111 insertions(+), 37 deletions(-) create mode 100644 tests/lean/712.lean create mode 100644 tests/lean/712.lean.expected.out diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 7002463a7d..0977f3d91a 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -145,7 +145,9 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota } if (p.curr_is_token(get_colon_tk())) { - if (reserved_pt) + // Remark: we do not throw an exception, if it is local notation. + // We allow local notation to override reserved one. + if (!g_allow_local && reserved_pt) throw parser_error("invalid notation declaration, invalid ':' occurrence " "(declaration matches reserved notation)", p.pos()); p.next(); @@ -182,7 +184,7 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota "solution: use the 'precedence' command", p.pos()); } - if (reserved_action) { + if (!g_allow_local && reserved_action) { switch (k) { case mixfix_kind::infixl: if (reserved_action->kind() != notation::action_kind::Expr || reserved_action->rbp() != *prec) @@ -439,6 +441,35 @@ static unsigned parse_binders_rbp(parser & p) { } } +static transition parse_transition(parser & p, optional const & pt, name const & tk, + buffer & locals, buffer & new_tokens, notation_entry_group grp) { + if (p.curr_is_token_or_id(get_binder_tk())) { + p.next(); + unsigned rbp = parse_binders_rbp(p); + return transition(tk, mk_binder_action(rbp)); + } else if (p.curr_is_token_or_id(get_binders_tk())) { + p.next(); + unsigned rbp = parse_binders_rbp(p); + return transition(tk, mk_binders_action(rbp)); + } else if (p.curr_is_identifier()) { + unsigned default_prec = get_default_prec(pt, tk); + name n = p.get_name_val(); + p.next(); + action a = parse_action(p, tk, default_prec, locals, new_tokens, grp); + expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant + expr l = mk_local(n, local_type); + p.add_local(l); + locals.push_back(l); + return transition(tk, a); + } else if (p.curr_is_quoted_symbol() || p.curr_is_keyword() || + p.curr_is_token(get_assign_tk()) || p.curr_is_command() || p.curr_is_eof()) { + return transition(tk, mk_skip_action()); + } else { + throw parser_error("invalid notation declaration, quoted-symbol, identifier, " + "'binder', 'binders' expected", p.pos()); + } +} + static notation_entry parse_notation_core(parser & p, bool overload, notation_entry_group grp, buffer & new_tokens, bool parse_only, unsigned priority) { buffer locals; @@ -477,6 +508,10 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en switch (a.kind()) { case notation::action_kind::Skip: if (!p.curr_is_quoted_symbol() && !p.curr_is_keyword() && !p.curr_is_token(get_assign_tk())) { + if (g_allow_local && !p.curr_is_token_or_id(get_binders_tk())) { + ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, grp)); + break; + } p.check_token_or_id_next(get_binders_tk(), "invalid notation declaration, quoted-symbol, keyword or `:=` expected " "(declaration prefix matches reserved notation)"); @@ -484,12 +519,20 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en ts.push_back(transition(tk, a)); break; case notation::action_kind::Binder: - p.check_token_or_id_next(get_binders_tk(), + if (g_allow_local && !p.curr_is_token_or_id(get_binder_tk())) { + ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, grp)); + break; + } + p.check_token_or_id_next(get_binder_tk(), "invalid notation declaration, 'binder' expected " "(declaration prefix matches reserved notation)"); ts.push_back(transition(tk, a)); break; case notation::action_kind::Binders: + if (g_allow_local && !p.curr_is_token_or_id(get_binders_tk())) { + ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, grp)); + break; + } p.check_token_or_id_next(get_binders_tk(), "invalid notation declaration, 'binders' expected " "(declaration prefix matches reserved notation)"); @@ -497,45 +540,38 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en break; case notation::action_kind::Expr: case notation::action_kind::Exprs: case notation::action_kind::ScopedExpr: case notation::action_kind::Ext: case notation::action_kind::LuaExt: { + if (g_allow_local && !p.curr_is_identifier()) { + ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, grp)); + break; + } name n = p.check_id_next("invalid notation declaration, identifier expected " "(declaration prefix matches reserved notation)"); - expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant - expr l = mk_local(n, local_type); - p.add_local(l); - locals.push_back(l); - ts.push_back(transition(tk, a)); - break; + if (p.curr_is_token(get_colon_tk())) { + if (g_allow_local) { + unsigned default_prec = get_default_prec(pt, tk); + action a = parse_action(p, tk, default_prec, locals, new_tokens, grp); + expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant + expr l = mk_local(n, local_type); + p.add_local(l); + locals.push_back(l); + ts.push_back(transition(tk, a)); + break; + } else { + throw parser_error("invalid notation declaration, invalid ':' occurrence " + "(declaration prefix matches reserved notation)", p.pos()); + } + } else { + expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant + expr l = mk_local(n, local_type); + p.add_local(l); + locals.push_back(l); + ts.push_back(transition(tk, a)); + break; + } }} - if (p.curr_is_token(get_colon_tk())) - throw parser_error("invalid notation declaration, invalid ':' occurrence " - "(declaration prefix matches reserved notation)", p.pos()); } else { reserved_pt = optional(); - if (p.curr_is_token_or_id(get_binder_tk())) { - p.next(); - unsigned rbp = parse_binders_rbp(p); - ts.push_back(transition(tk, mk_binder_action(rbp))); - } else if (p.curr_is_token_or_id(get_binders_tk())) { - p.next(); - unsigned rbp = parse_binders_rbp(p); - ts.push_back(transition(tk, mk_binders_action(rbp))); - } else if (p.curr_is_identifier()) { - unsigned default_prec = get_default_prec(pt, tk); - name n = p.get_name_val(); - p.next(); - action a = parse_action(p, tk, default_prec, locals, new_tokens, grp); - expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant - expr l = mk_local(n, local_type); - p.add_local(l); - locals.push_back(l); - ts.push_back(transition(tk, a)); - } else if (p.curr_is_quoted_symbol() || p.curr_is_keyword() || - p.curr_is_token(get_assign_tk()) || p.curr_is_command() || p.curr_is_eof()) { - ts.push_back(transition(tk, mk_skip_action())); - } else { - throw parser_error("invalid notation declaration, quoted-symbol, identifier, " - "'binder', 'binders' expected", p.pos()); - } + ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, grp)); } pt = find_match(pt, ts.back()); } diff --git a/tests/lean/712.lean b/tests/lean/712.lean new file mode 100644 index 0000000000..8b899e5661 --- /dev/null +++ b/tests/lean/712.lean @@ -0,0 +1,30 @@ +reserve infix `~~~`:50 +reserve notation `[` a `][` b:10 `]` + +section +local infix `~~~` := eq + +print notation ~~~ + +local infix `~~~`:50 := eq + +print notation ~~~ + +local infix `~~~`:100 := eq + +infix `~~~`:100 := eq -- FAIL + +print notation ~~~ + +local notation `[` a `][`:10 b:20 `]` := a = b + +print notation ][ +end + +notation `[` a `][`:10 b:20 `]` := a = b -- FAIL + +notation `[` a `][` b `]` := a = b +infix `~~~` := eq + +print notation ~~~ +print notation ][ diff --git a/tests/lean/712.lean.expected.out b/tests/lean/712.lean.expected.out new file mode 100644 index 0000000000..1ee2ecf9cd --- /dev/null +++ b/tests/lean/712.lean.expected.out @@ -0,0 +1,8 @@ +_ `~~~`:50 _:50 := eq #1 #0 +_ `~~~`:50 _:50 := eq #1 #0 +712.lean:15:11: error: invalid notation declaration, invalid ':' occurrence (declaration matches reserved notation) +_ `~~~`:100 _:100 := eq #1 #0 +`[`:1024 _:1 `][`:10 _:20 `]`:0 := eq #1 #0 +712.lean:24:24: error: invalid notation declaration, invalid ':' occurrence (declaration prefix matches reserved notation) +_ `~~~`:50 _:50 := eq #1 #0 +`[`:1024 _:1 `][`:1 _:10 `]`:0 := eq #1 #0