diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index a6b0a1287f..87ac428569 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -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() { diff --git a/src/kernel/inductive.h b/src/kernel/inductive.h index ca19a674ea..7e90153c13 100644 --- a/src/kernel/inductive.h +++ b/src/kernel/inductive.h @@ -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 mk_nullary_cnstr(environment const & env, expr const & type, unsigned num_params); diff --git a/src/kernel/local_ctx.h b/src/kernel/local_ctx.h index c3add56133..31c62b8ed6 100644 --- a/src/kernel/local_ctx.h +++ b/src/kernel/local_ctx.h @@ -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 const & fn) const; optional find_if(std::function const & pred) const; // NOLINT diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp index 8bd26c157b..7478928c7b 100644 --- a/src/library/constructions/cases_on.cpp +++ b/src/library/constructions/cases_on.cpp @@ -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 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 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 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 ind_names; + to_buffer(rec_val.get_all(), ind_names); + /* Populate `rec_fvars` with a free variable for each recursor argument */ + buffer 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 cases_on_params; + expr rec_cnst = mk_constant(rec_name, lvls); + buffer 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 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 minor_non_rec_params; + buffer 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); +} } diff --git a/src/library/constructions/cases_on.h b/src/library/constructions/cases_on.h index d01ca45f82..5053d435b7 100644 --- a/src/library/constructions/cases_on.h +++ b/src/library/constructions/cases_on.h @@ -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); } diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp index a134918186..e4aa1835b9 100644 --- a/src/library/inductive_compiler/basic.cpp +++ b/src/library/inductive_compiler/basic.cpp @@ -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";);