From 23988f528cb3f47726e958459d8b0910fad80592 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Feb 2014 09:53:55 -0800 Subject: [PATCH] refactor(kernel/expr): add expr constructors, and expression equality test Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/expr.cpp | 285 +++++++++++++++------------------- src/kernel/expr.h | 316 +++++++++++--------------------------- src/kernel/expr_eq.h | 102 ------------ src/kernel/expr_eq_fn.cpp | 71 +++++++++ src/kernel/expr_eq_fn.h | 25 +++ 6 files changed, 306 insertions(+), 495 deletions(-) delete mode 100644 src/kernel/expr_eq.h create mode 100644 src/kernel/expr_eq_fn.cpp create mode 100644 src/kernel/expr_eq_fn.h diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 683de6c19..3e1db1ada 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp +add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp # free_vars.cpp abstract.cpp instantiate.cpp # normalizer.cpp context.cpp level.cpp object.cpp environment.cpp # type_checker.cpp kernel.cpp occurs.cpp metavar.cpp diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 51ed6a387..561970ce1 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -9,35 +9,33 @@ Author: Leonardo de Moura #include #include #include +#include "util/list_fn.h" #include "util/hash.h" #include "util/buffer.h" #include "util/object_serializer.h" #include "kernel/expr.h" +#include "kernel/expr_eq_fn.h" // #include "kernel/free_vars.h" -// #include "kernel/expr_eq.h" // #include "kernel/metavar.h" // #include "kernel/max_sharing.h" namespace lean { -#if 0 static expr g_dummy(mk_var(0)); expr::expr():expr(g_dummy) {} -// Local context entries -local_entry::local_entry(unsigned s, unsigned n):m_kind(local_entry_kind::Lift), m_s(s), m_n(n) {} -local_entry::local_entry(unsigned s, expr const & v):m_kind(local_entry_kind::Inst), m_s(s), m_v(v) {} -local_entry::~local_entry() {} -bool local_entry::operator==(local_entry const & e) const { - if (m_kind != e.m_kind || m_s != e.m_s) - return false; - if (is_inst()) - return m_v == e.m_v; - else - return m_n == e.m_n; +unsigned hash_levels(levels const & ls) { + unsigned r = 23; + for (auto const & l : ls) + r = hash(hash(l), r); + return r; } -unsigned hash_args(unsigned size, expr const * args) { - return hash(size, [&args](unsigned i){ return args[i].hash(); }); +bool has_meta(levels const & ls) { + for (auto const & l : ls) { + if (has_meta(l)) + return true; + } + return false; } expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv): @@ -46,7 +44,7 @@ expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv): m_hash(h), m_rc(0) { // m_hash_alloc does not need to be a unique identifier. - // We want diverse hash codes such that given expr_cell * c1 and expr_cell * c2, + // We want diverse hash codes because given expr_cell * c1 and expr_cell * c2, // if c1 != c2, then there is high probability c1->m_hash_alloc != c2->m_hash_alloc. // Remark: using pointer address as a hash code is not a good idea. // - each execution run will behave differently. @@ -95,30 +93,31 @@ expr_var::expr_var(unsigned idx): m_vidx(idx) {} // Expr constants -expr_const::expr_const(name const & n, optional const & t): - expr_cell(expr_kind::Constant, n.hash(), t && t->has_metavar()), +expr_const::expr_const(name const & n, levels const & ls): + expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), has_meta(ls)), + m_name(n), + m_levels(ls) {} + +// Expr metavariables and local variables +expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t): + expr_cell(is_meta ? expr_kind::Meta : expr_kind::Local, n.hash(), t.has_metavar()), m_name(n), m_type(t) {} -void expr_const::dealloc(buffer & todelete) { +void expr_mlocal::dealloc(buffer & todelete) { dec_ref(m_type, todelete); delete(this); } -// Expr heterogeneous equality -expr_heq::expr_heq(expr const & lhs, expr const & rhs): - expr_cell(expr_kind::HEq, ::lean::hash(lhs.hash(), rhs.hash()), lhs.has_metavar() || rhs.has_metavar()), - m_lhs(lhs), m_rhs(rhs), m_depth(std::max(get_depth(lhs), get_depth(rhs))+1) { -} -void expr_heq::dealloc(buffer & todelete) { - dec_ref(m_lhs, todelete); - dec_ref(m_rhs, todelete); - delete(this); -} +// Composite expressions +expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, unsigned d): + expr_cell(k, h, has_mv), + m_depth(d) {} // Expr dependent pairs expr_dep_pair::expr_dep_pair(expr const & f, expr const & s, expr const & t): - expr_cell(expr_kind::Pair, ::lean::hash(f.hash(), s.hash()), f.has_metavar() || s.has_metavar() || t.has_metavar()), - m_first(f), m_second(s), m_type(t), m_depth(std::max(get_depth(f), get_depth(s))+1) { + expr_composite(expr_kind::Pair, ::lean::hash(f.hash(), s.hash()), f.has_metavar() || s.has_metavar() || t.has_metavar(), + std::max(get_depth(f), get_depth(s))+1), + m_first(f), m_second(s), m_type(t) { } void expr_dep_pair::dealloc(buffer & todelete) { dec_ref(m_first, todelete); @@ -129,100 +128,54 @@ void expr_dep_pair::dealloc(buffer & todelete) { // Expr pair projection expr_proj::expr_proj(bool f, expr const & e): - expr_cell(expr_kind::Proj, ::lean::hash(17, e.hash()), e.has_metavar()), - m_first(f), m_depth(get_depth(e)+1), m_expr(e) {} + expr_composite(f ? expr_kind::Fst : expr_kind::Snd, ::lean::hash(17, e.hash()), e.has_metavar(), get_depth(e)+1), + m_expr(e) {} void expr_proj::dealloc(buffer & todelete) { dec_ref(m_expr, todelete); delete(this); } // Expr applications -expr_app::expr_app(unsigned num_args, bool has_mv): - expr_cell(expr_kind::App, 0, has_mv), - m_num_args(num_args) { -} +expr_app::expr_app(expr const & fn, expr const & arg): + expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()), fn.has_metavar() || arg.has_metavar(), + std::max(get_depth(fn), get_depth(arg)) + 1), + m_fn(fn), m_arg(arg) {} void expr_app::dealloc(buffer & todelete) { - unsigned i = m_num_args; - while (i > 0) { - --i; - dec_ref(m_args[i], todelete); - } - delete[] reinterpret_cast(this); -} -expr mk_app(unsigned n, expr const * as) { - lean_assert(n > 1); - unsigned new_n; - unsigned n0 = 0; - expr const & arg0 = as[0]; - bool has_mv = std::any_of(as, as + n, [](expr const & c) { return c.has_metavar(); }); - // Remark: we represent ((app a b) c) as (app a b c) - if (is_app(arg0)) { - n0 = num_args(arg0); - new_n = n + n0 - 1; - } else { - new_n = n; - } - char * mem = new char[sizeof(expr_app) + new_n*sizeof(expr)]; - expr r(new (mem) expr_app(new_n, has_mv)); - expr * m_args = to_app(r)->m_args; - unsigned i = 0; - unsigned j = 0; - unsigned depth = 0; - if (new_n != n) { - for (; i < n0; ++i) { - new (m_args+i) expr(arg(arg0, i)); - depth = std::max(depth, get_depth(m_args[i])); - } - j++; - } - for (; i < new_n; ++i, ++j) { - lean_assert(j < n); - new (m_args+i) expr(as[j]); - depth = std::max(depth, get_depth(m_args[i])); - } - to_app(r)->m_hash = hash_args(new_n, m_args); - to_app(r)->m_depth = depth + 1; - return r; + dec_ref(m_fn, todelete); + dec_ref(m_arg, todelete); + delete(this); } -// Expr abstractions (and subclasses: Lambda, Pi and Sigma) -expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b): - expr_cell(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar()), +// Expr binders (Lambda, Pi and Sigma) +expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b): + expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar(), + std::max(get_depth(m_domain), get_depth(m_body)) + 1), m_name(n), m_domain(t), m_body(b) { - m_depth = 1 + std::max(get_depth(m_domain), get_depth(m_body)); + lean_assert(k == expr_kind::Lambda || k == expr_kind::Pi || k == expr_kind::Sigma); } -void expr_abstraction::dealloc(buffer & todelete) { +void expr_binder::dealloc(buffer & todelete) { dec_ref(m_body, todelete); dec_ref(m_domain, todelete); delete(this); } -expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Lambda, n, t, e) {} - -expr_pi::expr_pi(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Pi, n, t, e) {} - -expr_sigma::expr_sigma(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Sigma, n, t, e) {} - -// Expr Type -expr_type::expr_type(level const & l): - expr_cell(expr_kind::Type, l.hash(), false), +// Expr Sort +expr_sort::expr_sort(level const & l): + expr_cell(expr_kind::Sort, ::lean::hash(l), has_meta(l)), m_level(l) { } -expr_type::~expr_type() {} +expr_sort::~expr_sort() {} // Expr Let expr_let::expr_let(name const & n, optional const & t, expr const & v, expr const & b): - expr_cell(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), v.has_metavar() || b.has_metavar() || (t && t->has_metavar())), + expr_composite(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), v.has_metavar() || b.has_metavar() || ::lean::has_metavar(t), + std::max({get_depth(t), get_depth(v), get_depth(b)}) + 1), m_name(n), m_type(t), m_value(v), m_body(b) { - unsigned depth = std::max(get_depth(m_value), get_depth(m_body)); - if (m_type) - depth = std::max(depth, get_depth(*m_type)); - m_depth = 1 + depth; } void expr_let::dealloc(buffer & todelete) { dec_ref(m_body, todelete); @@ -232,55 +185,49 @@ void expr_let::dealloc(buffer & todelete) { } expr_let::~expr_let() {} -// Expr Semantic attachment -name value::get_unicode_name() const { return get_name(); } -optional value::normalize(unsigned, expr const *) const { return none_expr(); } -void value::display(std::ostream & out) const { out << get_name(); } -bool value::operator==(value const & other) const { return typeid(*this) == typeid(other); } -bool value::operator<(value const & other) const { +// Macro attachment +int macro::push_lua(lua_State *) const { return 0; } // NOLINT +void macro::display(std::ostream & out) const { out << get_name(); } +bool macro::operator==(macro const & other) const { return typeid(*this) == typeid(other); } +bool macro::operator<(macro const & other) const { if (get_name() == other.get_name()) return lt(other); else return get_name() < other.get_name(); } -format value::pp() const { return format(get_name()); } -format value::pp(bool unicode, bool) const { return unicode ? format(get_unicode_name()) : pp(); } -unsigned value::hash() const { return get_name().hash(); } -int value::push_lua(lua_State *) const { return 0; } // NOLINT -expr_value::expr_value(value & v): - expr_cell(expr_kind::Value, v.hash(), false), - m_val(v) { - m_val.inc_ref(); -} -expr_value::~expr_value() { - m_val.dec_ref(); -} -typedef std::unordered_map value_readers; -static std::unique_ptr g_value_readers; -value_readers & get_value_readers() { - if (!g_value_readers) - g_value_readers.reset(new value_readers()); - return *(g_value_readers.get()); +format macro::pp(formatter const &, options const &) const { return format(get_name()); } +bool macro::is_atomic_pp(bool, bool) const { return true; } +unsigned macro::hash() const { return get_name().hash(); } + +typedef std::unordered_map macro_readers; +static std::unique_ptr g_macro_readers; +macro_readers & get_macro_readers() { + if (!g_macro_readers) + g_macro_readers.reset(new macro_readers()); + return *(g_macro_readers.get()); } -void value::register_deserializer(std::string const & k, value::reader rd) { - value_readers & readers = get_value_readers(); +void macro::register_deserializer(std::string const & k, macro::reader rd) { + macro_readers & readers = get_macro_readers(); lean_assert(readers.find(k) == readers.end()); readers[k] = rd; } -static expr read_value(deserializer & d) { +static expr read_macro(deserializer & d) { auto k = d.read_string(); - value_readers & readers = get_value_readers(); + macro_readers & readers = get_macro_readers(); auto it = readers.find(k); lean_assert(it != readers.end()); return it->second(d); } -// Expr Metavariable -expr_metavar::expr_metavar(name const & n, local_context const & lctx): - expr_cell(expr_kind::MetaVar, n.hash(), true), - m_name(n), m_lctx(lctx) {} -expr_metavar::~expr_metavar() {} +expr_macro::expr_macro(macro * m): + expr_cell(expr_kind::Macro, m->hash(), false), + m_macro(m) { + m_macro->inc_ref(); +} +expr_macro::~expr_macro() { + m_macro->dec_ref(); +} void expr_cell::dealloc() { try { @@ -292,17 +239,18 @@ void expr_cell::dealloc() { lean_assert(it->get_rc() == 0); switch (it->kind()) { case expr_kind::Var: delete static_cast(it); break; - case expr_kind::Value: delete static_cast(it); break; - case expr_kind::MetaVar: delete static_cast(it); break; - case expr_kind::Type: delete static_cast(it); break; - case expr_kind::Constant: static_cast(it)->dealloc(todo); break; + case expr_kind::Macro: delete static_cast(it); break; + case expr_kind::Meta: + case expr_kind::Local: static_cast(it)->dealloc(todo); break; + case expr_kind::Constant: delete static_cast(it); break; + case expr_kind::Sort: delete static_cast(it); break; case expr_kind::Pair: static_cast(it)->dealloc(todo); break; - case expr_kind::Proj: static_cast(it)->dealloc(todo); break; + case expr_kind::Fst: + case expr_kind::Snd: static_cast(it)->dealloc(todo); break; case expr_kind::App: static_cast(it)->dealloc(todo); break; - case expr_kind::Lambda: static_cast(it)->dealloc(todo); break; - case expr_kind::Pi: static_cast(it)->dealloc(todo); break; - case expr_kind::Sigma: static_cast(it)->dealloc(todo); break; - case expr_kind::HEq: static_cast(it)->dealloc(todo); break; + case expr_kind::Lambda: + case expr_kind::Pi: + case expr_kind::Sigma: static_cast(it)->dealloc(todo); break; case expr_kind::Let: static_cast(it)->dealloc(todo); break; } } @@ -312,15 +260,44 @@ void expr_cell::dealloc() { } } -expr mk_type() { - static LEAN_THREAD_LOCAL expr r = mk_type(level()); +// Auxiliary constructors +expr mk_app(unsigned num_args, expr const * args) { + lean_assert(num_args >= 2); + expr r = mk_app(args[0], args[1]); + for (unsigned i = 2; i < num_args; i++) + r = mk_app(r, args[i]); return r; } -bool operator==(expr const & a, expr const & b) { - return expr_eq_fn<>()(a, b); +static name g_default_var_name("a"); +bool is_default_var_name(name const & n) { return n == g_default_var_name; } +expr mk_arrow(expr const & t, expr const & e) { return mk_pi(g_default_var_name, t, e); } +expr mk_cartesian_product(expr const & t, expr const & e) { return mk_sigma(g_default_var_name, t, e); } + +expr Bool = mk_sort(mk_level_zero()); +expr Type = mk_sort(mk_level_one()); +expr mk_Bool() { return Bool; } +expr mk_Type() { return Type; } + +unsigned get_depth(expr const & e) { + switch (e.kind()) { + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort: + case expr_kind::Meta: case expr_kind::Local: case expr_kind::Macro: + return 1; + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + case expr_kind::Pair: case expr_kind::Fst: case expr_kind::Snd: + case expr_kind::App: case expr_kind::Let: + return static_cast(e.raw())->m_depth; + } + lean_unreachable(); // LCOV_EXCL_LINE } +bool operator==(expr const & a, expr const & b) { return expr_eq_fn()(a, b); } + +#if 0 + + + bool is_arrow(expr const & t) { optional r = t.raw()->is_arrow(); if (r) { @@ -336,26 +313,6 @@ bool is_cartesian(expr const & t) { return is_sigma(t) && !has_free_var(abst_body(t), 0); } -unsigned get_depth(expr const & e) { - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: - case expr_kind::Value: case expr_kind::MetaVar: - return 1; - case expr_kind::HEq: - return to_heq(e)->m_depth; - case expr_kind::Pair: - return to_pair(e)->m_depth; - case expr_kind::Proj: - return to_proj(e)->m_depth; - case expr_kind::App: - return to_app(e)->m_depth; - case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Sigma: - return to_abstraction(e)->m_depth; - case expr_kind::Let: - return to_let(e)->m_depth; - } - lean_unreachable(); // LCOV_EXCL_LINE -} expr copy(expr const & a) { switch (a.kind()) { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 51d20c0da..d579197dc 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -25,6 +25,7 @@ Author: Leonardo de Moura namespace lean { class expr; +typedef list levels; /* ======================================= Expressions expr ::= Var idx @@ -120,7 +121,7 @@ public: friend expr mk_var(unsigned idx); friend expr mk_sort(level const & l); - friend expr mk_constant(name const & n, list const & ls); + friend expr mk_constant(name const & n, levels const & ls); friend expr mk_metavar(name const & n, expr const & t); friend expr mk_local(name const & n, expr const & t); friend expr mk_app(expr const & f, expr const & a); @@ -173,22 +174,22 @@ public: /** \brief (parametric) Constants. */ class expr_const : public expr_cell { - name m_name; - list m_levels; - friend class expr_cell; - void dealloc(buffer & to_delete); + name m_name; + levels m_levels; public: - expr_const(name const & n, list const & ls); + expr_const(name const & n, levels const & ls); name const & get_name() const { return m_name; } - list const & get_level_params() const { return m_levels; } + levels const & get_level_params() const { return m_levels; } }; /** \brief Metavariables and local constants */ -class expr_meta_local : public expr_cell { +class expr_mlocal : public expr_cell { name m_name; expr m_type; + friend expr_cell; + void dealloc(buffer & todelete); public: - expr_meta_local(bool is_meta, name const & n, expr const & t); + expr_mlocal(bool is_meta, name const & n, expr const & t); name const & get_name() const { return m_name; } expr const & get_type() const { return m_type; } }; @@ -218,8 +219,8 @@ class expr_dep_pair : public expr_composite { expr m_first; expr m_second; expr m_type; - friend expr_cell; friend expr mk_pair(expr const & f, expr const & s, expr const & t); + friend expr_cell; void dealloc(buffer & todelete); public: expr_dep_pair(expr const & f, expr const & s, expr const & t); @@ -343,7 +344,7 @@ inline bool is_sort(expr_cell * e) { return e->kind() == expr_kind::Sort; inline bool is_let(expr_cell * e) { return e->kind() == expr_kind::Let; } inline bool is_binder(expr_cell * e) { return is_lambda(e) || is_pi(e) || is_sigma(e); } inline bool is_proj(expr_cell * e) { return is_fst(e) || is_snd(e); } -inline bool is_meta_local(expr_cell * e) { return is_metavar(e) || is_local(e); } +inline bool is_mlocal(expr_cell * e) { return is_metavar(e) || is_local(e); } inline bool is_var(expr const & e) { return e.kind() == expr_kind::Var; } inline bool is_constant(expr const & e) { return e.kind() == expr_kind::Constant; } @@ -361,19 +362,19 @@ inline bool is_sort(expr const & e) { return e.kind() == expr_kind::Sort; inline bool is_let(expr const & e) { return e.kind() == expr_kind::Let; } inline bool is_binder(expr const & e) { return is_lambda(e) || is_pi(e) || is_sigma(e); } inline bool is_proj(expr const & e) { return is_fst(e) || is_snd(e); } -inline bool is_meta_local(expr const & e) { return is_metavar(e) || is_local(e); } +inline bool is_mlocal(expr const & e) { return is_metavar(e) || is_local(e); } // ======================================= // ======================================= // Constructors inline expr mk_var(unsigned idx) { return expr(new expr_var(idx)); } inline expr Var(unsigned idx) { return mk_var(idx); } -inline expr mk_constant(name const & n, list const & ls) { return expr(new expr_const(n, ls)); } -inline expr mk_constant(name const & n) { return mk_constant(n, list()); } +inline expr mk_constant(name const & n, levels const & ls) { return expr(new expr_const(n, ls)); } +inline expr mk_constant(name const & n) { return mk_constant(n, levels()); } inline expr Const(name const & n) { return mk_constant(n); } inline expr mk_macro(macro * m) { return expr(new expr_macro(m)); } -inline expr mk_metavar(name const & n, expr const & t) { return expr(new expr_meta_local(true, n, t)); } -inline expr mk_local(name const & n, expr const & t) { return expr(new expr_meta_local(false, n, t)); } +inline expr mk_metavar(name const & n, expr const & t) { return expr(new expr_mlocal(true, n, t)); } +inline expr mk_local(name const & n, expr const & t) { return expr(new expr_mlocal(false, n, t)); } inline expr mk_pair(expr const & f, expr const & s, expr const & t) { return expr(new expr_dep_pair(f, s, t)); } inline expr mk_fst(expr const & a) { return expr(new expr_proj(true, a)); } inline expr mk_snd(expr const & a) { return expr(new expr_proj(false, a)); } @@ -384,21 +385,23 @@ template expr mk_app(T const & args) { return mk_app(args.size(), ar inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Lambda, n, t, e)); } inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Pi, n, t, e)); } inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Sigma, n, t, e)); } -inline bool is_default_arrow_var_name(name const & n) { return n == "a"; } -inline expr mk_arrow(expr const & t, expr const & e) { return mk_pi(name("a"), t, e); } -inline expr mk_cartesian_product(expr const & t, expr const & e) { return mk_sigma(name("a"), t, e); } -inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); } inline expr mk_let(name const & n, optional const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); } inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return mk_let(n, some_expr(t), v, e); } inline expr mk_let(name const & n, expr const & v, expr const & e) { return mk_let(n, none_expr(), v, e); } inline expr mk_sort(level const & l) { return expr(new expr_sort(l)); } + expr mk_Bool(); expr mk_Type(); extern expr Type; extern expr Bool; +bool is_default_var_name(name const & n); +expr mk_arrow(expr const & t, expr const & e); +expr mk_cartesian_product(expr const & t, expr const & e); +inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); } + // Auxiliary inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); } inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); } @@ -438,9 +441,9 @@ inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); inline expr_binder * to_binder(expr_cell * e) { lean_assert(is_binder(e)); return static_cast(e); } inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast(e); } inline expr_sort * to_sort(expr_cell * e) { lean_assert(is_sort(e)); return static_cast(e); } -inline expr_meta_local * to_meta_local(expr_cell * e) { lean_assert(is_meta_local(e)); return static_cast(e); } -inline expr_meta_local * to_local(expr_cell * e) { lean_assert(is_local(e)); return static_cast(e); } -inline expr_meta_local * to_metavar(expr_cell * e) { lean_assert(is_metavar(e)); return static_cast(e); } +inline expr_mlocal * to_mlocal(expr_cell * e) { lean_assert(is_mlocal(e)); return static_cast(e); } +inline expr_mlocal * to_local(expr_cell * e) { lean_assert(is_local(e)); return static_cast(e); } +inline expr_mlocal * to_metavar(expr_cell * e) { lean_assert(is_metavar(e)); return static_cast(e); } inline expr_var * to_var(expr const & e) { return to_var(e.raw()); } inline expr_const * to_constant(expr const & e) { return to_constant(e.raw()); } @@ -450,88 +453,71 @@ inline expr_app * to_app(expr const & e) { return to_app(e.raw() inline expr_binder * to_binder(expr const & e) { return to_binder(e.raw()); } inline expr_let * to_let(expr const & e) { return to_let(e.raw()); } inline expr_sort * to_sort(expr const & e) { return to_sort(e.raw()); } -inline expr_meta_local * to_meta_local(expr const & e) { return to_meta_local(e.raw()); } -inline expr_meta_local * to_metavar(expr const & e) { return to_metavar(e.raw()); } -inline expr_meta_local * to_local(expr const & e) { return to_local(e.raw()); } +inline expr_mlocal * to_mlocal(expr const & e) { return to_mlocal(e.raw()); } +inline expr_mlocal * to_metavar(expr const & e) { return to_metavar(e.raw()); } +inline expr_mlocal * to_local(expr const & e) { return to_local(e.raw()); } // ======================================= -#if 0 - - // ======================================= // Accessors -inline unsigned get_rc(expr_cell * e) { return e->get_rc(); } -inline bool is_shared(expr_cell * e) { return get_rc(e) > 1; } -inline unsigned var_idx(expr_cell * e) { return to_var(e)->get_vidx(); } -inline bool is_var(expr_cell * e, unsigned i) { return is_var(e) && var_idx(e) == i; } -inline name const & const_name(expr_cell * e) { return to_constant(e)->get_name(); } -// Remark: the following function should not be exposed in the internal API. -inline optional const & const_type(expr_cell * e) { return to_constant(e)->get_type(); } -inline expr const & pair_first(expr_cell * e) { return to_pair(e)->get_first(); } -inline expr const & pair_second(expr_cell * e) { return to_pair(e)->get_second(); } -inline expr const & pair_type(expr_cell * e) { return to_pair(e)->get_type(); } -inline bool proj_first(expr_cell * e) { return to_proj(e)->first(); } -inline expr const & proj_arg(expr_cell * e) { return to_proj(e)->get_arg(); } -inline value const & to_value(expr_cell * e) { lean_assert(is_value(e)); return static_cast(e)->get_value(); } -inline unsigned num_args(expr_cell * e) { return to_app(e)->get_num_args(); } -inline expr const & arg(expr_cell * e, unsigned idx) { return to_app(e)->get_arg(idx); } -inline name const & abst_name(expr_cell * e) { return to_abstraction(e)->get_name(); } -inline expr const & abst_domain(expr_cell * e) { return to_abstraction(e)->get_domain(); } -inline expr const & abst_body(expr_cell * e) { return to_abstraction(e)->get_body(); } -inline level const & ty_level(expr_cell * e) { return to_type(e)->get_level(); } -inline name const & let_name(expr_cell * e) { return to_let(e)->get_name(); } -inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); } -inline optional const & let_type(expr_cell * e) { return to_let(e)->get_type(); } -inline expr const & let_body(expr_cell * e) { return to_let(e)->get_body(); } -inline expr const & heq_lhs(expr_cell * e) { return to_heq(e)->get_lhs(); } -inline expr const & heq_rhs(expr_cell * e) { return to_heq(e)->get_rhs(); } -inline name const & metavar_name(expr_cell * e) { return to_metavar(e)->get_name(); } -inline local_context const & metavar_lctx(expr_cell * e) { return to_metavar(e)->get_lctx(); } +inline unsigned get_rc(expr_cell * e) { return e->get_rc(); } +inline bool is_shared(expr_cell * e) { return get_rc(e) > 1; } +inline unsigned var_idx(expr_cell * e) { return to_var(e)->get_vidx(); } +inline bool is_var(expr_cell * e, unsigned i) { return is_var(e) && var_idx(e) == i; } +inline name const & const_name(expr_cell * e) { return to_constant(e)->get_name(); } +inline levels const & const_level_params(expr_cell * e) { return to_constant(e)->get_level_params(); } +inline expr const & pair_first(expr_cell * e) { return to_pair(e)->get_first(); } +inline expr const & pair_second(expr_cell * e) { return to_pair(e)->get_second(); } +inline expr const & pair_type(expr_cell * e) { return to_pair(e)->get_type(); } +inline expr const & proj_arg(expr_cell * e) { return to_proj(e)->get_arg(); } +inline macro const & to_macro(expr_cell * e) { + lean_assert(is_macro(e)); return static_cast(e)->get_macro(); } +inline expr const & app_fn(expr_cell * e) { return to_app(e)->get_fn(); } +inline expr const & app_arg(expr_cell * e) { return to_app(e)->get_arg(); } +inline name const & binder_name(expr_cell * e) { return to_binder(e)->get_name(); } +inline expr const & binder_domain(expr_cell * e) { return to_binder(e)->get_domain(); } +inline expr const & binder_body(expr_cell * e) { return to_binder(e)->get_body(); } +inline level const & sort_level(expr_cell * e) { return to_sort(e)->get_level(); } +inline name const & let_name(expr_cell * e) { return to_let(e)->get_name(); } +inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); } +inline optional const & let_type(expr_cell * e) { return to_let(e)->get_type(); } +inline expr const & let_body(expr_cell * e) { return to_let(e)->get_body(); } +inline name const & mlocal_name(expr_cell * e) { return to_mlocal(e)->get_name(); } +inline expr const & mlocal_type(expr_cell * e) { return to_mlocal(e)->get_type(); } -/** \brief Return the reference counter of the given expression. */ -inline unsigned get_rc(expr const & e) { return e.raw()->get_rc(); } -/** \brief Return true iff the reference counter of the given expression is greater than 1. */ -inline bool is_shared(expr const & e) { return get_rc(e) > 1; } -/** \brief Return the de Bruijn index of the given expression. \pre is_var(e) */ -inline unsigned var_idx(expr const & e) { return to_var(e)->get_vidx(); } -/** \brief Return true iff the given expression is a variable with de Bruijn index equal to \c i. */ -inline bool is_var(expr const & e, unsigned i) { return is_var(e) && var_idx(e) == i; } -inline name const & const_name(expr const & e) { return to_constant(e)->get_name(); } -// Remark: the following function should not be exposed in the internal API. -inline optional const & const_type(expr const & e) { return to_constant(e)->get_type(); } -/** \brief Return true iff the given expression is a constant with name \c n. */ -inline bool is_constant(expr const & e, name const & n) { - return is_constant(e) && const_name(e) == n; -} -inline value const & to_value(expr const & e) { return to_value(e.raw()); } -inline expr const & pair_first(expr const & e) { return to_pair(e)->get_first(); } -inline expr const & pair_second(expr const & e) { return to_pair(e)->get_second(); } -inline expr const & pair_type(expr const & e) { return to_pair(e)->get_type(); } -inline bool proj_first(expr const & e) { return to_proj(e)->first(); } -inline expr const & proj_arg(expr const & e) { return to_proj(e)->get_arg(); } -inline unsigned num_args(expr const & e) { return to_app(e)->get_num_args(); } -inline expr const & arg(expr const & e, unsigned idx) { return to_app(e)->get_arg(idx); } -inline expr const * begin_args(expr const & e) { return to_app(e)->begin_args(); } -inline expr const * end_args(expr const & e) { return to_app(e)->end_args(); } -inline name const & abst_name(expr const & e) { return to_abstraction(e)->get_name(); } -inline expr const & abst_domain(expr const & e) { return to_abstraction(e)->get_domain(); } -inline expr const & abst_body(expr const & e) { return to_abstraction(e)->get_body(); } -inline level const & ty_level(expr const & e) { return to_type(e)->get_level(); } -inline name const & let_name(expr const & e) { return to_let(e)->get_name(); } -inline optional const & let_type(expr const & e) { return to_let(e)->get_type(); } -inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); } -inline expr const & let_body(expr const & e) { return to_let(e)->get_body(); } -inline expr const & heq_lhs(expr const & e) { return to_heq(e)->get_lhs(); } -inline expr const & heq_rhs(expr const & e) { return to_heq(e)->get_rhs(); } -inline name const & metavar_name(expr const & e) { return to_metavar(e)->get_name(); } -inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)->get_lctx(); } -/** \brief Return the depth of the given expression */ -unsigned get_depth(expr const & e); +inline unsigned get_rc(expr const & e) { return e.raw()->get_rc(); } +inline bool is_shared(expr const & e) { return get_rc(e) > 1; } +inline unsigned var_idx(expr const & e) { return to_var(e)->get_vidx(); } +inline bool is_var(expr const & e, unsigned i) { return is_var(e) && var_idx(e) == i; } +inline name const & const_name(expr const & e) { return to_constant(e)->get_name(); } +inline levels const & const_level_params(expr const & e) { return to_constant(e)->get_level_params(); } +inline expr const & pair_first(expr const & e) { return to_pair(e)->get_first(); } +inline expr const & pair_second(expr const & e) { return to_pair(e)->get_second(); } +inline expr const & pair_type(expr const & e) { return to_pair(e)->get_type(); } +inline expr const & proj_arg(expr const & e) { return to_proj(e)->get_arg(); } +inline macro const & to_macro(expr const & e) { return to_macro(e.raw()); } +inline expr const & app_fn(expr const & e) { return to_app(e)->get_fn(); } +inline expr const & app_arg(expr const & e) { return to_app(e)->get_arg(); } +inline name const & binder_name(expr const & e) { return to_binder(e)->get_name(); } +inline expr const & binder_domain(expr const & e) { return to_binder(e)->get_domain(); } +inline expr const & binder_body(expr const & e) { return to_binder(e)->get_body(); } +inline level const & sort_level(expr const & e) { return to_sort(e)->get_level(); } +inline name const & let_name(expr const & e) { return to_let(e)->get_name(); } +inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); } +inline optional const & let_type(expr const & e) { return to_let(e)->get_type(); } +inline expr const & let_body(expr const & e) { return to_let(e)->get_body(); } +inline name const & mlocal_name(expr const & e) { return to_mlocal(e)->get_name(); } +inline expr const & mlocal_type(expr const & e) { return to_mlocal(e)->get_type(); } +inline bool is_constant(expr const & e, name const & n) { return is_constant(e) && const_name(e) == n; } inline bool has_metavar(expr const & e) { return e.has_metavar(); } +inline bool has_metavar(optional const & e) { return e && has_metavar(*e); } +unsigned get_depth(expr const & e); +inline unsigned get_depth(optional const & e) { return e ? get_depth(*e) : 0; } // ======================================= + // ======================================= // Expression+Offset typedef std::pair expr_offset; @@ -565,147 +551,22 @@ struct expr_cell_offset_hash { unsigned operator()(expr_cell_offset const & p) c struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, expr_cell_offset const & p2) const { return p1 == p2; } }; // ======================================= -// ======================================= -// Miscellaneous -/** - \brief Wrapper for iterating over application arguments. - - If \c n is an application, it allows us to write - - \code - for (expr const & arg : app_args(n)) { - ... do something with argument - } - \endcode -*/ -struct args { - expr const & m_app; - args(expr const & a):m_app(a) { lean_assert(is_app(a)); } - expr const * begin() const { return &arg(m_app, 0); } - expr const * end() const { return begin() + num_args(m_app); } -}; /** \brief Return a shallow copy of \c e */ expr copy(expr const & e); -// ======================================= + // ======================================= // Update -template expr update_app(expr const & e, F f) { - static_assert(std::is_same::type, expr>::value, - "update_app: return type of f is not expr"); - buffer new_args; - bool modified = false; - for (expr const & a : args(e)) { - new_args.push_back(f(a)); - if (!is_eqp(a, new_args.back())) - modified = true; - } - if (modified) - return mk_app(new_args.size(), new_args.data()); - else - return e; -} -template expr update_abst(expr const & e, F f) { - static_assert(std::is_same::type, - std::pair>::value, - "update_abst: return type of f is not pair"); - expr const & old_t = abst_domain(e); - expr const & old_b = abst_body(e); - std::pair p = f(old_t, old_b); - if (!is_eqp(p.first, old_t) || !is_eqp(p.second, old_b)) { - name const & n = abst_name(e); - switch (e.kind()) { - case expr_kind::Pi: return mk_pi(n, p.first, p.second); - case expr_kind::Lambda: return mk_lambda(n, p.first, p.second); - case expr_kind::Sigma: return mk_sigma(n, p.first, p.second); - default: lean_unreachable(); - } - } else { - return e; - } -} -template expr update_let(expr const & e, F f) { - static_assert(std::is_same const &, expr const &, expr const &)>::type, - std::tuple, expr, expr>>::value, - "update_let: return type of f is not tuple, expr, expr>"); - optional const & old_t = let_type(e); - expr const & old_v = let_value(e); - expr const & old_b = let_body(e); - std::tuple, expr, expr> r = f(old_t, old_v, old_b); - if (!is_eqp(std::get<0>(r), old_t) || !is_eqp(std::get<1>(r), old_v) || !is_eqp(std::get<2>(r), old_b)) - return mk_let(let_name(e), std::get<0>(r), std::get<1>(r), std::get<2>(r)); - else - return e; -} -template expr update_metavar(expr const & e, name const & n, F f) { - static_assert(std::is_same::type, local_entry>::value, - "update_metavar: return type of f(local_entry) is not local_entry"); - buffer new_entries; - bool modified = n != metavar_name(e); - for (local_entry const & me : metavar_lctx(e)) { - local_entry new_me = f(me); - if (new_me.kind() != me.kind() || new_me.s() != me.s()) { - modified = true; - } else if (new_me.is_inst()) { - if (!is_eqp(new_me.v(), me.v())) - modified = true; - } else if (new_me.n() != me.n()) { - modified = true; - } - new_entries.push_back(new_me); - } - if (modified) - return mk_metavar(n, to_list(new_entries.begin(), new_entries.end())); - else - return e; -} -template expr update_metavar(expr const & e, F f) { - static_assert(std::is_same::type, local_entry>::value, - "update_metavar: return type of f(local_entry) is not local_entry"); - return update_metavar(e, metavar_name(e), f); -} -inline expr update_metavar(expr const & e, local_context const & lctx) { - if (metavar_lctx(e) != lctx) - return mk_metavar(metavar_name(e), lctx); - else - return e; -} -inline expr update_const(expr const & e, optional const & t) { - if (!is_eqp(const_type(e), t)) - return mk_constant(const_name(e), t); - else - return e; -} -template expr update_pair(expr const & e, F f) { - expr const & old_f = pair_first(e); - expr const & old_s = pair_second(e); - expr const & old_t = pair_type(e); - auto r = f(old_f, old_s, old_t); - if (!is_eqp(std::get<0>(r), old_t) || !is_eqp(std::get<1>(r), old_s) || !is_eqp(std::get<2>(r), old_t)) - return mk_pair(std::get<0>(r), std::get<1>(r), std::get<2>(r)); - else - return e; -} -inline expr update_pair(expr const & e, expr const & new_f, expr const & new_s, expr const & new_t) { - return update_pair(e, [&](expr const &, expr const &, expr const &) { return std::make_tuple(new_f, new_s, new_t); }); -} -inline expr update_proj(expr const & e, expr const & new_arg) { - if (!is_eqp(proj_arg(e), new_arg)) - return mk_proj(proj_first(e), new_arg); - else - return e; -} -inline expr update_heq(expr const & e, expr const & new_lhs, expr const & new_rhs) { - if (!is_eqp(heq_lhs(e), new_lhs) || !is_eqp(heq_rhs(e), new_rhs)) - return mk_heq(new_lhs, new_rhs); - else - return e; -} +expr update_app(expr const & e, expr const & new_fn, expr const & new_arg); +expr update_proj(expr const & e, expr const & new_arg); +expr update_pair(expr const & e, expr const & new_first, expr const & new_second, expr const & new_type); +expr update_binder(expr const & e, expr const & new_domain, expr const & new_body); +expr update_let(expr const & e, optional const & new_type, expr const & new_val, expr const & new_body); +expr update_mlocal(expr const & e, expr const & new_type); // ======================================= - // ======================================= // Serializer/Deserializer serializer & operator<<(serializer & s, expr const & e); @@ -714,5 +575,4 @@ inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); // ======================================= std::ostream & operator<<(std::ostream & out, expr const & e); -#endif } diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h deleted file mode 100644 index 28fa25154..000000000 --- a/src/kernel/expr_eq.h +++ /dev/null @@ -1,102 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "util/interrupt.h" -#include "kernel/expr.h" -#include "kernel/expr_sets.h" - -namespace lean { -/** \brief Identity function for expressions. */ -struct id_expr_fn { - expr const & operator()(expr const & e) const { return e; } -}; - -/** - \brief Functional object for comparing expressions. - The parameter N is a normalization function that can be used - to normalize sub-expressions before comparing them. - The hashcode of expressions is used to optimize the comparison when - parameter UseHash == true. We should set UseHash to false when N - is not the identity function. -*/ -template -class expr_eq_fn { - std::unique_ptr m_eq_visited; - N m_norm; - - bool apply(optional const & a0, optional const & b0) { - if (is_eqp(a0, b0)) - return true; - else if (!a0 || !b0) - return false; - else - return apply(*a0, *b0); - } - - bool apply(expr const & a0, expr const & b0) { - check_system("expression equality test"); - if (is_eqp(a0, b0)) return true; - if (UseHash && a0.hash() != b0.hash()) return false; - expr const & a = m_norm(a0); - expr const & b = m_norm(b0); - if (a.kind() != b.kind()) return false; - if (is_var(a)) return var_idx(a) == var_idx(b); - if (is_shared(a) && is_shared(b)) { - auto p = std::make_pair(a.raw(), b.raw()); - if (!m_eq_visited) - m_eq_visited.reset(new expr_cell_pair_set); - if (m_eq_visited->find(p) != m_eq_visited->end()) - return true; - m_eq_visited->insert(p); - } - switch (a.kind()) { - case expr_kind::Var: lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Constant: return const_name(a) == const_name(b); - case expr_kind::App: - if (num_args(a) != num_args(b)) - return false; - for (unsigned i = 0; i < num_args(a); i++) - if (!apply(arg(a, i), arg(b, i))) - return false; - return true; - case expr_kind::HEq: return heq_lhs(a) == heq_lhs(b) && heq_rhs(a) == heq_rhs(b); - case expr_kind::Pair: return pair_first(a) == pair_first(b) && pair_second(a) == pair_second(b) && pair_type(a) == pair_type(b); - case expr_kind::Proj: return proj_first(a) == proj_first(b) && proj_arg(a) == proj_arg(b); - case expr_kind::Sigma: - case expr_kind::Lambda: // Remark: we ignore get_abs_name because we want alpha-equivalence - case expr_kind::Pi: return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b)); - case expr_kind::Type: return ty_level(a) == ty_level(b); - case expr_kind::Value: return to_value(a) == to_value(b); - case expr_kind::Let: return apply(let_type(a), let_type(b)) && apply(let_value(a), let_value(b)) && apply(let_body(a), let_body(b)); - case expr_kind::MetaVar: - return - metavar_name(a) == metavar_name(b) && - compare(metavar_lctx(a), metavar_lctx(b), [&](local_entry const & e1, local_entry const & e2) { - if (e1.kind() != e2.kind() || e1.s() != e2.s()) - return false; - if (e1.is_inst()) - return apply(e1.v(), e2.v()); - else - return e1.n() == e2.n(); - }); - } - lean_unreachable(); // LCOV_EXCL_LINE - } -public: - expr_eq_fn(N const & norm = N()):m_norm(norm) { - // the return type of N()(e) should be expr const & - static_assert(std::is_same())(expr const &)>::type, - expr const &>::value, - "The return type of CMP()(k1, k2) is not int."); - } - bool operator()(expr const & a, expr const & b) { - return apply(a, b); - } - void clear() { m_eq_visited.reset(); } -}; -} diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp new file mode 100644 index 000000000..153bd237e --- /dev/null +++ b/src/kernel/expr_eq_fn.cpp @@ -0,0 +1,71 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/expr_eq_fn.h" + +namespace lean { +bool expr_eq_fn::apply(optional const & a0, optional const & b0) { + if (is_eqp(a0, b0)) + return true; + else if (!a0 || !b0) + return false; + else + return apply(*a0, *b0); +} + +bool expr_eq_fn::apply(expr const & a, expr const & b) { + check_system("expression equality test"); + if (is_eqp(a, b)) return true; + if (a.hash() != b.hash()) return false; + if (a.kind() != b.kind()) return false; + if (is_var(a)) return var_idx(a) == var_idx(b); + if (is_shared(a) && is_shared(b)) { + auto p = std::make_pair(a.raw(), b.raw()); + if (!m_eq_visited) + m_eq_visited.reset(new expr_cell_pair_set); + if (m_eq_visited->find(p) != m_eq_visited->end()) + return true; + m_eq_visited->insert(p); + } + switch (a.kind()) { + case expr_kind::Var: + lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Constant: + return + const_name(a) == const_name(b) && + compare(const_level_params(a), const_level_params(b), [](level const & l1, level const & l2) { return l1 == l2; }); + case expr_kind::Local: case expr_kind::Meta: + return + mlocal_name(a) == mlocal_name(b) && + apply(mlocal_type(a), mlocal_type(b)); + case expr_kind::App: + return + apply(app_fn(a), app_fn(b)) && + apply(app_arg(a), app_arg(b)); + case expr_kind::Pair: + return + apply(pair_first(a), pair_first(b)) && + apply(pair_second(a), pair_second(b)) && + apply(pair_type(a), pair_type(b)); + case expr_kind::Fst: case expr_kind::Snd: + return apply(proj_arg(a), proj_arg(b)); + case expr_kind::Sigma: case expr_kind::Lambda: case expr_kind::Pi: + return + apply(binder_domain(a), binder_domain(b)) && + apply(binder_body(a), binder_body(b)); + case expr_kind::Sort: + return sort_level(a) == sort_level(b); + case expr_kind::Macro: + return to_macro(a) == to_macro(b); + case expr_kind::Let: + return + apply(let_type(a), let_type(b)) && + apply(let_value(a), let_value(b)) && + apply(let_body(a), let_body(b)); + } + lean_unreachable(); // LCOV_EXCL_LINE +} +} diff --git a/src/kernel/expr_eq_fn.h b/src/kernel/expr_eq_fn.h new file mode 100644 index 000000000..b96014495 --- /dev/null +++ b/src/kernel/expr_eq_fn.h @@ -0,0 +1,25 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "util/interrupt.h" +#include "kernel/expr.h" +#include "kernel/expr_sets.h" + +namespace lean { +/** + \brief Functional object for comparing expressions. +*/ +class expr_eq_fn { + std::unique_ptr m_eq_visited; + bool apply(optional const & a0, optional const & b0); + bool apply(expr const & a, expr const & b); +public: + bool operator()(expr const & a, expr const & b) { return apply(a, b); } + void clear() { m_eq_visited.reset(); } +}; +}