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

feat(kernel): add expr_kind::Quote

Browse source 
This is a temporary expr constructor. We need it to be able to eliminate
expr_macro, and then define expr using runtime/object
This commit is contained in:
Leonardo de Moura 2018-06-12 17:40:00 -07:00
parent e590ebf54d
commit 335c58f8a7
37 changed files with 508 additions and 350 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -970,6 +970,8 @@ expr elaborator::visit_function(expr const & fn, bool has_args, optional<expr> c
case expr_kind::Macro: r = visit_macro(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:
throw elaborator_exception(ref, "invalid application, function expected");
}
save_identifier_info(r);
if (has_args)
@ -3654,6 +3656,8 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
return copy_pos(e, visit_app(e, expected_type));
case expr_kind::Let:
return copy_pos(e, visit_let(e, expected_type));
case expr_kind::Quote:
return copy_pos(e, visit_expr_quote(e, expected_type));
}
lean_unreachable(); // LCOV_EXCL_LINE
}

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

@ -309,6 +309,12 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
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);
} else {
return save_pos(e, p);
}
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -1719,43 +1725,45 @@ struct to_pattern_fn {
static expr quote(expr const & e) {
switch (e.kind()) {
case expr_kind::BVar:
return mk_app(mk_constant({"expr", "bvar"}), quote(var_idx(e)));
case expr_kind::Sort:
return mk_app(mk_constant({"expr", "sort"}), mk_expr_placeholder());
case expr_kind::Constant:
return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
case expr_kind::Meta:
case expr_kind::BVar:
return mk_app(mk_constant({"expr", "bvar"}), quote(var_idx(e)));
case expr_kind::Sort:
return mk_app(mk_constant({"expr", "sort"}), mk_expr_placeholder());
case expr_kind::Constant:
return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
case expr_kind::Meta:
return mk_expr_placeholder();
case expr_kind::FVar:
throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
<< mlocal_pp_name(e) << "'");
case expr_kind::App:
if (is_metavar_app(e)) {
/* Remark: metavariable applications of the form `?m x1 ... xn` may be introduced
by type_context::elim_mvar_deps when we create lambda/pi-expressions. */
return mk_expr_placeholder();
case expr_kind::FVar:
throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
<< mlocal_pp_name(e) << "'");
case expr_kind::App:
if (is_metavar_app(e)) {
/* Remark: metavariable applications of the form `?m x1 ... xn` may be introduced
by type_context::elim_mvar_deps when we create lambda/pi-expressions. */
return mk_expr_placeholder();
} else {
return mk_app(mk_constant({"expr", "app"}), quote(app_fn(e)), quote(app_arg(e)));
}
case expr_kind::Lambda:
return mk_app(mk_constant({"expr", "lam"}), mk_expr_placeholder(), mk_expr_placeholder(),
quote(binding_domain(e)), quote(binding_body(e)));
case expr_kind::Pi:
return mk_app(mk_constant({"expr", "pi"}), mk_expr_placeholder(), mk_expr_placeholder(),
quote(binding_domain(e)), quote(binding_body(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:
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))
return mk_expr_placeholder();
throw elaborator_exception(e, sstream() << "invalid quotation, unsupported macro '"
<< macro_def(e).get_name() << "'");
} else {
return mk_app(mk_constant({"expr", "app"}), quote(app_fn(e)), quote(app_arg(e)));
}
case expr_kind::Lambda:
return mk_app(mk_constant({"expr", "lam"}), mk_expr_placeholder(), mk_expr_placeholder(),
quote(binding_domain(e)), quote(binding_body(e)));
case expr_kind::Pi:
return mk_app(mk_constant({"expr", "pi"}), mk_expr_placeholder(), mk_expr_placeholder(),
quote(binding_domain(e)), quote(binding_body(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:
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))
return mk_expr_placeholder();
throw elaborator_exception(e, sstream() << "invalid quotation, unsupported macro '"
<< macro_def(e).get_name() << "'");
case expr_kind::Quote:
throw elaborator_exception(e, sstream() << "invalid quotation, quote found");
}
lean_unreachable();
}

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

@ -1781,6 +1781,11 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
case expr_kind::Pi: return pp_pi(e);
case expr_kind::Macro: return pp_macro(e);
case expr_kind::Let: return pp_let(e);
case expr_kind::Quote:
if (quote_is_reflected(e))
return result(format("`(") + nest(4, pp(quote_value(e)).fmt()) + format(")"));
else
return result(format("``(") + nest(2, pp(quote_value(e)).fmt()) + format(")"));
}
lean_unreachable(); // LCOV_EXCL_LINE
}

5
src/kernel/equiv_manager.cpp
View file

@ -107,6 +107,11 @@ bool equiv_manager::is_equiv_core(expr const & a, expr const & b) {
}
result = true;
break;
case expr_kind::Quote:
if (quote_is_reflected(a) != quote_is_reflected(b) || quote_value(a) != quote_value(b))
return false;
result = true;
break;
}
if (result)
merge(r1, r2);

203
src/kernel/expr.cpp
View file

