From 283d8ade1ad826fce3c9707bc0d99da37ec2c177 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 7 Jun 2017 13:54:49 +0200 Subject: [PATCH] fix(library/quote): use opaque macro for elaborated expr quotations --- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/elaborator.cpp | 2 +- src/library/compiler/comp_irrelevant.cpp | 2 +- .../compiler/compiler_step_visitor.cpp | 2 - src/library/compiler/erase_irrelevant.cpp | 2 - src/library/quote.cpp | 106 +++++++++--------- src/library/quote.h | 3 +- src/library/type_context.cpp | 2 +- src/library/vm/vm_expr.cpp | 2 +- tests/lean/expr_quote.lean.expected.out | 2 +- tests/lean/reflect.lean | 1 + tests/lean/reflect.lean.expected.out | 1 + 12 files changed, 64 insertions(+), 63 deletions(-) create mode 100644 tests/lean/reflect.lean create mode 100644 tests/lean/reflect.lean.expected.out diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index cce9be77b2..8b7c32edff 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -684,7 +684,7 @@ static expr parse_quoted_expr(parser_state & p, unsigned, expr const *, pos_info } p.check_token_next(get_rparen_tk(), "invalid quoted expression, `)` expected"); } - return p.save_pos(mk_expr_quote(e), pos); + return p.save_pos(mk_unelaborated_expr_quote(e), pos); } static expr parse_antiquote_expr(parser_state & p, unsigned, expr const *, pos_info const & pos) { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b3ed79bffd..495398997b 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2913,7 +2913,7 @@ expr elaborator::visit_expr_quote(expr const & e, optional const & expecte throw elaborator_exception(e, "invalid quotation, contains universe metavariable"); if (has_local(new_s)) throw elaborator_exception(e, "invalid quotation, contains local constant"); - q = mk_expr_quote(new_s); + q = mk_elaborated_expr_quote(new_s); q = mk_as_is(q); expr subst_fn = mk_app(mk_explicit(mk_constant(get_expr_subst_name())), mk_bool_tt()); for (expr const & subst : substs) { diff --git a/src/library/compiler/comp_irrelevant.cpp b/src/library/compiler/comp_irrelevant.cpp index 2dcc2d43c1..c1e0f36ba1 100644 --- a/src/library/compiler/comp_irrelevant.cpp +++ b/src/library/compiler/comp_irrelevant.cpp @@ -62,7 +62,7 @@ protected: } virtual expr visit_macro(expr const & e) override { - if (is_marked_as_comp_irrelevant(e) || is_expr_quote(e)) + if (is_marked_as_comp_irrelevant(e)) return e; else if (auto v = mark_if_irrel_core(e)) return *v; diff --git a/src/library/compiler/compiler_step_visitor.cpp b/src/library/compiler/compiler_step_visitor.cpp index 4635e28395..6cfe5a2a1b 100644 --- a/src/library/compiler/compiler_step_visitor.cpp +++ b/src/library/compiler/compiler_step_visitor.cpp @@ -53,8 +53,6 @@ expr compiler_step_visitor::visit_let(expr const & e) { expr compiler_step_visitor::visit_macro(expr const & e) { if (is_marked_as_comp_irrelevant(e)) return e; - else if (is_expr_quote(e)) - return e; else return replace_visitor::visit_macro(e); } diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index 48fd82cc71..c5ca6c9c31 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -69,8 +69,6 @@ class erase_irrelevant_fn : public compiler_step_visitor { return mk_constant(get_rec_fn_name(e)); } else if (is_nat_value(e)) { return e; - } else if (is_expr_quote(e)) { - return e; } else if (auto r = macro_def(e).expand(e, m_ctx)) { return visit(*r); } else { diff --git a/src/library/quote.cpp b/src/library/quote.cpp index 102f0d28c3..3ecc8ee0f4 100644 --- a/src/library/quote.cpp +++ b/src/library/quote.cpp @@ -19,43 +19,29 @@ Author: Leonardo de Moura namespace lean { static std::string * g_expr_quote_opcode = nullptr; -static std::string * g_pexpr_quote_opcode = nullptr; static expr * g_expr = nullptr; static expr * g_pexpr = nullptr; +static name * g_expr_quote_pre = nullptr; static name * g_expr_quote_macro = nullptr; -static name * g_pexpr_quote_macro = nullptr; -/** \brief The quoted expression macro is a compact way of encoding quoted expressions inside Lean expressions. - It is used to represent values of types `reflected e` or `expr`. */ +/** \brief A compact way of encoding quoted expressions inside Lean expressions. Used for values of type + `reflected e` and `pexpr`. */ class expr_quote_macro : public macro_definition_cell { -public: - virtual name get_name() const { return *g_expr_quote_macro; } - virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const { - expr const & e = get_expr_quote_value(m); - expr ty = ctx.check(e, infer_only); - return mk_app(mk_constant(get_reflected_name(), {get_level(ctx, ty)}), ty, e); - } - virtual optional expand(expr const &, abstract_type_context &) const { - return optional(); - } - virtual unsigned trust_level() const { return 0; } - virtual void display(std::ostream & out) const { - out << "quote"; - } - virtual void write(serializer & s) const { s << *g_expr_quote_opcode; } -}; - -/** \brief A compact way of encoding quoted pre-expressions inside Lean expressions. */ -class pexpr_quote_macro : public macro_definition_cell { expr m_value; + bool m_reflected; public: - pexpr_quote_macro(expr const & v):m_value(v) {} + expr_quote_macro(expr const & v, bool reflected):m_value(v), m_reflected(reflected) {} virtual bool lt(macro_definition_cell const & d) const { - return m_value < static_cast(d).m_value; + return m_value < static_cast(d).m_value; } - virtual name get_name() const { return *g_pexpr_quote_macro; } - virtual expr check_type(expr const &, abstract_type_context &, bool) const { - return *g_pexpr; + virtual name get_name() const { return *g_expr_quote_macro; } + virtual expr check_type(expr const &, abstract_type_context & ctx, bool infer_only) const { + if (m_reflected) { + expr ty = ctx.check(m_value, infer_only); + return mk_app(mk_constant(get_reflected_name(), {get_level(ctx, ty)}), ty, m_value); + } else { + return *g_pexpr; + } } virtual optional expand(expr const &, abstract_type_context &) const { return optional(); @@ -68,38 +54,61 @@ public: return this == &other; } char const * prefix() const { - return "``("; + return m_reflected ? "`(" : "``("; } virtual void display(std::ostream & out) const { - out << "``(" << m_value << ")"; + out << prefix() << m_value << ")"; } virtual unsigned hash() const { return m_value.hash(); } - virtual void write(serializer & s) const { s << *g_pexpr_quote_opcode << m_value; } + virtual void write(serializer & s) const { s << *g_expr_quote_opcode << m_value << m_reflected; } expr const & get_value() const { return m_value; } + bool const & is_reflected() const { return m_reflected; } }; -expr mk_expr_quote(expr const & e) { - return mk_macro(macro_definition(new expr_quote_macro()), 1, &e); +expr mk_elaborated_expr_quote(expr const & e) { + return mk_macro(macro_definition(new expr_quote_macro(e, /* reflected */ true))); +} +expr mk_unelaborated_expr_quote(expr const & e) { + // We use a transparent annotation instead of the opaque macro above so that the quoted term is accessible to + // collect_locals etc. + return mk_annotation(*g_expr_quote_pre, e); } expr mk_pexpr_quote(expr const & e) { - return mk_macro(macro_definition(new pexpr_quote_macro(e))); + return mk_macro(macro_definition(new expr_quote_macro(e, /* reflected */ false))); } bool is_expr_quote(expr const & e) { - return is_macro(e) && dynamic_cast(macro_def(e).raw()) != nullptr; + if (is_annotation(e, *g_expr_quote_pre)) { + return true; + } + if (is_macro(e)) { + if (auto m = dynamic_cast(macro_def(e).raw())) { + return m->is_reflected(); + } + } + return false; } bool is_pexpr_quote(expr const & e) { - return is_macro(e) && dynamic_cast(macro_def(e).raw()) != nullptr; + if (is_macro(e)) { + if (auto m = dynamic_cast(macro_def(e).raw())) { + return !m->is_reflected(); + } + } + return false; } expr const & get_expr_quote_value(expr const & e) { lean_assert(is_expr_quote(e)); - return macro_arg(e, 0); + if (auto m = dynamic_cast(macro_def(e).raw())) { + return m->get_value(); + } else { + return get_annotation_arg(e); + } } expr const & get_pexpr_quote_value(expr const & e) { lean_assert(is_pexpr_quote(e)); - return static_cast(macro_def(e).raw())->get_value(); + return static_cast(macro_def(e).raw())->get_value(); } static name * g_antiquote = nullptr; @@ -139,36 +148,29 @@ expr mk_pexpr_quote_and_substs(expr const & e, bool is_strict) { void initialize_quote() { g_expr_quote_macro = new name("expr_quote_macro"); - g_pexpr_quote_macro = new name("pexpr_quote_macro"); g_expr_quote_opcode = new std::string("Quote"); - g_pexpr_quote_opcode = new std::string("PQuote"); g_expr = new expr(mk_app(Const(get_expr_name()), mk_bool_tt())); g_pexpr = new expr(mk_app(Const(get_expr_name()), mk_bool_ff())); - g_antiquote = new name("antiquote"); + g_antiquote = new name("antiquote"); + g_expr_quote_pre = new name("expr_quote_pre"); register_annotation(*g_antiquote); + register_annotation(*g_expr_quote_pre); register_macro_deserializer(*g_expr_quote_opcode, - [](deserializer &, unsigned num, expr const * args) { - if (num != 1) - throw corrupted_stream_exception(); - return mk_expr_quote(args[0]); - }); - register_macro_deserializer(*g_pexpr_quote_opcode, [](deserializer & d, unsigned num, expr const *) { if (num != 0) throw corrupted_stream_exception(); - expr e; - d >> e; - return mk_pexpr_quote(e); + expr e; bool reflected; + d >> e >> reflected; + return mk_macro(macro_definition(new expr_quote_macro(e, reflected))); }); } void finalize_quote() { + delete g_expr_quote_pre; delete g_expr_quote_macro; - delete g_pexpr_quote_macro; delete g_expr_quote_opcode; - delete g_pexpr_quote_opcode; delete g_expr; delete g_pexpr; delete g_antiquote; diff --git a/src/library/quote.h b/src/library/quote.h index 1c49b4b0a1..7634cf7571 100644 --- a/src/library/quote.h +++ b/src/library/quote.h @@ -12,7 +12,8 @@ bool is_expr_quote(expr const &e); bool is_pexpr_quote(expr const &e); expr const & get_expr_quote_value(expr const & e); expr const & get_pexpr_quote_value(expr const & e); -expr mk_expr_quote(expr const & e); +expr mk_unelaborated_expr_quote(expr const & e); +expr mk_elaborated_expr_quote(expr const & e); expr mk_pexpr_quote(expr const & e); expr mk_antiquote(expr const & e); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index fb24163f8a..d02492ada7 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -3583,7 +3583,7 @@ struct instance_synthesizer { collect_locals(r, r_locals); r = m_ctx.mk_lambda(r_locals.get_collected(), r); expr r_ty = m_ctx.infer(r); - expr q = mk_expr_quote(r); + expr q = mk_elaborated_expr_quote(r); buffer new_inst_mvars; for (expr const & local : r_locals.get_collected()) { expr ty = m_ctx.infer(local); diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 2e79c9c0a8..f3248e1a6d 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -450,7 +450,7 @@ vm_obj expr_is_annotation(vm_obj const &, vm_obj const & _e) { vm_obj reflect_expr(vm_obj const & elab, vm_obj const & e) { if (to_bool(elab)) - return to_obj(mk_expr_quote(to_expr(e))); + return to_obj(mk_elaborated_expr_quote(to_expr(e))); else return to_obj(mk_pexpr_quote_and_substs(to_expr(e), /* is_strict */ false)); } diff --git a/tests/lean/expr_quote.lean.expected.out b/tests/lean/expr_quote.lean.expected.out index bdb11cba40..c5ecb9ea14 100644 --- a/tests/lean/expr_quote.lean.expected.out +++ b/tests/lean/expr_quote.lean.expected.out @@ -1,4 +1,4 @@ -expr_quote.lean:1:27: error: invalid quotation, contains universe metavariable +expr_quote.lean:1:30: error: invalid quotation, contains universe metavariable expr_quote.lean:1:9: error: don't know how to synthesize placeholder context: α a : expr diff --git a/tests/lean/reflect.lean b/tests/lean/reflect.lean new file mode 100644 index 0000000000..30255a06c7 --- /dev/null +++ b/tests/lean/reflect.lean @@ -0,0 +1 @@ +#eval (reflect 0).to_expr diff --git a/tests/lean/reflect.lean.expected.out b/tests/lean/reflect.lean.expected.out new file mode 100644 index 0000000000..b8dd2eaba9 --- /dev/null +++ b/tests/lean/reflect.lean.expected.out @@ -0,0 +1 @@ +has_zero.zero.{0} nat nat.has_zero