From d87dfbfb036d4efe3a6c510a37ff18627a8988de Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Jun 2018 13:37:18 -0700 Subject: [PATCH] chore(library/equations_compiler): remove `equations` macro --- library/init/lean/macro.lean | 17 -- src/frontends/lean/elaborator.cpp | 16 +- src/frontends/lean/pp.cpp | 19 +-- src/library/equations_compiler/equations.cpp | 158 +++++++++++-------- src/library/equations_compiler/equations.h | 2 +- 5 files changed, 109 insertions(+), 103 deletions(-) diff --git a/library/init/lean/macro.lean b/library/init/lean/macro.lean index b5d4be5a08..b1173b4232 100644 --- a/library/init/lean/macro.lean +++ b/library/init/lean/macro.lean @@ -8,26 +8,9 @@ we can bootstrap Lean4. -/ namespace lean -structure equations_header := -(num_fns : nat) -(fn_names : list name) -(fn_actual_names : list name) -(is_private : bool) -(is_lemma : bool) -(is_meta : bool) -(is_noncomputable : bool) -(aux_lemmas : bool) -(prev_errors : bool) -(gen_code : bool) - /- Cases missing: 1- projection -- It will be a primitive -/ -inductive macro_definition -/- The following macros will be Syntax object in Lean4 -/ -| equations : equations_header → macro_definition - - end lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index ad2239cba1..23198798ce 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -3404,6 +3404,9 @@ expr elaborator::visit_mdata(expr const & e, optional const & expected_typ return new_rhs; } else if (is_equation(e)) { throw elaborator_exception(e, "unexpected occurrence of equation"); + } else if (is_equations(e)) { + lean_assert(!is_app_fn); // visit_convoy is used in this case + return visit_equations(e); } else { expr new_e = visit(mdata_expr(e), expected_type); return update_mdata(e, new_e); @@ -3411,15 +3414,10 @@ expr elaborator::visit_mdata(expr const & e, optional const & expected_typ } expr elaborator::visit_macro(expr const & e, optional const & expected_type, bool is_app_fn) { - if (is_equations(e)) { - lean_assert(!is_app_fn); // visit_convoy is used in this case - return visit_equations(e); - } else { - buffer args; - for (unsigned i = 0; i < macro_num_args(e); i++) - args.push_back(visit(macro_arg(e, i), none_expr())); - return update_macro(e, args.size(), args.data()); - } + buffer args; + for (unsigned i = 0; i < macro_num_args(e); i++) + args.push_back(visit(macro_arg(e, i), none_expr())); + return update_macro(e, args.size(), args.data()); } /* If the instance fingerprint has been set, then make sure `type` is not a local instance. diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 065352aff7..a092de1e89 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1130,19 +1130,7 @@ auto pretty_fn::pp_macro_default(expr const & e) -> result { } auto pretty_fn::pp_macro(expr const & e) -> result { - if (is_marked_as_comp_irrelevant(e)) { - if (m_hide_comp_irrel) - return m_unicode ? format("◾") : format("irrel"); - else - return pp(get_annotation_arg(e)); - } 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); - } + return pp_macro_default(e); } auto pretty_fn::pp_mdata(expr const & e) -> result { @@ -1162,6 +1150,11 @@ auto pretty_fn::pp_mdata(expr const & e) -> result { 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); + } else if (is_equations(e)) { + if (auto r = pp_equations(e)) + return *r; + else + return pp_macro_default(e); } else { return pp(mdata_expr(e)); } diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp index 9d257dc789..2b792002d2 100644 --- a/src/library/equations_compiler/equations.cpp +++ b/src/library/equations_compiler/equations.cpp @@ -34,9 +34,6 @@ static name * g_no_equation_name = nullptr; static name * g_inaccessible_name = nullptr; static name * g_equations_result_name = nullptr; static name * g_as_pattern_name = nullptr; -static std::string * g_equations_opcode = nullptr; - -[[ noreturn ]] static void throw_asp_ex() { throw exception("unexpected occurrence of 'equations' expression"); } bool operator==(equations_header const & h1, equations_header const & h2) { return @@ -52,31 +49,6 @@ bool operator==(equations_header const & h1, equations_header const & h2) { h1.m_gen_code == h2.m_gen_code; } -[[ noreturn ]] static void throw_eqs_ex() { throw exception("unexpected occurrence of 'equations' expression"); } - -class equations_macro_cell : public macro_definition_cell { - equations_header m_header; -public: - equations_macro_cell(equations_header const & h):m_header(h) {} - virtual name get_name() const override { return *g_equations_name; } - virtual expr check_type(expr const &, abstract_type_context &, bool) const override { throw_eqs_ex(); } - virtual optional expand(expr const &, abstract_type_context &) const override { throw_eqs_ex(); } - virtual void write(serializer & s) const override { - s << *g_equations_opcode << m_header.m_num_fns << m_header.m_is_private << m_header.m_is_meta - << m_header.m_is_noncomputable << m_header.m_is_lemma << m_header.m_aux_lemmas << m_header.m_prev_errors << m_header.m_gen_code; - s << m_header.m_fn_names; - s << m_header.m_fn_actual_names; - } - virtual bool operator==(macro_definition_cell const & other) const override { - if (auto other_ptr = dynamic_cast(&other)) { - return m_header == other_ptr->m_header; - } else { - return false; - } - } - equations_header const & get_header() const { return m_header; } -}; - static kvmap * g_as_pattern = nullptr; static kvmap * g_equation = nullptr; static kvmap * g_equation_ignore_if_unused = nullptr; @@ -135,46 +107,125 @@ expr get_as_pattern_rhs(expr const & e) { return app_arg(mdata_expr(e)); } -bool is_equations(expr const & e) { return is_macro(e) && macro_def(e).get_name() == *g_equations_name; } +bool is_equations(expr const & e) { return is_mdata(e) && get_nat(mdata_data(e), *g_equations_name); } + +static void get_equations_args(expr const & e, buffer & r) { + lean_assert(is_equations(e)); + expr it = mdata_expr(e); + unsigned i = get_nat(mdata_data(e), *g_equations_name)->get_small_value(); + while (i > 1) { + --i; + lean_assert(is_app(it)); + r.push_back(app_fn(it)); + it = app_arg(it); + } + r.push_back(it); +} + bool is_wf_equations_core(expr const & e) { lean_assert(is_equations(e)); - return macro_num_args(e) >= 2 && !is_lambda_equation(macro_arg(e, macro_num_args(e) - 1)); + unsigned n = get_nat(mdata_data(e), *g_equations_name)->get_small_value(); + if (n >= 2) { + buffer args; + get_equations_args(e, args); + return !is_lambda_equation(args[n - 1]); + } else { + return false; + } } -bool is_wf_equations(expr const & e) { return is_equations(e) && is_wf_equations_core(e); } + +bool is_wf_equations(expr const & e) { + return is_equations(e) && is_wf_equations_core(e); +} + unsigned equations_size(expr const & e) { lean_assert(is_equations(e)); if (is_wf_equations_core(e)) - return macro_num_args(e) - 1; + return get_nat(mdata_data(e), *g_equations_name)->get_small_value() - 1; else - return macro_num_args(e); + return get_nat(mdata_data(e), *g_equations_name)->get_small_value(); } -equations_header const & get_equations_header(expr const & e) { + +equations_header get_equations_header(expr const & e) { lean_assert(is_equations(e)); - return static_cast(macro_def(e).raw())->get_header(); + equations_header h; + kvmap const & m = mdata_data(e); + h.m_num_fns = get_nat(m, name(*g_equations_name, "num_fns"))->get_small_value(); + h.m_is_private = *get_bool(m, name(*g_equations_name, "is_private")); + h.m_is_lemma = *get_bool(m, name(*g_equations_name, "is_lemma")); + h.m_is_meta = *get_bool(m, name(*g_equations_name, "is_meta")); + h.m_is_noncomputable = *get_bool(m, name(*g_equations_name, "is_noncomputable")); + h.m_aux_lemmas = *get_bool(m, name(*g_equations_name, "aux_lemmas")); + h.m_prev_errors = *get_bool(m, name(*g_equations_name, "prev_errors")); + h.m_gen_code = *get_bool(m, name(*g_equations_name, "gen_code")); + buffer ns; + buffer as; + for (unsigned i = 0; i < h.m_num_fns; i++) { + ns.push_back(*get_name(m, name(name(*g_equations_name, "name"), i))); + as.push_back(*get_name(m, name(name(*g_equations_name, "actual"), i))); + } + h.m_fn_names = names(ns); + h.m_fn_actual_names = names(as); + return h; } + unsigned equations_num_fns(expr const & e) { - return get_equations_header(e).m_num_fns; + lean_assert(is_equations(e)); + return get_nat(mdata_data(e), name(*g_equations_name, "num_fns"))->get_small_value(); } + expr const & equations_wf_tactics(expr const & e) { lean_assert(is_wf_equations(e)); - return macro_arg(e, macro_num_args(e) - 1); + buffer args; + get_equations_args(e, args); + return args.back(); } void to_equations(expr const & e, buffer & eqns) { lean_assert(is_equations(e)); - unsigned sz = equations_size(e); - for (unsigned i = 0; i < sz; i++) - eqns.push_back(macro_arg(e, i)); + unsigned n = get_nat(mdata_data(e), *g_equations_name)->get_small_value(); + get_equations_args(e, eqns); + if (n >= 2 && !is_lambda_equation(eqns.back())) + eqns.pop_back(); } + expr mk_equations(equations_header const & h, unsigned num_eqs, expr const * eqs) { + kvmap m; + m = set_nat(m, *g_equations_name, num_eqs); + m = set_nat(m, name(*g_equations_name, "num_fns"), h.m_num_fns); + m = set_bool(m, name(*g_equations_name, "is_private"), h.m_is_private); + m = set_bool(m, name(*g_equations_name, "is_lemma"), h.m_is_lemma); + m = set_bool(m, name(*g_equations_name, "is_meta"), h.m_is_meta); + m = set_bool(m, name(*g_equations_name, "is_noncomputable"), h.m_is_noncomputable); + m = set_bool(m, name(*g_equations_name, "aux_lemmas"), h.m_aux_lemmas); + m = set_bool(m, name(*g_equations_name, "prev_errors"), h.m_prev_errors); + m = set_bool(m, name(*g_equations_name, "gen_code"), h.m_gen_code); + lean_assert(length(h.m_fn_names) == h.m_num_fns); + lean_assert(length(h.m_fn_actual_names) == h.m_num_fns); + names it1 = h.m_fn_names; + names it2 = h.m_fn_actual_names; + for (unsigned i = 0; i < h.m_num_fns; i++) { + m = set_name(m, name(name(*g_equations_name, "name"), i), head(it1)); + m = set_name(m, name(name(*g_equations_name, "actual"), i), head(it2)); + it1 = tail(it1); + it2 = tail(it2); + } lean_assert(h.m_num_fns > 0); lean_assert(num_eqs > 0); lean_assert(std::all_of(eqs, eqs+num_eqs, [](expr const & e) { return is_lambda_equation(e) || is_lambda_no_equation(e); })); - macro_definition def(new equations_macro_cell(h)); - return mk_macro(def, num_eqs, eqs); + expr r = eqs[num_eqs - 1]; + unsigned i = num_eqs - 1; + while (i > 0) { + --i; + r = mk_app(eqs[i], r); + } + r = mk_mdata(m, r); + lean_assert(get_equations_header(r) == h); + return r; } + expr mk_equations(equations_header const & h, unsigned num_eqs, expr const * eqs, expr const & tacs) { lean_assert(h.m_num_fns > 0); lean_assert(num_eqs > 0); @@ -182,9 +233,9 @@ expr mk_equations(equations_header const & h, unsigned num_eqs, expr const * eqs buffer args; args.append(num_eqs, eqs); args.push_back(tacs); - macro_definition def(new equations_macro_cell(h)); - return mk_macro(def, args.size(), args.data()); + return mk_equations(h, args.size(), args.data()); } + expr update_equations(expr const & eqns, buffer const & new_eqs) { lean_assert(is_equations(eqns)); lean_assert(!new_eqs.empty()); @@ -265,29 +316,10 @@ void initialize_equations() { g_equation_ignore_if_unused = new kvmap(set_bool(kvmap(), *g_equation_name, true)); g_no_equation = new kvmap(set_bool(kvmap(), *g_no_equation_name, false)); g_as_pattern = new kvmap(set_bool(kvmap(), *g_as_pattern_name, true)); - g_equations_opcode = new std::string("Eqns"); register_annotation(*g_inaccessible_name); - register_macro_deserializer(*g_equations_opcode, - [](deserializer & d, unsigned num, expr const * args) { - equations_header h; - d >> h.m_num_fns >> h.m_is_private >> h.m_is_meta >> h.m_is_noncomputable - >> h.m_is_lemma >> h.m_aux_lemmas >> h.m_prev_errors >> h.m_gen_code; - h.m_fn_names = read_names(d); - h.m_fn_actual_names = read_names(d); - if (num == 0 || h.m_num_fns == 0) - throw corrupted_stream_exception(); - if (!is_lambda_equation(args[num-1]) && !is_lambda_no_equation(args[num-1])) { - if (num <= 1) - throw corrupted_stream_exception(); - return mk_equations(h, num-1, args, args[num-1]); - } else { - return mk_equations(h, num, args); - } - }); } void finalize_equations() { - delete g_equations_opcode; delete g_as_pattern; delete g_equation; delete g_equation_ignore_if_unused; diff --git a/src/library/equations_compiler/equations.h b/src/library/equations_compiler/equations.h index 0a883f661e..b8fb2b1992 100644 --- a/src/library/equations_compiler/equations.h +++ b/src/library/equations_compiler/equations.h @@ -66,7 +66,7 @@ expr remove_wf_annotation_from_equations(expr const & eqns); bool is_equations(expr const & e); bool is_wf_equations(expr const & e); unsigned equations_size(expr const & e); -equations_header const & get_equations_header(expr const & e); +equations_header get_equations_header(expr const & e); unsigned equations_num_fns(expr const & e); void to_equations(expr const & e, buffer & eqns); expr const & equations_wf_tactics(expr const & e);