@ -285,27 +285,6 @@ void expr_let::dealloc(buffer<expr_cell*> & todelete) {
delete this;
}
// Macro definition
bool macro_definition_cell::lt(macro_definition_cell const &) const { return false; }
bool macro_definition_cell::operator==(macro_definition_cell const & other) const { return typeid(*this) == typeid(other); }
unsigned macro_definition_cell::trust_level() const { return 0; }
void macro_definition_cell::display(std::ostream & out) const { out << get_name(); }
unsigned macro_definition_cell::hash() const { return get_name().hash(); }
macro_definition::macro_definition(macro_definition_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
macro_definition::macro_definition(macro_definition const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
macro_definition::macro_definition(macro_definition && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
macro_definition::~macro_definition() { if (m_ptr) m_ptr->dec_ref(); }
macro_definition & macro_definition::operator=(macro_definition const & s) { LEAN_COPY_REF(s); }
macro_definition & macro_definition::operator=(macro_definition && s) { LEAN_MOVE_REF(s); }
bool macro_definition::operator<(macro_definition const & other) const {
if (get_name() == other.get_name())
return m_ptr->lt(*other.m_ptr);
else
return get_name() < other.get_name();
}
static unsigned add_weight(unsigned num, expr const * args) {
unsigned r = 0;
for (unsigned i = 0; i < num; i++)
@ -323,44 +302,6 @@ static unsigned get_loose_bvar_range(unsigned num, expr const * args) {
return r;
}
expr_macro::expr_macro(expr_macro const & src, expr const * new_args):
expr_composite(src),
m_definition(src.m_definition),
m_num_args(src.m_num_args) {
expr * data = get_args_ptr();
std::uninitialized_copy(new_args, new_args + m_num_args, data);
}
expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * args):
expr_composite(expr_kind::Macro,
lean::hash(num, [&](unsigned i) { return args[i].hash(); }, m.hash()),
std::any_of(args, args+num, [](expr const & e) { return e.has_expr_metavar(); }),
std::any_of(args, args+num, [](expr const & e) { return e.has_univ_metavar(); }),
std::any_of(args, args+num, [](expr const & e) { return e.has_fvar(); }),
std::any_of(args, args+num, [](expr const & e) { return e.has_param_univ(); }),
inc_weight(add_weight(num, args)),
get_loose_bvar_range(num, args)),
m_definition(m),
m_num_args(num) {
expr * data = get_args_ptr();
m_depth = 0;
for (unsigned i = 0; i < num; i++) {
unsigned d = get_depth(args[i]);
if (d > m_depth)
m_depth = d;
}
m_depth++;
std::uninitialized_copy(args, args + num, data);
}
void expr_macro::dealloc(buffer<expr_cell*> & todelete) {
expr * args = get_args_ptr();
for (unsigned i = 0; i < m_num_args; i++) dec_ref(args[i], todelete);
this->~expr_macro();
char * mem = reinterpret_cast<char*>(this);
delete[] mem;
}
expr_macro::~expr_macro() {}
// =======================================
// Constructors
@ -373,10 +314,6 @@ expr mk_fvar(name const & n) {
expr mk_constant(name const & n, levels const & ls) {
return expr(new expr_const(n, ls));
}
expr mk_macro(macro_definition const & m, unsigned num, expr const * args) {
char * mem = new char[sizeof(expr_macro) + num*sizeof(expr const *)];
return expr(new (mem) expr_macro(m, num, args));
}
expr mk_metavar(name const & n, name const & pp_n, expr const & t) {
return expr(new expr_mlocal(true, n, pp_n, t));
}
@ -415,7 +352,6 @@ void expr_cell::dealloc() {
lean_assert(it->get_rc() == 0);
switch (it->kind()) {
case expr_kind::BVar: static_cast<expr_bvar*>(it)->dealloc(); break;
case expr_kind::Macro: static_cast<expr_macro*>(it)->dealloc(todo); break;
case expr_kind::Meta: static_cast<expr_mlocal*>(it)->dealloc(todo); break;
case expr_kind::FVar: static_cast<expr_fvar*>(it)->dealloc(todo); break;
case expr_kind::Constant: static_cast<expr_const*>(it)->dealloc(); break;
@ -424,6 +360,9 @@ void expr_cell::dealloc() {
case expr_kind::Lambda:
case expr_kind::Pi: static_cast<expr_binding*>(it)->dealloc(todo); break;
case expr_kind::Let: static_cast<expr_let*>(it)->dealloc(todo); break;
case expr_kind::Macro: static_cast<expr_macro*>(it)->dealloc(todo); break;
case expr_kind::Quote: static_cast<expr_quote*>(it)->dealloc(todo); break;
}
}
} catch (std::bad_alloc&) {
@ -539,9 +478,15 @@ unsigned get_weight(expr const & e) {
case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort:
case expr_kind::Meta: case expr_kind::FVar:
return 1;
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Macro:
case expr_kind::Lambda: case expr_kind::Pi:
case expr_kind::App: case expr_kind::Let:
return static_cast<expr_composite*>(e.raw())->m_weight;
case expr_kind::Macro:
return static_cast<expr_composite*>(e.raw())->m_weight;
case expr_kind::Quote:
return 1;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -551,9 +496,15 @@ unsigned get_depth(expr const & e) {
case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort:
case expr_kind::Meta: case expr_kind::FVar:
return 1;
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Macro:
case expr_kind::Lambda: case expr_kind::Pi:
case expr_kind::App: case expr_kind::Let:
return static_cast<expr_composite*>(e.raw())->m_depth;
case expr_kind::Macro:
return static_cast<expr_composite*>(e.raw())->m_depth;
case expr_kind::Quote:
return 1;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -613,19 +564,6 @@ expr update_constant(expr const & e, levels const & new_levels) {
return e;
}
expr update_macro(expr const & e, unsigned num, expr const * args) {
if (num == macro_num_args(e)) {
unsigned i = 0;
for (i = 0; i < num; i++) {
if (!is_eqp(macro_arg(e, i), args[i]))
break;
}
if (i == num)
return e;
}
return mk_macro(to_macro(e)->m_definition, num, args);
}
expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body) {
if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_value) || !is_eqp(let_body(e), new_body))
return mk_let(let_name(e), new_type, new_value, new_body);
@ -638,12 +576,16 @@ bool is_atomic(expr const & e) {
case expr_kind::Constant: case expr_kind::Sort:
case expr_kind::BVar:
return true;
case expr_kind::Macro:
return to_macro(e)->get_num_args() == 0;
case expr_kind::App: case expr_kind::Meta:
case expr_kind::FVar: case expr_kind::Lambda:
case expr_kind::Pi: case expr_kind::Let:
return false;
case expr_kind::Macro:
return to_macro(e)->get_num_args() == 0;
case expr_kind::Quote:
return true;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -798,8 +740,11 @@ std::ostream & operator<<(std::ostream & out, expr_kind const & k) {
case expr_kind::App: out << "App"; break;
case expr_kind::Lambda: out << "Lambda"; break;
case expr_kind::Pi: out << "Pi"; break;
case expr_kind::Macro: out << "Macro"; break;
case expr_kind::Let: out << "Let"; break;
case expr_kind::Macro: out << "Macro"; break;
case expr_kind::Quote: out << "Quote"; break;
}
return out;
}
@ -817,4 +762,98 @@ void finalize_expr() {
delete g_dummy;
delete g_default_name;
}
/* ================ LEGACY CODE ================ */
// Macro definition
bool macro_definition_cell::lt(macro_definition_cell const &) const { return false; }
bool macro_definition_cell::operator==(macro_definition_cell const & other) const { return typeid(*this) == typeid(other); }
unsigned macro_definition_cell::trust_level() const { return 0; }
void macro_definition_cell::display(std::ostream & out) const { out << get_name(); }
unsigned macro_definition_cell::hash() const { return get_name().hash(); }
macro_definition::macro_definition(macro_definition_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
macro_definition::macro_definition(macro_definition const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
macro_definition::macro_definition(macro_definition && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
macro_definition::~macro_definition() { if (m_ptr) m_ptr->dec_ref(); }
macro_definition & macro_definition::operator=(macro_definition const & s) { LEAN_COPY_REF(s); }
macro_definition & macro_definition::operator=(macro_definition && s) { LEAN_MOVE_REF(s); }
bool macro_definition::operator<(macro_definition const & other) const {
if (get_name() == other.get_name())
return m_ptr->lt(*other.m_ptr);
else
return get_name() < other.get_name();
}
expr_macro::expr_macro(expr_macro const & src, expr const * new_args):
expr_composite(src),
m_definition(src.m_definition),
m_num_args(src.m_num_args) {
expr * data = get_args_ptr();
std::uninitialized_copy(new_args, new_args + m_num_args, data);
}
expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * args):
expr_composite(expr_kind::Macro,
lean::hash(num, [&](unsigned i) { return args[i].hash(); }, m.hash()),
std::any_of(args, args+num, [](expr const & e) { return e.has_expr_metavar(); }),
std::any_of(args, args+num, [](expr const & e) { return e.has_univ_metavar(); }),
std::any_of(args, args+num, [](expr const & e) { return e.has_fvar(); }),
std::any_of(args, args+num, [](expr const & e) { return e.has_param_univ(); }),
inc_weight(add_weight(num, args)),
get_loose_bvar_range(num, args)),
m_definition(m),
m_num_args(num) {
expr * data = get_args_ptr();
m_depth = 0;
for (unsigned i = 0; i < num; i++) {
unsigned d = get_depth(args[i]);
if (d > m_depth)
m_depth = d;
}
m_depth++;
std::uninitialized_copy(args, args + num, data);
}
void expr_macro::dealloc(buffer<expr_cell*> & todelete) {
expr * args = get_args_ptr();
for (unsigned i = 0; i < m_num_args; i++) dec_ref(args[i], todelete);
this->~expr_macro();
char * mem = reinterpret_cast<char*>(this);
delete[] mem;
}
expr_macro::~expr_macro() {}
expr mk_macro(macro_definition const & m, unsigned num, expr const * args) {
char * mem = new char[sizeof(expr_macro) + num*sizeof(expr const *)];
return expr(new (mem) expr_macro(m, num, args));
}
expr update_macro(expr const & e, unsigned num, expr const * args) {
if (num == macro_num_args(e)) {
unsigned i = 0;
for (i = 0; i < num; i++) {
if (!is_eqp(macro_arg(e, i), args[i]))
break;
}
if (i == num)
return e;
}
return mk_macro(to_macro(e)->m_definition, num, args);
}
expr_quote::expr_quote(bool r, expr const & v):
expr_cell(expr_kind::Quote, v.hash(), false, false, false, false),
m_reflected(r),
m_value(v) {
}
void expr_quote::dealloc(buffer<expr_cell*> & todelete) {
dec_ref(m_value, todelete);
delete this;
}
expr mk_quote(bool reflected, expr const & val) {
return expr(new expr_quote(reflected, val));
}
}

205
src/kernel/expr.h
View file

@ -38,9 +38,13 @@ class expr;
| Lambda name expr expr
| Pi name expr expr
| Let name expr expr expr
The following constructors will be deleted in the future
| Quote bool expr
| Macro macro
*/
enum class expr_kind { BVar, FVar, Sort, Constant, Meta, App, Lambda, Pi, Let, Macro };
enum class expr_kind { BVar, FVar, Sort, Constant, Meta, App, Lambda, Pi, Let, Macro, Quote };
class expr_cell {
protected:
// The bits of the following field mean:
@ -128,8 +132,10 @@ public:
friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b);
friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
// TODO(Leo): delete
friend expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi);
friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args);
friend expr mk_quote(bool reflected, expr const & val);
};
SPECIALIZE_OPTIONAL_FOR_SMART_PTR(expr)
@ -329,98 +335,13 @@ public:
level const & get_level() const { return m_level; }
};
/** \brief Abstract class for macro_definitions */
class macro_definition_cell {
protected:
void dealloc() { delete this; }
MK_LEAN_RC();
/**
\brief Auxiliary method used for implementing a total order on macro
attachments. It is invoked by operator<, and it is only invoked when
<tt>get_name() == other.get_name()</tt>
*/
virtual bool lt(macro_definition_cell const &) const;
public:
macro_definition_cell():m_rc(0) {}
virtual ~macro_definition_cell() {}
virtual name get_name() const = 0;
virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const = 0;
virtual optional<expr> expand(expr const & m, abstract_type_context & ctx) const = 0;
virtual optional<expr> expand1(expr const & m, abstract_type_context & ctx) const { return expand(m, ctx); }
virtual unsigned trust_level() const;
virtual bool operator==(macro_definition_cell const & other) const;
virtual void display(std::ostream & out) const;
virtual unsigned hash() const;
virtual void write(serializer & s) const = 0;
typedef std::function<expr(deserializer&, unsigned, expr const *)> reader;
};
/** \brief Smart pointer for macro definitions */
class macro_definition {
public:
macro_definition_cell * m_ptr;
public:
explicit macro_definition(macro_definition_cell * ptr);
macro_definition(macro_definition const & s);
macro_definition(macro_definition && s);
~macro_definition();
macro_definition & operator=(macro_definition const & s);
macro_definition & operator=(macro_definition && s);
name get_name() const { return m_ptr->get_name(); }
expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const {
return m_ptr->check_type(m, ctx, infer_only);
}
optional<expr> expand(expr const & m, abstract_type_context & ctx) const { return m_ptr->expand(m, ctx); }
optional<expr> expand1(expr const & m, abstract_type_context & ctx) const { return m_ptr->expand1(m, ctx); }
unsigned trust_level() const { return m_ptr->trust_level(); }
bool operator==(macro_definition const & other) const { return m_ptr->operator==(*other.m_ptr); }
bool operator!=(macro_definition const & other) const { return !operator==(other); }
bool operator<(macro_definition const & other) const;
void display(std::ostream & out) const { return m_ptr->display(out); }
unsigned hash() const { return m_ptr->hash(); }
void write(serializer & s) const { return m_ptr->write(s); }
macro_definition_cell const * raw() const { return m_ptr; }
friend bool is_eqp(macro_definition const & d1, macro_definition const & d2) {
return d1.m_ptr == d2.m_ptr;
}
};
/** \brief Macro attachments */
class expr_macro : public expr_composite {
macro_definition m_definition;
unsigned m_num_args;
friend class expr_cell;
friend expr copy(expr const & a);
friend expr update_macro(expr const & e, unsigned num, expr const * args);
void dealloc(buffer<expr_cell*> & todelete);
expr * get_args_ptr() {
return reinterpret_cast<expr *>(reinterpret_cast<char *>(this)+sizeof(expr_macro));
}
expr const * get_args_ptr() const {
return reinterpret_cast<expr const *>(reinterpret_cast<char const *>(this)+sizeof(expr_macro));
}
friend struct cache_expr_insert_fn;
expr_macro(expr_macro const & src, expr const * new_args); // for hash_consing
public:
expr_macro(macro_definition const & v, unsigned num, expr const * args);
~expr_macro();
macro_definition const & get_def() const { return m_definition; }
expr const * get_args() const { return get_args_ptr(); }
expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return get_args_ptr()[idx]; }
unsigned get_num_args() const { return m_num_args; }
};
// =======================================
// Testers
inline bool is_bvar(expr_ptr e) { return e->kind() == expr_kind::BVar; }
inline bool is_fvar(expr_ptr e) { return e->kind() == expr_kind::FVar; }
inline bool is_fvar(expr_ptr e) { return e->kind() == expr_kind::FVar; }
inline bool is_constant(expr_ptr e) { return e->kind() == expr_kind::Constant; }
inline bool is_metavar(expr_ptr e) { return e->kind() == expr_kind::Meta; }
inline bool is_macro(expr_ptr e) { return e->kind() == expr_kind::Macro; }
inline bool is_app(expr_ptr e) { return e->kind() == expr_kind::App; }
inline bool is_lambda(expr_ptr e) { return e->kind() == expr_kind::Lambda; }
inline bool is_pi(expr_ptr e) { return e->kind() == expr_kind::Pi; }
@ -547,6 +468,7 @@ inline unsigned get_loose_bvar_range(expr const & e) {
switch (e.kind()) {
case expr_kind::BVar: return bvar_idx(e) + 1;
case expr_kind::Constant: case expr_kind::Sort: return 0;
case expr_kind::Quote: return 0;
default: return static_cast<expr_composite*>(e.raw())->m_loose_bvar_range;
}
}
@ -596,7 +518,6 @@ expr update_local(expr const & e, expr const & new_type, binder_info const & bi)
expr update_local(expr const & e, binder_info const & bi);
expr update_sort(expr const & e, level const & new_level);
expr update_constant(expr const & e, levels const & new_levels);
expr update_macro(expr const & e, unsigned num, expr const * args);
expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body);
// =======================================
@ -649,15 +570,117 @@ void finalize_expr();
The following API is to support legacy code
-------------------------------- */
// TODO(Leo): delete
class expr_quote : public expr_cell {
bool m_reflected;
expr m_value;
friend class expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_quote(bool r, expr const & v);
~expr_quote() {}
bool is_reflected() const { return m_reflected; }
expr const & get_value() const { return m_value; }
};
/** \brief Abstract class for macro_definitions */
class macro_definition_cell {
protected:
void dealloc() { delete this; }
MK_LEAN_RC();
/**
\brief Auxiliary method used for implementing a total order on macro
attachments. It is invoked by operator<, and it is only invoked when
<tt>get_name() == other.get_name()</tt>
*/
virtual bool lt(macro_definition_cell const &) const;
public:
macro_definition_cell():m_rc(0) {}
virtual ~macro_definition_cell() {}
virtual name get_name() const = 0;
virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const = 0;
virtual optional<expr> expand(expr const & m, abstract_type_context & ctx) const = 0;
virtual optional<expr> expand1(expr const & m, abstract_type_context & ctx) const { return expand(m, ctx); }
virtual unsigned trust_level() const;
virtual bool operator==(macro_definition_cell const & other) const;
virtual void display(std::ostream & out) const;
virtual unsigned hash() const;
virtual void write(serializer & s) const = 0;
typedef std::function<expr(deserializer&, unsigned, expr const *)> reader;
};
/** \brief Smart pointer for macro definitions */
class macro_definition {
public:
macro_definition_cell * m_ptr;
public:
explicit macro_definition(macro_definition_cell * ptr);
macro_definition(macro_definition const & s);
macro_definition(macro_definition && s);
~macro_definition();
macro_definition & operator=(macro_definition const & s);
macro_definition & operator=(macro_definition && s);
name get_name() const { return m_ptr->get_name(); }
expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const {
return m_ptr->check_type(m, ctx, infer_only);
}
optional<expr> expand(expr const & m, abstract_type_context & ctx) const { return m_ptr->expand(m, ctx); }
optional<expr> expand1(expr const & m, abstract_type_context & ctx) const { return m_ptr->expand1(m, ctx); }
unsigned trust_level() const { return m_ptr->trust_level(); }
bool operator==(macro_definition const & other) const { return m_ptr->operator==(*other.m_ptr); }
bool operator!=(macro_definition const & other) const { return !operator==(other); }
bool operator<(macro_definition const & other) const;
void display(std::ostream & out) const { return m_ptr->display(out); }
unsigned hash() const { return m_ptr->hash(); }
void write(serializer & s) const { return m_ptr->write(s); }
macro_definition_cell const * raw() const { return m_ptr; }
friend bool is_eqp(macro_definition const & d1, macro_definition const & d2) {
return d1.m_ptr == d2.m_ptr;
}
};
/** \brief Macro attachments */
class expr_macro : public expr_composite {
macro_definition m_definition;
unsigned m_num_args;
friend class expr_cell;
friend expr copy(expr const & a);
friend expr update_macro(expr const & e, unsigned num, expr const * args);
void dealloc(buffer<expr_cell*> & todelete);
expr * get_args_ptr() {
return reinterpret_cast<expr *>(reinterpret_cast<char *>(this)+sizeof(expr_macro));
}
expr const * get_args_ptr() const {
return reinterpret_cast<expr const *>(reinterpret_cast<char const *>(this)+sizeof(expr_macro));
}
friend struct cache_expr_insert_fn;
expr_macro(expr_macro const & src, expr const * new_args); // for hash_consing
public:
expr_macro(macro_definition const & v, unsigned num, expr const * args);
~expr_macro();
macro_definition const & get_def() const { return m_definition; }
expr const * get_args() const { return get_args_ptr(); }
expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return get_args_ptr()[idx]; }
unsigned get_num_args() const { return m_num_args; }
};
inline bool is_var(expr_ptr e) { return is_bvar(e); }
inline bool is_local(expr_ptr e) { return is_fvar(e); }
inline bool is_mlocal(expr_ptr e) { return is_metavar(e) || is_local(e); }
inline bool is_quote(expr_ptr e) { return e->kind() == expr_kind::Quote; }
inline bool is_macro(expr_ptr e) { return e->kind() == expr_kind::Macro; }
inline unsigned var_idx(expr_ptr e) { return bvar_idx(e); }
inline bool is_var(expr_ptr e, unsigned i) { return is_bvar(e, i); }
inline expr_bvar * to_var(expr_ptr e) { return to_bvar(e); }
inline expr_mlocal * to_mlocal(expr_ptr e) { lean_assert(is_mlocal(e)); return static_cast<expr_mlocal*>(e); }
inline expr_fvar * to_local(expr_ptr e) { return to_fvar(e); }
inline expr_macro * to_macro(expr_ptr e) { lean_assert(is_macro(e)); return static_cast<expr_macro*>(e); }
inline expr_quote * to_quote(expr_ptr e) { lean_assert(is_quote(e)); return static_cast<expr_quote*>(e); }
inline name const & mlocal_name(expr_ptr e) { return to_mlocal(e)->get_name(); }
inline expr const & mlocal_type(expr_ptr e) { return to_mlocal(e)->get_type(); }
inline name const & mlocal_pp_name(expr_ptr e) { return to_mlocal(e)->get_pp_name(); }
@ -669,6 +692,7 @@ inline unsigned macro_num_args(expr_ptr e) { return to_macro(e)->ge
inline expr mk_var(unsigned idx) { return mk_bvar(idx); }
inline expr Var(unsigned idx) { return mk_bvar(idx); }
expr mk_macro(macro_definition const & m, unsigned num = 0, expr const * args = nullptr);
expr mk_quote(bool reflected, expr const & val);
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi);
inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t, binder_info()); }
inline expr mk_local(name const & n, expr const & t, binder_info const & bi) {
@ -678,4 +702,9 @@ inline expr Local(name const & n, expr const & t, binder_info const & bi = binde
return mk_local(n, t, bi);
}
inline bool has_local(expr const & e) { return has_fvar(e); }
expr update_macro(expr const & e, unsigned num, expr const * args);
inline bool quote_is_reflected(expr const & e) { return to_quote(e)->is_reflected(); }
inline expr const & quote_value(expr const & e) { return to_quote(e)->get_value(); }
}

