max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(kernel/declaration): implement definition/constant/axiom/theorem using runtime/object

Browse source 
TODO: inductive, constructor, recursor
This commit is contained in:
Leonardo de Moura 2018-06-25 10:05:45 -07:00
parent 9c6238e1ac
commit ec1aa2553c
19 changed files with 168 additions and 180 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/definition_cmds.cpp
View file

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

8
src/frontends/lean/print_cmd.cpp
View file

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

143
src/kernel/declaration.cpp
View file

@ -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<bool>(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<unsigned char>(r, constant_scalar_offset(), static_cast<unsigned char>(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<unsigned char>(r, definition_scalar_offset(), static_cast<unsigned char>(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<unsigned char>(get_val_obj(), definition_scalar_offset()) != 0;
case declaration_kind::Constant: return cnstr_scalar<unsigned char>(get_val_obj(), constant_scalar_offset()) != 0;
case declaration_kind::Inductive: return (cnstr_scalar<unsigned char>(get_val_obj(), inductive_scalar_offset()) & 2) != 0;
case declaration_kind::Constructor: return cnstr_scalar<unsigned char>(get_val_obj(), constructor_scalar_offset()) != 0;
case declaration_kind::Recursor: return (cnstr_scalar<unsigned char>(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<reducibility_hints const &>(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<unsigned>(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<unsigned>(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<unsigned>(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<unsigned>(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;
}
}

103
src/kernel/declaration.h
View file

@ -48,7 +48,7 @@ public:
bool is_regular() const { return kind() == reducibility_hints_kind::Regular; }
unsigned get_height() const { return is_regular() ? cnstr_scalar<unsigned>(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<expr> 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<declaration_kind>(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<name const &>(cnstr_obj_ref(get_declaration_val(), 0)); }
level_param_names const & get_univ_params() const { return static_cast<level_param_names const &>(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<expr const &>(cnstr_obj_ref(get_declaration_val(), 2)); }
expr const & get_value() const { lean_assert(has_value()); return static_cast<expr const &>(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<declaration> none_declaration() { return optional<declaration>(); }
inline optional<declaration> some_declaration(declaration const & o) { return optional<declaration>(o); }
inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }

2
src/kernel/old_type_checker.cpp
View file

@ -400,7 +400,7 @@ optional<declaration> 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();

6
src/kernel/type_checker.cpp
View file

@ -429,7 +429,7 @@ optional<declaration> 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);

2
src/library/abstract_context_cache.cpp
View file

@ -94,7 +94,7 @@ bool context_cacheless::is_transparent(type_context_old & ctx, transparency_mode
optional<declaration> 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;
}
}

7
src/library/compiler/inliner.cpp
View file

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

2
src/library/compiler/preprocess.cpp
View file

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

2
src/library/compiler/vm_compiler.cpp
View file

@ -394,7 +394,7 @@ static optional<environment> 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()))

46
src/library/kernel_serializer.cpp
View file

@ -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();

4
src/library/kernel_serializer.h
View file

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

2
src/library/module.cpp
View file

@ -398,7 +398,7 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
}
environment update_module_defs(environment const & env, declaration const & d) {
if (d.is_definition() && !d.is_theorem()) {
if (d.is_definition()) {
module_ext ext = get_extension(env);
ext.m_module_decls = cons(d.get_name(), ext.m_module_decls);
ext.m_module_defs.insert(d.get_name());

2
src/library/noncomputable.cpp
View file

@ -211,7 +211,7 @@ struct get_noncomputable_reason_fn {
optional<name> 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<name>();
old_type_checker tc(env);
if (tc.is_prop(d.get_type()))

2
src/library/sorry.cpp
View file

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

2
src/library/type_context.cpp
View file

@ -599,7 +599,7 @@ optional<expr> type_context_old::unfold_definition(expr const & e) {
return none_expr();
}
optional<declaration> 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();
}

2
src/library/update_declaration.cpp
View file

@ -12,7 +12,7 @@ static declaration update_declaration(declaration d, optional<level_param_names>
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);

6
src/library/util.cpp
View file

@ -117,7 +117,7 @@ optional<expr> 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<expr> args;
@ -159,7 +159,7 @@ optional<level> 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<name> is_constructor_app_ext(environment const & env, expr const & e) {
if (!is_constant(f))
return optional<name>();
auto decl = env.find(const_name(f));
if (!decl || !decl->is_definition())
if (!decl || !decl->has_value())
return optional<name>();
expr const * it = &decl->get_value();
while (is_lambda(*it))

2
src/library/vm/vm_declaration.cpp
View file

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