michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel): remove "opaque" field from kernel declarations

Browse source 
see issue #576
This commit is contained in:
Leonardo de Moura 2015-05-08 15:42:42 -07:00
parent 6c958a25e7
commit cf7e60e5a6
24 changed files with 57 additions and 109 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/builtin_cmds.cpp
View file

@ -626,12 +626,11 @@ static environment add_abbrev(parser & p, environment const & env, name const &
for (name const & l : decl.get_univ_params())
ls.push_back(mk_param_univ(l));
expr value = mk_constant(d, to_list(ls.begin(), ls.end()));
bool opaque = false;
name const & ns = get_namespace(env);
name full_id = ns + id;
p.add_abbrev_index(full_id, d);
environment new_env =
module::add(env, check(env, mk_definition(env, full_id, decl.get_univ_params(), decl.get_type(), value, opaque)));
module::add(env, check(env, mk_definition(env, full_id, decl.get_univ_params(), decl.get_type(), value)));
if (full_id != id)
new_env = add_expr_alias_rec(new_env, id, full_id);
return new_env;

10
src/frontends/lean/decl_cmds.cpp
View file

@ -1064,7 +1064,7 @@ class definition_cmd_fn {
cd = check(mk_axiom(m_real_name, c_ls, c_type));
}
} else {
cd = check(mk_definition(m_env, m_real_name, c_ls, c_type, c_value, m_is_opaque));
cd = check(mk_definition(m_env, m_real_name, c_ls, c_type, c_value));
}
if (!m_is_private)
m_p.add_decl_index(m_real_name, m_pos, m_p.get_cmd_token(), c_type);
@ -1176,11 +1176,10 @@ class definition_cmd_fn {
aux_values[i] = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, aux_values[i]));
}
if (is_definition()) {
m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls,
m_type, m_value, m_is_opaque)));
m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls, m_type, m_value)));
for (unsigned i = 0; i < aux_values.size(); i++)
m_env = module::add(m_env, check(mk_definition(m_env, m_real_aux_names[i], new_ls,
m_aux_types[i], aux_values[i], m_is_opaque)));
m_aux_types[i], aux_values[i])));
} else {
m_env = module::add(m_env, check(mk_theorem(m_real_name, new_ls, m_type, m_value)));
for (unsigned i = 0; i < aux_values.size(); i++)
@ -1232,8 +1231,7 @@ class definition_cmd_fn {
new_ls = append(m_ls, new_ls);
m_type = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_type));
m_value = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_value));
m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls,
m_type, m_value, m_is_opaque)));
m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls, m_type, m_value)));
m_p.cache_definition(m_real_name, pre_type, pre_value, new_ls, m_type, m_value);
}
}

3
src/frontends/lean/migrate_cmd.cpp
View file

@ -229,8 +229,7 @@ struct migrate_cmd_fn {
else if (d.is_theorem())
m_env = module::add(m_env, check(m_env, mk_theorem(full_name, ls, new_type, new_value)));
else
m_env = module::add(m_env, check(m_env, mk_definition(m_env, full_name, ls,
new_type, new_value, d.is_opaque())));
m_env = module::add(m_env, check(m_env, mk_definition(m_env, full_name, ls, new_type, new_value)));
m_p.add_decl_index(full_name, m_pos, d.is_theorem() ? name("theorem") : name("definition"), new_type);
if (short_name != full_name)
m_env = add_expr_alias_rec(m_env, short_name, full_name);

9
src/frontends/lean/structure_cmd.cpp
View file

@ -718,12 +718,10 @@ struct structure_cmd_fn {
}
void add_rec_on_alias(name const & n) {
bool opaque = false;
name rec_on_name(m_name, "rec_on");
declaration rec_on_decl = m_env.get(rec_on_name);
declaration new_decl = mk_definition(m_env, n, rec_on_decl.get_univ_params(),
rec_on_decl.get_type(), rec_on_decl.get_value(),
opaque);
rec_on_decl.get_type(), rec_on_decl.get_value());
m_env = module::add(m_env, check(m_env, new_decl));
m_env = set_reducible(m_env, n, reducible_status::Reducible);
if (optional<unsigned> idx = has_unfold_c_hint(m_env, rec_on_name))
@ -817,10 +815,7 @@ struct structure_cmd_fn {
}
coercion_value = Fun(m_params, Fun(st, coercion_value));
name coercion_name = coercion_names[i];
bool opaque = false;
declaration coercion_decl = mk_definition(m_env, coercion_name, lnames, coercion_type, coercion_value,
opaque);
declaration coercion_decl = mk_definition(m_env, coercion_name, lnames, coercion_type, coercion_value);
m_env = module::add(m_env, check(m_env, coercion_decl));
m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible);
save_def_info(coercion_name);

