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

feat(library/annotation): remove annonation macro

Browse source 
We now use the new `expr.mdata` constructor.
This commit is contained in:
Leonardo de Moura 2018-06-18 13:33:21 -07:00
parent 9d7609ac66
commit b84090aaca
18 changed files with 132 additions and 213 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/init/lean/macro.lean
View file

@ -26,7 +26,6 @@ Cases missing:
-/
inductive macro_definition
| annotation : name → macro_definition
/- The following macros will be Syntax object in Lean4 -/
| struct_instance : name → bool → list name → macro_definition
| field_notation : name → nat → macro_definition

2
library/init/meta/tactic.lean
View file

@ -505,7 +505,7 @@ meta def istep {α : Type u} (line0 col0 : ℕ) (line col : ℕ) (t : tactic α)
meta def is_prop (e : expr) : tactic bool :=
do t ← infer_type e,
return (t = `(Prop))
return (t = expr.sort level.zero)
/-- Return true iff n is the name of declaration that is a proposition. -/
meta def is_prop_decl (n : name) : tactic bool :=

79
src/frontends/lean/elaborator.cpp
View file

@ -969,7 +969,7 @@ expr elaborator::visit_function(expr const & fn, bool has_args, optional<expr> c
case expr_kind::FVar: r = fn; break;
case expr_kind::Constant: r = visit_const_core(fn); break;
case expr_kind::Macro: r = visit_macro(fn, expected_type, true); break;
case expr_kind::MData: r = visit_mdata(fn, expected_type); break;
case expr_kind::MData: r = visit_mdata(fn, expected_type, true); break;
case expr_kind::Lambda: r = visit_lambda(fn, expected_type); break;
case expr_kind::Let: r = visit_let(fn, expected_type); break;
case expr_kind::Quote:
@ -2525,10 +2525,16 @@ class validate_and_collect_lhs_mvars : public replace_visitor {
return visit_app(e);
}
virtual expr visit_macro(expr const & e) override {
virtual expr visit_mdata(expr const & e) override {
if (is_inaccessible(e)) {
return e;
} else if (is_as_pattern(e)) {
} else {
return visit(mdata_expr(e));
}
}
virtual expr visit_macro(expr const & e) override {
if (is_as_pattern(e)) {
expr new_lhs = visit(get_as_pattern_lhs(e));
expr new_rhs = visit(get_as_pattern_rhs(e));
return mk_as_pattern(new_lhs, new_rhs);
@ -2541,8 +2547,6 @@ class validate_and_collect_lhs_mvars : public replace_visitor {
return mk_structure_instance(info);
} else if (auto r = ctx().expand_macro(e)) {
return visit(*r);
} else if (is_synthetic_sorry(e)) {
return e;
} else {
throw_invalid_pattern("invalid occurrence of macro expression in pattern", e);
return e;
@ -2652,7 +2656,7 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
for (expr const & local_mvar : local_mvars) {
expr s = instantiate_mvars(local_mvar);
if (!is_local(s)) {
/* The `as_is` macro affects how applications are elaborated.
/* The `as_is` annotation affects how applications are elaborated.
See comment at first_pass method.
So, we only use it if it is really needed. That is,
the metavariable was fixed to a non trivial term by type inference rules.
@ -3355,24 +3359,44 @@ expr elaborator::visit_expr_quote(expr const & e, optional<expr> const & expecte
return visit(q, expected_type);
}
expr elaborator::visit_mdata(expr const & e, optional<expr> const & expected_type) {
expr new_e = visit(mdata_expr(e), expected_type);
return update_mdata(e, new_e);
}
expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
expr elaborator::visit_mdata(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
if (is_as_is(e)) {
return get_as_is_arg(e);
} else if (is_hole(e)) {
return visit_hole(e, expected_type);
} else if (is_explicit(e) || is_partial_explicit(e)) {
return visit_app_core(e, buffer<expr>(), expected_type, e);
} else if (is_anonymous_constructor(e)) {
if (is_app_fn)
throw elaborator_exception(e, "invalid constructor ⟨...⟩, function expected");
return visit_anonymous_constructor(e, expected_type);
} else if (is_choice(e) || is_explicit(e) || is_partial_explicit(e)) {
return visit_app_core(e, buffer<expr>(), expected_type, e);
} else if (is_by(e)) {
return visit_by(e, expected_type);
} else if (is_hole(e)) {
return visit_hole(e, expected_type);
} else if (is_as_atomic(e)) {
/* ignore annotation */
expr new_e = visit(get_as_atomic_arg(e), none_expr());
if (is_app_fn)
return new_e;
/* If the as_atomic macro is not the the function in a function application, then we need to consume
implicit arguments. */
return visit_base_app_core(new_e, arg_mask::Default, buffer<expr>(), true, expected_type, e);
} else if (is_expr_quote(e)) {
return visit_expr_quote(e, expected_type);
} else if (is_inaccessible(e)) {
if (is_app_fn)
throw elaborator_exception(e, "invalid inaccessible term, function expected");
return visit_inaccessible(e, expected_type);
} else if (is_frozen_name(e)) {
return visit(get_annotation_arg(e), expected_type);
} else {
expr new_e = visit(mdata_expr(e), expected_type);
return update_mdata(e, new_e);
}
}
expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
if (is_choice(e)) {
return visit_app_core(e, buffer<expr>(), expected_type, e);
} else if (is_equations(e)) {
lean_assert(!is_app_fn); // visit_convoy is used in this case
return visit_equations(e);
@ -3388,29 +3412,8 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
return new_rhs;
} else if (is_field_notation(e)) {
return visit_field(e, expected_type);
} else if (is_expr_quote(e)) {
return visit_expr_quote(e, expected_type);
} else if (is_inaccessible(e)) {
if (is_app_fn)
throw elaborator_exception(e, "invalid inaccessible term, function expected");
return visit_inaccessible(e, expected_type);
} else if (is_as_atomic(e)) {
/* ignore annotation */
expr new_e = visit(get_as_atomic_arg(e), none_expr());
if (is_app_fn)
return new_e;
/* If the as_atomic macro is not the the function in a function application, then we need to consume
implicit arguments. */
return visit_base_app_core(new_e, arg_mask::Default, buffer<expr>(), true, expected_type, e);
} else if (is_sorry(e)) {
return mk_sorry(expected_type, e, is_synthetic_sorry(e));
} else if (is_structure_instance(e)) {
return visit_structure_instance(e, expected_type);
} else if (is_frozen_name(e)) {
return visit(get_annotation_arg(e), expected_type);
} else if (is_annotation(e)) {
expr r = visit(get_annotation_arg(e), expected_type);
return update_macro(e, 1, &r);
} else {
buffer<expr> args;
for (unsigned i = 0; i < macro_num_args(e); i++)
@ -3654,7 +3657,7 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
}
lean_unreachable();
case expr_kind::MData:
return copy_pos(e, visit_mdata(e, expected_type));
return copy_pos(e, visit_mdata(e, expected_type, false));
case expr_kind::Sort:
return copy_pos(e, visit_sort(e));
case expr_kind::FVar:

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

@ -236,7 +236,7 @@ private:
expr visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn);
expr visit_lambda(expr const & e, optional<expr> const & expected_type);
expr visit_pi(expr const & e);
expr visit_mdata(expr const & e, optional<expr> const & expected_type);
expr visit_mdata(expr const & e, optional<expr> const & expected_type, bool is_app_fn);
expr visit_app(expr const & e, optional<expr> const & expected_type);
expr visit_let(expr const & e, optional<expr> const & expected_type);
expr visit_convoy(expr const & e, optional<expr> const & expected_type);

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

@ -302,15 +302,12 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
copy_with_new_pos(let_value(e), p),
copy_with_new_pos(let_body(e), p)),
p);
case expr_kind::Macro:
if (is_pexpr_quote(e)) {
return save_pos(mk_pexpr_quote(copy_with_new_pos(get_pexpr_quote_value(e), p)), p);
} else {
buffer<expr> args;
for (unsigned i = 0; i < macro_num_args(e); i++)
args.push_back(copy_with_new_pos(macro_arg(e, i), p));
return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
}
case expr_kind::Macro: {
buffer<expr> args;
for (unsigned i = 0; i < macro_num_args(e); i++)
args.push_back(copy_with_new_pos(macro_arg(e, i), p));
return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
}
case expr_kind::Quote:
if (is_pexpr_quote(e)) {
return save_pos(mk_pexpr_quote(copy_with_new_pos(get_pexpr_quote_value(e), p)), p);
@ -1745,8 +1742,6 @@ static expr quote(expr const & e) {
return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
case expr_kind::MVar:
return mk_expr_placeholder();
case expr_kind::MData:
throw exception("expr.mdata is not supported at quote function");
case expr_kind::FVar:
throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
<< mlocal_pp_name(e) << "'");
@ -1767,13 +1762,14 @@ static expr quote(expr const & e) {
case expr_kind::Let:
return mk_app(mk_constant({"expr", "elet"}), mk_expr_placeholder(), quote(let_type(e)),
quote(let_value(e)), quote(let_body(e)));
case expr_kind::Macro:
case expr_kind::MData:
if (is_antiquote(e))
return get_antiquote_expr(e);
if (is_typed_expr(e))
return mk_typed_expr(quote(get_typed_expr_expr(e)), quote(get_typed_expr_type(e)));
if (is_inaccessible(e))
else if (is_inaccessible(e))
return mk_expr_placeholder();
else
throw exception("expr.mdata is not supported at quote function");
case expr_kind::Macro:
throw elaborator_exception(e, sstream() << "invalid quotation, unsupported macro '"
<< macro_def(e).get_name() << "'");
case expr_kind::Quote:
@ -1874,11 +1870,11 @@ class patexpr_to_expr_fn : public replace_visitor {
return update_let(e, new_type, new_val, new_body);
}
virtual expr visit_macro(expr const & e) override {
virtual expr visit_mdata(expr const & e) override {
if (is_inaccessible(e) && is_placeholder(get_annotation_arg(e))) {
return get_annotation_arg(e);
} else {
return replace_visitor::visit_macro(e);
return replace_visitor::visit_mdata(e);
}
}

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

@ -1130,16 +1130,7 @@ auto pretty_fn::pp_macro_default(expr const & e) -> result {
}
auto pretty_fn::pp_macro(expr const & e) -> result {
if (is_explicit(e)) {
return pp_explicit(e);
} else if (is_expr_quote(e)) {
return result(format("`(") + nest(4, pp(get_expr_quote_value(e)).fmt()) + format(")"));
} else if (is_pexpr_quote(e)) {
return result(format("``(") + nest(2, pp(get_pexpr_quote_value(e)).fmt()) + format(")"));
} else if (is_inaccessible(e)) {
format r = format(".") + pp_child(get_annotation_arg(e), max_bp()).fmt();
return result(r);
} else if (is_as_pattern(e)) {
if (is_as_pattern(e)) {
auto lhs_fmt = pp_child(get_as_pattern_lhs(e), max_bp()).fmt();
auto rhs_fmt = pp_child(get_as_pattern_rhs(e), max_bp()).fmt();
return result(lhs_fmt + format("@") + rhs_fmt);
@ -1152,25 +1143,31 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
return m_unicode ? format("◾") : format("irrel");
else
return pp(get_annotation_arg(e));
} else if (!m_strings && to_string(e)) {
expr n = *macro_def(e).expand(e, m_ctx);
return pp(n);
} else if (is_equations(e)) {
if (auto r = pp_equations(e))
return *r;
else
return pp_macro_default(e);
} else {
return pp_macro_default(e);
}
}
auto pretty_fn::pp_mdata(expr const & e) -> result {
if (is_explicit(e)) {
return pp_explicit(e);
} else if (is_expr_quote(e)) {
return result(format("`(") + nest(4, pp(get_expr_quote_value(e)).fmt()) + format(")"));
} else if (is_inaccessible(e)) {
format r = format(".") + pp_child(get_annotation_arg(e), max_bp()).fmt();
return result(r);
} else if (is_annotation(e)) {
if (m_annotations)
return format("[") + format(get_annotation_kind(e)) + space() + pp(get_annotation_arg(e)).fmt() + format("]");
else
return pp(get_annotation_arg(e));
} else if (is_synthetic_sorry(e)) {
return m_unicode ? format("⁇") : format("??");
} else if (is_sorry(e)) {
return format("sorry");
} else {
return pp_macro_default(e);
return pp(mdata_expr(e));
}
}
@ -1784,7 +1781,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
case expr_kind::BVar: return pp_var(e);
case expr_kind::FVar: return pp_local(e);
case expr_kind::Sort: return pp_sort(e);
case expr_kind::MData: return pp(mdata_expr(e), ignore_hide);
case expr_kind::MData: return pp_mdata(e);
case expr_kind::Constant: return pp_const(e);
case expr_kind::MVar: return pp_meta(e);
case expr_kind::App: return pp_app(e);

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

