From ec1aa2553c16bea2bc97c3ebde4ee6032a7dea6f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Jun 2018 10:05:45 -0700 Subject: [PATCH] refactor(kernel/declaration): implement `definition/constant/axiom/theorem` using `runtime/object` TODO: inductive, constructor, recursor --- src/frontends/lean/definition_cmds.cpp | 5 +- src/frontends/lean/print_cmd.cpp | 8 +- src/kernel/declaration.cpp | 143 ++++++++++++++++--------- src/kernel/declaration.h | 103 +++++++++--------- src/kernel/old_type_checker.cpp | 2 +- src/kernel/type_checker.cpp | 6 +- src/library/abstract_context_cache.cpp | 2 +- src/library/compiler/inliner.cpp | 7 +- src/library/compiler/preprocess.cpp | 2 +- src/library/compiler/vm_compiler.cpp | 2 +- src/library/kernel_serializer.cpp | 46 +------- src/library/kernel_serializer.h | 4 - src/library/module.cpp | 2 +- src/library/noncomputable.cpp | 2 +- src/library/sorry.cpp | 2 +- src/library/type_context.cpp | 2 +- src/library/update_declaration.cpp | 2 +- src/library/util.cpp | 6 +- src/library/vm/vm_declaration.cpp | 2 +- 19 files changed, 168 insertions(+), 180 deletions(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 99a93f7352..f5c9c4007a 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -182,7 +182,7 @@ static certified_declaration check(parser & p, environment const & env, name con format("this is usually due to a buggy tactic or a bug in the builtin elaborator"); msg += line() + format("elaborated type:"); msg += nest(i, line() + pp_fn(d.get_type())); - if (d.is_definition()) { + if (d.has_value()) { msg += line() + format("elaborated value:"); msg += nest(i, line() + pp_fn(d.get_value())); } @@ -612,9 +612,8 @@ static expr inline_new_defs(environment const & old_env, environment const & new return none_expr(); } else if (is_constant(e) && !old_env.find(const_name(e))) { auto decl = new_env.get(const_name(e)); - if (decl.is_definition()) { + if (decl.has_value()) { expr val = instantiate_value_univ_params(decl, const_levels(e)); - lean_assert(decl.is_definition()); return some_expr(inline_new_defs(old_env, new_env, n, val)); } else { throw exception(sstream() << "invalid theorem '" << n << "', theorems should not depend on axioms introduced using " diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index 969f59f681..555d4b07f8 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -49,12 +49,12 @@ struct print_axioms_deps { return; m_visited.insert(n); declaration const & d = m_env.get(n); - if (!d.is_definition() && !m_env.is_builtin(n)) { + if ((d.is_axiom() || d.is_constant_assumption()) && !m_env.is_builtin(n)) { m_use_axioms = true; m_ios << d.get_name() << "\n"; } visit(d.get_type()); - if (d.is_definition()) + if (d.has_value()) visit(d.get_value()); } @@ -88,7 +88,7 @@ static void print_axioms(parser & p, message_builder & out) { bool has_axioms = false; p.env().for_each_declaration([&](declaration const & d) { name const & n = d.get_name(); - if (!d.is_definition() && !p.env().is_builtin(n) && !d.is_meta()) { + if ((d.is_axiom() || d.is_constant_assumption()) && !p.env().is_builtin(n) && !d.is_meta()) { out << n << " : " << d.get_type() << endl; has_axioms = true; } @@ -220,7 +220,7 @@ static name to_user_name(environment const & env, name const & n) { static void print_definition(environment const & env, message_builder & out, name const & n, pos_info const & pos) { declaration d = env.get(n); - if (!d.is_definition()) + if (!d.has_value()) throw parser_error(sstream() << "invalid '#print definition', '" << to_user_name(env, n) << "' is not a definition", pos); options opts = out.get_text_stream().get_options(); opts = opts.update_if_undef(get_pp_beta_name(), false); diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 15bfa6a8d2..bc1a6bbde9 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -37,38 +37,95 @@ int compare(reducibility_hints const & h1, reducibility_hints const & h2) { } } -static declaration * g_dummy = nullptr; +static unsigned definition_scalar_offset() { return sizeof(object*)*3; } +static unsigned constant_scalar_offset() { return sizeof(object*); } +static unsigned inductive_scalar_offset() { return sizeof(object*)*6; } +static unsigned constructor_scalar_offset() { return sizeof(object*)*3; } +static unsigned recursor_scalar_offset() { return sizeof(object*)*7; } -declaration::declaration():declaration(*g_dummy) {} -declaration::declaration(cell * ptr):m_ptr(ptr) {} -declaration::declaration(declaration const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } -declaration::declaration(declaration && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } -declaration::~declaration() { if (m_ptr) m_ptr->dec_ref(); } - -declaration & declaration::operator=(declaration const & s) { LEAN_COPY_REF(s); } -declaration & declaration::operator=(declaration && s) { LEAN_MOVE_REF(s); } - -bool declaration::is_definition() const { return static_cast(m_ptr->m_value); } -bool declaration::is_constant_assumption() const { return !is_definition(); } -bool declaration::is_axiom() const { return is_constant_assumption() && m_ptr->m_theorem; } -bool declaration::is_theorem() const { return is_definition() && m_ptr->m_theorem; } -bool declaration::is_meta() const { return m_ptr->m_meta; } - -name const & declaration::get_name() const { return m_ptr->m_name; } -level_param_names const & declaration::get_univ_params() const { return m_ptr->m_params; } -unsigned declaration::get_num_univ_params() const { return length(get_univ_params()); } -expr const & declaration::get_type() const { return m_ptr->m_type; } - -expr const & declaration::get_value() const { - lean_assert(is_definition()); - return *(m_ptr->m_value); +object * declaration::mk_declaration_val(name const & n, level_param_names const & params, expr const & t) { + object * r = alloc_cnstr(0, 3, 0); + inc(n.raw()); cnstr_set_obj(r, 0, n.raw()); + inc(params.raw()); cnstr_set_obj(r, 1, params.raw()); + inc(t.raw()); cnstr_set_obj(r, 2, t.raw()); + return r; } -reducibility_hints const & declaration::get_hints() const { return m_ptr->m_hints; } + +object * declaration::mk_constant_val(name const & n, level_param_names const & params, expr const & t, bool meta) { + object * r = alloc_cnstr(0, 1, sizeof(unsigned char)); + cnstr_set_obj(r, 0, mk_declaration_val(n, params, t)); + cnstr_set_scalar(r, constant_scalar_offset(), static_cast(meta)); + return r; +} + +object * declaration::mk_definition_val(name const & n, level_param_names const & params, expr const & t, expr const & v, + reducibility_hints const & h, bool meta) { + object * r = alloc_cnstr(0, 3, sizeof(unsigned char)); + cnstr_set_obj(r, 0, mk_declaration_val(n, params, t)); + inc(v.raw()); cnstr_set_obj(r, 1, v.raw()); + inc(h.raw()); cnstr_set_obj(r, 2, h.raw()); + cnstr_set_scalar(r, definition_scalar_offset(), static_cast(meta)); + return r; +} + +object * declaration::mk_axiom_val(name const & n, level_param_names const & params, expr const & t) { + return mk_declaration_val(n, params, t); +} + +object * declaration::mk_theorem_val(name const & n, level_param_names const & params, expr const & t, expr const & v) { + object * r = alloc_cnstr(0, 2, 0); + cnstr_set_obj(r, 0, mk_declaration_val(n, params, t)); + inc(v.raw()); cnstr_set_obj(r, 1, v.raw()); + return r; +} + +bool declaration::is_meta() const { + switch (kind()) { + case declaration_kind::Definition: return cnstr_scalar(get_val_obj(), definition_scalar_offset()) != 0; + case declaration_kind::Constant: return cnstr_scalar(get_val_obj(), constant_scalar_offset()) != 0; + case declaration_kind::Inductive: return (cnstr_scalar(get_val_obj(), inductive_scalar_offset()) & 2) != 0; + case declaration_kind::Constructor: return cnstr_scalar(get_val_obj(), constructor_scalar_offset()) != 0; + case declaration_kind::Recursor: return (cnstr_scalar(get_val_obj(), recursor_scalar_offset()) & 2) != 0; + case declaration_kind::Axiom: return false; + case declaration_kind::Theorem: return false; + } + lean_unreachable(); +} + +static reducibility_hints * g_opaque = nullptr; + +reducibility_hints const & declaration::get_hints() const { + if (is_definition()) + return static_cast(cnstr_obj_ref(get_val(), 2)); + else + return *g_opaque; +} + +bool use_meta(environment const & env, expr const & e) { + bool found = false; + for_each(e, [&](expr const & e, unsigned) { + if (found) return false; + if (is_constant(e)) { + if (auto d = env.find(const_name(e))) { + if (d->is_meta()) { + found = true; + return false; + } + } + } + return true; + }); + return found; +} + +static declaration * g_dummy = nullptr; +declaration::declaration():declaration(*g_dummy) {} declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, reducibility_hints const & h, bool meta) { - return declaration(new declaration::cell(n, params, t, v, h, meta)); + return declaration(mk_cnstr(static_cast(declaration_kind::Definition), declaration::mk_definition_val(n, params, t, v, h, meta))); } + static unsigned get_max_height(environment const & env, expr const & v) { unsigned h = 0; for_each(v, [&](expr const & e, unsigned) { @@ -87,31 +144,17 @@ declaration mk_definition(environment const & env, name const & n, level_param_n unsigned h = get_max_height(env, v); return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1), meta); } + declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) { - return declaration(new declaration::cell(n, params, t, v)); -} -declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) { - return declaration(new declaration::cell(n, params, t, true, false)); -} -declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool meta) { - return declaration(new declaration::cell(n, params, t, false, meta)); + return declaration(mk_cnstr(static_cast(declaration_kind::Theorem), declaration::mk_theorem_val(n, params, t, v))); } -bool use_meta(environment const & env, expr const & e) { - bool found = false; - for_each(e, [&](expr const & e, unsigned) { - if (found) return false; - if (is_constant(e)) { - if (auto d = env.find(const_name(e))) { - if (d->is_meta()) { - found = true; - return false; - } - } - } - return true; - }); - return found; +declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) { + return declaration(mk_cnstr(static_cast(declaration_kind::Axiom), declaration::mk_axiom_val(n, params, t))); +} + +declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool meta) { + return declaration(mk_cnstr(static_cast(declaration_kind::Constant), declaration::mk_constant_val(n, params, t, meta))); } declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params, @@ -133,10 +176,12 @@ declaration mk_constant_assumption_inferring_meta(environment const & env, name } void initialize_declaration() { - g_dummy = new declaration(mk_axiom(name(), level_param_names(), expr())); + g_opaque = new reducibility_hints(reducibility_hints::mk_opaque()); + g_dummy = new declaration(mk_axiom(name(), level_param_names(), expr())); } void finalize_declaration() { delete g_dummy; + delete g_opaque; } } diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 76560ad0b0..c71a51ba94 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -48,7 +48,7 @@ public: bool is_regular() const { return kind() == reducibility_hints_kind::Regular; } unsigned get_height() const { return is_regular() ? cnstr_scalar(raw(), 0) : 0; } void serialize(serializer & s) const { s.write_object(raw()); } - static reducibility_hints deserialize(deserializer & d) { return reducibility_hints(d.read_object()); } + static reducibility_hints deserialize(deserializer & d) { object * o = d.read_object(); inc(o); return reducibility_hints(o); } }; inline serializer & operator<<(serializer & s, reducibility_hints const & l) { l.serialize(s); return s; } @@ -62,68 +62,54 @@ inline deserializer & operator>>(deserializer & d, reducibility_hints & l) { l = > 0 If f2 should be unfolded */ int compare(reducibility_hints const & h1, reducibility_hints const & h2); -/** \brief Environment definitions, theorems, axioms and variable declarations. */ -class declaration { - struct cell { - MK_LEAN_RC(); - name m_name; - level_param_names m_params; - expr m_type; - bool m_theorem; - optional m_value; // if none, then declaration is actually a postulate - reducibility_hints m_hints; - /* Definitions are non-meta by default. We use this feature to define tactical-definitions. */ - bool m_meta; - void dealloc() { delete this; } - cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom, bool meta): - m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom), - m_hints(reducibility_hints::mk_opaque()), m_meta(meta) {} - cell(name const & n, level_param_names const & params, expr const & t, expr const & v, - reducibility_hints const & h, bool meta): - m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(false), - m_value(v), m_hints(h), m_meta(meta) {} - cell(name const & n, level_param_names const & params, expr const & t, expr const & v): - m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(true), - m_value(v), m_hints(reducibility_hints::mk_opaque()), m_meta(false) {} - }; - cell * m_ptr; - explicit declaration(cell * ptr); - friend struct cell; +/** + +inductive declaration +| const_decl (val : constant_val) +| defn_decl (val : definition_val) +| axiom_decl (val : axiom_val) +| thm_decl (val : theorem_val) +| induct_decl (val : inductive_val) +| cnstr_decl (val : constructor_val) +| rec_decl (val : recursor_val) + +*/ +enum class declaration_kind { Constant, Definition, Axiom, Theorem, Inductive, Constructor, Recursor }; +class declaration : public object_ref { + explicit declaration(object * o):object_ref(o) {} + explicit declaration(object_ref const & o):object_ref(o) {} + static object * mk_declaration_val(name const & n, level_param_names const & params, expr const & t); + static object * mk_constant_val(name const & n, level_param_names const & params, expr const & t, bool meta); + static object * mk_definition_val(name const & n, level_param_names const & params, expr const & t, expr const & v, reducibility_hints const & h, bool meta); + static object * mk_axiom_val(name const & n, level_param_names const & params, expr const & t); + static object * mk_theorem_val(name const & n, level_param_names const & params, expr const & t, expr const & v); + object * get_val_obj() const { return cnstr_obj(raw(), 0); } + object_ref const & get_val() const { return cnstr_obj_ref(*this, 0); } + object_ref const & get_declaration_val() const { return (kind() == declaration_kind::Axiom) ? get_val() : cnstr_obj_ref(get_val(), 0); } public: - /** - \brief The default constructor creates a reference to a "dummy" - declaration. The actual "dummy" declaration is not relevant, and - no procedure should rely on the kind of declaration used. - - We have a default constructor because some collections only work - with types that have a default constructor. - */ declaration(); - declaration(declaration const & s); - declaration(declaration && s); - ~declaration(); + declaration(declaration const & other):object_ref(other) {} + declaration(declaration && other):object_ref(other) {} + declaration_kind kind() const { return static_cast(cnstr_tag(raw())); } - friend void swap(declaration & a, declaration & b) { std::swap(a.m_ptr, b.m_ptr); } + declaration & operator=(declaration const & other) { object_ref::operator=(other); return *this; } + declaration & operator=(declaration && other) { object_ref::operator=(other); return *this; } - declaration & operator=(declaration const & s); - declaration & operator=(declaration && s); - - friend bool is_eqp(declaration const & d1, declaration const & d2) { return d1.m_ptr == d2.m_ptr; } - - bool is_definition() const; - bool is_axiom() const; - bool is_theorem() const; - bool is_constant_assumption() const; + friend bool is_eqp(declaration const & d1, declaration const & d2) { return d1.raw() == d2.raw(); } + bool is_constant_assumption() const { return kind() == declaration_kind::Constant; } + bool is_definition() const { return kind() == declaration_kind::Definition; } + bool is_axiom() const { return kind() == declaration_kind::Axiom; } + bool is_theorem() const { return kind() == declaration_kind::Theorem; } bool is_meta() const; + bool has_value() const { return is_theorem() || is_definition(); } - name const & get_name() const; - level_param_names const & get_univ_params() const; - unsigned get_num_univ_params() const; - expr const & get_type() const; - expr const & get_value() const; - + name const & get_name() const { return static_cast(cnstr_obj_ref(get_declaration_val(), 0)); } + level_param_names const & get_univ_params() const { return static_cast(cnstr_obj_ref(get_declaration_val(), 1)); } + unsigned get_num_univ_params() const { return length(get_univ_params()); } + expr const & get_type() const { return static_cast(cnstr_obj_ref(get_declaration_val(), 2)); } + expr const & get_value() const { lean_assert(has_value()); return static_cast(cnstr_obj_ref(get_val(), 1)); } reducibility_hints const & get_hints() const; friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, @@ -133,8 +119,15 @@ public: friend declaration mk_theorem(name const &, level_param_names const &, expr const &, expr const &); friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t); friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool meta); + + void serialize(serializer & s) const { s.write_object(raw()); } + static declaration deserialize(deserializer & d) { object * o = d.read_object(); inc(o); return declaration(o); } }; +inline serializer & operator<<(serializer & s, declaration const & l) { l.serialize(s); return s; } +inline declaration read_declaration(deserializer & d) { return declaration::deserialize(d); } +inline deserializer & operator>>(deserializer & d, declaration & l) { l = read_declaration(d); return d; } + inline optional none_declaration() { return optional(); } inline optional some_declaration(declaration const & o) { return optional(o); } inline optional some_declaration(declaration && o) { return optional(std::forward(o)); } diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp index e33afc7a18..6db4d15235 100644 --- a/src/kernel/old_type_checker.cpp +++ b/src/kernel/old_type_checker.cpp @@ -400,7 +400,7 @@ optional old_type_checker::is_delta(expr const & e) const { expr const & f = get_app_fn(e); if (is_constant(f)) { if (auto d = m_env.find(const_name(f))) - if (d->is_definition()) + if (d->has_value()) return d; } return none_declaration(); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index d9fc33aa3c..dd2451322a 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -429,7 +429,7 @@ optional type_checker::is_delta(expr const & e) const { expr const & f = get_app_fn(e); if (is_constant(f)) { if (auto d = m_env.find(const_name(f))) - if (d->is_definition()) + if (d->has_value()) return d; } return none_declaration(); @@ -861,7 +861,7 @@ void check_decl_type(environment const & env, declaration const & d) { void check_decl_value(environment const & env, declaration const & d) { bool memoize = true; bool non_meta_only = !d.is_meta(); type_checker checker(env, memoize, non_meta_only); - if (d.is_definition()) { + if (d.has_value()) { check_definition(env, d, checker); } } @@ -870,7 +870,7 @@ certified_declaration check(environment const & env, declaration const & d) { bool memoize = true; bool non_meta_only = !d.is_meta(); type_checker checker(env, memoize, non_meta_only); check_decl_type(env, d, checker); - if (d.is_definition()) { + if (d.has_value()) { check_definition(env, d, checker); } return certified_declaration(env.get_id(), d); diff --git a/src/library/abstract_context_cache.cpp b/src/library/abstract_context_cache.cpp index 2d49a04c45..d3693b0a0a 100644 --- a/src/library/abstract_context_cache.cpp +++ b/src/library/abstract_context_cache.cpp @@ -94,7 +94,7 @@ bool context_cacheless::is_transparent(type_context_old & ctx, transparency_mode optional context_cacheless::get_decl(type_context_old & ctx, transparency_mode m, name const & n) { if (auto d = ctx.env().find(n)) { - if (d->is_definition() && is_transparent(ctx, m, *d)) { + if (d->has_value() && is_transparent(ctx, m, *d)) { return d; } } diff --git a/src/library/compiler/inliner.cpp b/src/library/compiler/inliner.cpp index 41103469ef..9d198975af 100644 --- a/src/library/compiler/inliner.cpp +++ b/src/library/compiler/inliner.cpp @@ -33,9 +33,8 @@ void initialize_inliner() { "inline", "mark definition to always be inlined", [](environment const & env, name const & d, bool) -> void { auto decl = env.get(d); - if (!decl.is_definition() || decl.is_theorem()) - throw exception( - "invalid 'inline' use, only definitions can be marked as inline"); + if (!decl.is_definition()) + throw exception("invalid 'inline' use, only definitions can be marked as inline"); })); } @@ -143,7 +142,7 @@ class inline_simple_definitions_fn : public compiler_step_visitor { return visit_cases_on_app(e); unsigned nargs = get_app_num_args(e); declaration d = env().get(n); - if (!d.is_definition() || d.is_theorem()) + if (!d.is_definition()) return default_visit_app(e); expr v = d.get_value(); unsigned arity = 0; diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index d7a99e357a..1504080a0b 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -81,7 +81,7 @@ class expand_aux_fn : public compiler_step_visitor { return false; name const & n = const_name(fn); declaration d = env().get(n); - if (!d.is_definition() || d.is_theorem() || is_projection(env(), n) || is_no_confusion(env(), n) || + if (!d.is_definition() || is_projection(env(), n) || is_no_confusion(env(), n) || ::lean::is_aux_recursor(env(), n) || is_user_defined_recursor(env(), n)) return false; return !is_vm_function(env(), n); diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index d23c22d97f..713b125018 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -394,7 +394,7 @@ static optional try_reuse_aux_meta_code(environment const & env, na } environment vm_compile(environment const & env, declaration const & d, bool optimize_bytecode) { - if (!d.is_definition() || d.is_theorem() || is_noncomputable(env, d.get_name()) || is_vm_builtin_function(d.get_name())) + if (!d.is_definition() || is_noncomputable(env, d.get_name()) || is_vm_builtin_function(d.get_name())) return env; if (auto new_env = try_reuse_aux_meta_code(env, d.get_name())) diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 62aca54d5e..ca9415bd87 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -9,52 +9,8 @@ Author: Leonardo de Moura #include "kernel/declaration.h" #include "library/kernel_serializer.h" -// Procedures for serializing and deserializing kernel objects (levels, exprs, declarations) namespace lean { -// Declaration serialization -level_param_names read_level_params(deserializer & d) { return read_names(d); } -serializer & operator<<(serializer & s, declaration const & d) { - char k = 0; - if (d.is_definition()) - k |= 1; - if (d.is_theorem() || d.is_axiom()) - k |= 2; - if (d.is_meta()) - k |= 4; - s << k << d.get_name() << d.get_univ_params() << d.get_type(); - if (d.is_definition()) { - s << d.get_value(); - if (!d.is_theorem()) - s << d.get_hints(); - } - return s; -} - -declaration read_declaration(deserializer & d) { - char k = d.read_char(); - bool has_value = (k & 1) != 0; - bool is_th_ax = (k & 2) != 0; - bool is_meta = (k & 4) != 0; - name n = read_name(d); - level_param_names ps = read_level_params(d); - expr t = read_expr(d); - if (has_value) { - expr v = read_expr(d); - if (is_th_ax) { - return mk_theorem(n, ps, t, v); - } else { - reducibility_hints hints = read_reducibility_hints(d); - return mk_definition(n, ps, t, v, hints, is_meta); - } - } else { - if (is_th_ax) - return mk_axiom(n, ps, t); - else - return mk_constant_assumption(n, ps, t, is_meta); - } -} - serializer & operator<<(serializer & s, inductive::certified_inductive_decl::comp_rule const & r) { s << r.m_num_bu << r.m_comp_rhs; return s; @@ -75,7 +31,7 @@ serializer & operator<<(serializer & s, inductive::inductive_decl const & d) { inductive::inductive_decl read_inductive_decl(deserializer & d) { name d_name = read_name(d); - level_param_names d_lparams = read_level_params(d); + level_param_names d_lparams = read_names(d); unsigned d_nparams = d.read_unsigned(); expr d_type = read_expr(d); unsigned num_intros = d.read_unsigned(); diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h index 223468ed13..aab1e914bd 100644 --- a/src/library/kernel_serializer.h +++ b/src/library/kernel_serializer.h @@ -11,10 +11,6 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" namespace lean { -serializer & operator<<(serializer & s, declaration const & d); -declaration read_declaration(deserializer & d); -inline deserializer & operator>>(deserializer & d, declaration & decl) { decl = read_declaration(d); return d; } - serializer & operator<<(serializer & s, inductive::certified_inductive_decl const & d); inductive::certified_inductive_decl read_certified_inductive_decl(deserializer & d); diff --git a/src/library/module.cpp b/src/library/module.cpp index 9f54027dbf..b598418c32 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -398,7 +398,7 @@ environment add_and_perform(environment const & env, std::shared_ptr get_noncomputable_reason(environment const & env, name const & n) { declaration const & d = env.get(n); - if (!d.is_definition()) + if (!d.has_value()) return optional(); old_type_checker tc(env); if (tc.is_prop(d.get_type())) diff --git a/src/library/sorry.cpp b/src/library/sorry.cpp index cd1d357078..148d7d7ccd 100644 --- a/src/library/sorry.cpp +++ b/src/library/sorry.cpp @@ -38,7 +38,7 @@ bool has_sorry(expr const & ex) { } bool has_sorry(declaration const & decl) { - return has_sorry(decl.get_type()) || (decl.is_definition() && has_sorry(decl.get_value())); + return has_sorry(decl.get_type()) || (decl.has_value() && has_sorry(decl.get_value())); } expr const & sorry_type(expr const & sry) { diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 298c88fcc3..e6270d1feb 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -599,7 +599,7 @@ optional type_context_old::unfold_definition(expr const & e) { return none_expr(); } optional new_it_d = env().find(const_name(new_it_fn)); - if (!new_it_d || !new_it_d->is_definition() || length(const_levels(new_it_fn)) != new_it_d->get_num_univ_params()) { + if (!new_it_d || !new_it_d->has_value() || length(const_levels(new_it_fn)) != new_it_d->get_num_univ_params()) { lean_trace(name({"type_context", "smart_unfolding"}), tout() << "fail 2 [" << m_unfold_depth << "] " << whnf_core(new_it, true) << "\n";); return none_expr(); } diff --git a/src/library/update_declaration.cpp b/src/library/update_declaration.cpp index f11fea3bce..f84604273e 100644 --- a/src/library/update_declaration.cpp +++ b/src/library/update_declaration.cpp @@ -12,7 +12,7 @@ static declaration update_declaration(declaration d, optional level_param_names _ps = ps ? *ps : d.get_univ_params(); expr _type = type ? *type : d.get_type(); expr _value; - if (d.is_definition()) { + if (d.has_value()) { _value = value ? *value : d.get_value(); } else { lean_assert(!value); diff --git a/src/library/util.cpp b/src/library/util.cpp index 8f37f4233f..a4b85e8a8a 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -117,7 +117,7 @@ optional unfold_term(environment const & env, expr const & e) { if (!is_constant(f)) return none_expr(); auto decl = env.find(const_name(f)); - if (!decl || !decl->is_definition()) + if (!decl || !decl->has_value()) return none_expr(); expr d = instantiate_value_univ_params(*decl, const_levels(f)); buffer args; @@ -159,7 +159,7 @@ optional dec_level(level const & l) { an element of the inductive datatype named \c I, and \c c must have \c nparams parameters. */ bool has_constructor(environment const & env, name const & c, name const & I, unsigned nparams) { auto d = env.find(c); - if (!d || d->is_definition()) + if (!d || d->has_value()) return false; expr type = d->get_type(); unsigned i = 0; @@ -302,7 +302,7 @@ optional is_constructor_app_ext(environment const & env, expr const & e) { if (!is_constant(f)) return optional(); auto decl = env.find(const_name(f)); - if (!decl || !decl->is_definition()) + if (!decl || !decl->has_value()) return optional(); expr const * it = &decl->get_value(); while (is_lambda(*it)) diff --git a/src/library/vm/vm_declaration.cpp b/src/library/vm/vm_declaration.cpp index dadc059ff1..9eea92bb61 100644 --- a/src/library/vm/vm_declaration.cpp +++ b/src/library/vm/vm_declaration.cpp @@ -118,7 +118,7 @@ meta_constant declaration.instantiate_value_univ_params : declaration → list l vm_obj declaration_instantiate_value_univ_params(vm_obj const & _d, vm_obj const & _ls) { declaration const & d = to_declaration(_d); levels ls = to_levels(_ls); - if (!d.is_definition() || d.get_num_univ_params() != length(ls)) + if (!d.has_value() || d.get_num_univ_params() != length(ls)) return mk_vm_none(); else return mk_vm_some(to_obj(instantiate_value_univ_params(d, ls)));