20
src/kernel/declaration.cpp
View file

@ -18,7 +18,6 @@ struct declaration::cell {
optional<expr> m_value; // if none, then declaration is actually a postulate
// The following fields are only meaningful for definitions (which are not theorems)
unsigned m_weight;
bool m_opaque;
// The following field affects the convertability checker.
// Let f be this definition, then if the following field is true,
// then whenever we are checking whether
@ -30,11 +29,11 @@ struct declaration::cell {
cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom),
m_weight(0), m_opaque(true), m_use_conv_opt(false) {}
m_weight(0), m_use_conv_opt(false) {}
cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
bool opaque, unsigned w, bool use_conv_opt):
unsigned w, bool use_conv_opt):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
m_value(v), m_weight(w), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
m_value(v), m_weight(w), m_use_conv_opt(use_conv_opt) {}
};
static declaration * g_dummy = nullptr;
@ -58,17 +57,16 @@ level_param_names const & declaration::get_univ_params() const { return m_ptr->m
unsigned declaration::get_num_univ_params() const { return length(get_univ_params()); }
expr const & declaration::get_type() const { return m_ptr->m_type; }
bool declaration::is_opaque() const { return m_ptr->m_opaque; }
expr const & declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
unsigned declaration::get_weight() const { return m_ptr->m_weight; }
bool declaration::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque, unsigned weight, bool use_conv_opt) {
return declaration(new declaration::cell(n, params, t, false, v, opaque, weight, use_conv_opt));
unsigned weight, bool use_conv_opt) {
return declaration(new declaration::cell(n, params, t, false, v, weight, use_conv_opt));
}
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque, bool use_conv_opt) {
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
expr const & v, bool use_conv_opt) {
unsigned w = 0;
for_each(v, [&](expr const & e, unsigned) {
if (is_constant(e)) {
@ -78,10 +76,10 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
}
return true;
});
return mk_definition(n, params, t, v, opaque, w+1, use_conv_opt);
return mk_definition(n, params, t, v, w+1, use_conv_opt);
}
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, true, v, true, 0, false));
return declaration(new declaration::cell(n, params, t, true, v, 0, false));
}
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, true));

9
src/kernel/declaration.h
View file

@ -50,13 +50,12 @@ public:
expr const & get_type() const;
expr const & get_value() const;
bool is_opaque() const;
unsigned get_weight() const;
bool use_conv_opt() const;
friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
expr const & v, bool opaque, bool use_conv_opt);
friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque,
expr const & v, bool use_conv_opt);
friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
unsigned weight, bool use_conv_opt);
friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
@ -68,9 +67,9 @@ inline optional<declaration> some_declaration(declaration const & o) { return op
inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, unsigned weight = 0, bool use_conv_opt = true);
unsigned weight = 0, bool use_conv_opt = true);
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, bool use_conv_opt = true);
bool use_conv_opt = true);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);

3
src/kernel/default_converter.cpp
View file

@ -111,8 +111,7 @@ expr default_converter::whnf_core(expr const & e) {
bool default_converter::is_opaque(declaration const & d) const {
lean_assert(d.is_definition());
if (d.is_theorem()) return true; // theorems are always opaque
if (!d.is_opaque()) return false; // d is a transparent definition
return true; // d is opaque
return false;
}
/** \brief Expand \c e if it is non-opaque constant with weight >= w */

6
src/library/definitional/brec_on.cpp
View file

@ -141,10 +141,9 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
expr below_type = Pi(args, Type_result);
expr below_value = Fun(args, rec);
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(env, below_name, blvls, below_type, below_value,
opaque, use_conv_opt);
use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, below_name, reducible_status::Reducible);
if (!ibelow)
@ -328,10 +327,9 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
expr brec_on_type = Pi(args, result_type);
expr brec_on_value = Fun(args, mk_pr1(tc, rec, ind));
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(env, brec_on_name, blps, brec_on_type, brec_on_value,
opaque, use_conv_opt);
use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible);
if (!ind)

3
src/library/definitional/cases_on.cpp
View file

@ -177,10 +177,9 @@ environment mk_cases_on(environment const & env, name const & n) {
expr cases_on_type = Pi(cases_on_params, rec_type);
expr cases_on_value = Fun(cases_on_params, mk_app(rec_cnst, rec_args));
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value,
opaque, use_conv_opt);
use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible);
new_env = add_unfold_c_hint(new_env, cases_on_name, cases_on_major_idx);

5
src/library/definitional/induction_on.cpp
View file

@ -24,7 +24,6 @@ environment mk_induction_on(environment const & env, name const & n) {
declaration ind_decl = env.get(n);
unsigned rec_on_num_univs = rec_on_decl.get_num_univ_params();
unsigned ind_num_univs = ind_decl.get_num_univ_params();
bool opaque = false;
bool use_conv_opt = true;
environment new_env = env;
if (rec_on_num_univs == ind_num_univs) {
@ -32,7 +31,7 @@ environment mk_induction_on(environment const & env, name const & n) {
certified_declaration cdecl = check(new_env,
mk_definition(new_env, induction_on_name, rec_on_decl.get_univ_params(),
rec_on_decl.get_type(), rec_on_decl.get_value(),
opaque, use_conv_opt));
use_conv_opt));
new_env = module::add(new_env, cdecl);
} else {
level_param_names induction_on_univs = tail(rec_on_decl.get_univ_params());
@ -43,7 +42,7 @@ environment mk_induction_on(environment const & env, name const & n) {
certified_declaration cdecl = check(new_env,
mk_definition(new_env, induction_on_name, induction_on_univs,
induction_on_type, induction_on_value,
opaque, use_conv_opt));
use_conv_opt));
new_env = module::add(new_env, cdecl);
}
return add_protected(new_env, induction_on_name);

6
src/library/definitional/no_confusion.cpp
View file

@ -134,10 +134,9 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
}
expr no_confusion_type_value = Fun(args, mk_app(cases_on1, outer_cases_on_args));
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value,
opaque, use_conv_opt);
use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible);
return some(add_protected(new_env, no_confusion_type_name));
@ -269,10 +268,9 @@ environment mk_no_confusion(environment const & env, name const & n) {
}
//
expr no_confusion_val = Fun(args, eq_rec);
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,
opaque, use_conv_opt);
use_conv_opt);
new_env = module::add(new_env, check(new_env, new_d));
new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible);
return add_protected(new_env, no_confusion_name);

3
src/library/definitional/projection.cpp
View file

@ -129,10 +129,9 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
expr proj_type = Pi(proj_args, result_type);
proj_type = infer_implicit_params(proj_type, nparams, infer_k);
expr proj_val = Fun(proj_args, rec_app);
bool opaque = false;
bool use_conv_opt = false;
declaration new_d = mk_definition(env, proj_name, lvl_params, proj_type, proj_val,
opaque, use_conv_opt);
use_conv_opt);
new_env = module::add(new_env, check(new_env, new_d));
new_env = set_reducible(new_env, proj_name, reducible_status::Reducible);
new_env = add_unfold_c_hint(new_env, proj_name, nparams);

4
src/library/definitional/rec_on.cpp
View file

@ -53,12 +53,10 @@ environment mk_rec_on(environment const & env, name const & n) {
expr rec = mk_constant(rec_decl.get_name(), ls);
expr rec_on_val = Fun(new_locals, mk_app(rec, locals));
bool opaque = false;
bool use_conv_opt = true;
environment new_env = module::add(env,
check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(),
rec_on_type, rec_on_val,
opaque, use_conv_opt)));
rec_on_type, rec_on_val, use_conv_opt)));
new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible);
new_env = add_unfold_c_hint(new_env, rec_on_name, rec_on_major_idx);
return add_protected(new_env, rec_on_name);

