From a74f02546b840097a154231c81fedd924df4a165 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 3 Sep 2016 17:11:29 -0700 Subject: [PATCH] refactor(*): remove `abbreviation` command --- src/emacs/lean-syntax.el | 6 +- src/frontends/lean/builtin_cmds.cpp | 8 +- src/frontends/lean/decl_cmds.cpp | 14 +-- src/frontends/lean/decl_cmds.h | 3 - src/frontends/lean/definition_cmds.cpp | 6 -- src/frontends/lean/init_module.cpp | 3 + src/frontends/lean/notation_cmd.cpp | 10 ++ src/frontends/lean/notation_cmd.h | 3 + src/frontends/lean/pp.cpp | 39 +------ src/frontends/lean/pp.h | 4 - src/frontends/lean/theorem_queue.cpp | 1 - src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 - src/frontends/lean/tokens.h | 1 - src/frontends/lean/tokens.txt | 1 - src/frontends/lean/util.cpp | 3 +- src/library/CMakeLists.txt | 5 +- src/library/abbreviation.cpp | 135 ------------------------- src/library/abbreviation.h | 19 ---- src/library/init_module.cpp | 3 - src/library/pp_options.cpp | 13 +-- src/library/pp_options.h | 2 - src/vim/syntax/lean.vim | 4 +- tests/lean/640b.lean | 3 - tests/lean/640b.lean.expected.out | 1 - tests/lean/abbrev1.lean | 20 ---- tests/lean/abbrev1.lean.expected.out | 6 -- tests/lean/abbrev2.lean | 26 ----- tests/lean/abbrev2.lean.expected.out | 14 --- tests/lean/pp_all.lean | 2 +- tests/lean/pp_all.lean.expected.out | 3 +- tests/lean/prodtst.lean | 2 +- tests/lean/run/fibrant_class1.lean | 16 --- tests/lean/run/fibrant_class2.lean | 32 ------ tests/lean/univ.lean | 4 +- tests/lean/univ.lean.expected.out | 2 - 36 files changed, 34 insertions(+), 386 deletions(-) delete mode 100644 src/library/abbreviation.cpp delete mode 100644 src/library/abbreviation.h delete mode 100644 tests/lean/640b.lean delete mode 100644 tests/lean/640b.lean.expected.out delete mode 100644 tests/lean/abbrev1.lean delete mode 100644 tests/lean/abbrev1.lean.expected.out delete mode 100644 tests/lean/abbrev2.lean delete mode 100644 tests/lean/abbrev2.lean.expected.out delete mode 100644 tests/lean/run/fibrant_class1.lean delete mode 100644 tests/lean/run/fibrant_class2.lean diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 2b068721e8..2cc13eb0f1 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -11,7 +11,7 @@ '("import" "prelude" "tactic_hint" "protected" "private" "inline" "noncomputable" "definition" "meta_definition" "renaming" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants" "meta_constant" "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory" - "print" "theorem" "proposition" "example" "abbreviation" "abstract" + "print" "theorem" "proposition" "example" "abstract" "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes" "alias" "help" "precedence" "reserve" "declare_trace" "add_key_equivalence" "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" @@ -131,7 +131,7 @@ ;; attributes after definitions (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary" - "hypothesis" "definition" "meta_definition" "constant" "meta_constant" "abbreviation")) + "hypothesis" "definition" "meta_definition" "constant" "meta_constant")) word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace))) (zero-or-more whitespace) (group (zero-or-more (not (any " \t\n\r{(["))))) @@ -161,7 +161,7 @@ ;; universe/inductive/theorem... "names" (without attributes) (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary" - "hypothesis" "definition" "meta_definition" "constant" "meta_constant" "abbreviation")) + "hypothesis" "definition" "meta_definition" "constant" "meta_constant")) word-end (zero-or-more whitespace) (group (zero-or-more (not (any " \t\n\r{(["))))) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index b53441c251..37fb45b52e 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -21,7 +21,6 @@ Author: Leonardo de Moura #include "library/normalize.h" #include "library/class.h" #include "library/flycheck.h" -#include "library/abbreviation.h" #include "library/user_recursors.h" #include "library/pp_options.h" #include "library/attribute_manager.h" @@ -168,7 +167,6 @@ environment end_scoped_cmd(parser & p) { environment check_cmd(parser & p) { expr e; level_param_names ls; std::tie(e, ls) = parse_local_expr(p); - e = expand_abbreviations(p.env(), e); auto tc = mk_type_checker(p.env()); expr type = tc->check(e, ls).first; auto out = regular(p.env(), p.ios(), tc->get_type_context()); @@ -338,9 +336,6 @@ static environment local_cmd(parser & p) { if (p.curr_is_token_or_id(get_attribute_tk())) { p.next(); return local_attribute_cmd(p); - } else if (p.curr_is_token(get_abbreviation_tk())) { - p.next(); - return local_abbreviation_cmd(p); } else { return local_notation_cmd(p); } @@ -580,8 +575,7 @@ static environment run_command_cmd(parser & p) { void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces", 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("export", "create aliases for declarations", export_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/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 4883e47c9a..a55e4d77fd 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -21,7 +21,6 @@ Author: Leonardo de Moura #include "library/placeholder.h" #include "library/locals.h" #include "library/explicit.h" -#include "library/abbreviation.h" #include "library/flycheck.h" #include "library/error_handling.h" #include "library/equations_compiler/equations.h" @@ -621,7 +620,7 @@ class definition_cmd_fn { bool is_meta() const { return m_kind == MetaDefinition; } bool is_trusted() const { return !is_meta(); } - bool is_definition() const { return m_kind == Definition || m_kind == MetaDefinition || m_kind == Abbreviation || m_kind == LocalAbbreviation; } + bool is_definition() const { return m_kind == Definition || m_kind == MetaDefinition; } bool is_example() const { return m_kind == Example; } unsigned start_line() const { return m_pos.first; } unsigned end_line() const { return m_end_pos.first; } @@ -875,10 +874,6 @@ class definition_cmd_fn { else m_env = add_expr_alias_rec(m_env, n, real_n); } - if (m_kind == Abbreviation || m_kind == LocalAbbreviation) { - bool persistent = m_kind == Abbreviation; - m_env = add_abbreviation(m_env, real_n, m_attributes.is_parsing_only(), persistent); - } if (generate_bytecode) compile_decl(); m_env = m_attributes.apply(m_env, m_p.ios(), real_n); @@ -1114,9 +1109,6 @@ static environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_pr decl_attributes const & attributes) { return definition_cmd_fn(p, kind, is_private, is_protected, is_noncomputable, attributes)(); } -environment local_abbreviation_cmd(parser & p) { - return definition_cmd_core(p, LocalAbbreviation, true, false, false, {}); -} static environment example_cmd(parser & p) { definition_cmd_core(p, Example, false, false, false, {}); return p.env(); @@ -1174,9 +1166,6 @@ static environment definition_cmd_ex(parser & p, decl_attributes const & attribu } else if (p.curr_is_token_or_id(get_meta_definition_tk())) { kind = MetaDefinition; p.next(); - } else if (p.curr_is_token_or_id(get_abbreviation_tk())) { - kind = Abbreviation; - p.next(); } else if (p.curr_is_token_or_id(get_theorem_tk())) { p.next(); kind = Theorem; @@ -1304,7 +1293,6 @@ void register_decl_cmds(cmd_table & r) { add_cmd(r, cmd_info("reveal", "reveal given theorems", reveal_cmd)); add_cmd(r, cmd_info("include", "force section parameter/variable to be included", include_cmd)); add_cmd(r, cmd_info("attribute", "set declaration attributes", attribute_cmd)); - add_cmd(r, cmd_info("abbreviation", "declare a new abbreviation", definition_cmd, false)); add_cmd(r, cmd_info("omit", "undo 'include' command", omit_cmd)); add_cmd(r, cmd_info("mutual_definition", "declare a mutually recursive definition", definition_cmd, false)); add_cmd(r, cmd_info("mutual_meta_definition", "declare a mutually recursive meta_definition", definition_cmd, false)); diff --git a/src/frontends/lean/decl_cmds.h b/src/frontends/lean/decl_cmds.h index 27a0ee3a8a..76451226c8 100644 --- a/src/frontends/lean/decl_cmds.h +++ b/src/frontends/lean/decl_cmds.h @@ -24,9 +24,6 @@ expr parse_local_equations(parser & p, expr const & fn); Then sort \c ls_buffer (using the order in which the universe levels were declared). */ void update_univ_parameters(buffer & ls_buffer, name_set const & found_ls, parser const & p); -/** \brief Parse a local abbreviation command */ -environment local_abbreviation_cmd(parser & p); - /** \brief Parse a local attribute command */ environment local_attribute_cmd(parser & p); void register_decl_cmds(cmd_table & r); diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 0779ad4da0..d1e1dd0247 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "library/typed_expr.h" #include "library/private.h" #include "library/protected.h" -#include "library/abbreviation.h" #include "library/scoped_ext.h" #include "library/noncomputable.h" #include "library/module.h" @@ -320,11 +319,6 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe new_env = ensure_decl_namespaces(new_env, c_real_name); } - if (kind == Abbreviation || kind == LocalAbbreviation) { - bool persistent = kind == Abbreviation; - new_env = add_abbreviation(new_env, c_real_name, attrs.is_parsing_only(), persistent); - } - new_env = attrs.apply(new_env, p.ios(), c_real_name); new_env = compile_decl(p, new_env, kind, is_noncomputable, c_name, c_real_name, pos); return mk_pair(new_env, c_real_name); diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index a0abe52d2e..2ef179f78e 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -29,6 +29,7 @@ Author: Leonardo de Moura #include "frontends/lean/old_attributes.h" #include "frontends/lean/elaborator.h" #include "frontends/lean/match_expr.h" +#include "frontends/lean/notation_cmd.h" namespace lean { void initialize_frontend_lean_module() { @@ -57,8 +58,10 @@ void initialize_frontend_lean_module() { initialize_nested_declaration(); initialize_match_expr(); initialize_elaborator(); + initialize_notation_cmd(); } void finalize_frontend_lean_module() { + finalize_notation_cmd(); finalize_elaborator(); finalize_match_expr(); finalize_old_attributes(); diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 0b87fdc481..6c678b2d04 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -829,4 +829,14 @@ bool is_notation_cmd(name const & n) { 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(); } + +void initialize_notation_cmd() { + register_system_attribute(basic_attribute::with_check( + "parsing_only", "parsing-only notation declaration", + [](environment const &, name const &, bool) { + throw exception("invalid '[parsing_only]' attribute can only be used in notation declarations"); + })); +} +void finalize_notation_cmd() { +} } diff --git a/src/frontends/lean/notation_cmd.h b/src/frontends/lean/notation_cmd.h index 98ffc15bbc..3552037591 100644 --- a/src/frontends/lean/notation_cmd.h +++ b/src/frontends/lean/notation_cmd.h @@ -23,4 +23,7 @@ environment local_notation_cmd(parser & p); void register_notation_cmds(cmd_table & r); bool is_notation_cmd(name const & cmd_name); + +void initialize_notation_cmd(); +void finalize_notation_cmd(); } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 1fe46146cf..62a0f6fe81 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -29,7 +29,6 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/let.h" #include "library/print.h" -#include "library/abbreviation.h" #include "library/pp_options.h" #include "library/delayed_abstraction.h" #include "library/constants.h" @@ -302,7 +301,6 @@ void pretty_fn::set_options_core(options const & _o) { o = o.update_if_undef(get_pp_beta_name(), false); o = o.update_if_undef(get_pp_numerals_name(), false); o = o.update_if_undef(get_pp_strings_name(), false); - o = o.update_if_undef(get_pp_abbreviations_name(), false); o = o.update_if_undef(get_pp_binder_types_name(), true); } m_options = o; @@ -322,7 +320,6 @@ void pretty_fn::set_options_core(options const & _o) { m_beta = get_pp_beta(o); m_numerals = get_pp_numerals(o); m_strings = get_pp_strings(o); - m_abbreviations = get_pp_abbreviations(o); m_preterm = get_pp_preterm(o); m_binder_types = get_pp_binder_types(o); m_hide_comp_irrel = get_pp_hide_comp_irrel(o); @@ -578,8 +575,6 @@ auto pretty_fn::pp_hide_coercion_fn(expr const & e, unsigned bp, bool ignore_hid } auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result { - if (auto it = is_abbreviated(e)) - return pp_abbreviation(e, *it, false, bp, ignore_hide); if (is_app(e)) { if (auto r = pp_local_ref(e)) return add_paren_if_needed(*r, bp); @@ -592,9 +587,7 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> resul if (auto r = to_char(e)) return pp_char_literal(*r); } expr const & f = app_fn(e); - if (auto it = is_abbreviated(f)) { - return pp_abbreviation(e, *it, true, bp, ignore_hide); - } else if (is_implicit(f)) { + if (is_implicit(f)) { return pp_child(f, bp, ignore_hide); } else if (!m_coercion && is_coercion(e)) { return pp_hide_coercion(e, bp, ignore_hide); @@ -633,19 +626,11 @@ optional pretty_fn::is_aliased(name const & n) const { } } -optional pretty_fn::is_abbreviated(expr const & e) const { - if (m_abbreviations) - return ::lean::is_abbreviated(m_env, e); - return optional(); -} - auto pretty_fn::pp_const(expr const & e, optional const & num_ref_univ_params) -> result { if (is_neutral_expr(e) && m_unicode) return format("◾"); if (is_unreachable_expr(e) && m_unicode) return format("⊥"); - if (auto it = is_abbreviated(e)) - return pp_abbreviation(e, *it, false); name n = const_name(e); if (m_notation && n == get_unit_star_name()) return format("()"); @@ -752,8 +737,6 @@ auto pretty_fn::pp_app(expr const & e) -> result { if (auto r = pp_local_ref(e)) return *r; expr const & fn = app_fn(e); - if (auto it = is_abbreviated(fn)) - return pp_abbreviation(e, *it, true); // If the application contains a metavariable, then we want to // show the function, otherwise it would be hard to understand the // context where the metavariable occurs. This is hack to implement @@ -1244,8 +1227,6 @@ static unsigned get_some_precedence(token_table const & t, name const & tk) { } auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> result { - if (auto it = is_abbreviated(e)) - return pp_abbreviation(e, *it, false, rbp); if (is_app(e)) { if (m_numerals) { if (auto n = to_num(e)) return pp_num(*n); @@ -1255,9 +1236,7 @@ auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> if (auto r = to_string(e)) return pp_string_literal(*r); } expr const & f = app_fn(e); - if (auto it = is_abbreviated(f)) { - return pp_abbreviation(e, *it, true, rbp); - } else if (is_implicit(f)) { + if (is_implicit(f)) { return pp_notation_child(f, lbp, rbp); } else if (!m_coercion && is_coercion(e)) { return pp_hide_coercion(e, rbp); @@ -1471,18 +1450,6 @@ auto pretty_fn::pp_notation(expr const & e) -> optional { return optional(); } -auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn, unsigned bp, bool ignore_hide) -> result { - declaration const & d = m_env.get(abbrev); - unsigned num_univs = d.get_num_univ_params(); - buffer ls; - for (unsigned i = 0; i < num_univs; i++) - ls.push_back(mk_meta_univ(name("?l", i+1))); - expr r = mk_constant(abbrev, to_list(ls)); - if (fn) - r = mk_app(r, app_arg(e)); - return pp_child(r, bp, ignore_hide); -} - static bool is_pp_atomic(expr const & e) { switch (e.kind()) { case expr_kind::App: @@ -1541,8 +1508,6 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result { return pp_proof_type(*t); } - if (auto n = is_abbreviated(e)) - return pp_abbreviation(e, *n, false); if (auto r = pp_notation(e)) return *r; diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 87ae742e76..bfd0a2581c 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -68,7 +68,6 @@ private: bool m_beta; bool m_numerals; bool m_strings; - bool m_abbreviations; bool m_hide_full_terms; bool m_hide_comp_irrel; bool m_preterm; @@ -87,7 +86,6 @@ private: bool is_prop(expr const & e); bool has_implicit_args(expr const & f); optional is_aliased(name const & n) const; - optional is_abbreviated(expr const & e) const; format pp_child(level const & l); format pp_max(level l); @@ -135,8 +133,6 @@ private: result pp_let(expr e); result pp_num(mpz const & n); result pp_proof_type(expr const & t); - // If fn is true, then \c e is of the form (f a), and the abbreviation is \c f. - result pp_abbreviation(expr const & e, name const & abbrev, bool fn, unsigned bp = 0, bool ignore_hide = false); void set_options_core(options const & o); expr infer_type(expr const & e); diff --git a/src/frontends/lean/theorem_queue.cpp b/src/frontends/lean/theorem_queue.cpp index e1d3631fe2..0d61fb817c 100644 --- a/src/frontends/lean/theorem_queue.cpp +++ b/src/frontends/lean/theorem_queue.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include #include "library/unfold_macros.h" -#include "library/abbreviation.h" #include "kernel/type_checker.h" #include "frontends/lean/theorem_queue.h" #include "frontends/lean/parser.h" diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 37fdcd0f23..57047252df 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -104,7 +104,7 @@ void init_token_table(token_table & t) { char const * commands[] = {"theorem", "axiom", "axioms", "variable", "protected", "private", "reveal", "definition", "meta_definition", "mutual_definition", "mutual_meta_definition", - "example", "coercion", "abbreviation", "noncomputable", + "example", "coercion", "noncomputable", "variables", "parameter", "parameters", "constant", "meta_constant", "constants", "[visible]", "[none]", "evaluate", "check", "eval", "vm_eval", "using_well_founded", "[whnf]", "[unfold_hints]", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 70ff8734ca..7cf07aa3dd 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -84,7 +84,6 @@ static name const * g_inline_tk = nullptr; static name const * g_definition_tk = nullptr; static name const * g_meta_definition_tk = nullptr; static name const * g_theorem_tk = nullptr; -static name const * g_abbreviation_tk = nullptr; static name const * g_axiom_tk = nullptr; static name const * g_axioms_tk = nullptr; static name const * g_constant_tk = nullptr; @@ -204,7 +203,6 @@ void initialize_tokens() { g_definition_tk = new name{"definition"}; g_meta_definition_tk = new name{"meta_definition"}; g_theorem_tk = new name{"theorem"}; - g_abbreviation_tk = new name{"abbreviation"}; g_axiom_tk = new name{"axiom"}; g_axioms_tk = new name{"axioms"}; g_constant_tk = new name{"constant"}; @@ -325,7 +323,6 @@ void finalize_tokens() { delete g_definition_tk; delete g_meta_definition_tk; delete g_theorem_tk; - delete g_abbreviation_tk; delete g_axiom_tk; delete g_axioms_tk; delete g_constant_tk; @@ -445,7 +442,6 @@ name const & get_inline_tk() { return *g_inline_tk; } name const & get_definition_tk() { return *g_definition_tk; } name const & get_meta_definition_tk() { return *g_meta_definition_tk; } name const & get_theorem_tk() { return *g_theorem_tk; } -name const & get_abbreviation_tk() { return *g_abbreviation_tk; } name const & get_axiom_tk() { return *g_axiom_tk; } name const & get_axioms_tk() { return *g_axioms_tk; } name const & get_constant_tk() { return *g_constant_tk; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index d73fe11430..81372e5316 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -86,7 +86,6 @@ name const & get_inline_tk(); name const & get_definition_tk(); name const & get_meta_definition_tk(); name const & get_theorem_tk(); -name const & get_abbreviation_tk(); name const & get_axiom_tk(); name const & get_axioms_tk(); name const & get_constant_tk(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index 9e706cedf4..30c9cb8a98 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -79,7 +79,6 @@ inline inline definition definition meta_definition meta_definition theorem theorem -abbreviation abbreviation axiom axiom axioms axioms constant constant diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 28438bf0d8..b7e7700bf2 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -19,7 +19,6 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/typed_expr.h" #include "library/placeholder.h" -#include "library/abbreviation.h" #include "library/unfold_macros.h" #include "library/choice.h" #include "library/num.h" @@ -372,7 +371,7 @@ char const * close_binder_string(binder_info const & bi, bool unicode) { } expr postprocess(environment const & env, expr const & e) { - return eta_reduce(expand_abbreviations(env, unfold_untrusted_macros(env, e))); + return eta_reduce(unfold_untrusted_macros(env, e)); } // Auxiliary object for eliminating choice-expressions associated with numerals. diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index a646dafb09..62761be937 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -7,9 +7,8 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp declaration_index.cpp class.cpp util.cpp print.cpp annotation.cpp quote.cpp typed_expr.cpp protected.cpp reducible.cpp init_module.cpp generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp pp_options.cpp - unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp - relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp - noncomputable.cpp + unfold_macros.cpp app_builder.cpp projection.cpp relation_manager.cpp + export.cpp user_recursors.cpp idx_metavar.cpp noncomputable.cpp aux_recursors.cpp norm_num.cpp trace.cpp attribute_manager.cpp error_handling.cpp unification_hint.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp deleted file mode 100644 index d66b84445b..0000000000 --- a/src/library/abbreviation.cpp +++ /dev/null @@ -1,135 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/sstream.h" -#include "kernel/find_fn.h" -#include "kernel/replace_fn.h" -#include "kernel/instantiate.h" -#include "library/attribute_manager.h" -#include "library/scoped_ext.h" -#include "library/expr_lt.h" -#include "library/util.h" -#include "library/normalize.h" -#include "library/reducible.h" - -namespace lean { -typedef pair abbrev_entry; - -struct abbrev_state { - name_set m_abbrevs; - rb_map m_inv_map; // for pretty printer - - void add(environment const & env, name const & n, bool parsing_only) { - declaration const & d = env.get(n); - if (!d.is_definition()) - throw exception(sstream() << "invalid abbreviation '" << n << "', it is not a definition"); - m_abbrevs.insert(n); - if (!parsing_only) { - expr v = try_eta(d.get_value()); - m_inv_map.insert(v, n); - } - } - - bool is_abbreviation(name const & n) const { return m_abbrevs.contains(n); } - - optional is_abbreviated(expr const & e) const { - if (auto it = m_inv_map.find(e)) - return optional(*it); - else - return optional(); - } -}; - -static name * g_class_name = nullptr; -static std::string * g_key = nullptr; - -struct abbrev_config { - typedef abbrev_state state; - typedef abbrev_entry entry; - static void add_entry(environment const & env, io_state const &, state & s, entry const & e) { - s.add(env, e.first, e.second); - } - static name const & get_class_name() { - return *g_class_name; - } - static std::string const & get_serialization_key() { - return *g_key; - } - static void write_entry(serializer & s, entry const & e) { - s << e.first << e.second; - } - static entry read_entry(deserializer & d) { - entry e; - d >> e.first >> e.second; - return e; - } - static optional get_fingerprint(entry const & e) { - return some(e.first.hash()); - } -}; - -template class scoped_ext; -typedef scoped_ext abbrev_ext; - -environment add_abbreviation(environment const & env, name const & n, bool parsing_only, bool persistent) { - auto env2 = abbrev_ext::add_entry(env, get_dummy_ios(), abbrev_entry(n, parsing_only), persistent); - return set_reducible(env2, n, reducible_status::Reducible, persistent); -} - -bool is_abbreviation(environment const & env, name const & n) { - abbrev_state const & s = abbrev_ext::get_state(env); - return s.is_abbreviation(n); -} - -bool is_parsing_only_abbreviation(environment const & env, name const & n) { - return has_attribute(env, "parsing_only", n); -} - -optional is_abbreviated(environment const & env, expr const & e) { - abbrev_state const & s = abbrev_ext::get_state(env); - return s.is_abbreviated(e); -} - -bool contains_abbreviations(environment const & env, expr const & e) { - abbrev_state const & s = abbrev_ext::get_state(env); - return static_cast(find(e, [&](expr const & e, unsigned) { - return is_constant(e) && s.is_abbreviation(const_name(e)); - })); -} - -expr expand_abbreviations(environment const & env, expr const & e) { - if (!contains_abbreviations(env, e)) - return e; - abbrev_state const & s = abbrev_ext::get_state(env); - return replace(e, [&](expr const & e, unsigned) { - if (is_constant(e) && s.is_abbreviation(const_name(e))) - return some_expr(try_eta(instantiate_value_univ_params(env.get(const_name(e)), const_levels(e)))); - else - return none_expr(); - }); -} - -void initialize_abbreviation() { - g_class_name = new name("abbreviation"); - g_key = new std::string("ABBREV"); - abbrev_ext::initialize(); - register_system_attribute(basic_attribute::with_check( - "parsing_only", "parsing-only abbreviation", - [](environment const & env, name const & d, bool) { - if (!is_abbreviation(env, d)) - throw exception( - sstream() << "invalid '[parsing_only]' attribute, " << d - << " is not an abbreviation"); - })); -} - -void finalize_abbreviation() { - abbrev_ext::finalize(); - delete g_key; - delete g_class_name; -} -} diff --git a/src/library/abbreviation.h b/src/library/abbreviation.h deleted file mode 100644 index 75b1f8b6ab..0000000000 --- a/src/library/abbreviation.h +++ /dev/null @@ -1,19 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "kernel/environment.h" - -namespace lean { -environment add_abbreviation(environment const & env, name const & n, bool parsing_only, bool persistent); -bool is_abbreviation(environment const & env, name const & n); -bool is_parsing_only_abbreviation(environment const & env, name const & n); -optional is_abbreviated(environment const & env, expr const & e); -bool contains_abbreviations(environment const & env, expr const & e); -expr expand_abbreviations(environment const & env, expr const & e); -void initialize_abbreviation(); -void finalize_abbreviation(); -} diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index e112c80e8f..099e3c3e1f 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -34,7 +34,6 @@ Author: Leonardo de Moura #include "library/pp_options.h" #include "library/projection.h" #include "library/normalize.h" -#include "library/abbreviation.h" #include "library/relation_manager.h" #include "library/user_recursors.h" #include "library/noncomputable.h" @@ -115,7 +114,6 @@ void initialize_library_module() { initialize_pp_options(); initialize_projection(); initialize_normalize(); - initialize_abbreviation(); initialize_relation_manager(); initialize_user_recursors(); initialize_noncomputable(); @@ -153,7 +151,6 @@ void finalize_library_module() { finalize_noncomputable(); finalize_user_recursors(); finalize_relation_manager(); - finalize_abbreviation(); finalize_normalize(); finalize_projection(); finalize_pp_options(); diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 6aa634836e..ea83a92bbd 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -63,10 +63,6 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_STRINGS true #endif -#ifndef LEAN_DEFAULT_PP_ABBREVIATIONS -#define LEAN_DEFAULT_PP_ABBREVIATIONS true -#endif - #ifndef LEAN_DEFAULT_PP_PRETERM #define LEAN_DEFAULT_PP_PRETERM false #endif @@ -111,7 +107,6 @@ static name * g_pp_purify_locals = nullptr; static name * g_pp_beta = nullptr; static name * g_pp_numerals = nullptr; static name * g_pp_strings = nullptr; -static name * g_pp_abbreviations = nullptr; static name * g_pp_preterm = nullptr; static name * g_pp_goal_compact = nullptr; static name * g_pp_goal_max_hyps = nullptr; @@ -136,7 +131,6 @@ void initialize_pp_options() { g_pp_beta = new name{"pp", "beta"}; g_pp_numerals = new name{"pp", "numerals"}; g_pp_strings = new name{"pp", "strings"}; - g_pp_abbreviations = new name{"pp", "abbreviations"}; g_pp_preterm = new name{"pp", "preterm"}; g_pp_binder_types = new name{"pp", "binder_types"}; g_pp_hide_comp_irrel = new name{"pp", "hide_comp_irrelevant"}; @@ -175,8 +169,6 @@ void initialize_pp_options() { "(pretty printer) display nat/num numerals in decimal notation"); register_bool_option(*g_pp_strings, LEAN_DEFAULT_PP_STRINGS, "(pretty printer) pretty print string and character literals"); - register_bool_option(*g_pp_abbreviations, LEAN_DEFAULT_PP_ABBREVIATIONS, - "(pretty printer) display abbreviations (i.e., revert abbreviation expansion when pretty printing)"); register_bool_option(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM, "(pretty printer) assume the term is a preterm (i.e., a term before elaboration)"); register_bool_option(*g_pp_goal_compact, LEAN_DEFAULT_PP_GOAL_COMPACT, @@ -191,7 +183,7 @@ void initialize_pp_options() { "(pretty printer) display the location of delayed-abstractions (for debugging purposes)"); register_bool_option(*g_pp_all, LEAN_DEFAULT_PP_ALL, "(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universes, " - "and disable abbreviations, beta reduction and notation during pretty printing"); + "and disable beta reduction and notation during pretty printing"); options universes_true(*g_pp_universes, true); options full_names_true(*g_pp_full_names, true); options implicit_true(*g_pp_implicit, true); @@ -208,7 +200,6 @@ void initialize_pp_options() { void finalize_pp_options() { delete g_pp_preterm; - delete g_pp_abbreviations; delete g_pp_numerals; delete g_pp_strings; delete g_pp_max_depth; @@ -244,7 +235,6 @@ name const & get_pp_beta_name() { return *g_pp_beta; } name const & get_pp_preterm_name() { return *g_pp_preterm; } name const & get_pp_numerals_name() { return *g_pp_numerals; } name const & get_pp_strings_name() { return *g_pp_strings; } -name const & get_pp_abbreviations_name() { return *g_pp_abbreviations; } name const & get_pp_binder_types_name() { return *g_pp_binder_types; } unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } @@ -261,7 +251,6 @@ bool get_pp_purify_locals(options const & opts) { return opts.get_bool(* bool get_pp_beta(options const & opts) { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); } bool get_pp_numerals(options const & opts) { return opts.get_bool(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS); } bool get_pp_strings(options const & opts) { return opts.get_bool(*g_pp_strings, LEAN_DEFAULT_PP_STRINGS); } -bool get_pp_abbreviations(options const & opts) { return opts.get_bool(*g_pp_abbreviations, LEAN_DEFAULT_PP_ABBREVIATIONS); } bool get_pp_preterm(options const & opts) { return opts.get_bool(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM); } bool get_pp_goal_compact(options const & opts) { return opts.get_bool(*g_pp_goal_compact, LEAN_DEFAULT_PP_GOAL_COMPACT); } unsigned get_pp_goal_max_hyps(options const & opts) { return opts.get_unsigned(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS); } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index 7fe39c2138..f03dd7ca05 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -19,7 +19,6 @@ name const & get_pp_beta_name(); name const & get_pp_preterm_name(); name const & get_pp_numerals_name(); name const & get_pp_strings_name(); -name const & get_pp_abbreviations_name(); name const & get_pp_binder_types_name(); unsigned get_pp_max_depth(options const & opts); @@ -36,7 +35,6 @@ bool get_pp_purify_metavars(options const & opts); bool get_pp_purify_locals(options const & opts); bool get_pp_numerals(options const & opts); bool get_pp_strings(options const & opts); -bool get_pp_abbreviations(options const & opts); bool get_pp_preterm(options const & opts); bool get_pp_goal_compact(options const & opts); unsigned get_pp_goal_max_hyps(options const & opts); diff --git a/src/vim/syntax/lean.vim b/src/vim/syntax/lean.vim index 19673143b4..91fb870e45 100644 --- a/src/vim/syntax/lean.vim +++ b/src/vim/syntax/lean.vim @@ -26,7 +26,7 @@ syn keyword leanKeyword import prelude tactic_hint protected private noncomputab syn keyword leanKeyword definition renaming hiding exposing parameter parameters syn keyword leanKeyword begin proof qed conjecture constant constants hypothesis lemma syn keyword leanKeyword corollary variable variables premise premises theory print theorem proposition -syn keyword leanKeyword example abbreviation abstract open as export override axiom axioms inductive +syn keyword leanKeyword example abstract open as export override axiom axioms inductive syn keyword leanKeyword with structure record universe universes alias help environment options syn keyword leanKeyword precedence reserve match infix infixl infixr notation postfix prefix syn keyword leanKeyword tactic_infix tactic_infixl tactic_infixr tactic_notation tactic_postfix @@ -47,7 +47,7 @@ syn keyword leanConstant → ∃ ∀ syn keyword leanModifier contained containedin=leanBracketEncl persistent notation visible instance trans_instance class parsing_only syn keyword leanModifier contained containedin=leanBracketEncl coercion unfold_full constructor reducible irreducible semireducible syn keyword leanModifier contained containedin=leanBracketEncl wf whnf multiple_instances none decls declarations coercions -syn keyword leanModifier contained containedin=leanBracketEncl classes symm subst refl trans simp congr notations abbreviations +syn keyword leanModifier contained containedin=leanBracketEncl classes symm subst refl trans simp congr notations syn keyword leanModifier contained containedin=leanBracketEncl begin_end_hints tactic_hints reduce_hints unfold_hints aliases eqv syn keyword leanModifier contained containedin=leanBracketEncl localrefinfo diff --git a/tests/lean/640b.lean b/tests/lean/640b.lean deleted file mode 100644 index e24647743c..0000000000 --- a/tests/lean/640b.lean +++ /dev/null @@ -1,3 +0,0 @@ -attribute [parsing_only] -abbreviation bar := @eq -check @bar diff --git a/tests/lean/640b.lean.expected.out b/tests/lean/640b.lean.expected.out deleted file mode 100644 index ce37f00e1f..0000000000 --- a/tests/lean/640b.lean.expected.out +++ /dev/null @@ -1 +0,0 @@ -eq : Π {A}, A → A → Prop diff --git a/tests/lean/abbrev1.lean b/tests/lean/abbrev1.lean deleted file mode 100644 index 22158f4124..0000000000 --- a/tests/lean/abbrev1.lean +++ /dev/null @@ -1,20 +0,0 @@ -open nat - -abbreviation foo : Π (A : Type), nat := λ a, 2 + 3 - -definition tst := foo nat - -set_option pp.abbreviations false - -print definition tst - -set_option pp.abbreviations true - -print definition tst - -attribute [parsing_only] -abbreviation id2 {A : Type} (a : A) := a - -definition tst1 :nat := id2 10 - -print definition tst1 diff --git a/tests/lean/abbrev1.lean.expected.out b/tests/lean/abbrev1.lean.expected.out deleted file mode 100644 index 673c6b9d96..0000000000 --- a/tests/lean/abbrev1.lean.expected.out +++ /dev/null @@ -1,6 +0,0 @@ -definition tst : ℕ -(λ a, 2 + 3) ℕ -definition tst : ℕ -foo ℕ -definition tst1 : ℕ -(λ A a, a) ℕ 10 diff --git a/tests/lean/abbrev2.lean b/tests/lean/abbrev2.lean deleted file mode 100644 index faf0a3b5ce..0000000000 --- a/tests/lean/abbrev2.lean +++ /dev/null @@ -1,26 +0,0 @@ -open nat - -namespace bla - local abbreviation foo : nat := 10 + 1 - definition tst : nat := foo - print definition tst -end bla - --- abbreviation is gone -print definition bla.tst - -check bla.foo -open bla -check foo - -print definition tst - -namespace bla2 - abbreviation foo2 : nat := 1 - definition tst2 : nat := foo2 - print definition tst2 -end bla2 - -print definition bla2.tst2 -open bla2 -print definition tst2 diff --git a/tests/lean/abbrev2.lean.expected.out b/tests/lean/abbrev2.lean.expected.out deleted file mode 100644 index af3b5851e9..0000000000 --- a/tests/lean/abbrev2.lean.expected.out +++ /dev/null @@ -1,14 +0,0 @@ -definition bla.tst : ℕ -foo -definition bla.tst : ℕ -10 + 1 -abbrev2.lean:12:6: error: unknown identifier 'bla.foo' -abbrev2.lean:14:6: error: unknown identifier 'foo' -definition bla.tst : ℕ -10 + 1 -definition bla2.tst2 : ℕ -foo2 -definition bla2.tst2 : ℕ -bla2.foo2 -definition bla2.tst2 : ℕ -foo2 diff --git a/tests/lean/pp_all.lean b/tests/lean/pp_all.lean index 7eabb987e1..1848a1c324 100644 --- a/tests/lean/pp_all.lean +++ b/tests/lean/pp_all.lean @@ -3,7 +3,7 @@ open nat variables {a : nat} -abbreviation b : num := 2 +definition b : num := 2 check (λ x, x) a + of_num b = 10 set_option pp.all true diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out index 0ca48d7bbc..0935a7d5a2 100644 --- a/tests/lean/pp_all.lean.expected.out +++ b/tests/lean/pp_all.lean.expected.out @@ -1,6 +1,5 @@ a + of_num b = 10 : Prop -@eq.{1} nat - (@add.{1} nat nat_has_add ((λ (x : nat), x) a) (nat.of_num (@bit0.{1} num num_has_add (@one.{1} num num_has_one)))) +@eq.{1} nat (@add.{1} nat nat_has_add ((λ (x : nat), x) a) (nat.of_num b)) (@bit0.{1} nat nat_has_add (@bit1.{1} nat nat_has_one nat_has_add (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one)))) : Prop diff --git a/tests/lean/prodtst.lean b/tests/lean/prodtst.lean index 5efe2561a7..7adf7e0c11 100644 --- a/tests/lean/prodtst.lean +++ b/tests/lean/prodtst.lean @@ -1,6 +1,6 @@ -- -inductive prod2 (A B : Type₊) +inductive prod2 (A B : Type.{_+1}) | mk : A → B → prod2 set_option pp.universes true diff --git a/tests/lean/run/fibrant_class1.lean b/tests/lean/run/fibrant_class1.lean deleted file mode 100644 index c8f077cec9..0000000000 --- a/tests/lean/run/fibrant_class1.lean +++ /dev/null @@ -1,16 +0,0 @@ -inductive [class] fibrant (T : Type) : Type -| fibrant_mk : fibrant - -inductive path {A : Type'} [fA : fibrant A] (a : A) : A → Type -| idpath : path a - -notation a ≈ b := path a b - -axiom path_fibrant {A : Type'} [fA : fibrant A] (a b : A) : fibrant (path a b) -attribute path_fibrant [instance] - -axiom imp_fibrant {A : Type'} {B : Type'} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A → B) -attribute imp_fibrant [instance] - -noncomputable definition test {A : Type} [fA : fibrant A] {x y : A} : -Π (z : A), y ≈ z → fibrant (x ≈ y → x ≈ z) := _ diff --git a/tests/lean/run/fibrant_class2.lean b/tests/lean/run/fibrant_class2.lean deleted file mode 100644 index 3f700942e7..0000000000 --- a/tests/lean/run/fibrant_class2.lean +++ /dev/null @@ -1,32 +0,0 @@ -inductive [class] fibrant (T : Type) : Type -| fibrant_mk : fibrant - -axiom pi_fibrant {A : Type} {B : A → Type} [C1 : fibrant A] [C2 : Πx : A, fibrant (B x)] : - fibrant (Πx : A, B x) -attribute pi_fibrant [instance] - -inductive path {A : Type} [fA : fibrant A] (a : A) : A → Type -| idpath : path a - -axiom path_fibrant {A : Type} [fA : fibrant A] (a b : A) : fibrant (path a b) -attribute path_fibrant [instance] - -notation a ≈ b := path a b - -noncomputable definition test {A : Type} [fA : fibrant A] {x y : A} : - Π (z : A), y ≈ z → fibrant (x ≈ y → x ≈ z) := take z p, _ - -noncomputable definition test2 {A : Type} [fA : fibrant A] {x y : A} : -Π (z : A), y ≈ z → fibrant (x ≈ y → x ≈ z) := _ - -noncomputable definition test3 {A : Type} [fA : fibrant A] {x y : A} : - Π (z : A), y ≈ z → fibrant (x ≈ z) := _ - -noncomputable definition test4 {A : Type} [fA : fibrant A] {x y z : A} : - fibrant (x ≈ y → x ≈ z) := _ - -axiom imp_fibrant {A : Type} {B : Type} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A → B) -attribute imp_fibrant [instance] - -noncomputable definition test5 {A : Type} [fA : fibrant A] {x y : A} : -Π (z : A), y ≈ z → fibrant (x ≈ y → x ≈ z) := _ diff --git a/tests/lean/univ.lean b/tests/lean/univ.lean index bc8d460eed..79dd3fd6ea 100644 --- a/tests/lean/univ.lean +++ b/tests/lean/univ.lean @@ -4,7 +4,7 @@ definition id2 (A : Type) (a : A) := a check id2 Type num -check id2 Type' num + check id2 Type.{1} num @@ -15,5 +15,3 @@ check id2 Type.{_+1} num check id2 Type.{0+1} num check id2 Type Type.{1} - -check id2 Type' Type.{1} diff --git a/tests/lean/univ.lean.expected.out b/tests/lean/univ.lean.expected.out index c59b66dc70..a37b2a4ed2 100644 --- a/tests/lean/univ.lean.expected.out +++ b/tests/lean/univ.lean.expected.out @@ -3,6 +3,4 @@ id2 Type₁ num : Type₁ id2 Type₁ num : Type₁ id2 Type₁ num : Type₁ id2 Type₁ num : Type₁ -id2 Type₁ num : Type₁ -id2 Type₂ Type₁ : Type₂ id2 Type₂ Type₁ : Type₂