6
src/kernel/expr_eq_fn.cpp
View file

@ -108,6 +108,8 @@ class expr_eq_fn {
(!CompareBinderInfo || let_name(a) == let_name(b));
case expr_kind::Sort:
return sort_level(a) == sort_level(b);
case expr_kind::Macro:
check_system();
if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b))
@ -117,6 +119,10 @@ class expr_eq_fn {
return false;
}
return true;
case expr_kind::Quote:
/* Hack: we do *not* compare m_value's because quoted expressions may contain
relevant position information that is ignored by the equality predicate for expressions. */
return a.raw() == b.raw();
}
lean_unreachable(); // LCOV_EXCL_LINE
}

18
src/kernel/for_each_fn.cpp
View file

@ -95,14 +95,6 @@ class for_each_fn {
case expr_kind::Meta:
todo.emplace_back(mlocal_type(e), offset);
goto begin_loop;
case expr_kind::Macro: {
unsigned i = macro_num_args(e);
while (i > 0) {
--i;
todo.emplace_back(macro_arg(e, i), offset);
}
goto begin_loop;
}
case expr_kind::App:
todo.emplace_back(app_arg(e), offset);
todo.emplace_back(app_fn(e), offset);
@ -116,6 +108,16 @@ class for_each_fn {
todo.emplace_back(let_value(e), offset);
todo.emplace_back(let_type(e), offset);
goto begin_loop;
case expr_kind::Macro: {
unsigned i = macro_num_args(e);
while (i > 0) {
--i;
todo.emplace_back(macro_arg(e, i), offset);
}
goto begin_loop;
}
case expr_kind::Quote:
goto begin_loop;
}
}
}

