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

refactor(kernel): continue constant_info/declaration refactoring

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-27 17:23:26 -07:00
parent 96ff6b1718
commit 776c977742
10 changed files with 208 additions and 184 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/core.lean
View file

@ -2127,7 +2127,7 @@ namespace classical
axiom choice {α : Sort u} : nonempty α → α
noncomputable theorem indefinite_description {α : Sort u} (p : α → Prop)
noncomputable def indefinite_description {α : Sort u} (p : α → Prop)
(h : ∃ x, p x) : {x // p x} :=
choice $ let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩
@ -2214,7 +2214,7 @@ match (prop_decidable (nonempty α)) with
| (is_true hp) := psum.inl (@inhabited.default _ (inhabited_of_nonempty hp))
| (is_false hn) := psum.inr (λ a, absurd (nonempty.intro a) hn)
noncomputable theorem strong_indefinite_description {α : Sort u} (p : α → Prop)
noncomputable def strong_indefinite_description {α : Sort u} (p : α → Prop)
(h : nonempty α) : {x : α // (∃ y : α, p y) → p x} :=
if hp : ∃ x : α, p x then
let xp := indefinite_description _ hp in

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

@ -487,9 +487,9 @@ static void check_example(environment const & decl_env, options const & opts,
bool is_meta = modifiers.m_is_meta;
auto new_env = elab.env();
auto def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, is_meta);
declaration def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, is_meta);
new_env = module::add(new_env, def);
check_noncomputable(noncomputable_theory, new_env, decl_name, def.get_name(), modifiers.m_is_noncomputable,
check_noncomputable(noncomputable_theory, new_env, decl_name, decl_name, modifiers.m_is_noncomputable,
pos_provider.get_file_name(), pos_provider.get_some_pos());
} catch (throwable & ex) {
message_builder error_msg(tc, decl_env, get_global_ios(),

2
src/frontends/lean/inductive_cmds.cpp
View file

@ -756,13 +756,11 @@ public:
};
void parse_inductive_decl(parser & p, cmd_meta const & meta) {
auto pos = p.pos();
inductive_cmd_fn(p, meta).parse_and_elaborate();
}
environment inductive_cmd(parser & p, cmd_meta const & meta) {
p.next();
auto pos = p.pos();
return inductive_cmd_fn(p, meta).inductive_cmd();
}

2
src/frontends/lean/util.cpp
View file

@ -476,7 +476,7 @@ void initialize_frontend_lean_util() {
g_field_notation_name = new name("field_notation");
}
environment compile_expr(environment const & env, name const & n, level_param_names const & ls, expr const & type, expr const & e, pos_info const & pos) {
environment compile_expr(environment const & env, name const & n, level_param_names const & ls, expr const & type, expr const & e, pos_info const & /* pos */) {
environment new_env = env;
bool is_meta = true;
new_env = new_env.add(mk_definition(new_env, n, ls, type, e, is_meta));

140
src/kernel/declaration.cpp
View file

@ -37,14 +37,32 @@ int compare(reducibility_hints const & h1, reducibility_hints const & h2) {
}
}
recursor_rule::recursor_rule(name const & cnstr, unsigned nfields, expr const & rhs):
object_ref(mk_cnstr(0, cnstr.raw(), mk_nat_obj(nfields), rhs.raw())) {
inc(cnstr.raw());
inc(rhs.raw());
constant_val::constant_val(name const & n, level_param_names const & lparams, expr const & type):
object_ref(mk_cnstr(0, n, lparams, type)) {
}
axiom_val::axiom_val(name const & n, level_param_names const & lparams, expr const & type, bool is_meta):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), 1)) {
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*), static_cast<unsigned char>(is_meta));
}
bool axiom_val::is_meta() const { return cnstr_scalar<unsigned char>(raw(), sizeof(object*)) != 0; }
definition_val::definition_val(name const & n, level_param_names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_meta):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), val, hints, 1)) {
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*3, static_cast<unsigned char>(is_meta));
}
bool definition_val::is_meta() const { return cnstr_scalar<unsigned char>(raw(), sizeof(object*)*3) != 0; }
theorem_val::theorem_val(name const & n, level_param_names const & lparams, expr const & type, expr const & val):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), val)) {
}
recursor_rule::recursor_rule(name const & cnstr, unsigned nfields, expr const & rhs):
object_ref(mk_cnstr(0, cnstr, nat(nfields), rhs)) {
}
static unsigned definition_scalar_offset() { return sizeof(object*)*3; }
static unsigned axiom_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; }
@ -55,97 +73,18 @@ bool constructor_val::is_meta() const { return cnstr_scalar<unsigned char>(raw()
bool recursor_val::is_k() const { return (cnstr_scalar<unsigned char>(raw(), recursor_scalar_offset()) & 1) != 0; }
bool recursor_val::is_meta() const { return (cnstr_scalar<unsigned char>(raw(), recursor_scalar_offset()) & 2) != 0; }
static object * 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;
}
static object * mk_axiom_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, axiom_scalar_offset(), static_cast<unsigned char>(meta));
return r;
}
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) {
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;
}
static object * 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;
}
static object * mk_inductive_val(name const & n, level_param_names const & params, expr const & t, unsigned nparams, unsigned nindices,
names const & all, names const & cnstrs, names const & recs, bool is_rec, bool is_meta) {
object * r = alloc_cnstr(0, 6, 1);
cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
cnstr_set_obj(r, 1, mk_nat_obj(nparams));
cnstr_set_obj(r, 2, mk_nat_obj(nindices));
inc(all.raw()); cnstr_set_obj(r, 3, all.raw());
inc(cnstrs.raw()); cnstr_set_obj(r, 4, cnstrs.raw());
inc(recs.raw()); cnstr_set_obj(r, 5, recs.raw());
cnstr_set_scalar<unsigned char>(r, inductive_scalar_offset(), (is_rec ? 1 : 0) + (is_meta ? 2 : 0));
return r;
}
static object * mk_constructor_val(name const & n, level_param_names const & params, expr const & t, name const & induct, unsigned nparams,
bool is_meta) {
object * r = alloc_cnstr(0, 3, 1);
cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
inc(induct.raw()); cnstr_set_obj(r, 1, induct.raw());
cnstr_set_obj(r, 2, mk_nat_obj(nparams));
cnstr_set_scalar<unsigned char>(r, inductive_scalar_offset(), static_cast<unsigned char>(is_meta));
return r;
}
static object * mk_recursor_val(name const & n, level_param_names const & params, expr const & t, name const & induct, unsigned nparams,
unsigned nindices, unsigned nmotives, unsigned nminor, bool k, recursor_rules const & rules, bool is_meta) {
object * r = alloc_cnstr(0, 7, 1);
cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
inc(induct.raw()); cnstr_set_obj(r, 1, induct.raw());
cnstr_set_obj(r, 2, mk_nat_obj(nparams));
cnstr_set_obj(r, 3, mk_nat_obj(nindices));
cnstr_set_obj(r, 4, mk_nat_obj(nmotives));
cnstr_set_obj(r, 5, mk_nat_obj(nminor));
inc(rules.raw()); cnstr_set_obj(r, 6, rules.raw());
cnstr_set_scalar<unsigned char>(r, recursor_scalar_offset(), (k ? 1 : 0) + (is_meta ? 2 : 0));
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::Axiom: return cnstr_scalar<unsigned char>(get_val_obj(), axiom_scalar_offset()) != 0;
case declaration_kind::Theorem: return false;
case declaration_kind::Inductive: lean_unreachable(); // TODO(Leo):
case declaration_kind::Quot: return false;
case declaration_kind::Definition: return to_definition_val().is_meta();
case declaration_kind::Axiom: return to_axiom_val().is_meta();
case declaration_kind::Theorem: return false;
case declaration_kind::Inductive: lean_unreachable(); // TODO(Leo):
case declaration_kind::Quot: return false;
case declaration_kind::MutualDefinition: return true;
}
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(to_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) {
@ -168,7 +107,7 @@ 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(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(n, params, t, v, h, meta)));
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), definition_val(n, params, t, v, h, meta)));
}
static unsigned get_max_height(environment const & env, expr const & v) {
@ -191,11 +130,11 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
}
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), mk_theorem_val(n, params, t, v)));
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, params, t, v)));
}
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t, bool meta) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Axiom), mk_axiom_val(n, params, t, meta)));
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Axiom), axiom_val(n, params, t, meta)));
}
declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params,
@ -222,16 +161,13 @@ declaration mk_quot_decl(name const & n) {
}
inductive_type::inductive_type(name const & id, expr const & type, constructors const & cnstrs):
object_ref(mk_cnstr(0, id.raw(), type.raw(), cnstrs.raw())) {
inc(id.raw()); inc(type.raw()); inc(cnstrs.raw());
object_ref(mk_cnstr(0, id, type, cnstrs)) {
}
static unsigned inductive_decl_scalar_offset() { return sizeof(object*)*3; }
declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_meta) {
declaration r(mk_cnstr(static_cast<unsigned>(declaration_kind::Inductive),
lparams.raw(), nparams.raw(), types.raw(), 1));
inc(lparams.raw()); inc(nparams.raw()); inc(types.raw());
declaration r(mk_cnstr(static_cast<unsigned>(declaration_kind::Inductive), lparams, nparams, types, 1));
cnstr_set_scalar<unsigned char>(r.raw(), inductive_decl_scalar_offset(), static_cast<unsigned char>(is_meta));
return r;
}
@ -247,6 +183,8 @@ constant_info::constant_info(declaration const & d):object_ref(d.raw()) {
inc_ref(d.raw());
}
static reducibility_hints * g_opaque = nullptr;
reducibility_hints const & constant_info::get_hints() const {
if (is_definition())
return static_cast<reducibility_hints const &>(cnstr_obj_ref(to_val(), 2));
@ -256,13 +194,13 @@ reducibility_hints const & constant_info::get_hints() const {
bool constant_info::is_meta() const {
switch (kind()) {
case constant_info_kind::Definition: return cnstr_scalar<unsigned char>(get_val_obj(), definition_scalar_offset()) != 0;
case constant_info_kind::Axiom: return to_axiom_val().is_meta();
case constant_info_kind::Definition: return to_definition_val().is_meta();
case constant_info_kind::Theorem: return false;
case constant_info_kind::Inductive: return false; // TODO(Leo): to_inductive_val().is_meta();
case constant_info_kind::Quot: return false;
case constant_info_kind::Constructor: return false; // TODO(Leo): to_constructor_val().is_meta();
case constant_info_kind::Recursor: return false; // TODO(Leo): to_recursor_val().is_meta();
case constant_info_kind::Axiom: return cnstr_scalar<unsigned char>(get_val_obj(), axiom_scalar_offset()) != 0;
case constant_info_kind::Theorem: return false;
}
lean_unreachable();
}

114
src/kernel/declaration.h
View file

@ -63,20 +63,77 @@ inline deserializer & operator>>(deserializer & d, reducibility_hints & l) { l =
int compare(reducibility_hints const & h1, reducibility_hints const & h2);
/*
structure declaration_val :=
structure constant_val :=
(id : name) (lparams : list name) (type : expr)
*/
class declaration_val : public object_ref {
class constant_val : public object_ref {
public:
declaration_val(declaration_val const & other):object_ref(other) {}
declaration_val(declaration_val && other):object_ref(other) {}
declaration_val & operator=(declaration_val const & other) { object_ref::operator=(other); return *this; }
declaration_val & operator=(declaration_val && other) { object_ref::operator=(other); return *this; }
constant_val(name const & n, level_param_names const & lparams, expr const & type);
constant_val(constant_val const & other):object_ref(other) {}
constant_val(constant_val && other):object_ref(other) {}
constant_val & operator=(constant_val const & other) { object_ref::operator=(other); return *this; }
constant_val & operator=(constant_val && other) { object_ref::operator=(other); return *this; }
name const & get_name() const { return static_cast<name const &>(cnstr_obj_ref(*this, 0)); }
level_param_names const & get_lparams() const { return static_cast<level_param_names const &>(cnstr_obj_ref(*this, 1)); }
expr const & get_type() const { return static_cast<expr const &>(cnstr_obj_ref(*this, 2)); }
};
/*
structure axiom_val extends constant_val :=
(is_meta : bool)
*/
class axiom_val : public object_ref {
public:
axiom_val(name const & n, level_param_names const & lparams, expr const & type, bool is_meta);
axiom_val(axiom_val const & other):object_ref(other) {}
axiom_val(axiom_val && other):object_ref(other) {}
axiom_val & operator=(axiom_val const & other) { object_ref::operator=(other); return *this; }
axiom_val & operator=(axiom_val && other) { object_ref::operator=(other); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
name const & get_name() const { return to_constant_val().get_name(); }
level_param_names const & get_lparams() const { return to_constant_val().get_lparams(); }
expr const & get_type() const { return to_constant_val().get_type(); }
bool is_meta() const;
};
/*
structure definition_val extends constant_val :=
(value : expr) (hints : reducibility_hints) (is_meta : bool)
*/
class definition_val : public object_ref {
public:
definition_val(name const & n, level_param_names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_meta);
definition_val(definition_val const & other):object_ref(other) {}
definition_val(definition_val && other):object_ref(other) {}
definition_val & operator=(definition_val const & other) { object_ref::operator=(other); return *this; }
definition_val & operator=(definition_val && other) { object_ref::operator=(other); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
name const & get_name() const { return to_constant_val().get_name(); }
level_param_names const & get_lparams() const { return to_constant_val().get_lparams(); }
expr const & get_type() const { return to_constant_val().get_type(); }
expr const & get_value() const { return static_cast<expr const &>(cnstr_obj_ref(*this, 1)); }
reducibility_hints const & get_hints() const { return static_cast<reducibility_hints const &>(cnstr_obj_ref(*this, 2)); }
bool is_meta() const;
};
/*
structure theorem_val extends constant_val :=
(value : task expr)
*/
class theorem_val : public object_ref {
public:
theorem_val(name const & n, level_param_names const & lparams, expr const & type, expr const & val);
theorem_val(theorem_val const & other):object_ref(other) {}
theorem_val(theorem_val && other):object_ref(other) {}
theorem_val & operator=(theorem_val const & other) { object_ref::operator=(other); return *this; }
theorem_val & operator=(theorem_val && other) { object_ref::operator=(other); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
name const & get_name() const { return to_constant_val().get_name(); }
level_param_names const & get_lparams() const { return to_constant_val().get_lparams(); }
expr const & get_type() const { return to_constant_val().get_type(); }
expr const & get_value() const { return static_cast<expr const &>(cnstr_obj_ref(*this, 1)); }
};
/*
structure constructor :=
(id : name) (type : expr)
@ -116,12 +173,6 @@ enum class declaration_kind { Axiom, Definition, Theorem, Quot, MutualDefinition
class declaration : public object_ref {
object * get_val_obj() const { return cnstr_obj(raw(), 0); }
object_ref const & to_val() const { return cnstr_obj_ref(*this, 0); }
declaration_val const & to_declaration_val() const {
lean_assert(is_axiom() || is_definition() || is_theorem());
return static_cast<declaration_val const &>(cnstr_obj_ref(to_val(), 0));
}
public:
declaration();
declaration(declaration const & other):object_ref(other) {}
@ -143,12 +194,9 @@ public:
bool is_meta() const;
bool has_value() const { return is_theorem() || is_definition(); }
name const & get_name() const { return to_declaration_val().get_name(); }
level_param_names const & get_univ_params() const { return to_declaration_val().get_lparams(); }
unsigned get_num_univ_params() const { return length(get_univ_params()); }
expr const & get_type() const { return to_declaration_val().get_type(); }
expr const & get_value() const { lean_assert(has_value()); return static_cast<expr const &>(cnstr_obj_ref(to_val(), 1)); }
reducibility_hints const & get_hints() const;
axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(cnstr_obj_ref(raw(), 0)); }
definition_val const & to_definition_val() const { lean_assert(is_definition()); return static_cast<definition_val const &>(cnstr_obj_ref(raw(), 0)); }
theorem_val const & to_theorem_val() const { lean_assert(is_theorem()); return static_cast<theorem_val const &>(cnstr_obj_ref(raw(), 0)); }
void serialize(serializer & s) const { s.write_object(raw()); }
static declaration deserialize(deserializer & d) { object * o = d.read_object(); inc(o); return declaration(o); }
@ -190,7 +238,11 @@ declaration mk_axiom_inferring_meta(environment const & env, name const & n,
| induct_decl (lparams : list name) (nparams : nat) (types : list inductive_type) (is_meta : bool) */
class inductive_decl : public object_ref {
public:
inductive_decl(inductive_decl const & other):object_ref(other) {}
inductive_decl(inductive_decl && other):object_ref(other) {}
inductive_decl(declaration const & d):object_ref(d) { lean_assert(d.is_inductive()); }
inductive_decl & operator=(inductive_decl const & other) { object_ref::operator=(other); return *this; }
inductive_decl & operator=(inductive_decl && other) { object_ref::operator=(other); return *this; }
names const & get_lparams() const { return static_cast<names const &>(cnstr_obj_ref(raw(), 0)); }
nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(raw(), 1)); }
inductive_types const & get_types() const { return static_cast<inductive_types const &>(cnstr_obj_ref(raw(), 2)); }
@ -198,7 +250,7 @@ public:
};
/*
structure inductive_val extends declaration_val :=
structure inductive_val extends constant_val :=
(nparams : nat) -- Number of parameters
(nindices : nat) -- Number of indices
(all : list name) -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
@ -215,7 +267,7 @@ public:
inductive_val(inductive_val && other):object_ref(other) {}
inductive_val & operator=(inductive_val const & other) { object_ref::operator=(other); return *this; }
inductive_val & operator=(inductive_val && other) { object_ref::operator=(other); return *this; }
declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(*this, 0)); }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 1)); }
nat const & get_nindices() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 2)); }
names const & get_all() const { return static_cast<names const &>(cnstr_obj_ref(*this, 3)); }
@ -226,7 +278,7 @@ public:
};
/*
structure constructor_val extends declaration_val :=
structure constructor_val extends constant_val :=
(induct : name) -- Inductive type this constructor is a member of
(nparams : nat) -- Number of parameters in inductive datatype `induct`
(is_meta : bool)
@ -237,7 +289,7 @@ public:
constructor_val(constructor_val && other):object_ref(other) {}
constructor_val & operator=(constructor_val const & other) { object_ref::operator=(other); return *this; }
constructor_val & operator=(constructor_val && other) { object_ref::operator=(other); return *this; }
declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(*this, 0)); }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
name const & get_induct() const { return static_cast<name const &>(cnstr_obj_ref(*this, 1)); }
nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 2)); }
bool is_meta() const;
@ -264,7 +316,7 @@ public:
typedef list_ref<recursor_rule> recursor_rules;
/*
structure recursor_val extends declaration_val :=
structure recursor_val extends constant_val :=
(all : list name) -- List of all inductive datatypes in the mutual declaration that generated this recursor
(nparams : nat) -- Number of parameters
(nindices : nat) -- Number of indices
@ -280,7 +332,7 @@ public:
recursor_val(recursor_val && other):object_ref(other) {}
recursor_val & operator=(recursor_val const & other) { object_ref::operator=(other); return *this; }
recursor_val & operator=(recursor_val && other) { object_ref::operator=(other); return *this; }
declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(*this, 0)); }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
names const & get_all() const { return static_cast<names const &>(cnstr_obj_ref(*this, 1)); }
nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 2)); }
nat const & get_nindices() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 3)); }
@ -298,7 +350,7 @@ inductive quot_kind
| lift -- `quot.lift`
| ind -- `quot.ind`
structure quot_val extends declaration_val :=
structure quot_val extends constant_val :=
(kind : quot_kind)
*/
@ -317,7 +369,7 @@ enum class constant_info_kind { Axiom, Definition, Theorem, Quot, Inductive, Con
class constant_info : public object_ref {
object * get_val_obj() const { return cnstr_obj(raw(), 0); }
object_ref const & to_val() const { return cnstr_obj_ref(*this, 0); }
declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(to_val(), 0)); }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(to_val(), 0)); }
public:
constant_info();
constant_info(declaration const & d);
@ -336,14 +388,18 @@ public:
bool is_axiom() const { return kind() == constant_info_kind::Axiom; }
bool is_theorem() const { return kind() == constant_info_kind::Theorem; }
name const & get_name() const { return to_declaration_val().get_name(); }
level_param_names const & get_univ_params() const { return to_declaration_val().get_lparams(); }
name const & get_name() const { return to_constant_val().get_name(); }
level_param_names const & get_univ_params() const { return to_constant_val().get_lparams(); }
unsigned get_num_univ_params() const { return length(get_univ_params()); }
expr const & get_type() const { return to_declaration_val().get_type(); }
expr const & get_type() const { return to_constant_val().get_type(); }
bool has_value() const { return is_theorem() || is_definition(); }
expr const & get_value() const { lean_assert(has_value()); return static_cast<expr const &>(cnstr_obj_ref(to_val(), 1)); }
reducibility_hints const & get_hints() const;
axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(cnstr_obj_ref(raw(), 0)); }
definition_val const & to_definition_val() const { lean_assert(is_definition()); return static_cast<definition_val const &>(cnstr_obj_ref(raw(), 0)); }
theorem_val const & to_theorem_val() const { lean_assert(is_theorem()); return static_cast<theorem_val const &>(cnstr_obj_ref(raw(), 0)); }
// inductive_val const & to_inductive_val() const { lean_assert(is_inductive()); return static_cast<inductive_val const &>(to_val()); }
// constructor_val const & to_constructor_val() const { lean_assert(is_constructor()); return static_cast<constructor_val const &>(to_val()); }
// recursor_val const & to_recursor_val() const { lean_assert(is_recursor()); return static_cast<recursor_val const &>(to_val()); }

99
src/kernel/environment.cpp
View file

@ -79,8 +79,7 @@ static void check_name(environment const & env, name const & n) {
throw already_declared_exception(env, n);
}
static void check_duplicated_univ_params(environment const & env, declaration const & d) {
level_param_names ls = d.get_univ_params();
static void check_duplicated_univ_params(environment const & env, level_param_names ls) {
while (!is_nil(ls)) {
auto const & p = head(ls);
ls = tail(ls);
@ -92,54 +91,59 @@ static void check_duplicated_univ_params(environment const & env, declaration co
}
}
static void check_definition_value(environment const & env, declaration const & d, type_checker & checker) {
check_no_metavar_no_fvar(env, d.get_name(), d.get_value());
expr val_type = checker.check(d.get_value(), d.get_univ_params());
if (!checker.is_def_eq(val_type, d.get_type())) {
throw definition_type_mismatch_exception(env, d, val_type);
}
static void check_constant_val(environment const & env, constant_val const & v, type_checker & checker) {
check_name(env, v.get_name());
check_duplicated_univ_params(env, v.get_lparams());
check_no_metavar_no_fvar(env, v.get_name(), v.get_type());
expr sort = checker.check(v.get_type(), v.get_lparams());
checker.ensure_sort(sort, v.get_type());
}
static void check_definition_value(environment const & env, declaration const & d) {
bool memoize = true; bool non_meta_only = !d.is_meta();
static void check_constant_val(environment const & env, constant_val const & v, bool non_meta_only) {
bool memoize = true;
type_checker checker(env, memoize, non_meta_only);
if (d.has_value()) {
check_definition_value(env, d, checker);
}
check_constant_val(env, v, checker);
}
static void check_declaration_type(environment const & env, declaration const & d, type_checker & checker) {
check_no_metavar_no_fvar(env, d.get_name(), d.get_type());
check_duplicated_univ_params(env, d);
expr sort = checker.check(d.get_type(), d.get_univ_params());
checker.ensure_sort(sort, d.get_type());
environment environment::add_axiom(declaration const & d, bool check) const {
axiom_val const & v = d.to_axiom_val();
if (check)
check_constant_val(*this, v.to_constant_val(), !d.is_meta());
return environment(*this, insert(m_constants, v.get_name(), constant_info(d)));
}
static void check_declaration_type(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_declaration_type(env, d, checker);
}
environment environment::add_defn_thm_axiom(declaration const & d, bool check) const {
environment environment::add_definition(declaration const & d, bool check) const {
definition_val const & v = d.to_definition_val();
if (check) {
bool memoize = true; bool non_meta_only = !d.is_meta();
check_name(*this, d.get_name());
type_checker checker(*this, memoize, non_meta_only);
check_declaration_type(*this, d, checker);
if (d.has_value()) {
check_definition_value(*this, d, checker);
}
check_constant_val(*this, v.to_constant_val(), checker);
expr val_type = checker.check(v.get_value(), v.get_lparams());
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(*this, d, val_type);
}
return environment(*this, insert(m_constants, d.get_name(), constant_info(d)));
return environment(*this, insert(m_constants, v.get_name(), constant_info(d)));
}
environment environment::add_theorem(declaration const & d, bool check) const {
theorem_val const & v = d.to_theorem_val();
if (check) {
// TODO(Leo): we must add support for handling tasks here
bool memoize = true; bool non_meta_only = !d.is_meta();
type_checker checker(*this, memoize, non_meta_only);
check_constant_val(*this, v.to_constant_val(), checker);
expr val_type = checker.check(v.get_value(), v.get_lparams());
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(*this, d, val_type);
}
return environment(*this, insert(m_constants, v.get_name(), constant_info(d)));
}
environment environment::add(declaration const & d, bool check) const {
switch (d.kind()) {
case declaration_kind::Axiom:
case declaration_kind::Definition:
case declaration_kind::Theorem:
return add_defn_thm_axiom(d, check);
case declaration_kind::Axiom: return add_axiom(d, check);
case declaration_kind::Definition: return add_definition(d, check);
case declaration_kind::Theorem: return add_theorem(d, check);
default:
// NOT IMPLEMENTED YET.
lean_unreachable();
@ -149,18 +153,31 @@ environment environment::add(declaration const & d, bool check) const {
environment environment::add_meta(buffer<declaration> const & ds, bool check) const {
if (!check && trust_lvl() == 0)
throw kernel_exception(*this, "invalid meta declarations, type checking cannot be skipped at trust level 0");
/* Check declarations header */
if (check) {
bool memoize = true; bool non_meta_only = false;
type_checker checker(*this, memoize, non_meta_only);
for (declaration const & d : ds) {
definition_val const & v = d.to_definition_val();
if (check)
check_constant_val(*this, v.to_constant_val(), checker);
}
}
/* Add declarations */
environment new_env = *this;
/* Check declarations header, and add them to new_env.m_constants */
for (declaration const & d : ds) {
check_name(new_env, d.get_name());
if (check)
check_declaration_type(new_env, d);
new_env.m_constants.insert(d.get_name(), constant_info(d));
definition_val const & v = d.to_definition_val();
new_env.m_constants.insert(v.get_name(), constant_info(d));
}
/* Check actual definitions */
if (check) {
bool memoize = true; bool non_meta_only = false;
type_checker checker(new_env, memoize, non_meta_only);
for (declaration const & d : ds) {
check_definition_value(new_env, d);
definition_val const & v = d.to_definition_val();
expr val_type = checker.check(v.get_value(), v.get_lparams());
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(new_env, d, val_type);
}
}
return new_env;

4
src/kernel/environment.h
View file

@ -78,7 +78,9 @@ class environment {
environment(environment const & env, extensions const & exts):
m_header(env.m_header), m_quot_initialized(env.m_quot_initialized), m_constants(env.m_constants), m_extensions(exts) {}
environment add_defn_thm_axiom(declaration const & d, bool check) const;
environment add_axiom(declaration const & d, bool check) const;
environment add_definition(declaration const & d, bool check) const;
environment add_theorem(declaration const & d, bool check) const;
environment add_quot(declaration const & d) const;
public:

13
src/library/module.cpp
View file

@ -282,16 +282,21 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
environment add(environment const & env, declaration const & d) {
environment new_env = env.add(d);
if (!check_computable(new_env, d.get_name()))
new_env = mark_noncomputable(new_env, d.get_name());
if (d.is_definition()) {
definition_val const & v = d.to_definition_val();
if (!check_computable(new_env, v.get_name()))
new_env = mark_noncomputable(new_env, v.get_name());
}
return add(new_env, std::make_shared<decl_modification>(d));
}
environment add_meta(environment const & env, buffer<declaration> const & ds) {
environment new_env = env.add_meta(ds);
for (declaration const & d : ds) {
if (!check_computable(new_env, d.get_name()))
new_env = mark_noncomputable(new_env, d.get_name());
lean_assert(is_definition(d));
definition_val const & v = d.to_definition_val();
if (!check_computable(new_env, v.get_name()))
new_env = mark_noncomputable(new_env, v.get_name());
}
return add(new_env, std::make_shared<meta_decls_modification>(to_list(ds)));
}

10
src/library/sorry.cpp
View file

@ -38,7 +38,15 @@ bool has_sorry(expr const & ex) {
}
bool has_sorry(declaration const & decl) {
return has_sorry(decl.get_type()) || (decl.has_value() && has_sorry(decl.get_value()));
switch (decl.kind()) {
case declaration_kind::Axiom: return has_sorry(decl.to_axiom_val().get_type());
case declaration_kind::Definition: return has_sorry(decl.to_definition_val().get_type()) || has_sorry(decl.to_definition_val().get_value());
case declaration_kind::Theorem: return has_sorry(decl.to_theorem_val().get_type()) || has_sorry(decl.to_theorem_val().get_value());
case declaration_kind::Quot: return false;
case declaration_kind::Inductive: return false; // TODO(Leo):
case declaration_kind::MutualDefinition: return false; // TODO(Leo):
}
lean_unreachable();
}
bool has_sorry(constant_info const & info) {