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

refactor(*): remove abbreviation command

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-03 17:11:29 -07:00
parent 9a17d567ec
commit a74f02546b
36 changed files with 34 additions and 386 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/emacs/lean-syntax.el
View file

@ -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{([")))))

8
src/frontends/lean/builtin_cmds.cpp
View file

@ -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));

14
src/frontends/lean/decl_cmds.cpp
View file

@ -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));

3
src/frontends/lean/decl_cmds.h
View file

@ -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<name> & 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);

6
src/frontends/lean/definition_cmds.cpp
View file

@ -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);

3
src/frontends/lean/init_module.cpp
View file

@ -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();

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

@ -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() {
}
}

3
src/frontends/lean/notation_cmd.h
View file

@ -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();
}

39
src/frontends/lean/pp.cpp
View file

@ -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<name> pretty_fn::is_aliased(name const & n) const {
}
}
optional<name> pretty_fn::is_abbreviated(expr const & e) const {
if (m_abbreviations)
return ::lean::is_abbreviated(m_env, e);
return optional<name>();
}
auto pretty_fn::pp_const(expr const & e, optional<unsigned> 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<result> {
return optional<result>();
}
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<level> 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;

4
src/frontends/lean/pp.h
View file

@ -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<name> is_aliased(name const & n) const;
optional<name> 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);

1
src/frontends/lean/theorem_queue.cpp
View file

@ -6,7 +6,6 @@ Author: Leonardo de Moura
*/
#include <vector>
#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"

2
src/frontends/lean/token_table.cpp
View file

@ -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]",

4
src/frontends/lean/tokens.cpp
View file

@ -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; }

1
src/frontends/lean/tokens.h
View file

@ -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();

1
src/frontends/lean/tokens.txt
View file

@ -79,7 +79,6 @@ inline inline
definition definition
meta_definition meta_definition
theorem theorem
abbreviation abbreviation
axiom axiom
axioms axioms
constant constant

3
src/frontends/lean/util.cpp
View file

@ -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.

5
src/library/CMakeLists.txt
View file

@ -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

135
src/library/abbreviation.cpp
View file

@ -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 <string>
#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<name, bool> abbrev_entry;
struct abbrev_state {
name_set m_abbrevs;
rb_map<expr, name, expr_cmp_no_level_params> 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<name> is_abbreviated(expr const & e) const {
if (auto it = m_inv_map.find(e))
return optional<name>(*it);
else
return optional<name>();
}
};
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<unsigned> get_fingerprint(entry const & e) {
return some(e.first.hash());
}
};
template class scoped_ext<abbrev_config>;
typedef scoped_ext<abbrev_config> 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<name> 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<bool>(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;
}
}

19
src/library/abbreviation.h
View file

@ -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<name> 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();
}

3
src/library/init_module.cpp
View file

@ -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();

13
src/library/pp_options.cpp
View file

@ -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); }

2
src/library/pp_options.h
View file

@ -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);

4
src/vim/syntax/lean.vim
View file

@ -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

3
tests/lean/640b.lean
View file

@ -1,3 +0,0 @@
attribute [parsing_only]
abbreviation bar := @eq
check @bar

1
tests/lean/640b.lean.expected.out
View file

@ -1 +0,0 @@
eq : Π {A}, A → A → Prop

20
tests/lean/abbrev1.lean
View file

@ -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

6
tests/lean/abbrev1.lean.expected.out
View file

@ -1,6 +0,0 @@
definition tst : ℕ
(λ a, 2 + 3) ℕ
definition tst : ℕ
foo ℕ
definition tst1 : ℕ
(λ A a, a) ℕ 10

26
tests/lean/abbrev2.lean
View file

@ -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

14
tests/lean/abbrev2.lean.expected.out
View file

@ -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

2
tests/lean/pp_all.lean
View file

@ -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

3
tests/lean/pp_all.lean.expected.out
View file

@ -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

2
tests/lean/prodtst.lean
View file

@ -1,6 +1,6 @@
--
inductive prod2 (A B : Type₊)
inductive prod2 (A B : Type.{_+1})
| mk : A → B → prod2
set_option pp.universes true

16
tests/lean/run/fibrant_class1.lean
View file

@ -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) := _

32
tests/lean/run/fibrant_class2.lean
View file

@ -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) := _

4
tests/lean/univ.lean
View file

@ -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}

2
tests/lean/univ.lean.expected.out
View file

@ -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₂