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

refactor(library/definitional/no_confusion): cleanup API

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-11 16:12:44 -08:00
parent f6889951c6
commit e2bfe6ee36
3 changed files with 13 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/frontends/lean/inductive_cmd.cpp
View file

@ -637,6 +637,12 @@ struct inductive_cmd_fn {
m_decl_info.emplace_back(n, *g_definition, pos); m_decl_info.emplace_back(n, *g_definition, pos);
} }
void save_if_defined(name const & n, pos_info pos) {
if (m_env.find(n)) {
m_decl_info.emplace_back(n, *g_definition, pos);
}
}
environment mk_aux_decls(environment env, buffer<inductive_decl> const & decls) { environment mk_aux_decls(environment env, buffer<inductive_decl> const & decls) {
bool has_unit = has_unit_decls(env); bool has_unit = has_unit_decls(env);
bool has_eq = has_eq_decls(env); bool has_eq = has_eq_decls(env);
@ -653,11 +659,9 @@ struct inductive_cmd_fn {
env = mk_cases_on(env, inductive_decl_name(d)); env = mk_cases_on(env, inductive_decl_name(d));
save_def_info(name(n, "cases_on"), pos); save_def_info(name(n, "cases_on"), pos);
if (has_eq && has_heq) { if (has_eq && has_heq) {
if (optional<environment> new_env = mk_no_confusion(env, inductive_decl_name(d))) { env = mk_no_confusion(env, inductive_decl_name(d));
env = *new_env; save_if_defined(name{n, "no_confusion_type"}, pos);
save_def_info(name{n, "no_confusion_type"}, pos); save_if_defined(name(n, "no_confusion"), pos);
save_def_info(name(n, "no_confusion"), pos);
}
} }
// if (has_prod) { // if (has_prod) {
// env = mk_below(env, inductive_decl_name(d)); // env = mk_below(env, inductive_decl_name(d));

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

@ -138,10 +138,10 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
return some(add_protected(new_env, no_confusion_type_name)); return some(add_protected(new_env, no_confusion_type_name));
} }
optional<environment> mk_no_confusion(environment const & env, name const & n) { environment mk_no_confusion(environment const & env, name const & n) {
optional<environment> env1 = mk_no_confusion_type(env, n); optional<environment> env1 = mk_no_confusion_type(env, n);
if (!env1) if (!env1)
return env1; return env;
environment new_env = *env1; environment new_env = *env1;
type_checker tc(new_env); type_checker tc(new_env);
inductive::inductive_decls decls = *inductive::is_inductive_decl(new_env, n); inductive::inductive_decls decls = *inductive::is_inductive_decl(new_env, n);
@ -256,6 +256,6 @@ optional<environment> mk_no_confusion(environment const & env, name const & n) {
declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val, declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,
opaque, no_confusion_type_decl.get_module_idx(), use_conv_opt); opaque, no_confusion_type_decl.get_module_idx(), use_conv_opt);
new_env = module::add(new_env, check(new_env, new_d)); new_env = module::add(new_env, check(new_env, new_d));
return some(add_protected(new_env, no_confusion_name)); return add_protected(new_env, no_confusion_name);
} }
} }

2
src/library/definitional/no_confusion.h
View file

@ -15,5 +15,5 @@ namespace lean {
\remark Return none if did not create constructions because type is a proposition. \remark Return none if did not create constructions because type is a proposition.
*/ */
optional<environment> mk_no_confusion(environment const & env, name const & n); environment mk_no_confusion(environment const & env, name const & n);
} }