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

fix(library/quote): use opaque macro for elaborated expr quotations

Browse source
This commit is contained in:
Sebastian Ullrich 2017-06-07 13:54:49 +02:00 • committed by Leonardo de Moura
parent 82db0f874a
commit 283d8ade1a
12 changed files with 64 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

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

@ -2913,7 +2913,7 @@ expr elaborator::visit_expr_quote(expr const & e, optional<expr> 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) {

2
src/library/compiler/comp_irrelevant.cpp
View file

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

2
src/library/compiler/compiler_step_visitor.cpp
View file

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

2
src/library/compiler/erase_irrelevant.cpp
View file

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

106
src/library/quote.cpp
View file

@ -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<expr> expand(expr const &, abstract_type_context &) const {
return optional<expr>();
}
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<pexpr_quote_macro const &>(d).m_value;
return m_value < static_cast<expr_quote_macro const &>(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<expr> expand(expr const &, abstract_type_context &) const {
return optional<expr>();
@ -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<expr_quote_macro const *>(macro_def(e).raw()) != nullptr;
if (is_annotation(e, *g_expr_quote_pre)) {
return true;
}
if (is_macro(e)) {
if (auto m = dynamic_cast<expr_quote_macro const *>(macro_def(e).raw())) {
return m->is_reflected();
}
}
return false;
}
bool is_pexpr_quote(expr const & e) {
return is_macro(e) && dynamic_cast<pexpr_quote_macro const *>(macro_def(e).raw()) != nullptr;
if (is_macro(e)) {
if (auto m = dynamic_cast<expr_quote_macro const *>(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<expr_quote_macro const *>(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<pexpr_quote_macro const *>(macro_def(e).raw())->get_value();
return static_cast<expr_quote_macro const *>(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;

3
src/library/quote.h
View file

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

2
src/library/type_context.cpp
View file

@ -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<expr> new_inst_mvars;
for (expr const & local : r_locals.get_collected()) {
expr ty = m_ctx.infer(local);

2
src/library/vm/vm_expr.cpp
View file

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

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

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

1
tests/lean/reflect.lean Normal file
View file

@ -0,0 +1 @@
#eval (reflect 0).to_expr

1
tests/lean/reflect.lean.expected.out Normal file
View file

@ -0,0 +1 @@
has_zero.zero.{0} nat nat.has_zero