10
src/kernel/old_type_checker.cpp
View file

@ -25,6 +25,10 @@ namespace lean {
static name * g_kernel_fresh = nullptr;
static expr * g_dont_care = nullptr;
[[noreturn]] static void throw_found_quote(environment const & env) {
throw kernel_exception(env, "unexpected quoted expression");
}
optional<expr> old_type_checker::expand_macro(expr const & m) {
lean_assert(is_macro(m));
return macro_def(m).expand(m, *this);
@ -227,6 +231,8 @@ expr old_type_checker::infer_type_core(expr const & e, bool infer_only) {
case expr_kind::Pi: r = infer_pi(e, infer_only); break;
case expr_kind::App: r = infer_app(e, infer_only); break;
case expr_kind::Let: r = infer_let(e, infer_only); break;
case expr_kind::Quote: throw_found_quote(m_env);
}
if (m_memoize)
@ -282,6 +288,7 @@ expr old_type_checker::whnf_core(expr const & e) {
return e;
case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
break;
case expr_kind::Quote: throw_found_quote(m_env);
}
// check cache
@ -331,6 +338,7 @@ expr old_type_checker::whnf_core(expr const & e) {
case expr_kind::Let:
r = whnf_core(instantiate(let_body(e), let_value(e)));
break;
case expr_kind::Quote: throw_found_quote(m_env);
}
if (m_memoize)
@ -385,6 +393,7 @@ expr old_type_checker::whnf(expr const & e) {
case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App:
case expr_kind::Constant: case expr_kind::Let:
break;
case expr_kind::Quote: throw_found_quote(m_env);
}
// check cache
@ -479,6 +488,7 @@ lbool old_type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use
case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let:
// We do not handle these cases in this method.
break;
case expr_kind::Quote: throw_found_quote(m_env);
}
}
return l_undef; // This is not an "easy case"

