Remove Prop from kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
6452c69b96
commit
08b750c825
9 changed files with 33 additions and 48 deletions
|
@ -21,7 +21,7 @@ class deep_copy_fn {
|
|||
}
|
||||
expr r;
|
||||
switch (a.kind()) {
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
|
||||
r = copy(a); break; // shallow copy is equivalent to deep copy for these ones.
|
||||
case expr_kind::App: {
|
||||
buffer<expr> new_args;
|
||||
|
|
|
@ -97,7 +97,6 @@ void expr_cell::dealloc() {
|
|||
case expr_kind::App: static_cast<expr_app*>(this)->~expr_app(); delete[] reinterpret_cast<char*>(this); break;
|
||||
case expr_kind::Lambda: delete static_cast<expr_lambda*>(this); break;
|
||||
case expr_kind::Pi: delete static_cast<expr_pi*>(this); break;
|
||||
case expr_kind::Prop: delete static_cast<expr_prop*>(this); break;
|
||||
case expr_kind::Type: delete static_cast<expr_type*>(this); break;
|
||||
case expr_kind::Numeral: delete static_cast<expr_numeral*>(this); break;
|
||||
}
|
||||
|
@ -111,7 +110,6 @@ class eq_fn {
|
|||
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_prop(a)) return true;
|
||||
if (is_shared(a) && is_shared(b)) {
|
||||
auto p = std::make_pair(a.raw(), b.raw());
|
||||
if (m_eq_visited.find(p) != m_eq_visited.end())
|
||||
|
@ -133,7 +131,6 @@ class eq_fn {
|
|||
// Lambda and Pi
|
||||
// Remark: we ignore get_abs_name because we want alpha-equivalence
|
||||
return apply(abst_type(a), abst_type(b)) && apply(abst_body(a), abst_body(b));
|
||||
case expr_kind::Prop: lean_unreachable(); return true;
|
||||
case expr_kind::Type: return ty_level(a) == ty_level(b);
|
||||
case expr_kind::Numeral: return num_value(a) == num_value(b);
|
||||
}
|
||||
|
@ -165,7 +162,6 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
|
|||
break;
|
||||
case expr_kind::Lambda: out << "(fun (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")"; break;
|
||||
case expr_kind::Pi: out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")"; break;
|
||||
case expr_kind::Prop: out << "Prop"; break;
|
||||
case expr_kind::Type: out << "(Type " << ty_level(a) << ")"; break;
|
||||
case expr_kind::Numeral: out << num_value(a); break;
|
||||
}
|
||||
|
@ -176,7 +172,6 @@ expr copy(expr const & a) {
|
|||
switch (a.kind()) {
|
||||
case expr_kind::Var: return var(var_idx(a));
|
||||
case expr_kind::Constant: return constant(const_name(a), const_pos(a));
|
||||
case expr_kind::Prop: return prop();
|
||||
case expr_kind::Type: return type(ty_level(a));
|
||||
case expr_kind::Numeral: return numeral(num_value(a));
|
||||
case expr_kind::App: return app(num_args(a), begin_args(a));
|
||||
|
|
|
@ -21,7 +21,6 @@ namespace lean {
|
|||
| App [expr]
|
||||
| Lambda name expr expr
|
||||
| Pi name expr expr
|
||||
| Prop
|
||||
| Type universe
|
||||
| Numeral value
|
||||
|
||||
|
@ -33,7 +32,7 @@ The main API is divided in the following sections
|
|||
- Accessors
|
||||
- Miscellaneous
|
||||
======================================= */
|
||||
enum class expr_kind { Var, Constant, App, Lambda, Pi, Prop, Type, Numeral };
|
||||
enum class expr_kind { Var, Constant, App, Lambda, Pi, Type, Numeral };
|
||||
|
||||
/**
|
||||
\brief Base class used to represent expressions.
|
||||
|
@ -171,11 +170,6 @@ class expr_pi : public expr_abstraction {
|
|||
public:
|
||||
expr_pi(name const & n, expr const & t, expr const & e);
|
||||
};
|
||||
/** \brief Propositions */
|
||||
class expr_prop : public expr_cell {
|
||||
public:
|
||||
expr_prop():expr_cell(expr_kind::Prop, 17) {}
|
||||
};
|
||||
/** \brief Type */
|
||||
class expr_type : public expr_cell {
|
||||
level m_level;
|
||||
|
@ -200,11 +194,9 @@ inline bool is_constant(expr_cell * e) { return e->kind() == expr_kind::Const
|
|||
inline bool is_app(expr_cell * e) { return e->kind() == expr_kind::App; }
|
||||
inline bool is_lambda(expr_cell * e) { return e->kind() == expr_kind::Lambda; }
|
||||
inline bool is_pi(expr_cell * e) { return e->kind() == expr_kind::Pi; }
|
||||
inline bool is_prop(expr_cell * e) { return e->kind() == expr_kind::Prop; }
|
||||
inline bool is_type(expr_cell * e) { return e->kind() == expr_kind::Type; }
|
||||
inline bool is_numeral(expr_cell * e) { return e->kind() == expr_kind::Numeral; }
|
||||
inline bool is_abstraction(expr_cell * e) { return is_lambda(e) || is_pi(e); }
|
||||
inline bool is_sort(expr_cell * e) { return is_prop(e) || is_type(e); }
|
||||
|
||||
inline bool is_null(expr const & e) { return e.raw() == nullptr; }
|
||||
inline bool is_var(expr const & e) { return e.kind() == expr_kind::Var; }
|
||||
|
@ -212,11 +204,9 @@ inline bool is_constant(expr const & e) { return e.kind() == expr_kind::Const
|
|||
inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; }
|
||||
inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; }
|
||||
inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; }
|
||||
inline bool is_prop(expr const & e) { return e.kind() == expr_kind::Prop; }
|
||||
inline bool is_type(expr const & e) { return e.kind() == expr_kind::Type; }
|
||||
inline bool is_numeral(expr const & e) { return e.kind() == expr_kind::Numeral; }
|
||||
inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
|
||||
inline bool is_sort(expr const & e) { return is_prop(e) || is_type(e); }
|
||||
// =======================================
|
||||
|
||||
// =======================================
|
||||
|
@ -234,7 +224,6 @@ inline expr lambda(name const & n, expr const & t, expr const & e) { return expr
|
|||
inline expr lambda(char const * n, expr const & t, expr const & e) { return lambda(name(n), t, e); }
|
||||
inline expr pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
|
||||
inline expr pi(char const * n, expr const & t, expr const & e) { return pi(name(n), t, e); }
|
||||
inline expr prop() { return expr(new expr_prop()); }
|
||||
inline expr type(level const & l) { return expr(new expr_type(l)); }
|
||||
inline expr numeral(mpz const & n) { return expr(new expr_numeral(n)); }
|
||||
inline expr numeral(int n) { return numeral(mpz(n)); }
|
||||
|
@ -253,7 +242,6 @@ inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e))
|
|||
inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstraction(e)); return static_cast<expr_abstraction*>(e); }
|
||||
inline expr_lambda * to_lambda(expr_cell * e) { lean_assert(is_lambda(e)); return static_cast<expr_lambda*>(e); }
|
||||
inline expr_pi * to_pi(expr_cell * e) { lean_assert(is_pi(e)); return static_cast<expr_pi*>(e); }
|
||||
inline expr_prop * to_prop(expr_cell * e) { lean_assert(is_prop(e)); return static_cast<expr_prop*>(e); }
|
||||
inline expr_type * to_type(expr_cell * e) { lean_assert(is_type(e)); return static_cast<expr_type*>(e); }
|
||||
inline expr_numeral * to_numeral(expr_cell * e) { lean_assert(is_numeral(e)); return static_cast<expr_numeral*>(e); }
|
||||
|
||||
|
@ -263,7 +251,6 @@ inline expr_app * to_app(expr const & e) { return to_app(e.raw()
|
|||
inline expr_abstraction * to_abstraction(expr const & e) { return to_abstraction(e.raw()); }
|
||||
inline expr_lambda * to_lambda(expr const & e) { return to_lambda(e.raw()); }
|
||||
inline expr_pi * to_pi(expr const & e) { return to_pi(e.raw()); }
|
||||
inline expr_prop * to_prop(expr const & e) { return to_prop(e.raw()); }
|
||||
inline expr_type * to_type(expr const & e) { return to_type(e.raw()); }
|
||||
inline expr_numeral * to_numeral(expr const & e) { return to_numeral(e.raw()); }
|
||||
// =======================================
|
||||
|
|
|
@ -23,7 +23,7 @@ protected:
|
|||
bool apply(expr const & e, unsigned offset) {
|
||||
// handle easy cases
|
||||
switch (e.kind()) {
|
||||
case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
|
||||
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
|
||||
return false;
|
||||
case expr_kind::Var:
|
||||
return process_var(e, offset);
|
||||
|
@ -44,7 +44,7 @@ protected:
|
|||
bool result = false;
|
||||
|
||||
switch (e.kind()) {
|
||||
case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Var:
|
||||
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Var:
|
||||
// easy cases were already handled
|
||||
lean_unreachable(); return false;
|
||||
case expr_kind::App:
|
||||
|
|
|
@ -32,7 +32,7 @@ struct max_sharing_fn::imp {
|
|||
return a;
|
||||
}
|
||||
switch (a.kind()) {
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
|
||||
cache(a);
|
||||
return a;
|
||||
case expr_kind::App: {
|
||||
|
|
|
@ -101,7 +101,7 @@ value normalize(expr const & a, context const & c, unsigned k) {
|
|||
switch (a.kind()) {
|
||||
case expr_kind::Var:
|
||||
return lookup(c, var_idx(a));
|
||||
case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
|
||||
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
|
||||
return value(a);
|
||||
case expr_kind::App: {
|
||||
value f = normalize(arg(a, 0), c, k);
|
||||
|
|
|
@ -35,7 +35,7 @@ class replace_fn {
|
|||
expr r = m_f(e, offset);
|
||||
if (eqp(e, r)) {
|
||||
switch (e.kind()) {
|
||||
case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Constant: case expr_kind::Var:
|
||||
case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Constant: case expr_kind::Var:
|
||||
break;
|
||||
case expr_kind::App: {
|
||||
buffer<expr> new_args;
|
||||
|
|
|
@ -21,6 +21,7 @@ void tst1() {
|
|||
expr f;
|
||||
f = var(0);
|
||||
expr fa = f(a);
|
||||
expr ty = type(level());
|
||||
std::cout << fa << "\n";
|
||||
std::cout << fa(a) << "\n";
|
||||
lean_assert(eqp(arg(fa, 0), f));
|
||||
|
@ -28,11 +29,11 @@ void tst1() {
|
|||
lean_assert(!eqp(fa, f(a)));
|
||||
lean_assert(app(fa, a) == f(a, a));
|
||||
std::cout << fa(fa, fa) << "\n";
|
||||
std::cout << lambda("x", prop(), var(0)) << "\n";
|
||||
std::cout << lambda("x", ty, var(0)) << "\n";
|
||||
lean_assert(f(a)(a) == f(a, a));
|
||||
lean_assert(f(a(a)) != f(a, a));
|
||||
lean_assert(lambda("x", prop(), var(0)) == lambda("y", prop(), var(0)));
|
||||
std::cout << pi("x", prop(), var(0)) << "\n";
|
||||
lean_assert(lambda("x", ty, var(0)) == lambda("y", ty, var(0)));
|
||||
std::cout << pi("x", ty, var(0)) << "\n";
|
||||
}
|
||||
|
||||
expr mk_dag(unsigned depth, bool _closed = false) {
|
||||
|
@ -47,7 +48,7 @@ expr mk_dag(unsigned depth, bool _closed = false) {
|
|||
|
||||
unsigned depth1(expr const & e) {
|
||||
switch (e.kind()) {
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
|
||||
return 1;
|
||||
case expr_kind::App: {
|
||||
unsigned m = 0;
|
||||
|
@ -64,7 +65,7 @@ unsigned depth1(expr const & e) {
|
|||
// This is the fastest depth implementation in this file.
|
||||
unsigned depth2(expr const & e) {
|
||||
switch (e.kind()) {
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
|
||||
return 1;
|
||||
case expr_kind::App:
|
||||
return
|
||||
|
@ -88,7 +89,7 @@ unsigned depth3(expr const & e) {
|
|||
unsigned c = p.second + 1;
|
||||
todo.pop_back();
|
||||
switch (e.kind()) {
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
|
||||
m = std::max(c, m);
|
||||
break;
|
||||
case expr_kind::App: {
|
||||
|
@ -149,7 +150,7 @@ unsigned count_core(expr const & a, expr_set & s) {
|
|||
return 0;
|
||||
s.insert(a);
|
||||
switch (a.kind()) {
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
|
||||
return 1;
|
||||
case expr_kind::App:
|
||||
return std::accumulate(begin_args(a), end_args(a), 1,
|
||||
|
@ -208,7 +209,7 @@ void tst8() {
|
|||
expr x = var(0);
|
||||
expr a = constant("a");
|
||||
expr n = numeral(mpz(10));
|
||||
expr p = prop();
|
||||
expr p = type(level());
|
||||
expr y = var(1);
|
||||
lean_assert(closed(a));
|
||||
lean_assert(!closed(x));
|
||||
|
@ -265,18 +266,19 @@ void tst11() {
|
|||
expr b = constant("b");
|
||||
expr x = var(0);
|
||||
expr y = var(1);
|
||||
std::cout << instantiate(f(a), lambda("x", prop(), f(f(y, b), f(x, y)))) << "\n";
|
||||
lean_assert(instantiate(f(a), lambda("x", prop(), f(f(y, b), f(x, y)))) ==
|
||||
lambda("x", prop(), f(f(f(a), b), f(x, f(a)))));
|
||||
std::cout << abstract(constant("a"), lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) << "\n";
|
||||
lean_assert(abstract(constant("a"), lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) ==
|
||||
lambda("x", prop(), f(var(1), lambda("y", prop(), f(b, var(2))))));
|
||||
std::cout << abstract_p(constant("a"), lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) << "\n";
|
||||
lean_assert(abstract_p(constant("a"), lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) ==
|
||||
lambda("x", prop(), f(a, lambda("y", prop(), f(b, a)))));
|
||||
std::cout << abstract_p(a, lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) << "\n";
|
||||
lean_assert(abstract_p(a, lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) ==
|
||||
lambda("x", prop(), f(var(1), lambda("y", prop(), f(b, var(2))))));
|
||||
expr t = type(level());
|
||||
std::cout << instantiate(f(a), lambda("x", t, f(f(y, b), f(x, y)))) << "\n";
|
||||
lean_assert(instantiate(f(a), lambda("x", t, f(f(y, b), f(x, y)))) ==
|
||||
lambda("x", t, f(f(f(a), b), f(x, f(a)))));
|
||||
std::cout << abstract(constant("a"), lambda("x", t, f(a, lambda("y", t, f(b, a))))) << "\n";
|
||||
lean_assert(abstract(constant("a"), lambda("x", t, f(a, lambda("y", t, f(b, a))))) ==
|
||||
lambda("x", t, f(var(1), lambda("y", t, f(b, var(2))))));
|
||||
std::cout << abstract_p(constant("a"), lambda("x", t, f(a, lambda("y", t, f(b, a))))) << "\n";
|
||||
lean_assert(abstract_p(constant("a"), lambda("x", t, f(a, lambda("y", t, f(b, a))))) ==
|
||||
lambda("x", t, f(a, lambda("y", t, f(b, a)))));
|
||||
std::cout << abstract_p(a, lambda("x", t, f(a, lambda("y", t, f(b, a))))) << "\n";
|
||||
lean_assert(abstract_p(a, lambda("x", t, f(a, lambda("y", t, f(b, a))))) ==
|
||||
lambda("x", t, f(var(1), lambda("y", t, f(b, var(2))))));
|
||||
|
||||
lean_assert(substitute(f(a), b, f(f(f(a)))) == f(f(b)));
|
||||
}
|
||||
|
@ -285,7 +287,8 @@ void tst12() {
|
|||
expr f = constant("f");
|
||||
expr a = constant("a");
|
||||
expr x = var(0);
|
||||
expr F = pi("y", prop(), lambda("x", prop(), f(f(f(x,a),numeral(10)),x)));
|
||||
expr t = type(level());
|
||||
expr F = pi("y", t, lambda("x", t, f(f(f(x,a),numeral(10)),x)));
|
||||
expr G = deep_copy(F);
|
||||
lean_assert(F == G);
|
||||
lean_assert(!eqp(F, G));
|
||||
|
|
|
@ -53,7 +53,7 @@ unsigned count_core(expr const & a, expr_set & s) {
|
|||
return 0;
|
||||
s.insert(a);
|
||||
switch (a.kind()) {
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
|
||||
return 1;
|
||||
case expr_kind::App:
|
||||
return std::accumulate(begin_args(a), end_args(a), 1,
|
||||
|
@ -102,7 +102,7 @@ static void tst1() {
|
|||
expr b = constant("b");
|
||||
expr x = var(0);
|
||||
expr y = var(1);
|
||||
expr t = prop();
|
||||
expr t = type(level());
|
||||
eval(app(lambda("x", t, x), a));
|
||||
eval(app(lambda("x", t, x), a, b));
|
||||
eval(lambda("x", t, f(x)));
|
||||
|
|
Loading…
Reference in a new issue