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

feat(library/constructions/cases_on): add cases_on for new inductive datatype module

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-04 09:26:16 -07:00
parent 5972a3038d
commit 10a7eccecd
6 changed files with 192 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -32,6 +32,7 @@ Authors: Daniel Selsam, Leonardo de Moura
#include "library/normalize.h"
#include "library/inductive_compiler/add_decl.h"
#include "library/tactic/tactic_evaluator.h"
#include "library/constructions/cases_on.h"
#include "frontends/lean/decl_cmds.h"
#include "frontends/lean/decl_util.h"
#include "frontends/lean/util.h"
@ -731,6 +732,9 @@ public:
ind_types.push_back(inductive_type(local_name_p(r.m_inds[i]), Pi(r.m_params, local_type_p(r.m_inds[i])), constructors(cnstrs)));
}
m_env = m_env.add(mk_inductive_decl(names(m_lp_names), nat(num_params), inductive_types(ind_types), m_meta_info.m_modifiers.m_is_meta));
for (inductive_type const & ind_type : ind_types) {
m_env = mk_cases_on(m_env, ind_type.get_name());
}
}
environment inductive_cmd() {

2
src/kernel/inductive.h
View file

@ -8,6 +8,8 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
#include "kernel/instantiate.h"
namespace lean {
/**\ brief Return recursor name for the given inductive datatype name */
name mk_rec_name(name const & I);
/* Auxiliary function for to_cnstr_when_K */
optional<expr> mk_nullary_cnstr(environment const & env, expr const & type, unsigned num_params);

4
src/kernel/local_ctx.h
View file

@ -104,6 +104,10 @@ public:
local_decl const & get_local_decl(name const & n) const;
local_decl const & get_local_decl(expr const & e) const { return get_local_decl(fvar_name(e)); }
/* \brief Return type of the given free variable.
\pre is_fvar(e) */
expr get_type(expr const & e) const { return get_local_decl(e).get_type(); }
/** \brief Traverse local declarations based on the order they were created */
void for_each(std::function<void(local_decl const &)> const & fn) const;
optional<local_decl> find_if(std::function<bool(local_decl const &)> const & pred) const; // NOLINT

183
src/library/constructions/cases_on.cpp
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/old_type_checker.h"
#include "kernel/abstract.h"
#include "kernel/inductive.h"
#include "kernel/inductive/inductive.h"
#include "library/module.h"
#include "library/protected.h"
@ -25,12 +26,11 @@ static bool is_type_former_arg(name const & C_name, expr const & arg) {
return is_local(fn) && local_name(fn) == C_name;
}
environment mk_cases_on(environment const & env, name const & n) {
environment mk_old_cases_on(environment const & env, name const & n) {
optional<inductive::inductive_decl> decl = inductive::is_inductive_decl(env, n);
if (!decl)
throw exception(sstream() << "error in 'cases_on' generation, '" << n << "' is not an inductive datatype");
// TODO(Leo): cleanup, this code still has leftovers from the time the kernel had support for
// mutually inductive types
// TODO(Leo): delete
name cases_on_name(n, "cases_on");
name_generator ngen = mk_constructions_name_generator();
name rec_name = inductive::get_elim_name(n);
@ -118,4 +118,181 @@ environment mk_cases_on(environment const & env, name const & n) {
new_env = add_aux_recursor(new_env, cases_on_name);
return add_protected(new_env, cases_on_name);
}
/** \brief Given a `C := As -> Type`, return `fun (xs : As), unit` */
static expr mk_fun_unit(expr const & C, expr const & unit) {
if (is_pi(C)) {
return mk_lambda(binding_name(C), binding_domain(C), mk_fun_unit(binding_body(C), unit));
} else {
return unit;
}
}
static bool is_type_former_arg(buffer<name> const & C_ids, expr const & arg) {
expr const & fn = get_app_fn(arg);
return is_fvar(fn) && std::find(C_ids.begin(), C_ids.end(), fvar_name(fn)) != C_ids.end();
}
/** \brief Given minor premise type `Pi (a_1 : A_1) ... (a_n : A_n), B`
return `fun (a_1 : A_1') ... (a_n : A_n'), unit.star`, where `A_i'` is
- `unit` IF `A_i` is a type forme application `C_ids[k] ...` which is not `C_main_id`.
- `A_i` otherwise. */
static expr mk_fun_star(expr const & minor, buffer<name> const & C_ids, name const & C_main_id,
expr const & unit, expr const & star) {
if (is_pi(minor)) {
expr const & domain = binding_domain(minor);
expr const & body = binding_body(minor);
if (is_type_former_arg(C_ids, domain) && fvar_name(get_app_fn(domain)) != C_main_id) {
return mk_lambda(binding_name(minor), unit, mk_fun_star(body, C_ids, C_main_id, unit, star));
} else {
return mk_lambda(binding_name(minor), binding_domain(minor), mk_fun_star(body, C_ids, C_main_id, unit, star));
}
} else {
return star;
}
}
environment mk_cases_on(environment const & env, name const & n) {
constant_info ind_info = env.get(n);
if (!ind_info.is_inductive())
throw exception(sstream() << "error in 'cases_on' generation, '" << n << "' is not an inductive datatype");
name cases_on_name(n, "cases_on");
local_ctx lctx;
inductive_val ind_val = ind_info.to_inductive_val();
name_generator ngen = mk_constructions_name_generator();
name rec_name = mk_rec_name(n);
constant_info rec_info = env.get(rec_name);
lean_assert(rec_info.is_recursor());
recursor_val rec_val = rec_info.to_recursor_val();
unsigned num_indices = rec_val.get_nindices();
unsigned num_minors = rec_val.get_nminors();
unsigned num_motives = rec_val.get_nmotives();
unsigned num_params = rec_val.get_nparams();
buffer<name> ind_names;
to_buffer(rec_val.get_all(), ind_names);
/* Populate `rec_fvars` with a free variable for each recursor argument */
buffer<expr> rec_fvars;
expr rec_type = rec_info.get_type();
while (is_pi(rec_type)) {
expr local = lctx.mk_local_decl(ngen, binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type));
rec_type = instantiate(binding_body(rec_type), local);
rec_fvars.push_back(local);
}
/* Remark `rec_fvars` free variables represent the recursor:
- Type parameters `As` (size == `num_params`)
- Motives `Cs` (size == `num_motives`)
- Minor premises (size == `num_minors`)
- Indices (size == `num_indices`)
- Major premise (size == 1)
The new `cases_on` recursor will have
- Type parameters `As` (size == `num_params`)
- Motive C[i] (size == 1)
- Minor premises C[i] (size == number of constructors of the main type)
- Indices (size == `num_indices`)
- Major premise (size == 1)
*/
/* Universe levels */
levels lvls = lparams_to_levels(rec_info.get_lparams());
bool elim_to_prop = rec_info.get_num_lparams() == ind_info.get_num_lparams();
level elim_lvl = elim_to_prop ? mk_level_zero() : head(lvls);
/* We need `unit` when `num_motives` > 0 */
expr unit = mk_unit(elim_lvl);
expr star = mk_unit_mk(elim_lvl);
buffer<expr> cases_on_params;
expr rec_cnst = mk_constant(rec_name, lvls);
buffer<expr> rec_args; // arguments for rec used to define cases_on
/* Add type parameters `As` */
for (unsigned i = 0; i < num_params; i++) {
cases_on_params.push_back(rec_fvars[i]);
rec_args.push_back(rec_fvars[i]);
}
/* Add C[i] */
buffer<name> C_ids; // unique ids of all motives (aka type formers)
unsigned i = num_params;
name C_main_id; // unique id of the main type former
for (unsigned j = 0; j < num_motives; j++) {
C_ids.push_back(fvar_name(rec_fvars[i]));
if (j < ind_names.size() && ind_names[j] == n) {
cases_on_params.push_back(rec_fvars[i]);
rec_args.push_back(rec_fvars[i]);
C_main_id = fvar_name(rec_fvars[i]);
} else {
rec_args.push_back(mk_fun_unit(lctx.get_type(rec_fvars[i]), unit));
}
i++;
}
/* Add indices and major-premise */
for (unsigned i = 0; i < num_indices + 1; i++)
cases_on_params.push_back(rec_fvars[num_params + num_motives + num_minors + i]);
/* Add minor premises */
unsigned minor_idx = 0;
for (name const & J_name : ind_names) {
constant_info J_info = env.get(J_name);
lean_assert(J_info.is_inductive());
inductive_val J_val = J_info.to_inductive_val();
unsigned num_cnstrs = length(J_val.get_cnstrs());
for (unsigned i = 0; i < num_cnstrs; i++) {
expr minor = rec_fvars[num_params + num_motives + minor_idx];
if (J_name == n) {
// A cases_on minor premise does not contain "recursive" arguments
buffer<expr> minor_non_rec_params;
buffer<expr> minor_params;
local_decl minor_decl = lctx.get_local_decl(minor);
expr minor_type = minor_decl.get_type();
while (is_pi(minor_type)) {
expr curr_type = binding_domain(minor_type);
expr local = lctx.mk_local_decl(ngen, binding_name(minor_type), curr_type, binding_info(minor_type));
while (is_pi(curr_type))
curr_type = binding_body(curr_type);
if (is_type_former_arg(C_ids, curr_type)) {
if (fvar_name(get_app_fn(curr_type)) == C_main_id) {
minor_params.push_back(local);
} else {
expr new_local = lctx.mk_local_decl(ngen, binding_name(minor_type), unit, binding_info(minor_type));
minor_params.push_back(new_local);
}
} else {
minor_params.push_back(local);
minor_non_rec_params.push_back(local);
}
minor_type = instantiate(binding_body(minor_type), local);
}
expr new_C = lctx.mk_local_decl(ngen, minor_decl.get_user_name(), lctx.mk_pi(minor_non_rec_params, minor_type),
minor_decl.get_info());
cases_on_params.push_back(new_C);
expr new_C_app = mk_app(new_C, minor_non_rec_params);
expr rec_arg = lctx.mk_lambda(minor_params, new_C_app);
rec_args.push_back(rec_arg);
} else {
rec_args.push_back(mk_fun_star(lctx.get_type(minor), C_ids, C_main_id, unit, star));
}
minor_idx++;
}
}
for (; minor_idx < num_minors; minor_idx++) {
expr minor = rec_fvars[num_params + num_motives + minor_idx];
rec_args.push_back(mk_fun_star(lctx.get_type(minor), C_ids, C_main_id, unit, star));
}
/* Add indices and major-premise to rec_args */
for (unsigned i = 0; i < num_indices+1; i++)
rec_args.push_back(rec_fvars[num_params + num_motives + num_minors + i]);
expr cases_on_type = lctx.mk_pi(cases_on_params, rec_type);
expr cases_on_value = lctx.mk_lambda(cases_on_params, mk_app(rec_cnst, rec_args));
declaration new_d = mk_definition_inferring_meta(env, cases_on_name, rec_info.get_lparams(), cases_on_type, cases_on_value,
reducibility_hints::mk_abbreviation());
environment new_env = module::add(env, new_d);
new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible, true);
new_env = add_aux_recursor(new_env, cases_on_name);
return add_protected(new_env, cases_on_name);
}
}

1
src/library/constructions/cases_on.h
View file

@ -13,5 +13,6 @@ namespace lean {
\remark Throws an exception if \c n is not an inductive datatype.
*/
environment mk_old_cases_on(environment const & env, name const & n);
environment mk_cases_on(environment const & env, name const & n);
}

2
src/library/inductive_compiler/basic.cpp
View file

@ -87,7 +87,7 @@ class add_basic_inductive_decl_fn {
if (has_unit) {
lean_trace(name({"inductive_compiler"}), tout() << ">> generate cases_on\n";);
if (gen_cases_on)
m_env = mk_cases_on(m_env, ind_name);
m_env = mk_old_cases_on(m_env, ind_name);
if (gen_cases_on && gen_no_confusion && has_eq && has_heq) {
lean_trace(name({"inductive_compiler"}), tout() << ">> generate no_confusion\n";);