5
src/kernel/replace_fn.cpp
View file

@ -111,7 +111,10 @@ class replace_rec_fn {
for (unsigned i = 0; i < nargs; i++)
new_args.push_back(apply(macro_arg(e, i), offset));
return save_result(e, offset, update_macro(e, new_args.size(), new_args.data()), shared);
}}
}
case expr_kind::Quote:
return save_result(e, offset, e, shared);
}
lean_unreachable();
}
}

24
src/kernel/type_checker.cpp
View file

@ -227,11 +227,20 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
r = mk_sort(mk_succ(sort_level(e)));
break;
case expr_kind::Constant: r = infer_constant(e, infer_only); break;
case expr_kind::Macro: r = infer_macro(e, infer_only); break;
case expr_kind::Lambda: r = infer_lambda(e, infer_only); break;
case expr_kind::Pi: r = infer_pi(e, infer_only); break;
case expr_kind::App: r = infer_app(e, infer_only); break;
case expr_kind::Let: r = infer_let(e, infer_only); break;
case expr_kind::Macro: r = infer_macro(e, infer_only); break;
case expr_kind::Quote:
if (quote_is_reflected(e)) {
expr type = infer_type_core(quote_value(e), true);
level u = sort_level(ensure_sort_core(infer_type_core(type, true), e));
return mk_app(mk_constant(name("reflected"), {u}), type, quote_value(e));
} else {
return mk_constant(name("pexpr"));
}
}
if (m_memoize)
@ -299,6 +308,9 @@ expr type_checker::whnf_core(expr const & e) {
return whnf_fvar(e);
case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
break;
case expr_kind::Quote:
return e;
}
// check cache
@ -314,6 +326,10 @@ expr type_checker::whnf_core(expr const & e) {
case expr_kind::BVar: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::FVar:
case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Quote:
lean_unreachable();
case expr_kind::Macro:
if (auto m = expand_macro(e))
r = whnf_core(*m);
@ -404,6 +420,9 @@ expr type_checker::whnf(expr const & e) {
case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App:
case expr_kind::Constant: case expr_kind::Let:
break;
case expr_kind::Quote:
return e;
}
// check cache
@ -499,6 +518,9 @@ lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_has
case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let:
// We do not handle these cases in this method.
break;
case expr_kind::Quote:
return to_lbool(t.raw() == s.raw());
}
}
return l_undef; // This is not an "easy case"

6
src/library/check.cpp
View file

@ -116,8 +116,6 @@ struct check_fn {
return visit_constant(e);
case expr_kind::BVar:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Macro:
return visit_macro(e);
case expr_kind::Lambda:
return visit_lambda(e);
case expr_kind::Pi:
@ -126,6 +124,10 @@ struct check_fn {
return visit_app(e);
case expr_kind::Let:
return visit_let(e);
case expr_kind::Macro:
return visit_macro(e);
case expr_kind::Quote:
break; /* do nothing */
}
}

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

@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/annotation.h"
#include "library/quote.h"
#include "library/compiler/util.h"
#include "library/compiler/compiler_step_visitor.h"

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

@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/instantiate.h"
#include "library/quote.h"
#include "library/compiler/compiler_step_visitor.h"
#include "library/compiler/comp_irrelevant.h"

3
src/library/compiler/cse.cpp
View file

@ -56,7 +56,8 @@ class cse_fn : public compiler_step_visitor {
case expr_kind::Macro: visit_macro(e); break;
case expr_kind::App: visit_app(e); break;
case expr_kind::Let: visit_let(e); break;
default: break;
case expr_kind::Quote:
break;
}
}
public:

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

@ -12,7 +12,6 @@ Author: Leonardo de Moura
#include "library/normalize.h"
#include "library/inverse.h"
#include "library/aux_recursors.h"
#include "library/quote.h"
#include "library/inductive_compiler/ginductive.h"
#include "library/compiler/util.h"
#include "library/compiler/nat_value.h"

1
src/library/compiler/preprocess.cpp
View file

@ -16,7 +16,6 @@ Author: Leonardo de Moura
#include "library/aux_recursors.h"
#include "library/user_recursors.h"
#include "library/util.h"
#include "library/quote.h"
#include "library/noncomputable.h"
#include "library/context_cache.h"
#include "library/module.h"

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

@ -289,6 +289,10 @@ class vm_compiler_fn {
}
}
void compile_quote(expr const & e) {
emit(mk_expr_instr(quote_value(e)));
}
void compile(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
switch (e.kind()) {
case expr_kind::BVar: lean_unreachable();
@ -301,6 +305,7 @@ class vm_compiler_fn {
case expr_kind::FVar: compile_local(e, m); break;
case expr_kind::App: compile_app(e, bpz, m); break;
case expr_kind::Let: compile_let(e, bpz, m); break;
case expr_kind::Quote: compile_quote(e); break;
}
}

1
src/library/deep_copy.cpp
View file

@ -21,6 +21,7 @@ expr copy(expr const & a) {
case expr_kind::Meta: return mk_metavar(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a));
case expr_kind::FVar: return mk_local(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a), local_info(a));
case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
case expr_kind::Quote: return mk_quote(quote_is_reflected(a), quote_value(a));
}
lean_unreachable(); // LCOV_EXCL_LINE
}

14
src/library/equations_compiler/structural_rec.cpp
View file

@ -118,11 +118,6 @@ struct structural_rec_fn {
case expr_kind::FVar: case expr_kind::Constant:
case expr_kind::Sort:
return true;
case expr_kind::Macro:
for (unsigned i = 0; i < macro_num_args(e); i++)
if (!check_rhs(macro_arg(e, i)))
return false;
return true;
case expr_kind::App: {
buffer<expr> args;
expr const & fn = get_app_args(e, args);
@ -171,6 +166,15 @@ struct structural_rec_fn {
type_context_old::tmp_locals locals(m_ctx);
return check_rhs(instantiate(binding_body(e), locals.push_local_from_binding(e)));
}
case expr_kind::Macro:
for (unsigned i = 0; i < macro_num_args(e); i++)
if (!check_rhs(macro_arg(e, i)))
return false;
return true;
case expr_kind::Quote:
return true;
}
lean_unreachable();
}

4
src/library/expr_lt.cpp
View file

@ -69,6 +69,8 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const *
return is_lt(macro_arg(a, i), macro_arg(b, i), use_hash, lctx);
}
return false;
case expr_kind::Quote:
return quote_value(a) < quote_value(b);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -179,6 +181,8 @@ bool is_lt_no_level_params(expr const & a, expr const & b) {
return false;
}
return false;
case expr_kind::Quote:
return quote_value(a) < quote_value(b);
}
lean_unreachable();
}

2
src/library/inductive_compiler/nested.cpp
View file

@ -533,6 +533,7 @@ class add_nested_inductive_decl_fn {
case expr_kind::Sort:
case expr_kind::FVar:
case expr_kind::Macro:
case expr_kind::Quote:
return _e;
case expr_kind::Lambda:
case expr_kind::Pi:
@ -587,6 +588,7 @@ class add_nested_inductive_decl_fn {
case expr_kind::Sort:
case expr_kind::FVar:
case expr_kind::Macro:
case expr_kind::Quote:
return _e;
case expr_kind::Lambda:
case expr_kind::Pi:

44
src/library/kernel_serializer.cpp
View file

@ -84,13 +84,6 @@ class expr_serializer : public object_serializer<expr, expr_hash, is_bi_equal_pr
case expr_kind::Sort:
s << sort_level(a);
break;
case expr_kind::Macro:
s << macro_num_args(a);
for (unsigned i = 0; i < macro_num_args(a); i++) {
write_core(macro_arg(a, i));
}
macro_def(a).write(s);
break;
case expr_kind::App:
write_core(app_fn(a)); write_core(app_arg(a));
break;
@ -112,6 +105,18 @@ class expr_serializer : public object_serializer<expr, expr_hash, is_bi_equal_pr
lean_assert(!mlocal_pp_name(a).is_anonymous());
s << mlocal_name(a) << mlocal_pp_name(a) << local_info(a); write_core(mlocal_type(a));
break;
case expr_kind::Macro:
s << macro_num_args(a);
for (unsigned i = 0; i < macro_num_args(a); i++) {
write_core(macro_arg(a, i));
}
macro_def(a).write(s);
break;
case expr_kind::Quote:
s << quote_is_reflected(a);
write_core(quote_value(a));
break;
}
});
}
@ -146,14 +151,6 @@ public:
}
case expr_kind::Sort:
return mk_sort(read_level(d));
case expr_kind::Macro: {
unsigned n = d.read_unsigned();
buffer<expr> args;
for (unsigned i = 0; i < n; i++) {
args.push_back(read());
}
return read_macro_definition(d, args.size(), args.data());
}
case expr_kind::App: {
expr f = read();
return mk_app(f, read());
@ -176,7 +173,22 @@ public:
name pp_n = read_name(d);
binder_info bi = read_binder_info(d);
return mk_local(n, pp_n, read(), bi);
}}
}
case expr_kind::Macro: {
unsigned n = d.read_unsigned();
buffer<expr> args;
for (unsigned i = 0; i < n; i++) {
args.push_back(read());
}
return read_macro_definition(d, args.size(), args.data());
}
case expr_kind::Quote: {
bool r = d.read_bool();
expr v = read();
return mk_quote(r, v);
}
}
throw corrupted_stream_exception(); // LCOV_EXCL_LINE
});
}

