1234 lines
56 KiB
C++
1234 lines
56 KiB
C++
/*
|
|
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#include "runtime/sstream.h"
|
|
#include "runtime/utf8.h"
|
|
#include "util/name_generator.h"
|
|
#include "kernel/environment.h"
|
|
#include "kernel/type_checker.h"
|
|
#include "kernel/instantiate.h"
|
|
#include "kernel/abstract.h"
|
|
#include "kernel/find_fn.h"
|
|
#include "kernel/replace_fn.h"
|
|
#include "kernel/kernel_exception.h"
|
|
|
|
namespace lean {
|
|
static name * g_ind_fresh = nullptr;
|
|
|
|
/**\ brief Return recursor name for the given inductive datatype name */
|
|
name mk_rec_name(name const & I) {
|
|
return I + name("rec");
|
|
}
|
|
|
|
/** \brief Return true if the given declaration is a structure */
|
|
bool is_structure_like(environment const & env, name const & decl_name) {
|
|
constant_info I = env.get(decl_name);
|
|
if (!I.is_inductive()) return false;
|
|
inductive_val I_val = I.to_inductive_val();
|
|
return I_val.get_ncnstrs() == 1 && I_val.get_nindices() == 0 && !I_val.is_rec();
|
|
}
|
|
|
|
bool is_inductive(environment const & env, name const & n) {
|
|
if (optional<constant_info> info = env.find(n))
|
|
return info->is_inductive();
|
|
return false;
|
|
}
|
|
|
|
bool is_constructor(environment const & env, name const & n) {
|
|
if (optional<constant_info> info = env.find(n))
|
|
return info->is_constructor();
|
|
return false;
|
|
}
|
|
|
|
bool is_recursor(environment const & env, name const & n) {
|
|
if (optional<constant_info> info = env.find(n))
|
|
return info->is_recursor();
|
|
return false;
|
|
}
|
|
|
|
optional<name> is_constructor_app(environment const & env, expr const & e) {
|
|
expr const & fn = get_app_fn(e);
|
|
if (is_constant(fn)) {
|
|
if (is_constructor(env, const_name(fn)))
|
|
return optional<name>(const_name(fn));
|
|
}
|
|
return optional<name>();
|
|
}
|
|
|
|
/** Return the names of all inductive datatypes */
|
|
static names get_all_inductive_names(buffer<inductive_type> const & ind_types) {
|
|
buffer<name> all_names;
|
|
for (inductive_type const & ind_type : ind_types) {
|
|
all_names.push_back(ind_type.get_name());
|
|
}
|
|
return names(all_names);
|
|
}
|
|
|
|
/** Return the names of all inductive datatypes in the given inductive declaration */
|
|
static names get_all_inductive_names(inductive_decl const & d) {
|
|
buffer<inductive_type> ind_types;
|
|
to_buffer(d.get_types(), ind_types);
|
|
return get_all_inductive_names(ind_types);
|
|
}
|
|
|
|
/** \brief If \c d_name is the name of a non-empty inductive datatype, then return the
|
|
name of the first constructor. Return none otherwise. */
|
|
static optional<name> get_first_cnstr(environment const & env, name const & d_name) {
|
|
constant_info info = env.get(d_name);
|
|
if (!info.is_inductive()) return optional<name>();
|
|
names const & cnstrs = info.to_inductive_val().get_cnstrs();
|
|
if (empty(cnstrs)) return optional<name>();
|
|
return optional<name>(head(cnstrs));
|
|
}
|
|
|
|
optional<expr> mk_nullary_cnstr(environment const & env, expr const & type, unsigned num_params) {
|
|
buffer<expr> args;
|
|
expr const & d = get_app_args(type, args);
|
|
if (!is_constant(d)) return none_expr();
|
|
name const & d_name = const_name(d);
|
|
auto cnstr_name = get_first_cnstr(env, d_name);
|
|
if (!cnstr_name) return none_expr();
|
|
args.shrink(num_params);
|
|
return some(mk_app(mk_constant(*cnstr_name, const_levels(d)), args));
|
|
}
|
|
|
|
expr expand_eta_struct(environment const & env, expr const & e_type, expr const & e) {
|
|
buffer<expr> args;
|
|
expr const & I = get_app_args(e_type, args);
|
|
if (!is_constant(I)) return e;
|
|
auto ctor_name = get_first_cnstr(env, const_name(I));
|
|
if (!ctor_name) return e;
|
|
constructor_val ctor_val = env.get(*ctor_name).to_constructor_val();
|
|
args.shrink(ctor_val.get_nparams());
|
|
expr result = mk_app(mk_constant(*ctor_name, const_levels(I)), args);
|
|
for (unsigned i = 0; i < ctor_val.get_nfields(); i++) {
|
|
result = mk_app(result, mk_proj(const_name(I), nat(i), e));
|
|
}
|
|
return result;
|
|
}
|
|
|
|
optional<recursor_rule> get_rec_rule_for(recursor_val const & rec_val, expr const & major) {
|
|
expr const & fn = get_app_fn(major);
|
|
if (!is_constant(fn)) return optional<recursor_rule>();
|
|
for (recursor_rule const & rule : rec_val.get_rules()) {
|
|
if (rule.get_cnstr() == const_name(fn))
|
|
return optional<recursor_rule>(rule);
|
|
}
|
|
return optional<recursor_rule>();
|
|
}
|
|
|
|
/* Auxiliary class for adding a mutual inductive datatype declaration. */
|
|
class add_inductive_fn {
|
|
environment m_env;
|
|
name_generator m_ngen;
|
|
local_ctx m_lctx;
|
|
names m_lparams;
|
|
unsigned m_nparams;
|
|
bool m_is_unsafe;
|
|
buffer<inductive_type> m_ind_types;
|
|
buffer<unsigned> m_nindices;
|
|
level m_result_level;
|
|
/* m_lparams ==> m_levels */
|
|
levels m_levels;
|
|
/* We track whether the resultant universe cannot be zero for any
|
|
universe level instantiation */
|
|
bool m_is_not_zero;
|
|
/* A free variable for each parameter */
|
|
buffer<expr> m_params;
|
|
/* A constant for each inductive type */
|
|
buffer<expr> m_ind_cnsts;
|
|
|
|
level m_elim_level;
|
|
bool m_K_target;
|
|
|
|
bool m_is_nested;
|
|
|
|
struct rec_info {
|
|
expr m_C; /* free variable for "main" motive */
|
|
buffer<expr> m_minors; /* minor premises */
|
|
buffer<expr> m_indices;
|
|
expr m_major; /* major premise */
|
|
};
|
|
|
|
/* We have an entry for each inductive datatype being declared,
|
|
and for nested inductive datatypes. */
|
|
buffer<rec_info> m_rec_infos;
|
|
|
|
public:
|
|
add_inductive_fn(environment const & env, inductive_decl const & decl, bool is_nested):
|
|
m_env(env), m_ngen(*g_ind_fresh), m_lparams(decl.get_lparams()), m_is_unsafe(decl.is_unsafe()),
|
|
m_is_nested(is_nested) {
|
|
if (!decl.get_nparams().is_small())
|
|
throw kernel_exception(env, "invalid inductive datatype, number of parameters is too big");
|
|
m_nparams = decl.get_nparams().get_small_value();
|
|
to_buffer(decl.get_types(), m_ind_types);
|
|
}
|
|
|
|
type_checker tc() { return type_checker(m_env, m_lctx, !m_is_unsafe); }
|
|
|
|
/** Return type of the parameter at position `i` */
|
|
expr get_param_type(unsigned i) const {
|
|
return m_lctx.get_local_decl(m_params[i]).get_type();
|
|
}
|
|
|
|
expr mk_local_decl(name const & n, expr const & t, binder_info const & bi = binder_info()) {
|
|
return m_lctx.mk_local_decl(m_ngen, n, consume_type_annotations(t), bi);
|
|
}
|
|
|
|
expr mk_local_decl_for(expr const & t) {
|
|
lean_assert(is_pi(t));
|
|
return m_lctx.mk_local_decl(m_ngen, binding_name(t), consume_type_annotations(binding_domain(t)), binding_info(t));
|
|
}
|
|
|
|
expr whnf(expr const & t) { return tc().whnf(t); }
|
|
|
|
expr infer_type(expr const & t) { return tc().infer(t); }
|
|
|
|
bool is_def_eq(expr const & t1, expr const & t2) { return tc().is_def_eq(t1, t2); }
|
|
|
|
expr mk_pi(buffer<expr> const & fvars, expr const & e) const { return m_lctx.mk_pi(fvars, e); }
|
|
expr mk_pi(expr const & fvar, expr const & e) const { return m_lctx.mk_pi(1, &fvar, e); }
|
|
expr mk_lambda(buffer<expr> const & fvars, expr const & e) const { return m_lctx.mk_lambda(fvars, e); }
|
|
expr mk_lambda(expr const & fvar, expr const & e) const { return m_lctx.mk_lambda(1, &fvar, e); }
|
|
|
|
/**
|
|
\brief Check whether the type of each datatype is well typed, and do not contain free variables or meta variables,
|
|
all inductive datatypes have the same parameters, the number of parameters match the argument m_nparams,
|
|
and the result universes are equivalent.
|
|
|
|
This method also initializes the fields:
|
|
- m_levels
|
|
- m_result_level
|
|
- m_nindices
|
|
- m_ind_cnsts
|
|
- m_params
|
|
|
|
\remark The local context m_lctx contains the free variables in m_params. */
|
|
void check_inductive_types() {
|
|
m_levels = lparams_to_levels(m_lparams);
|
|
bool first = true;
|
|
for (inductive_type const & ind_type : m_ind_types) {
|
|
expr type = ind_type.get_type();
|
|
m_env.check_name(ind_type.get_name());
|
|
m_env.check_name(mk_rec_name(ind_type.get_name()));
|
|
check_no_metavar_no_fvar(m_env, ind_type.get_name(), type);
|
|
tc().check(type, m_lparams);
|
|
m_nindices.push_back(0);
|
|
unsigned i = 0;
|
|
type = whnf(type);
|
|
while (is_pi(type)) {
|
|
if (i < m_nparams) {
|
|
if (first) {
|
|
expr param = mk_local_decl_for(type);
|
|
m_params.push_back(param);
|
|
type = instantiate(binding_body(type), param);
|
|
} else {
|
|
if (!is_def_eq(binding_domain(type), get_param_type(i)))
|
|
throw kernel_exception(m_env, "parameters of all inductive datatypes must match");
|
|
type = instantiate(binding_body(type), m_params[i]);
|
|
}
|
|
i++;
|
|
} else {
|
|
expr local = mk_local_decl_for(type);
|
|
type = instantiate(binding_body(type), local);
|
|
m_nindices.back()++;
|
|
}
|
|
type = whnf(type);
|
|
}
|
|
if (i != m_nparams)
|
|
throw kernel_exception(m_env, "number of parameters mismatch in inductive datatype declaration");
|
|
|
|
type = tc().ensure_sort(type);
|
|
|
|
if (first) {
|
|
m_result_level = sort_level(type);
|
|
m_is_not_zero = is_not_zero(m_result_level);
|
|
} else if (!is_equivalent(sort_level(type), m_result_level)) {
|
|
throw kernel_exception(m_env, "mutually inductive types must live in the same universe");
|
|
}
|
|
|
|
m_ind_cnsts.push_back(mk_constant(ind_type.get_name(), m_levels));
|
|
first = false;
|
|
}
|
|
|
|
lean_assert(length(m_levels) == length(m_lparams));
|
|
lean_assert(m_nindices.size() == m_ind_types.size());
|
|
lean_assert(m_ind_cnsts.size() == m_ind_types.size());
|
|
lean_assert(m_params.size() == m_nparams);
|
|
}
|
|
|
|
/** \brief Return true if declaration is recursive */
|
|
bool is_rec() {
|
|
for (unsigned idx = 0; idx < m_ind_types.size(); idx++) {
|
|
inductive_type const & ind_type = m_ind_types[idx];
|
|
for (constructor const & cnstr : ind_type.get_cnstrs()) {
|
|
expr t = constructor_type(cnstr);
|
|
while (is_pi(t)) {
|
|
if (find(binding_domain(t), [&](expr const & e, unsigned) {
|
|
if (is_constant(e)) {
|
|
for (expr const & I : m_ind_cnsts)
|
|
if (const_name(I) == const_name(e))
|
|
return true;
|
|
}
|
|
return false;
|
|
})) {
|
|
return true;
|
|
}
|
|
t = binding_body(t);
|
|
}
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
/* Return true if the given declarataion is reflexive.
|
|
|
|
Remark: We say an inductive type `T` is reflexive if it
|
|
contains at least one constructor that takes as an argument a
|
|
function returning `T'` where `T'` is another inductive datatype (possibly equal to `T`)
|
|
in the same mutual declaration. */
|
|
bool is_reflexive() {
|
|
for (unsigned idx = 0; idx < m_ind_types.size(); idx++) {
|
|
inductive_type const & ind_type = m_ind_types[idx];
|
|
for (constructor const & cnstr : ind_type.get_cnstrs()) {
|
|
expr t = constructor_type(cnstr);
|
|
while (is_pi(t)) {
|
|
expr arg_type = binding_domain(t);
|
|
if (is_pi(arg_type) && has_ind_occ(arg_type))
|
|
return true;
|
|
expr local = mk_local_decl_for(t);
|
|
t = instantiate(binding_body(t), local);
|
|
}
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
/** Return list with the names of all inductive datatypes in the mutual declaration. */
|
|
names get_all_inductive_names() const {
|
|
return ::lean::get_all_inductive_names(m_ind_types);
|
|
}
|
|
|
|
/** \brief Add all datatype declarations to environment. */
|
|
void declare_inductive_types() {
|
|
bool rec = is_rec();
|
|
bool reflexive = is_reflexive();
|
|
names all = get_all_inductive_names();
|
|
for (unsigned idx = 0; idx < m_ind_types.size(); idx++) {
|
|
inductive_type const & ind_type = m_ind_types[idx];
|
|
name const & n = ind_type.get_name();
|
|
buffer<name> cnstr_names;
|
|
for (constructor const & cnstr : ind_type.get_cnstrs()) {
|
|
cnstr_names.push_back(constructor_name(cnstr));
|
|
}
|
|
m_env.add_core(constant_info(inductive_val(n, m_lparams, ind_type.get_type(), m_nparams, m_nindices[idx],
|
|
all, names(cnstr_names), rec, m_is_unsafe, reflexive, m_is_nested)));
|
|
}
|
|
}
|
|
|
|
/** \brief Return true iff `t` is a term of the form `I As t`
|
|
where `I` is the inductive datatype at position `i` being declared and
|
|
`As` are the global parameters of this declaration. */
|
|
bool is_valid_ind_app(expr const & t, unsigned i) {
|
|
buffer<expr> args;
|
|
expr I = get_app_args(t, args);
|
|
if (I != m_ind_cnsts[i] || args.size() != m_nparams + m_nindices[i])
|
|
return false;
|
|
for (unsigned i = 0; i < m_nparams; i++) {
|
|
if (m_params[i] != args[i])
|
|
return false;
|
|
}
|
|
return true;
|
|
}
|
|
|
|
/** \brief Return some(i) iff `t` is of the form `I As t` where `I` the inductive `i`-th datatype being defined. */
|
|
optional<unsigned> is_valid_ind_app(expr const & t) {
|
|
for (unsigned i = 0; i < m_ind_types.size(); i++) {
|
|
if (is_valid_ind_app(t, i))
|
|
return optional<unsigned>(i);
|
|
}
|
|
return optional<unsigned>();
|
|
}
|
|
|
|
/** \brief Return true iff `e` is one of the inductive datatype being declared. */
|
|
bool is_ind_occ(expr const & e) {
|
|
return
|
|
is_constant(e) &&
|
|
std::any_of(m_ind_cnsts.begin(), m_ind_cnsts.end(),
|
|
[&](expr const & c) { return const_name(e) == const_name(c); });
|
|
}
|
|
|
|
/** \brief Return true iff `t` does not contain any occurrence of a datatype being declared. */
|
|
bool has_ind_occ(expr const & t) {
|
|
return static_cast<bool>(find(t, [&](expr const & e, unsigned) { return is_ind_occ(e); }));
|
|
}
|
|
|
|
/** \brief Return `some(d_idx)` iff `t` is a recursive argument, `d_idx` is the index of the
|
|
recursive inductive datatype. Otherwise, return `none`. */
|
|
optional<unsigned> is_rec_argument(expr t) {
|
|
t = whnf(t);
|
|
while (is_pi(t)) {
|
|
expr local = mk_local_decl_for(t);
|
|
t = whnf(instantiate(binding_body(t), local));
|
|
}
|
|
return is_valid_ind_app(t);
|
|
}
|
|
|
|
/** \brief Check if \c t contains only positive occurrences of the inductive datatypes being declared. */
|
|
void check_positivity(expr t, name const & cnstr_name, int arg_idx) {
|
|
t = whnf(t);
|
|
if (!has_ind_occ(t)) {
|
|
// nonrecursive argument
|
|
} else if (is_pi(t)) {
|
|
if (has_ind_occ(binding_domain(t)))
|
|
throw kernel_exception(m_env, sstream() << "arg #" << (arg_idx + 1) << " of '" << cnstr_name << "' "
|
|
"has a non positive occurrence of the datatypes being declared");
|
|
expr local = mk_local_decl_for(t);
|
|
check_positivity(instantiate(binding_body(t), local), cnstr_name, arg_idx);
|
|
} else if (is_valid_ind_app(t)) {
|
|
// recursive argument
|
|
} else {
|
|
throw kernel_exception(m_env, sstream() << "arg #" << (arg_idx + 1) << " of '" << cnstr_name << "' "
|
|
"contains a non valid occurrence of the datatypes being declared");
|
|
}
|
|
}
|
|
|
|
/** \brief Check whether the constructor declarations are type correct, parameters are in the expected positions,
|
|
constructor fields are in acceptable universe levels, positivity constraints, and returns the expected result. */
|
|
void check_constructors() {
|
|
for (unsigned idx = 0; idx < m_ind_types.size(); idx++) {
|
|
inductive_type const & ind_type = m_ind_types[idx];
|
|
name_set found_cnstrs;
|
|
for (constructor const & cnstr : ind_type.get_cnstrs()) {
|
|
name const & n = constructor_name(cnstr);
|
|
if (found_cnstrs.contains(n)) {
|
|
throw kernel_exception(m_env, sstream() << "duplicate constructor name '" << n << "'");
|
|
}
|
|
found_cnstrs.insert(n);
|
|
expr t = constructor_type(cnstr);
|
|
m_env.check_name(n);
|
|
check_no_metavar_no_fvar(m_env, n, t);
|
|
tc().check(t, m_lparams);
|
|
unsigned i = 0;
|
|
while (is_pi(t)) {
|
|
if (i < m_nparams) {
|
|
if (!is_def_eq(binding_domain(t), get_param_type(i)))
|
|
throw kernel_exception(m_env, sstream() << "arg #" << (i + 1) << " of '" << n << "' "
|
|
<< "does not match inductive datatypes parameters'");
|
|
t = instantiate(binding_body(t), m_params[i]);
|
|
} else {
|
|
expr s = tc().ensure_type(binding_domain(t));
|
|
// the sort is ok IF
|
|
// 1- its level is <= inductive datatype level, OR
|
|
// 2- is an inductive predicate
|
|
if (!(is_geq(m_result_level, sort_level(s)) || is_zero(m_result_level))) {
|
|
throw kernel_exception(m_env, sstream() << "universe level of type_of(arg #" << (i + 1) << ") "
|
|
<< "of '" << n << "' is too big for the corresponding inductive datatype");
|
|
}
|
|
if (!m_is_unsafe)
|
|
check_positivity(binding_domain(t), n, i);
|
|
expr local = mk_local_decl_for(t);
|
|
t = instantiate(binding_body(t), local);
|
|
}
|
|
i++;
|
|
}
|
|
if (!is_valid_ind_app(t, idx))
|
|
throw kernel_exception(m_env, sstream() << "invalid return type for '" << n << "'");
|
|
}
|
|
}
|
|
}
|
|
|
|
void declare_constructors() {
|
|
for (unsigned idx = 0; idx < m_ind_types.size(); idx++) {
|
|
inductive_type const & ind_type = m_ind_types[idx];
|
|
unsigned cidx = 0;
|
|
for (constructor const & cnstr : ind_type.get_cnstrs()) {
|
|
name const & n = constructor_name(cnstr);
|
|
expr const & t = constructor_type(cnstr);
|
|
unsigned arity = 0;
|
|
expr it = t;
|
|
while (is_pi(it)) {
|
|
it = binding_body(it);
|
|
arity++;
|
|
}
|
|
lean_assert(arity >= m_nparams);
|
|
unsigned nfields = arity - m_nparams;
|
|
m_env.add_core(constant_info(constructor_val(n, m_lparams, t, ind_type.get_name(), cidx, m_nparams, nfields, m_is_unsafe)));
|
|
cidx++;
|
|
}
|
|
}
|
|
}
|
|
|
|
/** \brief Return true if recursor can only map into Prop */
|
|
bool elim_only_at_universe_zero() {
|
|
if (m_is_not_zero) {
|
|
/* For every universe parameter assignment, the resultant universe is not 0.
|
|
So, it is not an inductive predicate */
|
|
return false;
|
|
}
|
|
|
|
if (m_ind_types.size() > 1) {
|
|
/* Mutually recursive inductive predicates only eliminate into Prop. */
|
|
return true;
|
|
}
|
|
|
|
unsigned num_intros = length(m_ind_types[0].get_cnstrs());
|
|
if (num_intros > 1) {
|
|
/* We have more than one constructor, then recursor for inductive predicate
|
|
can only eliminate intro Prop. */
|
|
return true;
|
|
}
|
|
|
|
if (num_intros == 0) {
|
|
/* empty inductive predicate (e.g., `false`) can eliminate into any universe */
|
|
return false;
|
|
}
|
|
|
|
/* We have only one constructor, the final check is, the type of each argument
|
|
that is not a parameter:
|
|
1- It must live in Prop, *OR*
|
|
2- It must occur in the return type. (this is essentially what is called a non-uniform parameter in Coq).
|
|
We can justify 2 by observing that this information is not a *secret* it is part of the type.
|
|
By eliminating to a non-proposition, we would not be revealing anything that is not already known. */
|
|
constructor const & cnstr = head(m_ind_types[0].get_cnstrs());
|
|
expr type = constructor_type(cnstr);
|
|
unsigned i = 0;
|
|
buffer<expr> to_check; /* Arguments that we must check if occur in the result type */
|
|
while (is_pi(type)) {
|
|
expr fvar = mk_local_decl_for(type);
|
|
if (i >= m_nparams) {
|
|
expr s = tc().ensure_type(binding_domain(type));
|
|
if (!is_zero(sort_level(s))) {
|
|
/* Current argument is not in Prop (i.e., condition 1 failed).
|
|
We save it in to_check to be able to try condition 2 above. */
|
|
to_check.push_back(fvar);
|
|
}
|
|
}
|
|
type = instantiate(binding_body(type), fvar);
|
|
i++;
|
|
}
|
|
buffer<expr> result_args;
|
|
get_app_args(type, result_args);
|
|
/* Check condition 2: every argument in to_check must occur in result_args */
|
|
for (expr const & arg : to_check) {
|
|
if (std::find(result_args.begin(), result_args.end(), arg) == result_args.end())
|
|
return true; /* Condition 2 failed */
|
|
}
|
|
return false;
|
|
}
|
|
|
|
/** \brief Initialize m_elim_level. */
|
|
void init_elim_level() {
|
|
if (elim_only_at_universe_zero()) {
|
|
m_elim_level = mk_level_zero();
|
|
} else {
|
|
name u("u");
|
|
int i = 1;
|
|
while (std::find(m_lparams.begin(), m_lparams.end(), u) != m_lparams.end()) {
|
|
u = name("u").append_after(i);
|
|
i++;
|
|
}
|
|
m_elim_level = mk_univ_param(u);
|
|
}
|
|
}
|
|
|
|
void init_K_target() {
|
|
/* A declaration is target for K-like reduction when
|
|
it has one intro, the intro has 0 arguments, and it is an inductive predicate.
|
|
In the following for-loop we check if the intro rule has 0 fields. */
|
|
m_K_target =
|
|
m_ind_types.size() == 1 && /* It is not a mutual declaration (for simplicity, we don't gain anything by supporting K in mutual declarations. */
|
|
is_zero(m_result_level) && /* It is an inductive predicate. */
|
|
length(m_ind_types[0].get_cnstrs()) == 1; /* Inductive datatype has only one constructor. */
|
|
if (!m_K_target)
|
|
return;
|
|
expr it = constructor_type(head(m_ind_types[0].get_cnstrs()));
|
|
unsigned i = 0;
|
|
while (is_pi(it)) {
|
|
if (i < m_nparams) {
|
|
it = binding_body(it);
|
|
} else {
|
|
/* See comment above */
|
|
m_K_target = false;
|
|
break;
|
|
}
|
|
i++;
|
|
}
|
|
}
|
|
|
|
/** \brief Given `t` of the form `I As is` where `I` is one of the inductive datatypes being defined,
|
|
As are the global parameters, and is the actual indices provided to it.
|
|
Return the index of `I`, and store is in the argument `indices`. */
|
|
unsigned get_I_indices(expr const & t, buffer<expr> & indices) {
|
|
optional<unsigned> r = is_valid_ind_app(t);
|
|
lean_assert(r);
|
|
buffer<expr> all_args;
|
|
get_app_args(t, all_args);
|
|
for (unsigned i = m_nparams; i < all_args.size(); i++)
|
|
indices.push_back(all_args[i]);
|
|
return *r;
|
|
}
|
|
|
|
/** \brief Populate m_rec_infos. */
|
|
void mk_rec_infos() {
|
|
unsigned d_idx = 0;
|
|
/* First, populate the fields, m_C, m_indices, m_major */
|
|
for (inductive_type const & ind_type : m_ind_types) {
|
|
rec_info info;
|
|
expr t = ind_type.get_type();
|
|
unsigned i = 0;
|
|
t = whnf(t);
|
|
while (is_pi(t)) {
|
|
if (i < m_nparams) {
|
|
t = instantiate(binding_body(t), m_params[i]);
|
|
} else {
|
|
expr idx = mk_local_decl_for(t);
|
|
info.m_indices.push_back(idx);
|
|
t = instantiate(binding_body(t), idx);
|
|
}
|
|
i++;
|
|
t = whnf(t);
|
|
}
|
|
info.m_major = mk_local_decl("t", mk_app(mk_app(m_ind_cnsts[d_idx], m_params), info.m_indices));
|
|
expr C_ty = mk_sort(m_elim_level);
|
|
C_ty = mk_pi(info.m_major, C_ty);
|
|
C_ty = mk_pi(info.m_indices, C_ty);
|
|
name C_name("motive");
|
|
if (m_ind_types.size() > 1)
|
|
C_name = name(C_name).append_after(d_idx+1);
|
|
info.m_C = mk_local_decl(C_name, C_ty);
|
|
m_rec_infos.push_back(info);
|
|
d_idx++;
|
|
}
|
|
/* First, populate the field m_minors */
|
|
unsigned minor_idx = 1;
|
|
d_idx = 0;
|
|
for (inductive_type const & ind_type : m_ind_types) {
|
|
name ind_type_name = ind_type.get_name();
|
|
for (constructor const & cnstr : ind_type.get_cnstrs()) {
|
|
buffer<expr> b_u; // nonrec and rec args;
|
|
buffer<expr> u; // rec args
|
|
buffer<expr> v; // inductive args
|
|
name cnstr_name = constructor_name(cnstr);
|
|
expr t = constructor_type(cnstr);
|
|
unsigned i = 0;
|
|
while (is_pi(t)) {
|
|
if (i < m_nparams) {
|
|
t = instantiate(binding_body(t), m_params[i]);
|
|
} else {
|
|
expr l = mk_local_decl_for(t);
|
|
b_u.push_back(l);
|
|
if (is_rec_argument(binding_domain(t)))
|
|
u.push_back(l);
|
|
t = instantiate(binding_body(t), l);
|
|
}
|
|
i++;
|
|
}
|
|
buffer<expr> it_indices;
|
|
unsigned it_idx = get_I_indices(t, it_indices);
|
|
expr C_app = mk_app(m_rec_infos[it_idx].m_C, it_indices);
|
|
expr intro_app = mk_app(mk_app(mk_constant(cnstr_name, m_levels), m_params), b_u);
|
|
C_app = mk_app(C_app, intro_app);
|
|
/* populate v using u */
|
|
for (unsigned i = 0; i < u.size(); i++) {
|
|
expr u_i = u[i];
|
|
expr u_i_ty = whnf(infer_type(u_i));
|
|
buffer<expr> xs;
|
|
while (is_pi(u_i_ty)) {
|
|
expr x = mk_local_decl_for(u_i_ty);
|
|
xs.push_back(x);
|
|
u_i_ty = whnf(instantiate(binding_body(u_i_ty), x));
|
|
}
|
|
buffer<expr> it_indices;
|
|
unsigned it_idx = get_I_indices(u_i_ty, it_indices);
|
|
expr C_app = mk_app(m_rec_infos[it_idx].m_C, it_indices);
|
|
expr u_app = mk_app(u_i, xs);
|
|
C_app = mk_app(C_app, u_app);
|
|
expr v_i_ty = mk_pi(xs, C_app);
|
|
local_decl u_i_decl = m_lctx.get_local_decl(fvar_name(u_i));
|
|
expr v_i = mk_local_decl(u_i_decl.get_user_name().append_after("_ih"), v_i_ty, binder_info());
|
|
v.push_back(v_i);
|
|
}
|
|
expr minor_ty = mk_pi(b_u, mk_pi(v, C_app));
|
|
name minor_name = cnstr_name.replace_prefix(ind_type_name, name());
|
|
expr minor = mk_local_decl(minor_name, minor_ty);
|
|
m_rec_infos[d_idx].m_minors.push_back(minor);
|
|
minor_idx++;
|
|
}
|
|
d_idx++;
|
|
}
|
|
}
|
|
|
|
/** \brief Return the levels for the recursor. */
|
|
levels get_rec_levels() {
|
|
if (is_param(m_elim_level))
|
|
return levels(m_elim_level, m_levels);
|
|
else
|
|
return m_levels;
|
|
}
|
|
|
|
/** \brief Return the level parameter names for the recursor. */
|
|
names get_rec_lparams() {
|
|
if (is_param(m_elim_level))
|
|
return names(param_id(m_elim_level), m_lparams);
|
|
else
|
|
return m_lparams;
|
|
}
|
|
|
|
|
|
/** \brief Store all type formers in `Cs` */
|
|
void collect_Cs(buffer<expr> & Cs) {
|
|
for (unsigned i = 0; i < m_ind_types.size(); i++)
|
|
Cs.push_back(m_rec_infos[i].m_C);
|
|
}
|
|
|
|
/** \brief Store all minor premises in `ms`. */
|
|
void collect_minor_premises(buffer<expr> & ms) {
|
|
for (unsigned i = 0; i < m_ind_types.size(); i++)
|
|
ms.append(m_rec_infos[i].m_minors);
|
|
}
|
|
|
|
recursor_rules mk_rec_rules(unsigned d_idx, buffer<expr> const & Cs, buffer<expr> const & minors, unsigned & minor_idx) {
|
|
inductive_type const & d = m_ind_types[d_idx];
|
|
levels lvls = get_rec_levels();
|
|
buffer<recursor_rule> rules;
|
|
for (constructor const & cnstr : d.get_cnstrs()) {
|
|
buffer<expr> b_u;
|
|
buffer<expr> u;
|
|
expr t = constructor_type(cnstr);
|
|
unsigned i = 0;
|
|
while (is_pi(t)) {
|
|
if (i < m_nparams) {
|
|
t = instantiate(binding_body(t), m_params[i]);
|
|
} else {
|
|
expr l = mk_local_decl_for(t);
|
|
b_u.push_back(l);
|
|
if (is_rec_argument(binding_domain(t)))
|
|
u.push_back(l);
|
|
t = instantiate(binding_body(t), l);
|
|
}
|
|
i++;
|
|
}
|
|
buffer<expr> v;
|
|
for (unsigned i = 0; i < u.size(); i++) {
|
|
expr u_i = u[i];
|
|
expr u_i_ty = whnf(infer_type(u_i));
|
|
buffer<expr> xs;
|
|
while (is_pi(u_i_ty)) {
|
|
expr x = mk_local_decl_for(u_i_ty);
|
|
xs.push_back(x);
|
|
u_i_ty = whnf(instantiate(binding_body(u_i_ty), x));
|
|
}
|
|
buffer<expr> it_indices;
|
|
unsigned it_idx = get_I_indices(u_i_ty, it_indices);
|
|
name rec_name = mk_rec_name(m_ind_types[it_idx].get_name());
|
|
expr rec_app = mk_constant(rec_name, lvls);
|
|
rec_app = mk_app(mk_app(mk_app(mk_app(mk_app(rec_app, m_params), Cs), minors), it_indices), mk_app(u_i, xs));
|
|
v.push_back(mk_lambda(xs, rec_app));
|
|
}
|
|
expr e_app = mk_app(mk_app(minors[minor_idx], b_u), v);
|
|
expr comp_rhs = mk_lambda(m_params, mk_lambda(Cs, mk_lambda(minors, mk_lambda(b_u, e_app))));
|
|
rules.push_back(recursor_rule(constructor_name(cnstr), b_u.size(), comp_rhs));
|
|
minor_idx++;
|
|
}
|
|
return recursor_rules(rules);
|
|
}
|
|
|
|
/** \brief Declare recursors. */
|
|
void declare_recursors() {
|
|
buffer<expr> Cs; collect_Cs(Cs);
|
|
buffer<expr> minors; collect_minor_premises(minors);
|
|
unsigned nminors = minors.size();
|
|
unsigned nmotives = Cs.size();
|
|
names all = get_all_inductive_names();
|
|
unsigned minor_idx = 0;
|
|
for (unsigned d_idx = 0; d_idx < m_ind_types.size(); d_idx++) {
|
|
rec_info const & info = m_rec_infos[d_idx];
|
|
expr C_app = mk_app(mk_app(info.m_C, info.m_indices), info.m_major);
|
|
expr rec_ty = mk_pi(info.m_major, C_app);
|
|
rec_ty = mk_pi(info.m_indices, rec_ty);
|
|
rec_ty = mk_pi(minors, rec_ty);
|
|
rec_ty = mk_pi(Cs, rec_ty);
|
|
rec_ty = mk_pi(m_params, rec_ty);
|
|
rec_ty = infer_implicit(rec_ty, true /* strict */);
|
|
recursor_rules rules = mk_rec_rules(d_idx, Cs, minors, minor_idx);
|
|
name rec_name = mk_rec_name(m_ind_types[d_idx].get_name());
|
|
names rec_lparams = get_rec_lparams();
|
|
m_env.add_core(constant_info(recursor_val(rec_name, rec_lparams, rec_ty, all,
|
|
m_nparams, m_nindices[d_idx], nmotives, nminors,
|
|
rules, m_K_target, m_is_unsafe)));
|
|
}
|
|
}
|
|
|
|
environment operator()() {
|
|
m_env.check_duplicated_univ_params(m_lparams);
|
|
check_inductive_types();
|
|
declare_inductive_types();
|
|
check_constructors();
|
|
declare_constructors();
|
|
init_elim_level();
|
|
init_K_target();
|
|
mk_rec_infos();
|
|
declare_recursors();
|
|
return m_env;
|
|
}
|
|
};
|
|
|
|
static name * g_nested = nullptr;
|
|
static name * g_nested_fresh = nullptr;
|
|
|
|
/* Result produced by elim_nested_inductive_fn */
|
|
struct elim_nested_inductive_result {
|
|
name_generator m_ngen;
|
|
buffer<expr> m_params;
|
|
name_map<expr> m_aux2nested; /* mapping from auxiliary type to nested inductive type. */
|
|
declaration m_aux_decl;
|
|
|
|
elim_nested_inductive_result(name_generator const & ngen, buffer<expr> const & params, buffer<pair<expr, name>> const & nested_aux, declaration const & d):
|
|
m_ngen(ngen), m_params(params), m_aux_decl(d) {
|
|
for (pair<expr, name> const & p : nested_aux) {
|
|
m_aux2nested.insert(p.second, p.first);
|
|
}
|
|
}
|
|
|
|
/* If `c` is an constructor name associated with an auxiliary inductive type, then return the
|
|
nested inductive associated with it and the name of its inductive type. Return none. */
|
|
optional<pair<expr, name>> get_nested_if_aux_constructor(environment const & aux_env, name const & c) const {
|
|
optional<constant_info> info = aux_env.find(c);
|
|
if (!info || !info->is_constructor()) return optional<pair<expr, name>>();
|
|
name auxI_name = info->to_constructor_val().get_induct();
|
|
expr const * nested = m_aux2nested.find(auxI_name);
|
|
if (!nested) return optional<pair<expr, name>>();
|
|
return optional<pair<expr, name>>(*nested, auxI_name);
|
|
}
|
|
|
|
name restore_constructor_name(environment const & aux_env, name const & cnstr_name) const {
|
|
optional<pair<expr, name>> p = get_nested_if_aux_constructor(aux_env, cnstr_name);
|
|
lean_assert(p);
|
|
expr const & I = get_app_fn(p->first);
|
|
lean_assert(is_constant(I));
|
|
return cnstr_name.replace_prefix(p->second, const_name(I));
|
|
}
|
|
|
|
expr restore_nested(expr e, environment const & aux_env, name_map<name> const & aux_rec_name_map = name_map<name>()) {
|
|
local_ctx lctx;
|
|
buffer<expr> As;
|
|
bool pi = is_pi(e);
|
|
for (unsigned i = 0; i < m_params.size(); i++) {
|
|
lean_assert(is_pi(e) || is_lambda(e));
|
|
As.push_back(lctx.mk_local_decl(m_ngen, binding_name(e), binding_domain(e), binding_info(e)));
|
|
e = instantiate(binding_body(e), As.back());
|
|
}
|
|
e = replace(e, [&](expr const & t, unsigned) {
|
|
if (is_constant(t)) {
|
|
if (name const * rec_name = aux_rec_name_map.find(const_name(t))) {
|
|
return some_expr(mk_constant(*rec_name, const_levels(t)));
|
|
}
|
|
}
|
|
expr const & fn = get_app_fn(t);
|
|
if (is_constant(fn)) {
|
|
if (expr const * nested = m_aux2nested.find(const_name(fn))) {
|
|
buffer<expr> args;
|
|
get_app_args(t, args);
|
|
lean_assert(args.size() >= m_params.size());
|
|
expr new_t = instantiate_rev(abstract(*nested, m_params.size(), m_params.data()), As.size(), As.data());
|
|
return some_expr(mk_app(new_t, args.size() - m_params.size(), args.data() + m_params.size()));
|
|
}
|
|
if (optional<pair<expr, name>> r = get_nested_if_aux_constructor(aux_env, const_name(fn))) {
|
|
expr nested = r->first;
|
|
name auxI_name = r->second;
|
|
/* `t` is a constructor-application of an auxiliary inductive type */
|
|
buffer<expr> args;
|
|
get_app_args(t, args);
|
|
lean_assert(args.size() >= m_params.size());
|
|
expr new_nested = instantiate_rev(abstract(nested, m_params.size(), m_params.data()), As.size(), As.data());
|
|
buffer<expr> I_args;
|
|
expr I = get_app_args(new_nested, I_args);
|
|
lean_assert(is_constant(I));
|
|
name new_fn_name = const_name(fn).replace_prefix(auxI_name, const_name(I));
|
|
expr new_fn = mk_constant(new_fn_name, const_levels(I));
|
|
expr new_t = mk_app(mk_app(new_fn, I_args), args.size() - m_params.size(), args.data() + m_params.size());
|
|
return some_expr(new_t);
|
|
}
|
|
}
|
|
return none_expr();
|
|
});
|
|
return pi ? lctx.mk_pi(As, e) : lctx.mk_lambda(As, e);
|
|
}
|
|
};
|
|
|
|
/* Eliminate nested inductive datatypes by creating a new (auxiliary) declaration which contains and inductive types in `d`
|
|
and copies of the nested inductive datatypes used in `d`. For each nested occurrence `I Ds is` where `I` is a nested inductive
|
|
datatype and `Ds` are the parametric arguments and `is` the indices, we create an auxiliary type `Iaux` in the (mutual) inductive
|
|
declaration `d`, and replace `I Ds is` with `Iaux As is` where `As` are `d`'s parameters.
|
|
Moreover, we add the pair `(I Ds, Iaux)` to `nested_aux`.
|
|
|
|
Note that, `As` and `Ds` may have a different sizes. */
|
|
struct elim_nested_inductive_fn {
|
|
environment const & m_env;
|
|
declaration const & m_d;
|
|
name_generator m_ngen;
|
|
local_ctx m_params_lctx;
|
|
buffer<expr> m_params;
|
|
buffer<pair<expr, name>> m_nested_aux; /* The expressions stored here contains free vars in `m_params` */
|
|
levels m_lvls;
|
|
buffer<inductive_type> m_new_types;
|
|
unsigned m_next_idx{1};
|
|
|
|
elim_nested_inductive_fn(environment const & env, declaration const & d):
|
|
m_env(env), m_d(d), m_ngen(*g_nested_fresh) {
|
|
m_lvls = lparams_to_levels(inductive_decl(m_d).get_lparams());
|
|
}
|
|
|
|
name mk_unique_name(name const & n) {
|
|
while (true) {
|
|
name r = n.append_after(m_next_idx);
|
|
m_next_idx++;
|
|
if (!m_env.find(r)) return r;
|
|
}
|
|
}
|
|
|
|
void throw_ill_formed() {
|
|
throw kernel_exception(m_env, "invalid nested inductive datatype, ill-formed declaration");
|
|
}
|
|
|
|
expr replace_params(expr const & e, buffer<expr> const & As) {
|
|
lean_assert(m_params.size() == As.size());
|
|
return instantiate_rev(abstract(e, As.size(), As.data()), m_params.size(), m_params.data());
|
|
}
|
|
|
|
/* IF `e` is of the form `I Ds is` where
|
|
1) `I` is a nested inductive datatype (i.e., a previously declared inductive datatype),
|
|
2) the parametric arguments `Ds` do not contain loose bound variables, and do contain inductive datatypes in `m_new_types`
|
|
THEN return the `inductive_val` in the `constant_info` associated with `I`.
|
|
Otherwise, return none. */
|
|
optional<inductive_val> is_nested_inductive_app(expr const & e) {
|
|
if (!is_app(e)) return optional<inductive_val>();
|
|
expr const & fn = get_app_fn(e);
|
|
if (!is_constant(fn)) return optional<inductive_val>();
|
|
optional<constant_info> info = m_env.find(const_name(fn));
|
|
if (!info || !info->is_inductive()) return optional<inductive_val>();
|
|
buffer<expr> args;
|
|
get_app_args(e, args);
|
|
unsigned nparams = info->to_inductive_val().get_nparams();
|
|
if (nparams > args.size()) return optional<inductive_val>();
|
|
bool is_nested = false;
|
|
bool loose_bvars = false;
|
|
for (unsigned i = 0; i < nparams; i++) {
|
|
if (has_loose_bvars(args[i])) {
|
|
loose_bvars = true;
|
|
}
|
|
if (find(args[i], [&](expr const & t, unsigned) {
|
|
if (is_constant(t)) {
|
|
for (inductive_type const & ind_type : m_new_types) {
|
|
if (const_name(t) == ind_type.get_name())
|
|
return true;
|
|
}
|
|
}
|
|
return false;
|
|
})) {
|
|
is_nested = true;
|
|
}
|
|
}
|
|
if (!is_nested) return optional<inductive_val>();
|
|
if (loose_bvars)
|
|
throw kernel_exception(m_env, sstream() << "invalid nested inductive datatype '" << const_name(fn) << "', nested inductive datatypes parameters cannot contain local variables.");
|
|
return optional<inductive_val>(info->to_inductive_val());
|
|
}
|
|
|
|
expr instantiate_pi_params(expr e, unsigned nparams, expr const * params) {
|
|
for (unsigned i = 0; i < nparams; i++) {
|
|
if (!is_pi(e)) throw_ill_formed();
|
|
e = binding_body(e);
|
|
}
|
|
return instantiate_rev(e, nparams, params);
|
|
}
|
|
|
|
/* If `e` is a nested occurrence `I Ds is`, return `Iaux As is` */
|
|
optional<expr> replace_if_nested(local_ctx const & lctx, buffer<expr> const & As, expr const & e) {
|
|
optional<inductive_val> I_val = is_nested_inductive_app(e);
|
|
if (!I_val) return none_expr();
|
|
/* `e` is of the form `I As is` where `As` are the parameters and `is` the indices */
|
|
buffer<expr> args;
|
|
expr const & fn = get_app_args(e, args);
|
|
name const & I_name = const_name(fn);
|
|
levels const & I_lvls = const_levels(fn);
|
|
lean_assert(I_val->get_nparams() <= args.size());
|
|
unsigned I_nparams = I_val->get_nparams();
|
|
expr IAs = mk_app(fn, I_nparams, args.data()); /* `I As` */
|
|
/* Check whether we have already created an auxiliary inductive_type for `I As` */
|
|
optional<name> auxI_name;
|
|
/* Replace `As` with `m_params` before searching at `m_nested_aux`.
|
|
We need this step because we re-create parameters for each constructor with the correct binding info */
|
|
expr Iparams = replace_params(IAs, As);
|
|
for (pair<expr, name> const & p : m_nested_aux) {
|
|
/* Remark: we could have used `is_def_eq` here instead of structural equality.
|
|
It is probably not needed, but if one day we decide to do it, we have to populate
|
|
an auxiliary environment with the inductive datatypes we are defining since `p.first` and `Iparams`
|
|
contain references to them. */
|
|
if (p.first == Iparams) {
|
|
auxI_name = p.second;
|
|
break;
|
|
}
|
|
}
|
|
if (auxI_name) {
|
|
expr auxI = mk_constant(*auxI_name, m_lvls);
|
|
auxI = mk_app(auxI, As);
|
|
return some_expr(mk_app(auxI, args.size() - I_nparams, args.data() + I_nparams));
|
|
} else {
|
|
optional<expr> result;
|
|
/* We should copy all inductive datatypes `J` in the mutual declaration containing `I` to
|
|
the `m_new_types` mutual declaration as new auxiliary types. */
|
|
for (name const & J_name : I_val->get_all()) {
|
|
constant_info J_info = m_env.get(J_name);
|
|
lean_assert(J_info.is_inductive());
|
|
expr J = mk_constant(J_name, I_lvls);
|
|
expr JAs = mk_app(J, I_nparams, args.data());
|
|
name auxJ_name = mk_unique_name(*g_nested + J_name);
|
|
expr auxJ_type = instantiate_lparams(J_info.get_type(), J_info.get_lparams(), I_lvls);
|
|
auxJ_type = instantiate_pi_params(auxJ_type, I_nparams, args.data());
|
|
auxJ_type = lctx.mk_pi(As, auxJ_type);
|
|
m_nested_aux.push_back(mk_pair(replace_params(JAs, As), auxJ_name));
|
|
if (J_name == I_name) {
|
|
/* Create result */
|
|
expr auxI = mk_constant(auxJ_name, m_lvls);
|
|
auxI = mk_app(auxI, As);
|
|
result = mk_app(auxI, args.size() - I_nparams, args.data() + I_nparams);
|
|
}
|
|
buffer<constructor> auxJ_constructors;
|
|
for (name const & J_cnstr_name : J_info.to_inductive_val().get_cnstrs()) {
|
|
constant_info J_cnstr_info = m_env.get(J_cnstr_name);
|
|
name auxJ_cnstr_name = J_cnstr_name.replace_prefix(J_name, auxJ_name);
|
|
/* auxJ_cnstr_type still has references to `J`, this will be fixed later when we process it. */
|
|
expr auxJ_cnstr_type = instantiate_lparams(J_cnstr_info.get_type(), J_cnstr_info.get_lparams(), I_lvls);
|
|
auxJ_cnstr_type = instantiate_pi_params(auxJ_cnstr_type, I_nparams, args.data());
|
|
auxJ_cnstr_type = lctx.mk_pi(As, auxJ_cnstr_type);
|
|
auxJ_constructors.push_back(constructor(auxJ_cnstr_name, auxJ_cnstr_type));
|
|
}
|
|
m_new_types.push_back(inductive_type(auxJ_name, auxJ_type, constructors(auxJ_constructors)));
|
|
}
|
|
lean_assert(result);
|
|
return result;
|
|
}
|
|
}
|
|
|
|
/* Replace all nested inductive datatype occurrences in `e`. */
|
|
expr replace_all_nested(local_ctx const & lctx, buffer<expr> const & As, expr const & e) {
|
|
return replace(e, [&](expr const & e, unsigned) { return replace_if_nested(lctx, As, e); });
|
|
}
|
|
|
|
expr get_params(expr type, unsigned nparams, local_ctx & lctx, buffer<expr> & params) {
|
|
lean_assert(params.empty());
|
|
for (unsigned i = 0; i < nparams; i++) {
|
|
if (!is_pi(type)) throw kernel_exception(m_env, "invalid inductive datatype declaration, incorrect number of parameters");
|
|
params.push_back(lctx.mk_local_decl(m_ngen, binding_name(type), binding_domain(type), binding_info(type)));
|
|
type = instantiate(binding_body(type), params.back());
|
|
}
|
|
return type;
|
|
}
|
|
|
|
elim_nested_inductive_result operator()() {
|
|
inductive_decl ind_d(m_d);
|
|
if (!ind_d.get_nparams().is_small()) throw_ill_formed();
|
|
unsigned d_nparams = ind_d.get_nparams().get_small_value();
|
|
to_buffer(ind_d.get_types(), m_new_types);
|
|
if (m_new_types.size() == 0) throw kernel_exception(m_env, "invalid empty (mutual) inductive datatype declaration, it must contain at least one inductive type.");
|
|
/* initialize m_params and m_params_lctx */
|
|
get_params(m_new_types[0].get_type(), d_nparams, m_params_lctx, m_params);
|
|
unsigned qhead = 0;
|
|
/* Main elimination loop. */
|
|
while (qhead < m_new_types.size()) {
|
|
inductive_type ind_type = m_new_types[qhead];
|
|
buffer<constructor> new_cnstrs;
|
|
for (constructor cnstr : ind_type.get_cnstrs()) {
|
|
expr cnstr_type = constructor_type(cnstr);
|
|
local_ctx lctx;
|
|
buffer<expr> As;
|
|
/* Consume parameters.
|
|
|
|
We (re-)create the parameters for each constructor because we want to preserve the binding_info. */
|
|
cnstr_type = get_params(cnstr_type, d_nparams, lctx, As);
|
|
lean_assert(As.size() == d_nparams);
|
|
expr new_cnstr_type = replace_all_nested(lctx, As, cnstr_type);
|
|
new_cnstr_type = lctx.mk_pi(As, new_cnstr_type);
|
|
new_cnstrs.push_back(constructor(constructor_name(cnstr), new_cnstr_type));
|
|
}
|
|
m_new_types[qhead] = inductive_type(ind_type.get_name(), ind_type.get_type(), constructors(new_cnstrs));
|
|
qhead++;
|
|
}
|
|
declaration aux_decl = mk_inductive_decl(ind_d.get_lparams(), ind_d.get_nparams(), inductive_types(m_new_types), ind_d.is_unsafe());
|
|
return elim_nested_inductive_result(m_ngen, m_params, m_nested_aux, aux_decl);
|
|
}
|
|
};
|
|
|
|
/* Given the auxiliary environment `aux_env` generated by processing the auxiliary mutual declaration,
|
|
and the original declaration `d`. This function return a pair `(aux_rec_names, aux_rec_name_map)`
|
|
where `aux_rec_names` contains the recursor names associated to auxiliary inductive types used to
|
|
eliminated nested inductive occurrences.
|
|
The mapping `aux_rec_name_map` contains an entry `(aux_rec_name -> rec_name)` for each
|
|
element in `aux_rec_names`. It provides the new names for these recursors.
|
|
|
|
We compute the new recursor names using the first inductive datatype in the original declaration `d`,
|
|
and the suffice `.rec_<idx>`. */
|
|
static pair<names, name_map<name>> mk_aux_rec_name_map(environment const & aux_env, inductive_decl const & d) {
|
|
unsigned ntypes = length(d.get_types());
|
|
lean_assert(ntypes > 0);
|
|
inductive_type const & main_type = head(d.get_types());
|
|
name const & main_name = main_type.get_name();
|
|
constant_info main_info = aux_env.get(main_name);
|
|
names const & all_names = main_info.to_inductive_val().get_all();
|
|
/* This function is only called if we have created auxiliary inductive types when eliminating
|
|
the nested inductives. */
|
|
lean_assert(length(all_names) > ntypes);
|
|
/* Remark: we use the `main_name` to declarate the auxiliary recursors as: <main_name>.rec_1, <main_name>.rec_2, ...
|
|
This is a little bit asymmetrical if `d` is a mutual declaration, but it makes sure we have simple names. */
|
|
buffer<name> old_rec_names;
|
|
name_map<name> rec_map;
|
|
unsigned i = 0;
|
|
unsigned next_idx = 1;
|
|
for (name const & ind_name : all_names) {
|
|
if (i >= ntypes) {
|
|
old_rec_names.push_back(mk_rec_name(ind_name));
|
|
name new_rec_name = mk_rec_name(main_name).append_after(next_idx);
|
|
next_idx++;
|
|
rec_map.insert(old_rec_names.back(), new_rec_name);
|
|
}
|
|
i++;
|
|
}
|
|
return mk_pair(names(old_rec_names), rec_map);
|
|
}
|
|
|
|
environment environment::add_inductive(declaration const & d) const {
|
|
elim_nested_inductive_result res = elim_nested_inductive_fn(*this, d)();
|
|
bool is_nested = !res.m_aux2nested.empty();
|
|
environment aux_env = add_inductive_fn(*this, inductive_decl(res.m_aux_decl), is_nested)();
|
|
if (!is_nested) {
|
|
/* `d` did not contain nested inductive types. */
|
|
return aux_env;
|
|
} else {
|
|
/* Restore nested inductives. */
|
|
inductive_decl ind_d(d);
|
|
names all_ind_names = get_all_inductive_names(ind_d);
|
|
names aux_rec_names; name_map<name> aux_rec_name_map;
|
|
std::tie(aux_rec_names, aux_rec_name_map) = mk_aux_rec_name_map(aux_env, d);
|
|
environment new_env = *this;
|
|
auto process_rec = [&](name const & rec_name) {
|
|
name new_rec_name = rec_name;
|
|
if (name const * new_name = aux_rec_name_map.find(rec_name))
|
|
new_rec_name = *new_name;
|
|
constant_info rec_info = aux_env.get(rec_name);
|
|
expr new_rec_type = res.restore_nested(rec_info.get_type(), aux_env, aux_rec_name_map);
|
|
recursor_val rec_val = rec_info.to_recursor_val();
|
|
buffer<recursor_rule> new_rules;
|
|
for (recursor_rule const & rule : rec_val.get_rules()) {
|
|
expr new_rhs = res.restore_nested(rule.get_rhs(), aux_env, aux_rec_name_map);
|
|
name cnstr_name = rule.get_cnstr();
|
|
name new_cnstr_name = cnstr_name;
|
|
if (new_rec_name != rec_name) {
|
|
/* We need to fix the constructor name */
|
|
new_cnstr_name = res.restore_constructor_name(aux_env, cnstr_name);
|
|
}
|
|
new_rules.push_back(recursor_rule(new_cnstr_name, rule.get_nfields(), new_rhs));
|
|
}
|
|
new_env.check_name(new_rec_name);
|
|
new_env.add_core(constant_info(recursor_val(new_rec_name, rec_info.get_lparams(), new_rec_type,
|
|
all_ind_names, rec_val.get_nparams(), rec_val.get_nindices(), rec_val.get_nmotives(),
|
|
rec_val.get_nminors(), recursor_rules(new_rules),
|
|
rec_val.is_k(), rec_val.is_unsafe())));
|
|
};
|
|
for (inductive_type const & ind_type : ind_d.get_types()) {
|
|
constant_info ind_info = aux_env.get(ind_type.get_name());
|
|
inductive_val ind_val = ind_info.to_inductive_val();
|
|
/* We just need to "fix" the `all` fields for ind_info.
|
|
|
|
Remark: if we decide to store the recursor names, we will also need to fix it. */
|
|
new_env.add_core(constant_info(inductive_val(ind_info.get_name(), ind_info.get_lparams(), ind_info.get_type(),
|
|
ind_val.get_nparams(), ind_val.get_nindices(),
|
|
all_ind_names, ind_val.get_cnstrs(),
|
|
ind_val.is_rec(), ind_val.is_unsafe(), ind_val.is_reflexive(), ind_val.is_nested())));
|
|
for (name const & cnstr_name : ind_val.get_cnstrs()) {
|
|
constant_info cnstr_info = aux_env.get(cnstr_name);
|
|
constructor_val cnstr_val = cnstr_info.to_constructor_val();
|
|
expr new_type = res.restore_nested(cnstr_info.get_type(), aux_env);
|
|
new_env.add_core(constant_info(constructor_val(cnstr_info.get_name(), cnstr_info.get_lparams(), new_type,
|
|
cnstr_val.get_induct(), cnstr_val.get_cidx(), cnstr_val.get_nparams(),
|
|
cnstr_val.get_nfields(), cnstr_val.is_unsafe())));
|
|
}
|
|
process_rec(mk_rec_name(ind_type.get_name()));
|
|
}
|
|
for (name const & aux_rec : aux_rec_names) {
|
|
process_rec(aux_rec);
|
|
}
|
|
return new_env;
|
|
}
|
|
}
|
|
|
|
static expr * g_nat_zero = nullptr;
|
|
static expr * g_nat_succ = nullptr;
|
|
static expr * g_string_mk = nullptr;
|
|
static expr * g_list_cons_char = nullptr;
|
|
static expr * g_list_nil_char = nullptr;
|
|
static expr * g_char_of_nat = nullptr;
|
|
|
|
expr nat_lit_to_constructor(expr const & e) {
|
|
lean_assert(is_nat_lit(e));
|
|
nat const & v = lit_value(e).get_nat();
|
|
if (v == 0u)
|
|
return *g_nat_zero;
|
|
else
|
|
return mk_app(*g_nat_succ, mk_lit(literal(v - nat(1))));
|
|
}
|
|
|
|
expr string_lit_to_constructor(expr const & e) {
|
|
lean_assert(is_string_lit(e));
|
|
string_ref const & s = lit_value(e).get_string();
|
|
std::vector<unsigned> cs;
|
|
utf8_decode(s.to_std_string(), cs);
|
|
expr r = *g_list_nil_char;
|
|
unsigned i = cs.size();
|
|
while (i > 0) {
|
|
i--;
|
|
r = mk_app(*g_list_cons_char, mk_app(*g_char_of_nat, mk_lit(literal(cs[i]))), r);
|
|
}
|
|
return mk_app(*g_string_mk, r);
|
|
}
|
|
|
|
|
|
void initialize_inductive() {
|
|
g_nested = new name("_nested");
|
|
mark_persistent(g_nested->raw());
|
|
g_ind_fresh = new name("_ind_fresh");
|
|
mark_persistent(g_ind_fresh->raw());
|
|
g_nested_fresh = new name("_nested_fresh");
|
|
mark_persistent(g_nested_fresh->raw());
|
|
g_nat_zero = new expr(mk_constant(name{"Nat", "zero"}));
|
|
mark_persistent(g_nat_zero->raw());
|
|
g_nat_succ = new expr(mk_constant(name{"Nat", "succ"}));
|
|
mark_persistent(g_nat_succ->raw());
|
|
g_string_mk = new expr(mk_constant(name{"String", "mk"}));
|
|
mark_persistent(g_string_mk->raw());
|
|
expr char_type = mk_constant(name{"Char"});
|
|
g_list_cons_char = new expr(mk_app(mk_constant(name{"List", "cons"}, {level()}), char_type));
|
|
mark_persistent(g_list_cons_char->raw());
|
|
g_list_nil_char = new expr(mk_app(mk_constant(name{"List", "nil"}, {level()}), char_type));
|
|
mark_persistent(g_list_nil_char->raw());
|
|
g_char_of_nat = new expr(mk_constant(name{"Char", "ofNat"}));
|
|
mark_persistent(g_char_of_nat->raw());
|
|
register_name_generator_prefix(*g_ind_fresh);
|
|
register_name_generator_prefix(*g_nested_fresh);
|
|
}
|
|
|
|
void finalize_inductive() {
|
|
delete g_nested;
|
|
delete g_ind_fresh;
|
|
delete g_nested_fresh;
|
|
delete g_nat_succ;
|
|
delete g_nat_zero;
|
|
delete g_string_mk;
|
|
delete g_list_cons_char;
|
|
delete g_list_nil_char;
|
|
}
|
|
}
|