23
src/library/kernel_bindings.cpp
View file

@ -742,7 +742,6 @@ DECLARATION_PRED(is_definition)
DECLARATION_PRED(is_theorem)
DECLARATION_PRED(is_axiom)
DECLARATION_PRED(is_constant_assumption)
DECLARATION_PRED(is_opaque)
DECLARATION_PRED(use_conv_opt)
static int declaration_get_name(lua_State * L) { return push_name(L, to_declaration(L, 1).get_name()); }
static int declaration_get_params(lua_State * L) { return push_list_name(L, to_declaration(L, 1).get_univ_params()); }
@ -774,37 +773,36 @@ static int mk_theorem(lua_State * L) {
else
return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4)));
}
static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, bool & use_conv_opt) {
opaque = get_bool_named_param(L, idx, "opaque", opaque);
static void get_definition_args(lua_State * L, int idx, unsigned & weight, bool & use_conv_opt) {
use_conv_opt = get_bool_named_param(L, idx, "use_conv_opt", use_conv_opt);
weight = get_uint_named_param(L, idx, "weight", weight);
}
static int mk_definition(lua_State * L) {
int nargs = lua_gettop(L);
bool opaque = false; unsigned weight = 0; bool use_conv_opt = true;
unsigned weight = 0; bool use_conv_opt = true;
if (nargs < 3) {
throw exception("mk_definition must have at least 3 arguments");
} else if (is_environment(L, 1)) {
if (nargs < 4) {
throw exception("mk_definition must have at least 4 arguments, when the first argument is an environment");
} else if (is_expr(L, 3)) {
get_definition_args(L, 5, opaque, weight, use_conv_opt);
get_definition_args(L, 5, weight, use_conv_opt);
return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(),
to_expr(L, 3), to_expr(L, 4), opaque, use_conv_opt));
to_expr(L, 3), to_expr(L, 4), use_conv_opt));
} else {
get_definition_args(L, 6, opaque, weight, use_conv_opt);
get_definition_args(L, 6, weight, use_conv_opt);
return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_level_param_names(L, 3),
to_expr(L, 4), to_expr(L, 5), opaque, use_conv_opt));
to_expr(L, 4), to_expr(L, 5), use_conv_opt));
}
} else {
if (is_expr(L, 2)) {
get_definition_args(L, 4, opaque, weight, use_conv_opt);
get_definition_args(L, 4, weight, use_conv_opt);
return push_declaration(L, mk_definition(to_name_ext(L, 1), level_param_names(), to_expr(L, 2),
to_expr(L, 3), opaque, weight, use_conv_opt));
to_expr(L, 3), weight, use_conv_opt));
} else {
get_definition_args(L, 5, opaque, weight, use_conv_opt);
get_definition_args(L, 5, weight, use_conv_opt);
return push_declaration(L, mk_definition(to_name_ext(L, 1), to_level_param_names(L, 2),
to_expr(L, 3), to_expr(L, 4), opaque, weight, use_conv_opt));
to_expr(L, 3), to_expr(L, 4), weight, use_conv_opt));
}
}
}
@ -815,7 +813,6 @@ static const struct luaL_Reg declaration_m[] = {
{"is_theorem", safe_function<declaration_is_theorem>},
{"is_axiom", safe_function<declaration_is_axiom>},
{"is_constant_assumption", safe_function<declaration_is_constant_assumption>},
{"opaque", safe_function<declaration_is_opaque>},
{"use_conv_opt", safe_function<declaration_use_conv_opt>},
{"name", safe_function<declaration_get_name>},
{"univ_params", safe_function<declaration_get_params>},

13
src/library/kernel_serializer.cpp
View file

@ -282,13 +282,11 @@ serializer & operator<<(serializer & s, declaration const & d) {
char k = 0;
if (d.is_definition()) {
k |= 1;
if (d.is_opaque())
k |= 2;
if (d.use_conv_opt())
k |= 4;
k |= 2;
}
if (d.is_theorem() || d.is_axiom())
k |= 8;
k |= 4;
s << k << d.get_name() << d.get_univ_params() << d.get_type();
if (d.is_definition()) {
s << d.get_value();
@ -301,7 +299,7 @@ serializer & operator<<(serializer & s, declaration const & d) {
declaration read_declaration(deserializer & d) {
char k = d.read_char();
bool has_value = (k & 1) != 0;
bool is_th_ax = (k & 8) != 0;
bool is_th_ax = (k & 4) != 0;
name n = read_name(d);
level_param_names ps = read_level_params(d);
expr t = read_expr(d);
@ -311,9 +309,8 @@ declaration read_declaration(deserializer & d) {
return mk_theorem(n, ps, t, v);
} else {
unsigned w = d.read_unsigned();
bool is_opaque = (k & 2) != 0;
bool use_conv_opt = (k & 4) != 0;
return mk_definition(n, ps, t, v, is_opaque, w, use_conv_opt);
bool use_conv_opt = (k & 2) != 0;
return mk_definition(n, ps, t, v, w, use_conv_opt);
}
} else {
if (is_th_ax)

1
src/library/module.cpp
View file

@ -409,7 +409,6 @@ struct import_modules_fn {
void import_decl(deserializer & d) {
declaration decl = read_declaration(d);
lean_assert(!decl.is_definition());
environment env = m_senv.env();
decl = unfold_untrusted_macros(env, decl);
if (decl.get_name() == get_sorry_name() && has_sorry(env))

4
src/library/normalize.cpp
View file

@ -105,7 +105,7 @@ typedef scoped_ext<unfold_hint_config> unfold_hint_ext;
environment add_unfold_c_hint(environment const & env, name const & n, unsigned idx, bool persistent) {
declaration const & d = env.get(n);
if (!d.is_definition() || d.is_opaque())
if (!d.is_definition())
throw exception("invalid unfold-c hint, declaration must be a non-opaque definition");
return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_c_entry(n, idx), persistent);
}
@ -124,7 +124,7 @@ environment erase_unfold_c_hint(environment const & env, name const & n, bool pe
environment add_unfold_f_hint(environment const & env, name const & n, bool persistent) {
declaration const & d = env.get(n);
if (!d.is_definition() || d.is_opaque())
if (!d.is_definition())
throw exception("invalid unfold-f hint, declaration must be a non-opaque definition");
return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_f_entry(n), persistent);
}

2
src/library/reducible.cpp
View file

@ -86,8 +86,6 @@ static void check_declaration(environment const & env, name const & n) {
throw exception(sstream() << "invalid reducible command, '" << n << "' is not a definition");
if (d.is_theorem())
throw exception(sstream() << "invalid reducible command, '" << n << "' is a theorem");
if (d.is_opaque())
throw exception(sstream() << "invalid reducible command, '" << n << "' is an opaque definition");
}
environment set_reducible(environment const & env, name const & n, reducible_status s, bool persistent) {

2
src/library/unfold_macros.cpp
View file

@ -147,7 +147,7 @@ declaration unfold_untrusted_macros(environment const & env, declaration const &
} else if (d.is_definition()) {
expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);
return mk_definition(d.get_name(), d.get_univ_params(), new_t, new_v,
d.is_opaque(), d.get_weight(), d.use_conv_opt());
d.get_weight(), d.use_conv_opt());
} else if (d.is_axiom()) {
return mk_axiom(d.get_name(), d.get_univ_params(), new_t);
} else if (d.is_constant_assumption()) {

2
src/library/update_declaration.cpp
View file

@ -30,7 +30,7 @@ static declaration update_declaration(declaration d, optional<level_param_names>
if (d.is_theorem())
return mk_theorem(d.get_name(), _ps, _type, _value);
else
return mk_definition(d.get_name(), _ps, _type, _value, d.is_opaque(),
return mk_definition(d.get_name(), _ps, _type, _value,
d.get_weight(), d.use_conv_opt());
}
}

14
src/library/util.cpp
View file

@ -21,16 +21,6 @@ bool is_standard(environment const & env) {
return env.prop_proof_irrel() && env.impredicative();
}
bool is_def_app(environment const & env, expr const & e) {
if (!is_app(e))
return false;
expr const & f = get_app_fn(e);
if (!is_constant(f))
return false;
auto decl = env.find(const_name(f));
return decl && decl->is_definition() && !decl->is_opaque();
}
optional<expr> unfold_app(environment const & env, expr const & e) {
if (!is_app(e))
return none_expr();
@ -38,7 +28,7 @@ optional<expr> unfold_app(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() || decl->is_opaque())
if (!decl || !decl->is_definition())
return none_expr();
expr d = instantiate_value_univ_params(*decl, const_levels(f));
buffer<expr> args;
@ -191,7 +181,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() || decl->is_opaque())
if (!decl || !decl->is_definition())
return optional<name>();
expr const * it = &decl->get_value();
while (is_lambda(*it))

5
src/library/util.h
View file

@ -10,11 +10,6 @@ Author: Leonardo de Moura
namespace lean {
typedef std::unique_ptr<type_checker> type_checker_ptr;
/** \brief Return true iff \c e is of the form <tt>(f ...)</tt> where
\c f is a non-opaque constant definition */
bool is_def_app(environment const & env, expr const & e);
/** \brief If \c e is of the form <tt>(f a_1 ... a_n)</tt>, where \c f is
a non-opaque definition, then unfold \c f, and beta reduce.
Otherwise, return none.

4
tests/lean/run/reducible.lean
View file

@ -1,7 +1,7 @@
definition x [reducible] := 10
definition y := 20
definition z [irreducible] := 30
opaque definition w := 40
definition w := 40
(*
local env = get_env()
@ -24,7 +24,6 @@ opaque definition w := 40
assert(tc:whnf(x) == val_x)
assert(tc:whnf(y) == val_y)
assert(tc:whnf(z) == z)
assert(tc:whnf(w) == w)
-- Only definitions marked as reducible are unfolded
local tc = reducible_type_checker(env)
assert(tc:whnf(x) == val_x)
@ -37,7 +36,6 @@ opaque definition w := 40
assert(tc:whnf(x) == val_x)
assert(tc:whnf(y) == val_y)
assert(tc:whnf(z) == val_z)
assert(tc:whnf(w) == w)
*)
eval [whnf] x

12
tests/lua/def1.lua
View file

@ -34,33 +34,29 @@ assert(d:use_conv_opt())
assert(d:name() == name("d1"))
assert(d:value() == B)
local d2 = mk_definition("d2", A, B, nil)
local d3 = mk_definition("d3", A, B, {opaque=false, weight=100, use_conv_opt=false})
assert(not d3:opaque())
local d3 = mk_definition("d3", A, B, {weight=100, use_conv_opt=false})
assert(d3:weight() == 100)
assert(not d3:use_conv_opt())
local env = bare_environment()
local d4 = mk_definition(env, "bool", Type, Prop)
assert(d4:weight() == 1)
local d5 = mk_definition(env, "bool", Type, Prop, {opaque=false, weight=100, use_conv_opt=true})
assert(not d5:opaque())
local d5 = mk_definition(env, "bool", Type, Prop, {weight=100, use_conv_opt=true})
assert(d5:weight() == 1)
assert(d5:use_conv_opt())
local d6 = mk_definition("d6", {"l1", "l2"}, A, B, {opaque=true, weight=5})
local d6 = mk_definition("d6", {"l1", "l2"}, A, B, {weight=5})
assert(d6:type() == A)
assert(d6:value() == B)
assert(#(d6:univ_params()) == 2)
assert(d6:univ_params():head() == name("l1"))
assert(d6:univ_params():tail():head() == name("l2"))
assert(d6:opaque())
assert(d6:weight() == 5)
local d7 = mk_definition(env, "d7", {"l1", "l2"}, A, B, {opaque=true, weight=5})
local d7 = mk_definition(env, "d7", {"l1", "l2"}, A, B, {weight=5})
assert(d7:type() == A)
assert(d7:value() == B)
assert(d7:weight() == 1)
assert(#(d7:univ_params()) == 2)
assert(d7:univ_params():head() == name("l1"))
assert(d7:univ_params():tail():head() == name("l2"))
assert(d7:opaque())
print("done")
assert(not pcall(function() mk_theorem("t1", {max_univ("l1", "l2")}, mk_arrow(mk_sort(l1), mk_sort(l2)), mk_lambda("x", mk_sort(l1), Var(0))) end))
local l1 = global_univ("l1")