12
src/library/locals.cpp
View file

@ -83,10 +83,6 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
lean_assert(!restricted);
visit(mlocal_type(e));
break;
case expr_kind::Macro:
for (unsigned i = 0; i < macro_num_args(e); i++)
visit(macro_arg(e, i));
break;
case expr_kind::App:
visit(app_fn(e));
visit(app_arg(e));
@ -101,6 +97,14 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
visit(let_value(e));
visit(let_body(e));
break;
case expr_kind::Macro:
for (unsigned i = 0; i < macro_num_args(e); i++)
visit(macro_arg(e, i));
break;
case expr_kind::Quote:
break; // do nothing
}
};
visit(e);

6
src/library/max_sharing.cpp
View file

@ -90,7 +90,11 @@ struct max_sharing_fn::imp {
new_args.push_back(macro_arg(a, i));
res = update_macro(a, new_args.size(), new_args.data());
break;
}}
}
case expr_kind::Quote:
res = a;
break;
}
m_expr_cache.insert(res);
return res;
}

1
src/library/noncomputable.cpp
View file

@ -199,6 +199,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::Quote: return;
}
}

6
src/library/normalize.cpp
View file

@ -117,7 +117,7 @@ class normalize_fn {
e = m_ctx.whnf(e);
switch (e.kind()) {
case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort:
case expr_kind::Meta: case expr_kind::FVar: case expr_kind::Macro:
case expr_kind::Meta: case expr_kind::FVar:
return e;
case expr_kind::Lambda: {
e = normalize_binding(e);
@ -133,6 +133,10 @@ class normalize_fn {
case expr_kind::Let:
// whnf unfolds let-exprs
lean_unreachable();
case expr_kind::Macro:
case expr_kind::Quote:
return e;
}
lean_unreachable(); // LCOV_EXCL_LINE
}

5
src/library/pos_info_provider.cpp
View file

@ -164,7 +164,10 @@ class replace_rec_fn2 {
for (unsigned i = 0; i < nargs; i++)
new_args.push_back(apply(macro_arg(e, i), offset));
return save_result(e, offset, copy_pos(e, update_macro(e, new_args.size(), new_args.data())), shared);
}}
}
case expr_kind::Quote:
return save_result(e, offset, e, shared);
}
lean_unreachable();
}
}

4
src/library/print.cpp
View file

@ -251,6 +251,10 @@ struct print_expr_fn {
case expr_kind::Macro:
print_macro(a);
break;
case expr_kind::Quote:
out() << "quote " << quote_is_reflected(a) << " ";
print(quote_value(a));
break;
}
}

85
src/library/quote.cpp
View file

