From 0a679074f0f6bb2abc2af9662e6676dd273b8fb5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 3 Aug 2013 16:09:21 -0700 Subject: [PATCH] Add support for semantic attachments. Remove expr_numeral Signed-off-by: Leonardo de Moura --- src/kernel/deep_copy.cpp | 2 +- src/kernel/expr.cpp | 31 ++++++++------ src/kernel/expr.h | 74 ++++++++++++++++++++-------------- src/kernel/free_vars.cpp | 4 +- src/kernel/max_sharing.cpp | 2 +- src/kernel/normalize.cpp | 36 ++++++++--------- src/kernel/replace.h | 2 +- src/kernel/type_check.cpp | 5 +-- src/tests/kernel/expr.cpp | 16 ++++---- src/tests/kernel/normalize.cpp | 2 +- 10 files changed, 96 insertions(+), 78 deletions(-) diff --git a/src/kernel/deep_copy.cpp b/src/kernel/deep_copy.cpp index 32459dcd3..dcc116452 100644 --- a/src/kernel/deep_copy.cpp +++ b/src/kernel/deep_copy.cpp @@ -23,7 +23,7 @@ class deep_copy_fn { } expr r; switch (a.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral: + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: 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 d3c35d707..ee7e78571 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -29,10 +29,9 @@ expr_var::expr_var(unsigned idx): expr_cell(expr_kind::Var, idx), m_vidx(idx) {} -expr_const::expr_const(name const & n, unsigned pos): +expr_const::expr_const(name const & n): expr_cell(expr_kind::Constant, n.hash()), - m_name(n), - m_pos(pos) {} + m_name(n) {} expr_app::expr_app(unsigned num_args): expr_cell(expr_kind::App, 0), @@ -90,9 +89,15 @@ expr_type::expr_type(level const & l): } expr_type::~expr_type() { } -expr_numeral::expr_numeral(mpz const & n): - expr_cell(expr_kind::Numeral, n.hash()), - m_numeral(n) {} + +expr_value::expr_value(value & v): + expr_cell(expr_kind::Value, v.hash()), + m_val(v) { + m_val.inc_ref(); +} +expr_value::~expr_value() { + m_val.dec_ref(); +} void expr_cell::dealloc() { switch (kind()) { @@ -102,7 +107,7 @@ void expr_cell::dealloc() { case expr_kind::Lambda: delete static_cast(this); break; case expr_kind::Pi: delete static_cast(this); break; case expr_kind::Type: delete static_cast(this); break; - case expr_kind::Numeral: delete static_cast(this); break; + case expr_kind::Value: delete static_cast(this); break; } } @@ -136,7 +141,7 @@ class eq_fn { // Remark: we ignore get_abs_name because we want alpha-equivalence 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::Numeral: return num_value(a) == num_value(b); + case expr_kind::Value: return to_value(a) == to_value(b); } lean_unreachable(); return false; @@ -185,7 +190,7 @@ std::ostream & operator<<(std::ostream & out, expr const & a) { out << "(Type " << ty_level(a) << ")"; break; } - case expr_kind::Numeral: out << num_value(a); break; + case expr_kind::Value: to_value(a).display(out); break; } return out; } @@ -193,9 +198,9 @@ std::ostream & operator<<(std::ostream & out, expr const & a) { 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::Constant: return constant(const_name(a)); case expr_kind::Type: return type(ty_level(a)); - case expr_kind::Numeral: return numeral(num_value(a)); + case expr_kind::Value: return to_expr(static_cast(a.raw())->m_val); case expr_kind::App: return app(num_args(a), begin_args(a)); case expr_kind::Lambda: return lambda(abst_name(a), abst_domain(a), abst_body(a)); case expr_kind::Pi: return pi(abst_name(a), abst_domain(a), abst_body(a)); @@ -212,6 +217,8 @@ lean::format pp_aux(lean::expr const & a) { return format{format("#"), format(static_cast(var_idx(a)))}; case expr_kind::Constant: return format(const_name(a)); + case expr_kind::Value: + return to_value(a).pp(); case expr_kind::App: { format r; @@ -247,8 +254,6 @@ lean::format pp_aux(lean::expr const & a) { return paren(format{format("Type "), format(ss.str())}); } - case expr_kind::Numeral: - return format(num_value(a)); } lean_unreachable(); return format(); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 2fe847d76..5d450b33b 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -9,21 +9,22 @@ Author: Leonardo de Moura #include #include "rc.h" #include "name.h" -#include "mpz.h" #include "level.h" #include "hash.h" #include "buffer.h" +#include "format.h" namespace lean { +class value; /* ======================================= Expressions - expr ::= Var idx - | Constant name - | App [expr] - | Lambda name expr expr - | Pi name expr expr - | Type universe - | Numeral value + expr ::= Var idx + | Constant name + | Value value + | App [expr] + | Lambda name expr expr + | Pi name expr expr + | Type universe TODO: add meta-variables, let, constructor references and match. @@ -33,7 +34,7 @@ The main API is divided in the following sections - Accessors - Miscellaneous ======================================= */ -enum class expr_kind { Var, Constant, App, Lambda, Pi, Type, Numeral }; +enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type }; /** \brief Base class used to represent expressions. @@ -92,14 +93,13 @@ public: friend expr var(unsigned idx); friend expr constant(name const & n); - friend expr constant(name const & n, unsigned pos); + friend expr to_expr(value & v); friend expr app(unsigned num_args, expr const * args); friend expr app(std::initializer_list const & l); friend expr lambda(name const & n, expr const & t, expr const & e); friend expr pi(name const & n, expr const & t, expr const & e); friend expr prop(); friend expr type(level const & l); - friend expr numeral(mpz const & n); friend bool eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } @@ -122,11 +122,9 @@ public: /** \brief Constants. */ class expr_const : public expr_cell { name m_name; - unsigned m_pos; // position in the environment. public: - expr_const(name const & n, unsigned pos = std::numeric_limits::max()); + expr_const(name const & n); name const & get_name() const { return m_name; } - unsigned get_pos() const { return m_pos; } }; /** \brief Function Applications */ class expr_app : public expr_cell { @@ -170,33 +168,55 @@ public: ~expr_type(); level const & get_level() const { return m_level; } }; -/** \brief Numerals (efficient encoding using GMP numbers) */ -class expr_numeral : public expr_cell { - mpz m_numeral; +/** + \brief Base class for semantic attachment cells. +*/ +class value { + void dealloc() { delete this; } + MK_LEAN_RC(); public: - expr_numeral(mpz const & n); - mpz const & get_num() const { return m_numeral; } + value():m_rc(0) {} + virtual ~value() {} + virtual char const * kind() const = 0; + virtual expr get_type() const = 0; + virtual expr normalize(unsigned num_args, expr const * args) const = 0; + virtual bool operator==(value const & other) const = 0; + virtual void display(std::ostream & out) const = 0; + virtual format pp() const = 0; + virtual unsigned hash() const = 0; +}; + +/** \brief Semantic attachments */ +class expr_value : public expr_cell { + value & m_val; + friend expr copy(expr const & a); +public: + expr_value(value & v); + ~expr_value(); + + value const & get_value() const { return m_val; } }; // ======================================= + // ======================================= // Testers inline bool is_var(expr_cell * e) { return e->kind() == expr_kind::Var; } inline bool is_constant(expr_cell * e) { return e->kind() == expr_kind::Constant; } +inline bool is_value(expr_cell * e) { return e->kind() == expr_kind::Value; } 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_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_var(expr const & e) { return e.kind() == expr_kind::Var; } inline bool is_constant(expr const & e) { return e.kind() == expr_kind::Constant; } +inline bool is_value(expr const & e) { return e.kind() == expr_kind::Value; } 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_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); } // ======================================= @@ -205,7 +225,7 @@ inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); } inline expr var(unsigned idx) { return expr(new expr_var(idx)); } inline expr constant(name const & n) { return expr(new expr_const(n)); } inline expr constant(char const * n) { return constant(name(n)); } -inline expr constant(name const & n, unsigned pos) { return expr(new expr_const(n, pos)); } +inline expr to_expr(value & v) { return expr(new expr_value(v)); } expr app(unsigned num_args, expr const * args); inline expr app(expr const & e1, expr const & e2) { expr args[2] = {e1, e2}; return app(2, args); } inline expr app(expr const & e1, expr const & e2, expr const & e3) { expr args[3] = {e1, e2, e3}; return app(3, args); } @@ -217,8 +237,6 @@ inline expr pi(name const & n, expr const & t, expr const & e) { return expr(new inline expr pi(char const * n, expr const & t, expr const & e) { return pi(name(n), t, e); } inline expr arrow(expr const & t, expr const & e) { return pi(name("_"), t, e); } 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)); } inline expr expr::operator()(expr const & a1) const { return app(*this, a1); } inline expr expr::operator()(expr const & a1, expr const & a2) const { return app(*this, a1, a2); } @@ -235,7 +253,6 @@ inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstrac 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_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); } 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()); } @@ -244,7 +261,6 @@ inline expr_abstraction * to_abstraction(expr const & e) { return to_abstraction 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_type * to_type(expr const & e) { return to_type(e.raw()); } -inline expr_numeral * to_numeral(expr const & e) { return to_numeral(e.raw()); } // ======================================= // ======================================= @@ -254,21 +270,20 @@ 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 unsigned const_pos(expr_cell * e) { return to_constant(e)->get_pos(); } +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 mpz const & num_value(expr_cell * e) { return to_numeral(e)->get_num(); } 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 unsigned const_pos(expr const & e) { return to_constant(e)->get_pos(); } +inline value const & to_value(expr const & e) { return to_value(e.raw()); } 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(); } @@ -277,7 +292,6 @@ inline name const & abst_name(expr const & e) { return to_abstractio 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 mpz const & num_value(expr const & e) { return to_numeral(e)->get_num(); } // ======================================= // ======================================= diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index b0d11b988..068be0b97 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::Type: case expr_kind::Numeral: + case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: 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::Type: case expr_kind::Numeral: case expr_kind::Var: + case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: 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 edd97fbd9..033118803 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::Type: case expr_kind::Numeral: + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: cache(a); return a; case expr_kind::App: { diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp index 175ff4be0..35de6e1a5 100644 --- a/src/kernel/normalize.cpp +++ b/src/kernel/normalize.cpp @@ -18,18 +18,18 @@ Author: Leonardo de Moura namespace lean { class svalue; -typedef list stack; //!< Normalization stack +typedef list value_stack; //!< Normalization stack enum class svalue_kind { Expr, Closure, BoundedVar }; /** \brief Stack value: simple expressions, closures and bounded variables. */ class svalue { svalue_kind m_kind; unsigned m_bvar; expr m_expr; - stack m_ctx; + value_stack m_ctx; public: - explicit svalue(expr const & e): m_kind(svalue_kind::Expr), m_expr(e) {} - explicit svalue(unsigned k): m_kind(svalue_kind::BoundedVar), m_bvar(k) {} - svalue(expr const & e, stack const & c):m_kind(svalue_kind::Closure), m_expr(e), m_ctx(c) { lean_assert(is_lambda(e)); } + explicit svalue(expr const & e): m_kind(svalue_kind::Expr), m_expr(e) {} + explicit svalue(unsigned k): m_kind(svalue_kind::BoundedVar), m_bvar(k) {} + svalue(expr const & e, value_stack const & c):m_kind(svalue_kind::Closure), m_expr(e), m_ctx(c) { lean_assert(is_lambda(e)); } svalue_kind kind() const { return m_kind; } @@ -38,25 +38,25 @@ public: bool is_bounded_var() const { return kind() == svalue_kind::BoundedVar; } expr const & get_expr() const { lean_assert(is_expr() || is_closure()); return m_expr; } - stack const & get_ctx() const { lean_assert(is_closure()); return m_ctx; } + value_stack const & get_ctx() const { lean_assert(is_closure()); return m_ctx; } unsigned get_var_idx() const { lean_assert(is_bounded_var()); return m_bvar; } }; -svalue_kind kind(svalue const & v) { return v.kind(); } -expr const & to_expr(svalue const & v) { return v.get_expr(); } -stack const & stack_of(svalue const & v) { return v.get_ctx(); } -unsigned to_bvar(svalue const & v) { return v.get_var_idx(); } +svalue_kind kind(svalue const & v) { return v.kind(); } +expr const & to_expr(svalue const & v) { return v.get_expr(); } +value_stack const & stack_of(svalue const & v) { return v.get_ctx(); } +unsigned to_bvar(svalue const & v) { return v.get_var_idx(); } -stack extend(stack const & s, svalue const & v) { return cons(v, s); } +value_stack extend(value_stack const & s, svalue const & v) { return cons(v, s); } /** \brief Expression normalizer. */ class normalize_fn { environment const & m_env; context const & m_ctx; - svalue lookup(stack const & s, unsigned i, unsigned k) { + svalue lookup(value_stack const & s, unsigned i, unsigned k) { unsigned j = i; - stack const * it1 = &s; + value_stack const * it1 = &s; while (*it1) { if (j == 0) return head(*it1); @@ -75,7 +75,7 @@ class normalize_fn { } /** \brief Convert the closure \c a into an expression using the given stack in a context that contains \c k binders. */ - expr reify_closure(expr const & a, stack const & s, unsigned k) { + expr reify_closure(expr const & a, value_stack const & s, unsigned k) { lean_assert(is_lambda(a)); expr new_t = reify(normalize(abst_domain(a), s, k), k); expr new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1); @@ -126,12 +126,12 @@ class normalize_fn { } /** \brief Normalize the expression \c a in a context composed of stack \c s and \c k binders. */ - svalue normalize(expr const & a, stack const & s, unsigned k) { + svalue normalize(expr const & a, value_stack const & s, unsigned k) { lean_trace("normalize", tout << "Normalize, k: " << k << "\n" << a << "\n";); switch (a.kind()) { case expr_kind::Var: return lookup(s, var_idx(a), k); - case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral: + case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: return svalue(a); case expr_kind::App: { svalue f = normalize(arg(a, 0), s, k); @@ -142,7 +142,7 @@ class normalize_fn { // beta reduction expr const & fv = to_expr(f); lean_trace("normalize", tout << "beta reduction...\n" << fv << "\n";); - stack new_s = extend(stack_of(f), normalize(arg(a, i), s, k)); + value_stack new_s = extend(stack_of(f), normalize(arg(a, i), s, k)); f = normalize(abst_body(fv), new_s, k); if (i == n - 1) return f; @@ -177,7 +177,7 @@ public: expr operator()(expr const & e) { unsigned k = length(m_ctx); - return reify(normalize(e, stack(), k), k); + return reify(normalize(e, value_stack(), k), k); } }; diff --git a/src/kernel/replace.h b/src/kernel/replace.h index 298a1da09..01d90e94d 100644 --- a/src/kernel/replace.h +++ b/src/kernel/replace.h @@ -39,7 +39,7 @@ class replace_fn { expr r = m_f(e, offset); if (eqp(e, r)) { switch (e.kind()) { - case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Constant: case expr_kind::Var: + case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant: case expr_kind::Var: break; case expr_kind::App: r = update_app(e, [=](expr const & c) { return apply(c, offset); }); diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp index a8487bf74..e874ce0b4 100644 --- a/src/kernel/type_check.cpp +++ b/src/kernel/type_check.cpp @@ -110,9 +110,8 @@ class infer_type_fn { level l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_domain(e))); return type(max(l1, l2)); } - case expr_kind::Numeral: - // TODO - return e; + case expr_kind::Value: + return to_value(e).get_type(); } lean_unreachable(); return e; diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index ef1def0e0..bed285ec3 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -18,7 +18,7 @@ using namespace lean; void tst1() { expr a; - a = numeral(mpz(10)); + a = constant("a"); expr f; f = var(0); expr fa = f(a); @@ -40,7 +40,7 @@ void tst1() { void tst1_pp() { std::cerr << "=============== PP =====================\n"; expr a; - a = numeral(mpz(10)); + a = constant("a"); expr f; f = var(0); expr fa = f(a); @@ -66,7 +66,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::Type: case expr_kind::Numeral: + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: return 1; case expr_kind::App: { unsigned m = 0; @@ -83,7 +83,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::Type: case expr_kind::Numeral: + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: return 1; case expr_kind::App: return @@ -107,7 +107,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::Type: case expr_kind::Numeral: + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: m = std::max(c, m); break; case expr_kind::App: { @@ -168,7 +168,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::Type: case expr_kind::Numeral: + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: return 1; case expr_kind::App: return std::accumulate(begin_args(a), end_args(a), 1, @@ -232,7 +232,7 @@ void tst8() { expr f = constant("f"); expr x = var(0); expr a = constant("a"); - expr n = numeral(mpz(10)); + expr n = constant("n"); expr p = type(level()); expr y = var(1); lean_assert(closed(a)); @@ -316,7 +316,7 @@ void tst12() { expr a = constant("a"); expr x = var(0); expr t = type(level()); - expr F = pi("y", t, lambda("x", t, f(f(f(x,a),numeral(10)),x))); + expr F = pi("y", t, lambda("x", t, f(f(f(x,a),constant("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 07f4c137d..a5e3645dc 100644 --- a/src/tests/kernel/normalize.cpp +++ b/src/tests/kernel/normalize.cpp @@ -57,7 +57,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::Type: case expr_kind::Numeral: + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: return 1; case expr_kind::App: return std::accumulate(begin_args(a), end_args(a), 1,