@ -153,6 +153,7 @@ private:
result pp_explicit(expr const & e);
result pp_delayed_abstraction(expr const & e);
result pp_let(expr e);
result pp_mdata(expr const & e);
result pp_num(mpz const & n, unsigned bp);
result pp_prod(expr const & e);
result pp_lit(expr const & e);

109
src/library/annotation.cpp
View file

@ -15,77 +15,26 @@ Author: Leonardo de Moura
namespace lean {
static name * g_annotation = nullptr;
static std::string * g_annotation_opcode = nullptr;
name const & get_annotation_name() { return *g_annotation; }
std::string const & get_annotation_opcode() { return *g_annotation_opcode; }
/** \brief We use a macro to mark expressions that denote "let" and "have"-expressions.
These marks have no real semantic meaning, but are useful for helping Lean's pretty printer.
*/
class annotation_macro_definition_cell : public macro_definition_cell {
name m_name;
void check_macro(expr const & m) const {
if (!is_macro(m) || macro_num_args(m) != 1)
throw exception(sstream() << "invalid '" << m_name << "' annotation, incorrect number of arguments");
}
public:
annotation_macro_definition_cell(name const & n):m_name(n) {}
name const & get_annotation_kind() const { return m_name; }
virtual name get_name() const override { return get_annotation_name(); }
virtual void display(std::ostream & out) const override { out << m_name; }
virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const override {
check_macro(m);
return ctx.check(macro_arg(m, 0), infer_only);
}
virtual optional<expr> expand(expr const & m, abstract_type_context &) const override {
check_macro(m);
return some_expr(macro_arg(m, 0));
}
virtual void write(serializer & s) const override {
s.write_string(get_annotation_opcode());
s << m_name;
}
virtual bool operator==(macro_definition_cell const & other) const override {
if (auto other_ptr = dynamic_cast<annotation_macro_definition_cell const *>(&other)) {
return m_name == other_ptr->m_name;
} else {
return false;
}
}
virtual unsigned hash() const override {
return ::lean::hash(m_name.hash(), g_annotation->hash());
}
};
typedef std::unordered_map<name, macro_definition, name_hash, name_eq> annotation_macros;
static annotation_macros * g_annotation_macros = nullptr;
annotation_macros & get_annotation_macros() { return *g_annotation_macros; }
void register_annotation(name const & n) {
annotation_macros & ms = get_annotation_macros();
lean_assert(ms.find(n) == ms.end());
ms.insert(mk_pair(n, macro_definition(new annotation_macro_definition_cell(n))));
kvmap mk_annotation_kvmap(name const & k) {
return set_name(kvmap(), *g_annotation, k);
}
expr mk_annotation(name const & kind, expr const & e) {
annotation_macros & ms = get_annotation_macros();
auto it = ms.find(kind);
if (it != ms.end()) {
return copy_pos(e, mk_macro(it->second, 1, &e));
} else {
throw exception(sstream() << "unknown annotation kind '" << kind << "'");
}
typedef std::unordered_map<name, kvmap, name_hash, name_eq> annotation_maps;
static annotation_maps * g_annotation_maps = nullptr;
void register_annotation(name const & kind) {
lean_assert(g_annotation_maps->find(kind) == g_annotation_maps->end());
g_annotation_maps->insert(mk_pair(kind, mk_annotation_kvmap(kind)));
}
bool is_annotation(expr const & e) {
return is_macro(e) && macro_def(e).get_name() == get_annotation_name();
return is_mdata(e) && get_name(mdata_data(e), *g_annotation);
}
name const & get_annotation_kind(expr const & e) {
name get_annotation_kind(expr const & e) {
lean_assert(is_annotation(e));
return static_cast<annotation_macro_definition_cell const*>(macro_def(e).raw())->get_annotation_kind();
return *get_name(mdata_data(e), *g_annotation);
}
bool is_annotation(expr const & e, name const & kind) {
@ -94,7 +43,19 @@ bool is_annotation(expr const & e, name const & kind) {
expr const & get_annotation_arg(expr const & e) {
lean_assert(is_annotation(e));
return macro_arg(e, 0);
return mdata_expr(e);
}
expr mk_annotation(name const & kind, expr const & e) {
auto it = g_annotation_maps->find(kind);
if (it != g_annotation_maps->end()) {
expr r = copy_pos(e, mk_mdata(it->second, e));
lean_assert(is_annotation(r));
lean_assert(get_annotation_kind(r) == kind);
return r;
} else {
throw exception(sstream() << "unknown annotation kind '" << kind << "'");
}
}
bool is_nested_annotation(expr const & e, name const & kind) {
@ -146,26 +107,16 @@ bool is_checkpoint_annotation(expr const & e) { return is_annotation(e, *g_check
void initialize_annotation() {
g_annotation = new name("annotation");
g_annotation_opcode = new std::string("Annot");
g_annotation_macros = new annotation_macros();
g_have = new name("have");
g_show = new name("show");
g_suffices = new name("suffices");
g_checkpoint = new name("checkpoint");
g_annotation_maps = new annotation_maps();
g_have = new name("have");
g_show = new name("show");
g_suffices = new name("suffices");
g_checkpoint = new name("checkpoint");
register_annotation(*g_have);
register_annotation(*g_show);
register_annotation(*g_suffices);
register_annotation(*g_checkpoint);
register_macro_deserializer(get_annotation_opcode(),
[](deserializer & d, unsigned num, expr const * args) {
if (num != 1)
throw corrupted_stream_exception();
name k;
d >> k;
return mk_annotation(k, args[0]);
});
}
void finalize_annotation() {
@ -173,8 +124,6 @@ void finalize_annotation() {
delete g_show;
delete g_have;
delete g_suffices;
delete g_annotation_macros;
delete g_annotation_opcode;
delete g_annotation;
}
}

5
src/library/annotation.h
View file

@ -10,8 +10,7 @@ Author: Leonardo de Moura
namespace lean {
/** \brief Declare a new kind of annotation. It must only be invoked at startup time
Use helper obect #register_annotation_fn.
*/
Use helper obect #register_annotation_fn. */
void register_annotation(name const & n);
/** \brief Create an annotated expression with tag \c kind based on \c e.
@ -41,7 +40,7 @@ expr const & get_annotation_arg(expr const & e);
\post get_annotation_arg(mk_annotation(k, e)) == k
*/
name const & get_annotation_kind(expr const & e);
name get_annotation_kind(expr const & e);
/** \brief Return the nested annotated expression, \c e must have been created using #mk_annotation.
This function is the "transitive" version of #get_annotation_arg.

16
src/library/compiler/eta_expansion.cpp
View file

@ -165,22 +165,6 @@ class eta_expand_fn : public compiler_step_visitor {
return expand_if_needed(e);
}
virtual expr visit_macro(expr const & e) override {
if (is_sorry(e)) {
/* We η-expand sorrys to be able to execute tactic scripts with syntax errors.
For example, when we parse and elaborate `by { simp, simmp }`, we get
something like `simp >> ??`.
With η-expansion, the composite tactic becomes `simp >> (λ s, ?? s)`,
and the execution only fails when we arrive at the syntax error.
*/
m_saw_sorry = true;
return eta_expand(e);
} else {
return compiler_step_visitor::visit_macro(e);
}
}
virtual expr visit_app(expr const & e) override {
if (is_constant(get_app_fn(e)))
return expand_if_needed(e);

5
src/library/compiler/lambda_lifting.cpp
View file

@ -205,11 +205,6 @@ class lambda_lifting_fn : public compiler_step_visitor {
}
}
virtual expr visit_macro(expr const & e) override {
if (is_sorry(e)) m_saw_sorry = true;
return compiler_step_visitor::visit_macro(e);
}
public:
lambda_lifting_fn(environment const & env, abstract_context_cache & cache, name const & prefix):
compiler_step_visitor(env, cache), m_prefix(prefix), m_idx(1) {

14
src/library/compiler/vm_compiler.cpp
View file

@ -274,17 +274,9 @@ class vm_compiler_fn {
emit(mk_drop_instr(counter));
}
void compile_macro(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
if (is_annotation(e)) {
compile(get_annotation_arg(e), bpz, m);
} else if (is_expr_quote(e)) {
emit(mk_expr_instr(get_expr_quote_value(e)));
} else if (is_pexpr_quote(e)) {
emit(mk_expr_instr(get_pexpr_quote_value(e)));
} else {
throw exception(sstream() << "code generation failed, unexpected kind of macro has been found: '"
<< macro_def(e).get_name() << "'");
}
void compile_macro(expr const & e, unsigned /* bpz */, name_map<unsigned> const & /* m */) {
throw exception(sstream() << "code generation failed, unexpected kind of macro has been found: '"
<< macro_def(e).get_name() << "'");
}
void compile_quote(expr const & e) {

4
src/library/equations_compiler/util.cpp
View file

@ -223,11 +223,11 @@ bool has_inaccessible_annotation(expr const & e) {
}
class erase_inaccessible_annotations_fn : public replace_visitor {
virtual expr visit_macro(expr const & e) override {
virtual expr visit_mdata(expr const & e) override {
if (is_inaccessible(e)) {
return visit(get_annotation_arg(e));
} else {
return replace_visitor::visit_macro(e);
return replace_visitor::visit_mdata(e);
}
}
};

4
src/library/metavar_util.h
View file

@ -170,6 +170,10 @@ class instantiate_mvars_fn : public replace_visitor {
return mk_rev_app(new_f, new_args);
}
virtual expr visit_mdata(expr const & e) override {
return update_mdata(e, visit(mdata_expr(e)));
}
virtual expr visit_macro(expr const & e) override {
lean_assert(is_macro(e));
buffer<expr> new_args;

10
src/library/noncomputable.cpp
View file

@ -142,6 +142,14 @@ struct get_noncomputable_reason_fn {
return !is_sort(type);
}
void visit_mdata(expr const & e) {
if (is_expr_quote(e) || is_pexpr_quote(e))
return;
if (should_visit(e)) {
visit(mdata_expr(e));
}
}
void visit_macro(expr const & e) {
if (is_expr_quote(e) || is_pexpr_quote(e))
return;
@ -200,7 +208,7 @@ struct get_noncomputable_reason_fn {
case expr_kind::Lambda: visit_binding(e); return;
case expr_kind::Pi: visit_binding(e); return;
case expr_kind::Let: visit_let(e); return;
case expr_kind::MData: visit(mdata_expr(e)); return;
case expr_kind::MData: visit_mdata(e); return;
case expr_kind::Quote: return;
}
}

4
src/library/replace_visitor.cpp
View file

@ -24,7 +24,9 @@ expr replace_visitor::visit_mlocal(expr const & e) {
}
expr replace_visitor::visit_meta(expr const & e) { return visit_mlocal(e); }
expr replace_visitor::visit_local(expr const & e) { return visit_mlocal(e); }
expr replace_visitor::visit_mdata(expr const & e) { return visit(mdata_expr(e)); }
expr replace_visitor::visit_mdata(expr const & e) {
return update_mdata(e, visit(mdata_expr(e)));
}
expr replace_visitor::visit_app(expr const & e) {
lean_assert(is_app(e));
expr new_fn = visit(app_fn(e));

6
src/library/tactic/simplify.cpp
View file

@ -1071,11 +1071,7 @@ simp_result simplify_ext_core_fn::visit_pi(expr const & e) {
}
simp_result simplify_ext_core_fn::visit_macro(expr const & e) {
if (is_annotation(e)) {
return visit(get_annotation_arg(e), none_expr());
} else {
return simplify_core_fn::visit_macro(e);
}
return simplify_core_fn::visit_macro(e);
}
simp_result simplify_ext_core_fn::visit_let(expr const & e) {

18
src/library/type_context.cpp
View file

@ -737,7 +737,6 @@ optional<expr> type_context_old::reduce_large_elim_recursor(expr const & e) {
return none_expr();
}
optional<expr> type_context_old::expand_macro(expr const & e) {
lean_assert(is_macro(e));
return macro_def(e).expand(e, *this);
@ -776,9 +775,6 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
case expr_kind::Constant: case expr_kind::Lit:
/* Remark: we do not unfold Constants eagerly in this method */
return e;
case expr_kind::MData:
e = mdata_expr(e);
continue;
case expr_kind::FVar:
if (use_zeta() && is_local_decl_ref(e)) {
if (auto d = m_lctx.find_local_decl(e)) {
@ -864,7 +860,9 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
continue;
}
}
case expr_kind::MData:
e = mdata_expr(e);
continue;
case expr_kind::Macro:
if (auto m = expand_macro(e)) {
check_system("whnf");
@ -2304,10 +2302,6 @@ struct check_assignment_fn : public replace_visitor {
}
}
expr visit_macro(expr const & e) override {
return replace_visitor::visit_macro(e);
}
expr operator()(expr const & v) {
if (!has_expr_metavar(v) && !has_local(v)) {
return v;
@ -3343,6 +3337,9 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
return l_false;
case expr_kind::Let:
return l_undef;
case expr_kind::MData:
it = &mdata_expr(*it);
break;
case expr_kind::Constant:
if (auto r = constant_is_class(*it)) {
result = *r;
@ -3372,9 +3369,6 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
case expr_kind::Pi:
it = &binding_body(*it);
break;
case expr_kind::MData:
it = &mdata_expr(*it);
break;
case expr_kind::Macro:
return l_undef;
case expr_kind::Quote: