From af3f0088f4ee4fd9303edd9315f80ad914c7bc80 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 May 2015 11:42:16 -0700 Subject: [PATCH] feat(frontends/lean): add 'override' (notation) command --- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_cmds.cpp | 36 +++++++++++++++++++++------- src/frontends/lean/builtin_exprs.cpp | 7 +++--- src/frontends/lean/parser_config.cpp | 6 ++--- src/frontends/lean/parser_config.h | 2 +- src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/util.cpp | 3 ++- tests/lean/run/override1.lean | 24 +++++++++++++++++++ 8 files changed, 63 insertions(+), 19 deletions(-) create mode 100644 tests/lean/run/override1.lean diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 9f4ea7dca..57bd2f39f 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -12,7 +12,7 @@ "hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants" "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "print" "theorem" "example" "abbreviation" - "open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes" + "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes" "alias" "help" "environment" "options" "precedence" "reserve" "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "tactic_infix" "tactic_infixl" "tactic_infixr" "tactic_notation" "tactic_postfix" "tactic_prefix" diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 774b9bf6f..9fbd645fe 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -690,11 +690,11 @@ environment open_export_cmd(parser & p, bool open) { fingerprint = hash(fingerprint, n.hash()); auto pos = p.pos(); name ns = p.check_id_next("invalid 'open/export' command, identifier expected"); - fingerprint = hash(fingerprint, ns.hash()); optional real_ns = to_valid_namespace_name(env, ns); if (!real_ns) throw parser_error(sstream() << "invalid namespace name '" << ns << "'", pos); ns = *real_ns; + fingerprint = hash(fingerprint, ns.hash()); name as; if (p.curr_is_token_or_id(get_as_tk())) { p.next(); @@ -778,16 +778,32 @@ environment open_export_cmd(parser & p, bool open) { } return update_fingerprint(env, fingerprint); } -environment open_cmd(parser & p) { return open_export_cmd(p, true); } -environment export_cmd(parser & p) { return open_export_cmd(p, false); } +static environment open_cmd(parser & p) { return open_export_cmd(p, true); } +static environment export_cmd(parser & p) { return open_export_cmd(p, false); } -environment erase_cache_cmd(parser & p) { +static environment override_cmd(parser & p) { + environment env = p.env(); + while (p.curr_is_identifier()) { + auto pos = p.pos(); + name ns = p.check_id_next("invalid 'override' command, identifier expected"); + optional real_ns = to_valid_namespace_name(env, ns); + if (!real_ns) + throw parser_error(sstream() << "invalid namespace name '" << ns << "'", pos); + ns = *real_ns; + bool persistent = false; + env = override_notation(env, ns, persistent); + env = update_fingerprint(env, ns.hash()); + } + return env; +} + +static environment erase_cache_cmd(parser & p) { name n = p.check_id_next("invalid #erase_cache command, identifier expected"); p.erase_cached_definition(n); return p.env(); } -environment projections_cmd(parser & p) { +static environment projections_cmd(parser & p) { name n = p.check_id_next("invalid #projections command, identifier expected"); if (p.curr_is_token(get_dcolon_tk())) { p.next(); @@ -802,7 +818,7 @@ environment projections_cmd(parser & p) { } } -environment telescope_eq_cmd(parser & p) { +static environment telescope_eq_cmd(parser & p) { expr e; level_param_names ls; std::tie(e, ls) = parse_local_expr(p); buffer t; @@ -821,7 +837,7 @@ environment telescope_eq_cmd(parser & p) { return p.env(); } -environment local_cmd(parser & p) { +static environment local_cmd(parser & p) { if (p.curr_is_token_or_id(get_attribute_tk())) { p.next(); return local_attribute_cmd(p); @@ -867,13 +883,13 @@ static environment help_cmd(parser & p) { return p.env(); } -environment init_quotient_cmd(parser & p) { +static environment init_quotient_cmd(parser & p) { if (!(p.env().prop_proof_irrel() && p.env().impredicative())) throw parser_error("invalid init_quotient command, this command is only available for kernels containing an impredicative and proof irrelevant Prop", p.cmd_pos()); return module::declare_quotient(p.env()); } -environment init_hits_cmd(parser & p) { +static environment init_hits_cmd(parser & p) { if (p.env().prop_proof_irrel() || p.env().impredicative()) throw parser_error("invalid init_hits command, this command is only available for proof relevant and predicative kernels", p.cmd_pos()); return module::declare_hits(p.env()); @@ -884,6 +900,8 @@ void init_cmd_table(cmd_table & r) { open_cmd)); add_cmd(r, cmd_info("export", "create abbreviations for declarations, " "and export objects defined in other namespaces", export_cmd)); + add_cmd(r, cmd_info("override", "override notation declarations using the ones defined in the given namespace", + override_cmd)); add_cmd(r, cmd_info("set_option", "set configuration option", set_option_cmd)); add_cmd(r, cmd_info("exit", "exit", exit_cmd)); add_cmd(r, cmd_info("print", "print a string", print_cmd)); diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 24b76def9..df0269988 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -559,9 +559,10 @@ static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const & return parse_calc(p); } -static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_info const &) { +static expr parse_override_notation(parser & p, unsigned, expr const *, pos_info const &) { name n = p.check_id_next("invalid '#' local notation, identifier expected"); - environment env = overwrite_notation(p.env(), n); + bool persistent = false; + environment env = override_notation(p.env(), n, persistent); return p.parse_expr_with_env(env); } @@ -630,7 +631,7 @@ parse_table init_nud_table() { r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0); r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0); r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0); - r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0); + r = r.add({transition("#", mk_ext_action(parse_override_notation))}, x0); r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0); r = r.add({transition("!", mk_ext_action(parse_consume_args_expr))}, x0); r = r.add({transition("begin", mk_ext_action_core(parse_begin_end))}, x0); diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 7c7474662..b81225043 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -411,20 +411,20 @@ list get_notation_entries(environment const & env, head_index co return list(); } -environment overwrite_notation(environment const & env, name const & n) { +environment override_notation(environment const & env, name const & n, bool persistent) { environment r = env; bool found = false; if (auto it = token_ext::get_entries(r, n)) { found = true; for (token_entry e : *it) { - r = add_token(r, e); + r = add_token(r, e, persistent); } } if (auto it = notation_ext::get_entries(env, n)) { found = true; for (notation_entry const & e : *it) { notation_entry new_e(e, false); - r = add_notation(r, new_e); + r = add_notation(r, new_e, persistent); } } if (!found) diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h index 574cfa030..34267eff1 100644 --- a/src/frontends/lean/parser_config.h +++ b/src/frontends/lean/parser_config.h @@ -85,7 +85,7 @@ 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 overwrite_notation(environment const & env, name const & n); +environment override_notation(environment const & env, name const & n, bool persistent = true); /** \brief Add \c n as notation for \c e */ environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload = true, bool parse_only = false); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 5411b0dc3..0e167e5ce 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -114,7 +114,7 @@ void init_token_table(token_table & t) { "import", "inductive", "record", "structure", "module", "universe", "universes", "local", "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "tactic_infixl", "tactic_infixr", "tactic_infix", "tactic_postfix", "tactic_prefix", "tactic_notation", - "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint", + "exit", "set_option", "open", "export", "override", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint", "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent", "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq", diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 0ac6da4e2..31c888bfd 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -409,7 +409,8 @@ name get_decl_short_name(name const & d, environment const & env) { environment open_num_notation(environment const & env) { name num("num"); try { - environment new_env = overwrite_notation(env, num); + bool persistent = false; + environment new_env = override_notation(env, num, persistent); return overwrite_aliases(new_env, num, name()); } catch (exception &) { // num namespace is not available, then use only the aliases diff --git a/tests/lean/run/override1.lean b/tests/lean/run/override1.lean new file mode 100644 index 000000000..ba5cf06e5 --- /dev/null +++ b/tests/lean/run/override1.lean @@ -0,0 +1,24 @@ +import data.finset data.set + +open set + +example (A : Type) (x : A) (S H : set A) (Pin : x ∈ S) + (Psub : S ⊆ H) : x ∈ H := Psub Pin + +open finset + +section + override set -- set notation overrides existing one + + example (A : Type) (x : A) (S H : set A) (Pin : x ∈ S) + (Psub : S ⊆ H) : x ∈ H := Psub Pin +end + +-- ⊆ is now overloaded +example (A : Type) (x : A) (S H : set A) (Pin : x ∈ S) + (Psub : S ⊆ H) : x ∈ H := Psub _ Pin + + +override set -- overrides existing notation + +example (A : Type) (x : A) (S H : set A) (Pin : x ∈ S) (Psub : S ⊆ H) : x ∈ H := Psub Pin