@ -22,85 +22,34 @@ static std::string * g_expr_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;
/** \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 {
expr m_value;
bool m_reflected;
public:
expr_quote_macro(expr const & v, bool reflected):m_value(v), m_reflected(reflected) {}
virtual bool lt(macro_definition_cell const & d) const override {
return m_value < static_cast<expr_quote_macro const &>(d).m_value;
}
virtual name get_name() const override { return *g_expr_quote_macro; }
virtual expr check_type(expr const &, abstract_type_context & ctx, bool infer_only) const override {
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 override {
return optional<expr>();
}
virtual unsigned trust_level() const override { return 0; }
virtual bool operator==(macro_definition_cell const & other) const override {
/* Hack: we do *not* compare m_value's because quoted expressions may contain
relevant position information that is ignored by the equality predicate for expressions.
*/
return this == &other;
}
char const * prefix() const {
return m_reflected ? "`(" : "``(";
}
virtual void display(std::ostream & out) const override {
out << prefix() << m_value << ")";
}
virtual unsigned hash() const override { return m_value.hash(); }
virtual void write(serializer & s) const override { 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_elaborated_expr_quote(expr const & e) {
return mk_macro(macro_definition(new expr_quote_macro(e, /* reflected */ true)));
return mk_quote(true, e);
}
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 expr_quote_macro(e, /* reflected */ false)));
return mk_quote(false, e);
}
bool is_expr_quote(expr const & e) {
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;
return
(is_annotation(e, *g_expr_quote_pre)) ||
(is_quote(e) && quote_is_reflected(e));
}
bool is_pexpr_quote(expr const & e) {
if (is_macro(e)) {
if (auto m = dynamic_cast<expr_quote_macro const *>(macro_def(e).raw())) {
return !m->is_reflected();
}
}
return false;
return is_quote(e) && !quote_is_reflected(e);
}
expr const & get_expr_quote_value(expr const & e) {
lean_assert(is_expr_quote(e));
if (auto m = dynamic_cast<expr_quote_macro const *>(macro_def(e).raw())) {
return m->get_value();
if (is_quote(e)) {
return quote_value(e);
} else {
return get_annotation_arg(e);
}
@ -108,7 +57,7 @@ expr const & get_expr_quote_value(expr const & e) {
expr const & get_pexpr_quote_value(expr const & e) {
lean_assert(is_pexpr_quote(e));
return static_cast<expr_quote_macro const *>(macro_def(e).raw())->get_value();
return quote_value(e);
}
static name * g_antiquote = nullptr;
@ -152,8 +101,6 @@ expr mk_pexpr_quote_and_substs(expr const & e, bool is_strict) {
void initialize_quote() {
g_quote_fresh = new name("_quote_fresh");
register_name_generator_prefix(*g_quote_fresh);
g_expr_quote_macro = new name("expr_quote_macro");
g_expr_quote_opcode = new std::string("Quote");
g_expr = new expr(mk_app(Const(get_expr_name()), mk_bool_tt()));
g_pexpr = new expr(mk_constant(get_pexpr_name()));
@ -161,21 +108,11 @@ void initialize_quote() {
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 & d, unsigned num, expr const *) {
if (num != 0)
throw corrupted_stream_exception();
expr e; bool reflected;
d >> e >> reflected;
return mk_macro(macro_definition(new expr_quote_macro(e, reflected)));
});
}
void finalize_quote() {
delete g_quote_fresh;
delete g_expr_quote_pre;
delete g_expr_quote_macro;
delete g_expr_quote_opcode;
delete g_expr;
delete g_pexpr;

6
src/library/replace_visitor.cpp
View file

@ -15,6 +15,7 @@ Author: Leonardo de Moura
namespace lean {
expr replace_visitor::visit_sort(expr const & e) { lean_assert(is_sort(e)); return e; }
expr replace_visitor::visit_var(expr const & e) { lean_assert(is_var(e)); return e; }
expr replace_visitor::visit_quote(expr const & e) { lean_assert(is_quote(e)); return e; }
expr replace_visitor::visit_constant(expr const & e) { lean_assert(is_constant(e)); return e; }
expr replace_visitor::visit_mlocal(expr const & e) {
lean_assert(is_mlocal(e));
@ -67,7 +68,6 @@ expr replace_visitor::visit(expr const & e) {
switch (e.kind()) {
case expr_kind::Sort: return save_result(e, visit_sort(e), shared);
case expr_kind::Macro: return save_result(e, visit_macro(e), shared);
case expr_kind::Constant: return save_result(e, visit_constant(e), shared);
case expr_kind::BVar: return save_result(e, visit_var(e), shared);
case expr_kind::Meta: return save_result(e, visit_meta(e), shared);
@ -76,8 +76,10 @@ expr replace_visitor::visit(expr const & e) {
case expr_kind::Lambda: return save_result(e, visit_lambda(e), shared);
case expr_kind::Pi: return save_result(e, visit_pi(e), shared);
case expr_kind::Let: return save_result(e, visit_let(e), shared);
}
case expr_kind::Macro: return save_result(e, visit_macro(e), shared);
case expr_kind::Quote: return save_result(e, visit_quote(e), shared);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
}

4
src/library/replace_visitor.h
View file

@ -19,7 +19,6 @@ protected:
cache m_cache;
expr save_result(expr const & e, expr && r, bool shared);
virtual expr visit_sort(expr const &);
virtual expr visit_macro(expr const &);
virtual expr visit_constant(expr const &);
virtual expr visit_var(expr const &);
virtual expr visit_mlocal(expr const &);
@ -31,6 +30,9 @@ protected:
virtual expr visit_pi(expr const &);
virtual expr visit_let(expr const & e);
virtual expr visit(expr const &);
virtual expr visit_macro(expr const &);
virtual expr visit_quote(expr const &);
public:
expr operator()(expr const & e) { return visit(e); }
void clear() { m_cache.clear(); }

11
src/library/tactic/dsimplify.cpp
View file

@ -264,9 +264,6 @@ expr dsimplify_core_fn::visit(expr const & e) {
case expr_kind::Meta:
new_e = visit_meta(curr_e);
break;
case expr_kind::Macro:
new_e = visit_macro(curr_e);
break;
case expr_kind::Lambda:
case expr_kind::Pi:
new_e = visit_binding(curr_e);
@ -277,6 +274,14 @@ expr dsimplify_core_fn::visit(expr const & e) {
case expr_kind::Let:
new_e = visit_let(curr_e);
break;
case expr_kind::Macro:
new_e = visit_macro(curr_e);
break;
case expr_kind::Quote:
new_e = curr_e;
break;
}
if (auto p2 = post(new_e)) {

2
src/library/tactic/simp_lemmas.cpp
View file

@ -665,6 +665,8 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset,
return false;
}
return true;
case expr_kind::Quote:
return lhs == rhs;
}
lean_unreachable();
}

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

@ -653,9 +653,6 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
new_result = curr_result;
new_result.update(m_ctx.instantiate_mvars(new_result.get_new()));
break;
case expr_kind::Macro:
new_result = join(curr_result, visit_macro(curr_result.get_new()));
break;
case expr_kind::BVar:
lean_unreachable();
case expr_kind::Lambda:
@ -670,6 +667,13 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
case expr_kind::Let:
new_result = join(curr_result, visit_let(curr_result.get_new()));
break;
case expr_kind::Macro:
new_result = join(curr_result, visit_macro(curr_result.get_new()));
break;
case expr_kind::Quote:
new_result = curr_result;
break;
}
if (m_cfg.m_constructor_eq && simplify_constructor_eq_constructor(new_result)) {

50
src/library/type_context.cpp
View file

@ -820,14 +820,6 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
}
}
return e;
case expr_kind::Macro:
if (auto m = expand_macro(e)) {
check_system("whnf");
e = *m;
continue;
} else {
return e;
}
case expr_kind::Let:
check_system("whnf");
if (use_zeta()) {
@ -882,7 +874,19 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
e = mk_rev_app(f, args.size(), args.data());
continue;
}
}}}
}
case expr_kind::Macro:
if (auto m = expand_macro(e)) {
check_system("whnf");
e = *m;
continue;
} else {
return e;
}
case expr_kind::Quote:
return e;
}}
}
expr type_context_old::whnf(expr const & e) {
@ -1011,9 +1015,6 @@ expr type_context_old::infer_core(expr const & e) {
case expr_kind::Constant:
r = infer_constant(e);
break;
case expr_kind::Macro:
r = infer_macro(e);
break;
case expr_kind::Lambda:
r = infer_lambda(e);
break;
@ -1026,6 +1027,17 @@ expr type_context_old::infer_core(expr const & e) {
case expr_kind::Let:
r = infer_let(e);
break;
case expr_kind::Macro:
r = infer_macro(e);
break;
case expr_kind::Quote:
if (quote_is_reflected(e)) {
expr type = infer_core(quote_value(e));
return mk_app(mk_constant(get_reflected_name(), {get_level(type)}), type, quote_value(e));
} else {
return mk_constant(get_pexpr_name());
}
}
if ((!in_tmp_mode() || (!has_expr_metavar(e) && !has_expr_metavar(r))) &&
@ -2704,10 +2716,16 @@ lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) {
return to_lbool(is_def_eq(sort_level(e1), sort_level(e2)));
case expr_kind::Meta: case expr_kind::BVar:
case expr_kind::FVar: case expr_kind::App:
case expr_kind::Constant: case expr_kind::Macro:
case expr_kind::Constant:
case expr_kind::Let:
// We do not handle these cases in this method.
break;
case expr_kind::Macro:
// We do not handle these cases in this method.
break;
case expr_kind::Quote:
return to_lbool(quote_is_reflected(e1) == quote_is_reflected(e2) && quote_value(e1) == quote_value(e2));
}
}
return l_undef; // This is not an "easy case"
@ -3326,8 +3344,6 @@ 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::Macro:
return l_undef;
case expr_kind::Constant:
if (auto r = constant_is_class(*it)) {
result = *r;
@ -3357,6 +3373,10 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
case expr_kind::Pi:
it = &binding_body(*it);
break;
case expr_kind::Macro:
return l_undef;
case expr_kind::Quote:
return l_false;
}
}
}

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

@ -196,13 +196,19 @@ unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
data.push_back(to_obj(let_value(e)));
data.push_back(to_obj(let_body(e)));
break;
case expr_kind::Macro:
case expr_kind::Macro: {
data.push_back(to_obj(macro_def(e)));
buffer<expr> args;
args.append(macro_num_args(e), macro_args(e));
data.push_back(to_obj(args));
break;
}
case expr_kind::Quote:
data.push_back(to_obj(quote_is_reflected(e)));
data.push_back(to_obj(quote_value(e)));
break;
}
return static_cast<unsigned>(e.kind());
}