max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(frontends/lean): remove tactic notation

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-10 15:50:29 -07:00
parent 0a6cc0ab5a
commit d302514933
7 changed files with 43 additions and 162 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

117
src/frontends/lean/notation_cmd.cpp
View file

@ -101,26 +101,8 @@ void check_not_forbidden(char const * tk) {
}
}
static optional<unsigned> get_precedence(environment const & env, char const * tk, bool is_expr) {
if (is_expr)
return get_expr_precedence(get_token_table(env), tk);
else
return get_tactic_precedence(get_token_table(env), tk);
}
static optional<unsigned> get_precedence(environment const & env, char const * tk, notation_entry_group grp) {
return get_precedence(env, tk, grp != notation_entry_group::Tactic);
}
static token_entry mk_token_entry(std::string const & tk, unsigned prec, bool is_expr) {
if (is_expr)
return mk_expr_token_entry(tk, prec);
else
return mk_tactic_token_entry(tk, prec);
}
static token_entry mk_token_entry(std::string const & tk, unsigned prec, notation_entry_group grp) {
return mk_token_entry(tk, prec, grp != notation_entry_group::Tactic);
static optional<unsigned> get_precedence(environment const & env, char const * tk) {
return get_expr_precedence(get_token_table(env), tk);
}
static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, notation_entry_group grp, bool parse_only,
@ -177,14 +159,14 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
lean_assert(grp == notation_entry_group::Main);
prec = reserved_action->rbp();
} else {
prec = get_precedence(env, tk.c_str(), grp);
prec = get_precedence(env, tk.c_str());
if (prec && k == mixfix_kind::infixr)
prec = *prec - 1;
}
} else {
auto old_prec = get_precedence(env, tk.c_str(), grp);
auto old_prec = get_precedence(env, tk.c_str());
if (!old_prec || k != mixfix_kind::prefix)
new_token = mk_token_entry(tk.c_str(), *prec, grp);
new_token = mk_token_entry(tk.c_str(), *prec);
if (k == mixfix_kind::infixr)
prec = *prec - 1;
}
@ -276,7 +258,7 @@ static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool over
return nt.first;
}
static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens, bool & used_default, notation_entry_group grp) {
static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens, bool & used_default) {
used_default = false;
if (p.curr_is_quoted_symbol()) {
environment const & env = p.env();
@ -288,9 +270,9 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
if (p.curr_is_token(get_colon_tk())) {
p.next();
unsigned prec = parse_precedence(p);
new_tokens.push_back(mk_token_entry(tkcs, prec, grp));
} else if (!get_precedence(env, tkcs, grp)) {
new_tokens.push_back(mk_token_entry(tkcs, LEAN_DEFAULT_PRECEDENCE, grp));
new_tokens.push_back(mk_token_entry(tkcs, prec));
} else if (!get_precedence(env, tkcs)) {
new_tokens.push_back(mk_token_entry(tkcs, LEAN_DEFAULT_PRECEDENCE));
used_default = true;
}
return pp_tk;
@ -304,9 +286,9 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
}
}
static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens, notation_entry_group grp) {
static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens) {
bool dummy;
return parse_quoted_symbol_or_token(p, new_tokens, dummy, grp);
return parse_quoted_symbol_or_token(p, new_tokens, dummy);
}
static expr parse_notation_expr(parser & p, buffer<expr> const & locals) {
@ -344,7 +326,7 @@ static unsigned get_precedence(environment const & env, buffer<token_entry> cons
}
static action parse_action(parser & p, name const & prev_token, unsigned default_prec,
buffer<expr> & locals, buffer<token_entry> & new_tokens, notation_entry_group grp) {
buffer<expr> & locals, buffer<token_entry> & new_tokens) {
if (p.curr_is_token(get_colon_tk())) {
p.next();
if (p.curr_is_numeral() || p.curr_is_token_or_id(get_max_tk())) {
@ -362,7 +344,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
bool is_fold_right = p.curr_is_token_or_id(get_foldr_tk());
p.next();
auto prec = parse_optional_precedence(p);
name sep = parse_quoted_symbol_or_token(p, new_tokens, grp);
name sep = parse_quoted_symbol_or_token(p, new_tokens);
expr rec;
{
parser::local_scope scope(p);
@ -380,7 +362,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
ini = parse_notation_expr(p, locals);
optional<name> terminator;
if (!p.curr_is_token(get_rparen_tk()))
terminator = parse_quoted_symbol_or_token(p, new_tokens, grp);
terminator = parse_quoted_symbol_or_token(p, new_tokens);
p.check_token_next(get_rparen_tk(), "invalid fold notation argument, ')' expected");
return mk_exprs_action(sep, rec, ini, terminator, is_fold_right, prec ? *prec : 0);
} else if (p.curr_is_token_or_id(get_scoped_tk())) {
@ -455,8 +437,7 @@ static unsigned parse_binders_rbp(parser & p) {
}
static transition parse_transition(parser & p, optional<parse_table> const & pt, name const & tk,
buffer<expr> & locals, buffer<token_entry> & new_tokens, notation_entry_group grp,
name const & pp_tk) {
buffer<expr> & locals, buffer<token_entry> & new_tokens, name const & pp_tk) {
if (p.curr_is_token_or_id(get_binder_tk())) {
p.next();
unsigned rbp = parse_binders_rbp(p);
@ -469,7 +450,7 @@ static transition parse_transition(parser & p, optional<parse_table> const & pt,
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);
action a = parse_action(p, tk, default_prec, locals, new_tokens);
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);
@ -515,7 +496,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
bool used_default = false;
while ((grp != notation_entry_group::Reserve && !p.curr_is_token(get_assign_tk())) ||
(grp == notation_entry_group::Reserve && !p.curr_is_command() && !p.curr_is_eof())) {
name pp_tk = parse_quoted_symbol_or_token(p, new_tokens, used_default, grp).to_string();
name pp_tk = parse_quoted_symbol_or_token(p, new_tokens, used_default).to_string();
name tk = utf8_trim(pp_tk.to_string());
if (auto at = find_next(reserved_pt, tk)) {
// Remark: we are ignoring multiple actions in the reserved notation table
@ -528,7 +509,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
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, pp_tk));
ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, pp_tk));
break;
}
p.check_token_or_id_next(get_binders_tk(),
@ -539,7 +520,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
break;
case notation::action_kind::Binder:
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, pp_tk));
ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, pp_tk));
break;
}
p.check_token_or_id_next(get_binder_tk(),
@ -549,7 +530,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
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, pp_tk));
ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, pp_tk));
break;
}
p.check_token_or_id_next(get_binders_tk(),
@ -560,7 +541,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
case notation::action_kind::Expr: case notation::action_kind::Exprs: case notation::action_kind::ScopedExpr:
case notation::action_kind::Ext: {
if (g_allow_local && !p.curr_is_identifier()) {
ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, grp, pp_tk));
ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, pp_tk));
break;
}
name n = p.check_id_next("invalid notation declaration, identifier expected "
@ -568,7 +549,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
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);
action a = parse_action(p, tk, default_prec, locals, new_tokens);
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);
@ -590,7 +571,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
}}
} else {
reserved_pt = optional<parse_table>();
ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, grp, pp_tk));
ts.push_back(parse_transition(p, pt, tk, locals, new_tokens, pp_tk));
}
pt = find_match(pt, ts.back());
}
@ -693,7 +674,7 @@ static environment add_user_token(environment const & env, token_entry const & e
static environment add_user_token(environment const & env, char const * val, unsigned prec) {
check_token(val);
return add_expr_token(env, val, prec);
return add_token(env, val, prec);
}
struct notation_modifiers {
@ -779,46 +760,6 @@ static environment prefix_cmd(parser & p) {
return mixfix_cmd(p, mixfix_kind::prefix, overload, grp, persistent);
}
static environment tactic_notation_cmd(parser & p) {
allow_nested_decls_scope scope(true);
bool overload = false;
notation_entry_group grp = notation_entry_group::Tactic;
bool persistent = true;
return notation_cmd_core(p, overload, grp, persistent);
}
static environment tactic_infixl_cmd(parser & p) {
allow_nested_decls_scope scope(true);
bool overload = false;
notation_entry_group grp = notation_entry_group::Tactic;
bool persistent = true;
return mixfix_cmd(p, mixfix_kind::infixl, overload, grp, persistent);
}
static environment tactic_infixr_cmd(parser & p) {
allow_nested_decls_scope scope(true);
bool overload = false;
notation_entry_group grp = notation_entry_group::Tactic;
bool persistent = true;
return mixfix_cmd(p, mixfix_kind::infixr, overload, grp, persistent);
}
static environment tactic_postfix_cmd(parser & p) {
allow_nested_decls_scope scope(true);
bool overload = false;
notation_entry_group grp = notation_entry_group::Tactic;
bool persistent = true;
return mixfix_cmd(p, mixfix_kind::postfix, overload, grp, persistent);
}
static environment tactic_prefix_cmd(parser & p) {
allow_nested_decls_scope scope(true);
bool overload = false;
notation_entry_group grp = notation_entry_group::Tactic;
bool persistent = true;
return mixfix_cmd(p, mixfix_kind::prefix, overload, grp, persistent);
}
// auxiliary procedure used by local_notation_cmd and reserve_cmd
static environment dispatch_notation_cmd(parser & p, bool overload, notation_entry_group grp, bool persistent) {
if (p.curr_is_token(get_notation_tk())) {
@ -877,20 +818,12 @@ void register_notation_cmds(cmd_table & r) {
add_cmd(r, cmd_info("postfix", "declare a new postfix notation", postfix_cmd));
add_cmd(r, cmd_info("prefix", "declare a new prefix notation", prefix_cmd));
add_cmd(r, cmd_info("notation", "declare a new notation", notation_cmd));
add_cmd(r, cmd_info("tactic_infixl", "declare a new tactic infix (left) notation", tactic_infixl_cmd));
add_cmd(r, cmd_info("tactic_infix", "declare a new tactic infix (left) notation", tactic_infixl_cmd));
add_cmd(r, cmd_info("tactic_infixr", "declare a new tactic infix (right) notation", tactic_infixr_cmd));
add_cmd(r, cmd_info("tactic_postfix", "declare a new tactic postfix notation", tactic_postfix_cmd));
add_cmd(r, cmd_info("tactic_prefix", "declare a new tactic prefix notation", tactic_prefix_cmd));
add_cmd(r, cmd_info("tactic_notation", "declare a new tacitc notation", tactic_notation_cmd));
add_cmd(r, cmd_info("reserve", "reserve notation", reserve_cmd));
}
bool is_notation_cmd(name const & n) {
return
n == get_infix_tk() || n == get_infixl_tk() || n == get_infixr_tk() || n == get_postfix_tk() ||
n == get_prefix_tk() || n == get_notation_tk() || n == get_precedence_tk() ||
n == get_tactic_infix_tk() || n == get_tactic_infixl_tk() || n == get_tactic_infixr_tk() || n == get_tactic_postfix_tk() ||
n == get_tactic_prefix_tk() || n == get_tactic_notation_tk();
n == get_prefix_tk() || n == get_notation_tk() || n == get_precedence_tk();
}
}

18
src/frontends/lean/parser.cpp
View file

@ -1994,8 +1994,6 @@ expr parser::parse_tactic_nud() {
} else {
return parse_expr();
}
} else if (curr_is_keyword()) {
return parse_tactic_notation(tactic_nud(), nullptr);
} else if (curr_is_numeral() || curr_is_decimal()) {
return parse_expr();
} else {
@ -2003,20 +2001,8 @@ expr parser::parse_tactic_nud() {
}
}
expr parser::parse_tactic_led(expr left) {
if (tactic_led().find(get_token_info().value())) {
return parse_tactic_notation(tactic_led(), &left);
} else {
throw parser_error("invalid tactic expression", pos());
}
}
expr parser::parse_tactic(unsigned rbp) {
expr left = parse_tactic_nud();
while (rbp < curr_tactic_lbp()) {
left = parse_tactic_led(left);
}
return left;
expr parser::parse_tactic(unsigned) {
lean_unreachable();
}
/** \brief Helper class for creating type context only if needed */

2
src/frontends/lean/parser.h
View file

@ -173,8 +173,6 @@ class parser {
parse_table const & nud() const { return get_nud_table(env()); }
parse_table const & led() const { return get_led_table(env()); }
parse_table const & tactic_nud() const { return get_tactic_nud_table(env()); }
parse_table const & tactic_led() const { return get_tactic_led_table(env()); }
unsigned curr_level_lbp() const;
level parse_max_imax(bool is_max);

33
src/frontends/lean/parser_config.cpp
View file

@ -83,10 +83,7 @@ struct token_config {
static std::string * g_key;
static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
if (e.m_expr)
s.m_table = add_token(s.m_table, e.m_token.c_str(), e.m_prec);
else
s.m_table = add_tactic_token(s.m_table, e.m_token.c_str(), e.m_prec);
s.m_table = add_token(s.m_table, e.m_token.c_str(), e.m_prec);
}
static name const & get_class_name() {
return *g_class_name;
@ -95,13 +92,12 @@ struct token_config {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
s << e.m_expr << e.m_token.c_str() << e.m_prec;
s << e.m_token.c_str() << e.m_prec;
}
static entry read_entry(deserializer & d) {
bool is_expr = d.read_bool();
std::string tk = d.read_string();
unsigned prec = d.read_unsigned();
return entry(is_expr, tk, prec);
return entry(tk, prec);
}
static optional<unsigned> get_fingerprint(entry const &) {
return optional<unsigned>();
@ -117,12 +113,8 @@ environment add_token(environment const & env, token_entry const & e, bool persi
return token_ext::add_entry(env, get_dummy_ios(), e, get_namespace(env), persistent);
}
environment add_expr_token(environment const & env, char const * val, unsigned prec) {
return add_token(env, token_entry(true, val, prec));
}
environment add_tactic_token(environment const & env, char const * val, unsigned prec) {
return add_token(env, token_entry(false, val, prec));
environment add_token(environment const & env, char const * val, unsigned prec) {
return add_token(env, token_entry(val, prec));
}
token_table const & get_token_table(environment const & env) {
@ -219,23 +211,17 @@ struct notation_state {
// The following two tables are used to implement `reserve notation` commands
parse_table m_reserved_nud;
parse_table m_reserved_led;
// The following two tables are used to implement `notation [tactic]` commands
parse_table m_tactic_nud;
parse_table m_tactic_led;
notation_state():
m_nud(get_builtin_nud_table()),
m_led(get_builtin_led_table()),
m_reserved_nud(true),
m_reserved_led(false) {
// m_tactic_nud(get_builtin_tactic_nud_table()),
// m_tactic_led(get_builtin_tactic_led_table()) {
}
parse_table & nud(notation_entry_group g) {
switch (g) {
case notation_entry_group::Main: return m_nud;
case notation_entry_group::Reserve: return m_reserved_nud;
case notation_entry_group::Tactic: return m_tactic_nud;
}
lean_unreachable();
}
@ -244,7 +230,6 @@ struct notation_state {
switch (g) {
case notation_entry_group::Main: return m_led;
case notation_entry_group::Reserve: return m_reserved_led;
case notation_entry_group::Tactic: return m_tactic_led;
}
lean_unreachable();
}
@ -361,14 +346,6 @@ parse_table const & get_reserved_led_table(environment const & env) {
return notation_ext::get_state(env).m_reserved_led;
}
parse_table const & get_tactic_nud_table(environment const & env) {
return notation_ext::get_state(env).m_tactic_nud;
}
parse_table const & get_tactic_led_table(environment const & env) {
return notation_ext::get_state(env).m_tactic_led;
}
environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload, bool parse_only) {
return add_notation(env, notation_entry(n, e, overload, parse_only));
}

14
src/frontends/lean/parser_config.h
View file

@ -13,16 +13,14 @@ Author: Leonardo de Moura
namespace lean {
struct token_entry {
bool m_expr; // true if it precedence for an expression token
std::string m_token;
unsigned m_prec;
token_entry(bool e, std::string const & tk, unsigned prec):m_expr(e), m_token(tk), m_prec(prec) {}
token_entry(std::string const & tk, unsigned prec): m_token(tk), m_prec(prec) {}
};
inline token_entry mk_expr_token_entry(std::string const & tk, unsigned prec) { return token_entry(true, tk, prec); }
inline token_entry mk_tactic_token_entry(std::string const & tk, unsigned prec) { return token_entry(false, tk, prec); }
inline token_entry mk_token_entry(std::string const & tk, unsigned prec) { return token_entry(tk, prec); }
enum class notation_entry_kind { NuD, LeD, Numeral };
enum class notation_entry_group { Main, Reserve, Tactic };
enum class notation_entry_group { Main, Reserve };
class notation_entry {
typedef notation::transition transition;
notation_entry_kind m_kind;
@ -67,16 +65,12 @@ notation_entry replace(notation_entry const & e, std::function<expr(expr const &
environment add_token(environment const & env, token_entry const & e, bool persistent = true);
environment add_notation(environment const & env, notation_entry const & e, bool persistent = true);
environment add_expr_token(environment const & env, char const * val, unsigned prec);
environment add_tactic_token(environment const & env, char const * val, unsigned prec);
environment add_token(environment const & env, char const * val, unsigned prec);
token_table const & get_token_table(environment const & env);
parse_table const & get_nud_table(environment const & env);
parse_table const & get_led_table(environment const & env);
parse_table const & get_reserved_nud_table(environment const & env);
parse_table const & get_reserved_led_table(environment const & env);
parse_table const & get_tactic_nud_table(environment const & env);
parse_table const & get_tactic_led_table(environment const & env);
cmd_table const & get_cmd_table(environment const & env);
/** \brief Force notation from namespace \c n to shadow any existing notation */
environment override_notation(environment const & env, name const & n, bool persistent = true);

7
src/frontends/lean/print_cmd.cpp
View file

@ -482,13 +482,6 @@ bool print_token_info(parser const & p, name const & tk) {
if (print_parse_table(p, get_led_table(p.env()), false, tokens)) {
found = true;
}
bool tactic_table = true;
if (print_parse_table(p, get_tactic_nud_table(p.env()), true, tokens, tactic_table)) {
found = true;
}
if (print_parse_table(p, get_tactic_led_table(p.env()), false, tokens, tactic_table)) {
found = true;
}
return found;
}

14
src/tests/frontends/lean/scanner.cpp
View file

@ -99,13 +99,13 @@ static void check_keyword(char const * str, name const & expected, environment c
static void tst1() {
environment env;
token_table s = get_token_table(env);
env = add_expr_token(env, "+", 0);
env = add_expr_token(env, "=", 0);
env = add_token(env, "+", 0);
env = add_token(env, "=", 0);
scan_success("a..a");
check("a..a", {tk::Identifier, tk::Keyword, tk::Keyword, tk::Identifier});
check("Type.{0}", {tk::Keyword, tk::Keyword, tk::Numeral, tk::Keyword});
env = add_expr_token(env, "ab+cde", 0);
env = add_expr_token(env, "+cd", 0);
env = add_token(env, "ab+cde", 0);
env = add_token(env, "+cd", 0);
scan_success("ab+cd", env);
check("ab+cd", {tk::Identifier, tk::Keyword}, env);
scan_success("ab+cde", env);
@ -139,9 +139,9 @@ static void tst2() {
scan_error("***");
environment env;
token_table s = mk_default_token_table();
env = add_expr_token(env, "***", 0);
env = add_token(env, "***", 0);
check_keyword("***", "***", env);
env = add_expr_token(env, "+", 0);
env = add_token(env, "+", 0);
check("x+y", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
check("-- testing", {});
check("/- testing -/", {});
@ -152,7 +152,7 @@ static void tst2() {
check("int -> int", {tk::Identifier, tk::Keyword, tk::Identifier});
check("int->int", {tk::Identifier, tk::Keyword, tk::Identifier});
check_keyword("->", "->");
env = add_expr_token(env, "-+->", 0);
env = add_token(env, "-+->", 0);
check("Int -+-> Int", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
check("x := 10", {tk::Identifier, tk::Keyword, tk::Numeral});
check("{x}", {tk::Keyword, tk::Identifier, tk::Keyword});