From 08b750c8253bb00edb3f4915137bcf1a2ce53826 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Jul 2013 19:49:34 -0700 Subject: [PATCH] Remove Prop from kernel Signed-off-by: Leonardo de Moura --- src/kernel/deep_copy.cpp | 2 +- src/kernel/expr.cpp | 5 ---- src/kernel/expr.h | 15 +----------- src/kernel/free_vars.cpp | 4 +-- src/kernel/max_sharing.cpp | 2 +- src/kernel/normalize.cpp | 2 +- src/kernel/replace.h | 2 +- src/tests/kernel/expr.cpp | 45 ++++++++++++++++++---------------- src/tests/kernel/normalize.cpp | 4 +-- 9 files changed, 33 insertions(+), 48 deletions(-) diff --git a/src/kernel/deep_copy.cpp b/src/kernel/deep_copy.cpp index 22e1b07cc6..2174fc64e1 100644 --- a/src/kernel/deep_copy.cpp +++ b/src/kernel/deep_copy.cpp @@ -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 new_args; diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 398851c9b1..fb7f8c4a54 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -97,7 +97,6 @@ void expr_cell::dealloc() { case expr_kind::App: static_cast(this)->~expr_app(); delete[] reinterpret_cast(this); break; case expr_kind::Lambda: delete static_cast(this); break; case expr_kind::Pi: delete static_cast(this); break; - case expr_kind::Prop: delete static_cast(this); break; case expr_kind::Type: delete static_cast(this); break; case expr_kind::Numeral: delete static_cast(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)); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index c5431c4878..832dfb4f99 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -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(e); } inline expr_lambda * to_lambda(expr_cell * e) { lean_assert(is_lambda(e)); return static_cast(e); } inline expr_pi * to_pi(expr_cell * e) { lean_assert(is_pi(e)); return static_cast(e); } -inline expr_prop * to_prop(expr_cell * e) { lean_assert(is_prop(e)); return static_cast(e); } inline expr_type * to_type(expr_cell * e) { lean_assert(is_type(e)); return static_cast(e); } inline expr_numeral * to_numeral(expr_cell * e) { lean_assert(is_numeral(e)); return static_cast(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()); } // ======================================= diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 05f2296671..ab3600a8c5 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -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: diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp index d9c03a52a0..c4d5c05855 100644 --- a/src/kernel/max_sharing.cpp +++ b/src/kernel/max_sharing.cpp @@ -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: { diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp index aab21de08c..9ca3d8f39a 100644 --- a/src/kernel/normalize.cpp +++ b/src/kernel/normalize.cpp @@ -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); diff --git a/src/kernel/replace.h b/src/kernel/replace.h index 7f31e57a69..9d699b2b0d 100644 --- a/src/kernel/replace.h +++ b/src/kernel/replace.h @@ -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 new_args; diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 42aef00195..7de3685be4 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -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)); diff --git a/src/tests/kernel/normalize.cpp b/src/tests/kernel/normalize.cpp index c77aeabd69..5c9904d5e3 100644 --- a/src/tests/kernel/normalize.cpp +++ b/src/tests/kernel/normalize.cpp @@ -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)));