michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel/expr): add expr constructors, and expression equality test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-16 09:53:55 -08:00
parent 9d3db8de1f
commit 23988f528c
6 changed files with 306 additions and 495 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/CMakeLists.txt
View file

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

285
src/kernel/expr.cpp
View file

@ -9,35 +9,33 @@ Author: Leonardo de Moura
#include <sstream>
#include <string>
#include <algorithm>
#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<expr> 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<expr_cell*> & todelete) {
void expr_mlocal::dealloc(buffer<expr_cell*> & 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<expr_cell*> & 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<expr_cell*> & todelete) {
dec_ref(m_first, todelete);
@ -129,100 +128,54 @@ void expr_dep_pair::dealloc(buffer<expr_cell*> & 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<expr_cell*> & 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<expr_cell*> & todelete) {
unsigned i = m_num_args;
while (i > 0) {
--i;
dec_ref(m_args[i], todelete);
}
delete[] reinterpret_cast<char*>(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<expr_cell*> & todelete) {
void expr_binder::dealloc(buffer<expr_cell*> & 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<expr> 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<expr_cell*> & todelete) {
dec_ref(m_body, todelete);
@ -232,55 +185,49 @@ void expr_let::dealloc(buffer<expr_cell*> & todelete) {
}
expr_let::~expr_let() {}
// Expr Semantic attachment
name value::get_unicode_name() const { return get_name(); }
optional<expr> 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<std::string, value::reader> value_readers;
static std::unique_ptr<value_readers> 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<std::string, macro::reader> macro_readers;
static std::unique_ptr<macro_readers> 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<expr_var*>(it); break;
case expr_kind::Value: delete static_cast<expr_value*>(it); break;
case expr_kind::MetaVar: delete static_cast<expr_metavar*>(it); break;
case expr_kind::Type: delete static_cast<expr_type*>(it); break;
case expr_kind::Constant: static_cast<expr_const*>(it)->dealloc(todo); break;
case expr_kind::Macro: delete static_cast<expr_macro*>(it); break;
case expr_kind::Meta:
case expr_kind::Local: static_cast<expr_mlocal*>(it)->dealloc(todo); break;
case expr_kind::Constant: delete static_cast<expr_const*>(it); break;
case expr_kind::Sort: delete static_cast<expr_sort*>(it); break;
case expr_kind::Pair: static_cast<expr_dep_pair*>(it)->dealloc(todo); break;
case expr_kind::Proj: static_cast<expr_proj*>(it)->dealloc(todo); break;
case expr_kind::Fst:
case expr_kind::Snd: static_cast<expr_proj*>(it)->dealloc(todo); break;
case expr_kind::App: static_cast<expr_app*>(it)->dealloc(todo); break;
case expr_kind::Lambda: static_cast<expr_lambda*>(it)->dealloc(todo); break;
case expr_kind::Pi: static_cast<expr_pi*>(it)->dealloc(todo); break;
case expr_kind::Sigma: static_cast<expr_sigma*>(it)->dealloc(todo); break;
case expr_kind::HEq: static_cast<expr_heq*>(it)->dealloc(todo); break;
case expr_kind::Lambda:
case expr_kind::Pi:
case expr_kind::Sigma: static_cast<expr_binder*>(it)->dealloc(todo); break;
case expr_kind::Let: static_cast<expr_let*>(it)->dealloc(todo); break;
}
}
@ -312,14 +260,43 @@ 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<expr_composite*>(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<bool> r = t.raw()->is_arrow();
@ -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()) {

264
src/kernel/expr.h
View file

@ -25,6 +25,7 @@ Author: Leonardo de Moura
namespace lean {
class expr;
typedef list<level> 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<level> 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);
@ -174,21 +175,21 @@ public:
/** \brief (parametric) Constants. */
class expr_const : public expr_cell {
name m_name;
list<level> m_levels;
friend class expr_cell;
void dealloc(buffer<expr_cell*> & to_delete);
levels m_levels;
public:
expr_const(name const & n, list<level> const & ls);
expr_const(name const & n, levels const & ls);
name const & get_name() const { return m_name; }
list<level> 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<expr_cell*> & 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<expr_cell*> & 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<level> const & ls) { return expr(new expr_const(n, ls)); }
inline expr mk_constant(name const & n) { return mk_constant(n, list<level>()); }
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<typename T> 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<expr> 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<expr_binder*>(e); }
inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast<expr_let*>(e); }
inline expr_sort * to_sort(expr_cell * e) { lean_assert(is_sort(e)); return static_cast<expr_sort*>(e); }
inline expr_meta_local * to_meta_local(expr_cell * e) { lean_assert(is_meta_local(e)); return static_cast<expr_meta_local*>(e); }
inline expr_meta_local * to_local(expr_cell * e) { lean_assert(is_local(e)); return static_cast<expr_meta_local*>(e); }
inline expr_meta_local * to_metavar(expr_cell * e) { lean_assert(is_metavar(e)); return static_cast<expr_meta_local*>(e); }
inline expr_mlocal * to_mlocal(expr_cell * e) { lean_assert(is_mlocal(e)); return static_cast<expr_mlocal*>(e); }
inline expr_mlocal * to_local(expr_cell * e) { lean_assert(is_local(e)); return static_cast<expr_mlocal*>(e); }
inline expr_mlocal * to_metavar(expr_cell * e) { lean_assert(is_metavar(e)); return static_cast<expr_mlocal*>(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,15 +453,12 @@ 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(); }
@ -466,72 +466,58 @@ 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<expr> const & const_type(expr_cell * e) { return to_constant(e)->get_type(); }
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 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<expr_value*>(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 macro const & to_macro(expr_cell * e) {
lean_assert(is_macro(e)); return static_cast<expr_macro*>(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<expr> 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 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<expr> 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 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 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 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 optional<expr> 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 optional<expr> 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 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 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<expr> const & e) { return e && has_metavar(*e); }
unsigned get_depth(expr const & e);
inline unsigned get_depth(optional<expr> const & e) { return e ? get_depth(*e) : 0; }
// =======================================
// =======================================
// Expression+Offset
typedef std::pair<expr, unsigned> 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<typename F> expr update_app(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(expr const &)>::type, expr>::value,
"update_app: return type of f is not expr");
buffer<expr> 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<typename F> expr update_abst(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(expr const &, expr const &)>::type,
std::pair<expr, expr>>::value,
"update_abst: return type of f is not pair<expr, expr>");
expr const & old_t = abst_domain(e);
expr const & old_b = abst_body(e);
std::pair<expr, expr> 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<typename F> expr update_let(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(optional<expr> const &, expr const &, expr const &)>::type,
std::tuple<optional<expr>, expr, expr>>::value,
"update_let: return type of f is not tuple<optional<expr>, expr, expr>");
optional<expr> const & old_t = let_type(e);
expr const & old_v = let_value(e);
expr const & old_b = let_body(e);
std::tuple<optional<expr>, 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<typename F> expr update_metavar(expr const & e, name const & n, F f) {
static_assert(std::is_same<typename std::result_of<F(local_entry const &)>::type, local_entry>::value,
"update_metavar: return type of f(local_entry) is not local_entry");
buffer<local_entry> 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<typename F> expr update_metavar(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(local_entry const &)>::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<expr> const & t) {
if (!is_eqp(const_type(e), t))
return mk_constant(const_name(e), t);
else
return e;
}
template<typename F> 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<expr> 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
}

102
src/kernel/expr_eq.h
View file

@ -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 <memory>
#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<typename N = id_expr_fn, bool UseHash = true>
class expr_eq_fn {
std::unique_ptr<expr_cell_pair_set> m_eq_visited;
N m_norm;
bool apply(optional<expr> const & a0, optional<expr> 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<typename std::result_of<decltype(std::declval<N>())(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(); }
};
}

71
src/kernel/expr_eq_fn.cpp Normal file
View file

@ -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<expr> const & a0, optional<expr> 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
}
}

25
src/kernel/expr_eq_fn.h Normal file
View file

@ -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 <memory>
#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<expr_cell_pair_set> m_eq_visited;
bool apply(optional<expr> const & a0, optional<expr> 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(); }
};
}