feat(library/constructions/no_confusion): add no_confusion_type for new inductive datatype module
This commit is contained in:
Leonardo de Moura
parent
9970019f76
commit
4773a3be5f
9 changed files with 218 additions and 18 deletions
|
|
@ -402,11 +402,25 @@ auto elaborator::get_elim_info_for_builtin(name const & fn) -> elim_info {
|
|||
only works for dependent elimination. */
|
||||
lean_assert(!fn.is_atomic());
|
||||
name const & I_name = fn.get_prefix();
|
||||
optional<inductive::inductive_decl> decl = inductive::is_inductive_decl(m_env, I_name);
|
||||
lean_assert(decl);
|
||||
unsigned nparams = decl->m_num_params;
|
||||
unsigned nindices = *inductive::get_num_indices(m_env, I_name);
|
||||
unsigned nminors = length(decl->m_intro_rules);
|
||||
|
||||
unsigned nparams;
|
||||
unsigned nindices;
|
||||
unsigned nminors;
|
||||
|
||||
// TODO(Leo): delete "then"-branch
|
||||
if (optional<inductive::inductive_decl> decl = inductive::is_inductive_decl(m_env, I_name)) {
|
||||
nparams = decl->m_num_params;
|
||||
nindices = *inductive::get_num_indices(m_env, I_name);
|
||||
nminors = length(decl->m_intro_rules);
|
||||
} else {
|
||||
constant_info I_info = m_env.get(I_name);
|
||||
lean_assert(I_info.is_inductive());
|
||||
inductive_val I_val = I_info.to_inductive_val();
|
||||
nparams = I_val.get_nparams();
|
||||
nindices = I_val.get_nindices();
|
||||
nminors = length(I_val.get_cnstrs());
|
||||
}
|
||||
|
||||
elim_info r;
|
||||
if (fn.get_string() == "brec_on" || fn.get_string() == "binduction_on") {
|
||||
r.m_arity = nparams + 1 /* motive */ + nindices + 1 /* major */ + 1;
|
||||
|
|
|
|||
|
|
@ -33,6 +33,7 @@ Authors: Daniel Selsam, Leonardo de Moura
|
|||
#include "library/tactic/tactic_evaluator.h"
|
||||
#include "library/constructions/cases_on.h"
|
||||
#include "library/constructions/rec_on.h"
|
||||
#include "library/constructions/no_confusion.h"
|
||||
#include "frontends/lean/decl_cmds.h"
|
||||
#include "frontends/lean/decl_util.h"
|
||||
#include "frontends/lean/util.h"
|
||||
|
|
@ -734,9 +735,19 @@ 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));
|
||||
|
||||
bool has_eq = has_eq_decls(m_env);
|
||||
bool has_heq = has_heq_decls(m_env);
|
||||
bool has_unit = has_punit_decls(m_env);
|
||||
// bool has_prod = has_pprod_decls(m_env);
|
||||
|
||||
for (inductive_type const & ind_type : ind_types) {
|
||||
m_env = mk_rec_on(m_env, ind_type.get_name());
|
||||
m_env = mk_cases_on(m_env, ind_type.get_name());
|
||||
if (has_unit) {
|
||||
m_env = mk_cases_on(m_env, ind_type.get_name());
|
||||
if (has_eq && has_heq)
|
||||
m_env = mk_no_confusion(m_env, ind_type.get_name());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1272,7 +1272,7 @@ struct structure_cmd_fn {
|
|||
return;
|
||||
if (!has_heq_decls(m_env))
|
||||
return;
|
||||
m_env = mk_no_confusion(m_env, m_name);
|
||||
m_env = old_mk_no_confusion(m_env, m_name);
|
||||
name no_confusion_name(m_name, "no_confusion");
|
||||
add_alias(no_confusion_name);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@ Author: Leonardo de Moura
|
|||
#include "kernel/abstract.h"
|
||||
#include "kernel/inductive/inductive.h"
|
||||
#include "kernel/old_type_checker.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "library/protected.h"
|
||||
#include "library/module.h"
|
||||
#include "library/util.h"
|
||||
|
|
@ -19,12 +20,14 @@ Author: Leonardo de Moura
|
|||
#include "library/aux_recursors.h"
|
||||
#include "library/constructions/util.h"
|
||||
|
||||
#include "library/trace.h"
|
||||
|
||||
namespace lean {
|
||||
static void throw_corrupted(name const & n) {
|
||||
throw exception(sstream() << "error in 'no_confusion' generation, '" << n << "' inductive datatype declaration is corrupted");
|
||||
}
|
||||
|
||||
optional<environment> mk_no_confusion_type(environment const & env, name const & n) {
|
||||
static optional<environment> old_mk_no_confusion_type(environment const & env, name const & n) {
|
||||
optional<inductive::inductive_decl> decl = inductive::is_inductive_decl(env, n);
|
||||
if (!decl)
|
||||
throw exception(sstream() << "error in 'no_confusion' generation, '" << n << "' is not an inductive datatype");
|
||||
|
|
@ -128,8 +131,8 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
|
|||
return some(add_protected(new_env, no_confusion_type_name));
|
||||
}
|
||||
|
||||
environment mk_no_confusion(environment const & env, name const & n) {
|
||||
optional<environment> env1 = mk_no_confusion_type(env, n);
|
||||
environment old_mk_no_confusion(environment const & env, name const & n) {
|
||||
optional<environment> env1 = old_mk_no_confusion_type(env, n);
|
||||
if (!env1)
|
||||
return env;
|
||||
environment new_env = *env1;
|
||||
|
|
@ -238,4 +241,116 @@ environment mk_no_confusion(environment const & env, name const & n) {
|
|||
new_env = add_no_confusion(new_env, no_confusion_name);
|
||||
return add_protected(new_env, no_confusion_name);
|
||||
}
|
||||
|
||||
|
||||
static optional<environment> mk_no_confusion_type(environment const & env, name const & n) {
|
||||
constant_info ind_info = env.get(n);
|
||||
if (!ind_info.is_inductive() || !can_elim_to_type(env, n))
|
||||
return optional<environment>();
|
||||
inductive_val ind_val = ind_info.to_inductive_val();
|
||||
local_ctx lctx;
|
||||
name_generator ngen = mk_constructions_name_generator();
|
||||
unsigned nparams = ind_val.get_nparams();
|
||||
constant_info cases_info = env.get(name(n, "cases_on"));
|
||||
names lps = cases_info.get_lparams();
|
||||
level plvl = mk_univ_param(head(lps));
|
||||
levels ilvls = lparams_to_levels(tail(lps));
|
||||
level rlvl = plvl;
|
||||
expr ind_type = instantiate_type_lparams(ind_info, ilvls);
|
||||
/* All inductive datatype parameters and indices are arguments */
|
||||
buffer<expr> args;
|
||||
ind_type = to_telescope(lctx, ngen, ind_type, args, some(mk_implicit_binder_info()));
|
||||
if (!is_sort(ind_type) || args.size() < nparams)
|
||||
throw_corrupted(n);
|
||||
level ind_lvl = sort_level(ind_type);
|
||||
unsigned nindices = ind_val.get_nindices();
|
||||
lean_assert(nindices == args.size() - nparams);
|
||||
/* Create inductive datatype */
|
||||
expr I = mk_app(mk_constant(n, ilvls), args);
|
||||
/* Add (P : Type) */
|
||||
expr P = lctx.mk_local_decl(ngen, "P", mk_sort(plvl), mk_binder_info());
|
||||
args.push_back(P);
|
||||
/* Add v1 and v2 elements of the inductive type */
|
||||
expr v1 = lctx.mk_local_decl(ngen, "v1", I, mk_binder_info());
|
||||
expr v2 = lctx.mk_local_decl(ngen, "v2", I, mk_binder_info());
|
||||
args.push_back(v1);
|
||||
args.push_back(v2);
|
||||
expr R = mk_sort(rlvl);
|
||||
expr Pres = P;
|
||||
name no_confusion_type_name{n, "no_confusion_type"};
|
||||
expr no_confusion_type_type = lctx.mk_pi(args, R);
|
||||
/* Create type former */
|
||||
buffer<expr> type_former_args;
|
||||
for (unsigned i = nparams; i < nparams + nindices; i++)
|
||||
type_former_args.push_back(args[i]);
|
||||
type_former_args.push_back(v1);
|
||||
expr type_former = lctx.mk_lambda(type_former_args, R);
|
||||
/* Create cases_on */
|
||||
levels clvls = levels(mk_succ(rlvl), ilvls);
|
||||
expr cases_on = mk_app(mk_app(mk_constant(cases_info.get_name(), clvls), nparams, args.data()), type_former);
|
||||
cases_on = mk_app(cases_on, nindices, args.data() + nparams);
|
||||
expr cases_on1 = mk_app(cases_on, v1);
|
||||
expr cases_on2 = mk_app(cases_on, v2);
|
||||
expr t1 = type_checker(env, lctx).infer(cases_on1);
|
||||
expr t2 = type_checker(env, lctx).infer(cases_on2);
|
||||
buffer<expr> outer_cases_on_args;
|
||||
unsigned idx1 = 0;
|
||||
while (is_pi(t1)) {
|
||||
buffer<expr> minor1_args;
|
||||
expr minor1 = to_telescope(env, lctx, ngen, binding_domain(t1), minor1_args);
|
||||
expr curr_t2 = t2;
|
||||
buffer<expr> inner_cases_on_args;
|
||||
unsigned idx2 = 0;
|
||||
while (is_pi(curr_t2)) {
|
||||
buffer<expr> minor2_args;
|
||||
expr minor2 = to_telescope(env, lctx, ngen, binding_domain(curr_t2), minor2_args);
|
||||
if (idx1 != idx2) {
|
||||
// infeasible case, constructors do not match
|
||||
inner_cases_on_args.push_back(lctx.mk_lambda(minor2_args, Pres));
|
||||
} else {
|
||||
if (minor1_args.size() != minor2_args.size())
|
||||
throw_corrupted(n);
|
||||
buffer<expr> rtype_hyp;
|
||||
// add equalities
|
||||
for (unsigned i = 0; i < minor1_args.size(); i++) {
|
||||
expr lhs = minor1_args[i];
|
||||
expr rhs = minor2_args[i];
|
||||
expr lhs_type = lctx.get_type(lhs);
|
||||
if (!type_checker(env, lctx).is_prop(lhs_type)) {
|
||||
expr rhs_type = lctx.get_type(rhs);
|
||||
level l = sort_level(type_checker(env, lctx).ensure_type(lhs_type));
|
||||
expr h_type;
|
||||
if (type_checker(env, lctx).is_def_eq(lhs_type, rhs_type)) {
|
||||
h_type = mk_app(mk_constant(get_eq_name(), levels(l)), lhs_type, lhs, rhs);
|
||||
} else {
|
||||
h_type = mk_app(mk_constant(get_heq_name(), levels(l)), lhs_type, lhs, rhs_type, rhs);
|
||||
}
|
||||
name lhs_user_name = lctx.get_local_decl(lhs).get_user_name();
|
||||
rtype_hyp.push_back(lctx.mk_local_decl(ngen, lhs_user_name.append_after("_eq"), h_type, mk_binder_info()));
|
||||
}
|
||||
}
|
||||
inner_cases_on_args.push_back(lctx.mk_lambda(minor2_args, mk_arrow(lctx.mk_pi(rtype_hyp, P), Pres)));
|
||||
}
|
||||
idx2++;
|
||||
curr_t2 = binding_body(curr_t2);
|
||||
}
|
||||
outer_cases_on_args.push_back(lctx.mk_lambda(minor1_args, mk_app(cases_on2, inner_cases_on_args)));
|
||||
idx1++;
|
||||
t1 = binding_body(t1);
|
||||
}
|
||||
expr no_confusion_type_value = lctx.mk_lambda(args, mk_app(cases_on1, outer_cases_on_args));
|
||||
declaration new_d = mk_definition_inferring_meta(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value,
|
||||
reducibility_hints::mk_abbreviation());
|
||||
environment new_env = module::add(env, new_d);
|
||||
new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible, true);
|
||||
return some(add_protected(new_env, no_confusion_type_name));
|
||||
}
|
||||
|
||||
environment mk_no_confusion(environment const & env, name const & n) {
|
||||
optional<environment> env1 = mk_no_confusion_type(env, n);
|
||||
if (!env1)
|
||||
return env;
|
||||
// TODO(Leo)
|
||||
return *env1;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -15,5 +15,6 @@ namespace lean {
|
|||
If the environment has an impredicative Prop, it also assumes heq is defined.
|
||||
If the environment does not have an impredicative Prop, then it also assumes lift is defined.
|
||||
*/
|
||||
environment old_mk_no_confusion(environment const & env, name const & n);
|
||||
environment mk_no_confusion(environment const & env, name const & n);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -91,7 +91,7 @@ class add_basic_inductive_decl_fn {
|
|||
|
||||
if (gen_cases_on && gen_no_confusion && has_eq && has_heq) {
|
||||
lean_trace(name({"inductive_compiler"}), tout() << ">> generate no_confusion\n";);
|
||||
m_env = mk_no_confusion(m_env, ind_name);
|
||||
m_env = old_mk_no_confusion(m_env, ind_name);
|
||||
}
|
||||
|
||||
if (gen_brec_on && has_prod) {
|
||||
|
|
|
|||
|
|
@ -10,8 +10,10 @@ Author: Leonardo de Moura
|
|||
#include "kernel/find_fn.h"
|
||||
#include "kernel/instantiate.h"
|
||||
#include "kernel/old_type_checker.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/abstract_type_context.h"
|
||||
#include "kernel/inductive.h"
|
||||
#include "kernel/inductive/inductive.h"
|
||||
#include "library/error_msgs.h"
|
||||
#include "library/locals.h"
|
||||
|
|
@ -272,10 +274,16 @@ bool is_inductive_predicate(environment const & env, name const & n) {
|
|||
}
|
||||
|
||||
bool can_elim_to_type(environment const & env, name const & n) {
|
||||
if (!inductive::is_inductive_decl(env, n))
|
||||
return false; // n is not inductive datatype
|
||||
// TODO(Leo): delete following if-statement
|
||||
if (inductive::is_inductive_decl(env, n)) {
|
||||
constant_info ind_info = env.get(n);
|
||||
constant_info rec_info = env.get(inductive::get_elim_name(n));
|
||||
return rec_info.get_num_lparams() > ind_info.get_num_lparams();
|
||||
}
|
||||
|
||||
constant_info ind_info = env.get(n);
|
||||
constant_info rec_info = env.get(inductive::get_elim_name(n));
|
||||
if (!ind_info.is_inductive()) return false;
|
||||
constant_info rec_info = env.get(mk_rec_name(n));
|
||||
return rec_info.get_num_lparams() > ind_info.get_num_lparams();
|
||||
}
|
||||
|
||||
|
|
@ -437,6 +445,39 @@ expr to_telescope(old_type_checker & ctx, expr type, buffer<expr> & telescope, o
|
|||
return type;
|
||||
}
|
||||
|
||||
expr to_telescope(bool pi, local_ctx & lctx, name_generator & ngen, expr e, buffer<expr> & telescope, optional<binder_info> const & binfo) {
|
||||
while ((pi && is_pi(e)) || (!pi && is_lambda(e))) {
|
||||
expr local;
|
||||
if (binfo)
|
||||
local = lctx.mk_local_decl(ngen, binding_name(e), binding_domain(e), *binfo);
|
||||
else
|
||||
local = lctx.mk_local_decl(ngen, binding_name(e), binding_domain(e), binding_info(e));
|
||||
telescope.push_back(local);
|
||||
e = instantiate(binding_body(e), local);
|
||||
}
|
||||
return e;
|
||||
}
|
||||
|
||||
expr to_telescope(local_ctx & lctx, name_generator & ngen, expr const & type, buffer<expr> & telescope, optional<binder_info> const & binfo) {
|
||||
return to_telescope(true, lctx, ngen, type, telescope, binfo);
|
||||
}
|
||||
|
||||
expr to_telescope(environment const & env, local_ctx & lctx, name_generator & ngen, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo) {
|
||||
expr new_type = type_checker(env, lctx).whnf(type);
|
||||
while (is_pi(new_type)) {
|
||||
type = new_type;
|
||||
expr local;
|
||||
if (binfo)
|
||||
local = lctx.mk_local_decl(ngen, binding_name(type), binding_domain(type), *binfo);
|
||||
else
|
||||
local = lctx.mk_local_decl(ngen, binding_name(type), binding_domain(type), binding_info(type));
|
||||
telescope.push_back(local);
|
||||
type = instantiate(binding_body(type), local);
|
||||
new_type = type_checker(env, lctx).whnf(type);
|
||||
}
|
||||
return type;
|
||||
}
|
||||
|
||||
/* ----------------------------------------------
|
||||
|
||||
Helper functions for creating basic operations
|
||||
|
|
|
|||
|
|
@ -141,24 +141,41 @@ unsigned get_expect_num_args(abstract_type_context & ctx, expr e);
|
|||
/** \brief "Consume" Pi-type \c type. This procedure creates local constants based on the domain of \c type
|
||||
and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given
|
||||
binder_info, otherwise the procedure uses the one attached in the domain.
|
||||
The procedure returns the "body" of type. */
|
||||
The procedure returns the "body" of type.
|
||||
|
||||
TODO(Leo): delete because it uses old APIs */
|
||||
expr to_telescope(expr const & type, buffer<expr> & telescope,
|
||||
optional<binder_info> const & binfo = optional<binder_info>());
|
||||
|
||||
/** \brief "Consume" fun/lambda. This procedure creates local constants based on the arguments of \c e
|
||||
and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given
|
||||
binder_info, otherwise the procedure uses the one attached to the arguments.
|
||||
The procedure returns the "body" of function. */
|
||||
The procedure returns the "body" of function.
|
||||
|
||||
TODO(Leo): delete because it uses old APIs */
|
||||
expr fun_to_telescope(expr const & e, buffer<expr> & telescope, optional<binder_info> const & binfo);
|
||||
|
||||
/** \brief Similar to previous procedure, but puts \c type in whnf */
|
||||
/** \brief Similar to previous procedure, but puts \c type in whnf
|
||||
|
||||
TODO(Leo): delete because it uses old APIs */
|
||||
expr to_telescope(old_type_checker & ctx, expr type, buffer<expr> & telescope,
|
||||
optional<binder_info> const & binfo = optional<binder_info>());
|
||||
|
||||
/** \brief Return the universe where inductive datatype resides
|
||||
\pre \c ind_type is of the form <tt>Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl}</tt> */
|
||||
\pre \c ind_type is of the form <tt>Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl}</tt>
|
||||
|
||||
TODO(Leo): delete because it uses old APIs */
|
||||
level get_datatype_level(environment const & env, expr const & ind_type);
|
||||
|
||||
/** \brief "Consume" Pi-type `type`. This procedure creates free variables based on the domain of `type` using `lctx`,
|
||||
and store them in telescope and updates . If `binfo` is provided, then the free variables are annotated with
|
||||
the given `binder_info`, otherwise the procedure uses the one attached in the domain.
|
||||
The procedure returns the "body" of type. */
|
||||
expr to_telescope(local_ctx & lctx, name_generator & ngen, expr const & type, buffer<expr> & telescope, optional<binder_info> const & binfo);
|
||||
|
||||
/** \brief Similar to previous procedure, but uses whnf to check whether `type` reduces to `Pi` or not. */
|
||||
expr to_telescope(environment const & env, local_ctx & lctx, name_generator & ngen, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo = optional<binder_info>());
|
||||
|
||||
/** \brief Update the result sort of the given type */
|
||||
expr update_result_sort(expr t, level const & l);
|
||||
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@ inductive term (α : Type) (β : Type)
|
|||
| foo (p : nat → my_pair term (my_list term)) (n : β) : my_list (my_list term) → term
|
||||
|
||||
#check @term.cases_on
|
||||
#print term.no_confusion_type
|
||||
|
||||
inductive arrow (α β : Type)
|
||||
| mk (s : nat → my_pair α β) : arrow
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue