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

fix(*): bugs in the type checker, inductive datatypes, and unifier

Browse source 
The bugs were indentified when performing the tiny change in the file
tests/lean/run/group.lean
This commit is contained in:
Leonardo de Moura 2014-07-06 16:46:34 -07:00
parent 9a13bef4f3
commit dcf7cf00ff
7 changed files with 138 additions and 159 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/kernel/inductive/inductive.cpp
View file

@ -765,9 +765,10 @@ optional<expr> inductive_normalizer_extension::operator()(expr const & e, extens
return none_expr(); // it is not an eliminator
buffer<expr> elim_args;
get_app_args(e, elim_args);
if (elim_args.size() != it1->m_num_ACe + it1->m_num_indices + 1)
return none_expr(); // number of arguments does not match
expr intro_app = ctx.whnf(elim_args.back());
unsigned major_idx = it1->m_num_ACe + it1->m_num_indices;
if (elim_args.size() < major_idx + 1)
return none_expr(); // major premise is missing
expr intro_app = ctx.whnf(elim_args[major_idx]);
expr const & intro_fn = get_app_fn(intro_app);
// Last argument must be a constant and an application of a constant.
if (!is_constant(intro_fn))
@ -800,11 +801,15 @@ optional<expr> inductive_normalizer_extension::operator()(expr const & e, extens
std::reverse(ACebu.begin(), ACebu.end());
expr r = instantiate_univ_params(it2->m_comp_rhs_body, it1->m_level_names, const_levels(elim_fn));
r = instantiate(r, ACebu.size(), ACebu.data());
if (elim_args.size() > major_idx + 1) {
unsigned num_args = elim_args.size() - major_idx - 1;
r = mk_app(r, num_args, elim_args.data() + major_idx + 1);
}
return some_expr(r);
}
// Return true if \c e is of the form (elim ... (?m ...))
bool inductive_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const {
template<typename Ctx>
bool is_elim_meta_app_core(Ctx & ctx, expr const & e) {
inductive_env_ext const & ext = get_extension(ctx.env());
expr const & elim_fn = get_app_fn(e);
if (!is_constant(elim_fn))
@ -814,12 +819,22 @@ bool inductive_normalizer_extension::may_reduce_later(expr const & e, extension_
return false;
buffer<expr> elim_args;
get_app_args(e, elim_args);
if (elim_args.size() != it1->m_num_ACe + it1->m_num_indices + 1)
unsigned major_idx = it1->m_num_ACe + it1->m_num_indices;
if (elim_args.size() < major_idx + 1)
return false;
expr intro_app = ctx.whnf(elim_args.back());
expr intro_app = ctx.whnf(elim_args[major_idx]);
return is_meta(intro_app);
}
bool is_elim_meta_app(type_checker & tc, expr const & e) {
return is_elim_meta_app_core(tc, e);
}
// Return true if \c e is of the form (elim ... (?m ...))
bool inductive_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const {
return is_elim_meta_app_core(ctx, e);
}
optional<inductive_decls> is_inductive_decl(environment const & env, name const & n) {
inductive_env_ext const & ext = get_extension(env);
if (auto it = ext.m_inductive_info.find(n))
@ -843,5 +858,13 @@ optional<name> is_elim_rule(environment const & env, name const & n) {
else
return optional<name>();
}
optional<unsigned> get_elim_major_idx(environment const & env, name const & n) {
inductive_env_ext const & ext = get_extension(env);
if (auto it = ext.m_elim_info.find(n))
return optional<unsigned>(it->m_num_ACe + it->m_num_indices);
else
return optional<unsigned>();
}
}
}

4
src/kernel/inductive/inductive.h
View file

@ -62,5 +62,9 @@ optional<name> is_intro_rule(environment const & env, name const & n);
s.t. \c n is an elimination rule of D. Otherwise, return none.
*/
optional<name> is_elim_rule(environment const & env, name const & n);
/** \brief Given the eliminator \c n, this function return the position of major premise */
optional<unsigned> get_elim_major_idx(environment const & env, name const & n);
bool is_elim_meta_app(type_checker & tc, expr const & e);
}
}

105
src/kernel/type_checker.cpp
View file

@ -24,6 +24,37 @@ Author: Leonardo de Moura
namespace lean {
static name g_x_name("x");
expr replace_range(expr const & type, expr const & new_range) {
if (is_pi(type))
return update_binding(type, binding_domain(type), replace_range(binding_body(type), new_range));
else
return new_range;
}
/** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */
static unsigned get_arity(expr type) {
unsigned r = 0;
while (is_pi(type)) {
type = binding_body(type);
r++;
}
return r;
}
expr mk_aux_type_metavar_for(name_generator & ngen, expr const & t) {
expr new_type = replace_range(t, mk_sort(mk_meta_univ(ngen.next())));
name n = ngen.next();
return mk_metavar(n, new_type);
}
expr mk_aux_metavar_for(name_generator & ngen, expr const & t) {
unsigned num = get_arity(t);
expr r = mk_app_vars(mk_aux_type_metavar_for(ngen, t), num);
expr new_type = replace_range(t, r);
name n = ngen.next();
return mk_metavar(n, new_type);
}
type_checker::scope::scope(type_checker & tc):
m_tc(tc), m_keep(false) {
m_tc.push();
@ -68,48 +99,6 @@ optional<constraint> type_checker::next_cnstr() {
}
}
/**
\brief Given a metavariable application ((?m t_1) ... t_k)
Create a telescope with the types of t_1 ... t_k.
If t_i is a local constant, then we abstract the occurrences of t_i in the types of t_{i+1} ... t_k.
Return false if the telescope still contains local constants after the abstraction step.
*/
bool type_checker::meta_to_telescope(expr const & e, buffer<expr> & telescope) {
lean_assert(is_meta(e));
lean_assert(closed(e));
buffer<optional<expr>> locals;
return meta_to_telescope_core(e, telescope, locals);
}
/** \brief Auxiliary method for meta_to_telescope */
bool type_checker::meta_to_telescope_core(expr const & e, buffer<expr> & telescope, buffer<optional<expr>> & locals) {
lean_assert(is_meta(e));
if (is_app(e)) {
if (!meta_to_telescope_core(app_fn(e), telescope, locals))
return false;
// infer type and abstract local constants
unsigned n = locals.size();
expr t = replace(infer_type(app_arg(e)),
[&](expr const & e, unsigned offset) -> optional<expr> {
if (is_local(e)) {
for (unsigned i = 0; i < n; i++) {
if (locals[i] && is_eqp(*locals[i], e))
return some_expr(mk_var(offset + n - i - 1));
}
}
return none_expr();
});
if (has_local(t))
return false;
telescope.push_back(t);
if (is_local(e))
locals.push_back(some_expr(e));
else
locals.push_back(none_expr());
}
return true;
}
/**
\brief Make sure \c e "is" a sort, and return the corresponding sort.
If \c e is not a sort, then the whnf procedure is invoked. Then, there are
@ -150,25 +139,19 @@ expr type_checker::ensure_pi_core(expr e, expr const & s) {
if (is_pi(e)) {
return e;
} else if (is_meta(e)) {
buffer<expr> telescope;
if (!meta_to_telescope(e, telescope)) {
environment env = m_env;
throw_kernel_exception(env, s,
[=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, env, o, s); });
}
expr ta = mk_sort(mk_meta_univ(m_gen.next()));
expr A = mk_metavar(m_gen.next(), mk_pi(telescope, ta));
expr A_xs = mk_app_vars(A, telescope.size());
telescope.push_back(A_xs);
expr tb = mk_sort(mk_meta_univ(m_gen.next()));
expr B = mk_metavar(m_gen.next(), mk_pi(telescope, tb));
buffer<expr> args;
get_app_args(e, args);
expr A_args = mk_app(A, args.size(), args.data());
args.push_back(Var(0));
expr B_args = mk_app(B, args.size(), args.data());
expr r = mk_pi(g_x_name, A_args, B_args);
justification j = mk_justification(s,
buffer<expr> margs;
expr const & m = get_app_args(e, margs);
expr const & mtype = mlocal_type(m);
expr maux1 = mk_aux_type_metavar_for(m_gen, mtype);
expr dontcare;
expr tmp_pi = mk_pi(g_x_name, mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context
expr mtype2 = replace_range(mtype, tmp_pi); // trick for "extending" the context
expr maux2 = mk_aux_type_metavar_for(m_gen, mtype2);
expr A = mk_app(maux1, margs);
margs.push_back(Var(0));
expr B = mk_app(maux2, margs);
expr r = mk_pi(g_x_name, A, B);
justification j = mk_justification(s,
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_function_expected(fmt, m_env, o, subst.instantiate(s));
});

26
src/kernel/type_checker.h
View file

@ -16,6 +16,30 @@ Author: Leonardo de Moura
#include "kernel/converter.h"
namespace lean {
/** \brief Given \c type of the form <tt>(Pi ctx, r)</tt>, return <tt>(Pi ctx, new_range)</tt> */
expr replace_range(expr const & type, expr const & new_range);
/**
\brief Given a type \c t of the form
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
return a new metavariable \c m1 with type
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u}</tt>
where \c u is a new universe metavariable.
*/
expr mk_aux_type_metavar_for(name_generator & ngen, expr const & t);
/**
\brief Given a type \c t of the form
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
return a new metavariable \c m1 with type
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), (m2 x_1 ... x_n)</tt>
where \c m2 is a new metavariable with type
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u}</tt>
where \c u is a new universe metavariable.
*/
expr mk_aux_metavar_for(name_generator & ngen, expr const & t);
/**
\brief Lean Type Checker. It can also be used to infer types, check whether a
type \c A is convertible to a type \c B, etc.
@ -59,8 +83,6 @@ class type_checker {
optional<expr> expand_macro(expr const & m);
std::pair<expr, expr> open_binding_body(expr const & e);
void add_cnstr(constraint const & c);
bool meta_to_telescope(expr const & e, buffer<expr> & telescope);
bool meta_to_telescope_core(expr const & e, buffer<expr> & telescope, buffer<optional<expr>> & locals);
expr ensure_sort_core(expr e, expr const & s);
expr ensure_pi_core(expr e, expr const & s);
justification mk_macro_jst(expr const & e);

58
src/library/inductive_unifier_plugin.cpp
View file

@ -11,36 +11,26 @@ Author: Leonardo de Moura
namespace lean {
class inductive_unifier_plugin_cell : public unifier_plugin_cell {
/** \brief Return true iff \c e is of the form (elim ... (?m ...)) */
bool is_elim_meta_app(type_checker & tc, expr const & e) const {
if (!is_app(e))
return false;
expr const & f = get_app_fn(e);
if (!is_constant(f))
return false;
auto it_name = inductive::is_elim_rule(tc.env(), const_name(f));
if (!it_name)
return false;
if (!is_meta(app_arg(e)))
return false;
if (is_pi(tc.whnf(tc.infer(e))))
return false;
return true;
}
/** \brief Return true iff the lhs or rhs of the constraint c is of the form (elim ... (?m ...)) */
/** \brief Return true iff the lhs or rhs of the constraint c is of the form (elim ... (?m ...) ...) */
bool is_elim_meta_cnstr(type_checker & tc, constraint const & c) const {
return is_eq_cnstr(c) && (is_elim_meta_app(tc, cnstr_lhs_expr(c)) || is_elim_meta_app(tc, cnstr_rhs_expr(c)));
return is_eq_cnstr(c) && (inductive::is_elim_meta_app(tc, cnstr_lhs_expr(c)) ||
inductive::is_elim_meta_app(tc, cnstr_rhs_expr(c)));
}
/** \brief Return true iff \c e is of the form (?m ... (intro ...)) */
/** \brief Return true iff \c e is of the form (?m ... (intro ...) ...) */
bool is_meta_intro_app(type_checker & tc, expr const & e) const {
if (!is_app(e) || !is_meta(e))
return false;
expr arg = get_app_fn(app_arg(e));
if (!is_constant(arg))
return false;
return (bool) inductive::is_intro_rule(tc.env(), const_name(arg)); // NOLINT
buffer<expr> args;
get_app_args(e, args);
for (expr const & a : args) {
expr arg = get_app_fn(a);
if (!is_constant(arg))
continue;
if (inductive::is_intro_rule(tc.env(), const_name(arg)))
return true;
}
return false;
}
/** \brief Return true iff the lhs or rhs of the constraint c is of the form (?m ... (intro ...)) */
@ -50,21 +40,21 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
/**
\brief Given (elim args) =?= t, where elim is the eliminator/recursor for the inductive declaration \c decl,
and the last argument of args is of the form (?m ...), we create a case split where we try to assign (?m ...)
and the major premise is of the form (?m ...), we create a case split where we try to assign (?m ...)
to the different constructors of decl.
*/
lazy_list<constraints> add_elim_meta_cnstrs(type_checker & tc, name_generator ngen, inductive::inductive_decl const & decl,
expr const & elim, buffer<expr> & args, expr const & t, justification const & j) const {
lean_assert(is_constant(elim));
environment const & env = tc.env();
levels elim_lvls = const_levels(elim);
unsigned elim_num_lvls = length(elim_lvls);
unsigned num_args = args.size();
expr meta = args[num_args - 1]; // save last argument, we will update it
unsigned major_idx = *inductive::get_elim_major_idx(env, const_name(elim));
expr meta = args[major_idx]; // save this argument, we will update it
lean_assert(is_meta(meta));
buffer<expr> margs;
expr const & m = get_app_args(meta, margs);
expr const & mtype = mlocal_type(m);
environment const & env = tc.env();
buffer<constraints> alts;
for (auto const & intro : inductive::inductive_decl_intros(decl)) {
name const & intro_name = inductive::intro_rule_name(intro);
@ -83,10 +73,10 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
hint = mk_app(hint, mk_app(mk_aux_metavar_for(ngen, mtype), margs));
intro_type = tc.whnf(binding_body(intro_type));
}
constraint c1 = mk_eq_cnstr(meta, hint, j);
args[num_args - 1] = hint;
constraint c1 = mk_eq_cnstr(meta, hint, j);
args[major_idx] = hint;
expr reduce_elim = tc.whnf(mk_app(elim, args));
constraint c2 = mk_eq_cnstr(reduce_elim, t, j);
constraint c2 = mk_eq_cnstr(reduce_elim, t, j);
alts.push_back(constraints({c1, c2}));
}
return to_lazy(to_list(alts.begin(), alts.end()));
@ -94,7 +84,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
lazy_list<constraints> process_elim_meta_core(type_checker & tc, name_generator const & ngen,
expr const & lhs, expr const & rhs, justification const & j) const {
lean_assert(is_elim_meta_app(tc, lhs));
lean_assert(inductive::is_elim_meta_app(tc, lhs));
buffer<expr> args;
expr const & elim = get_app_args(lhs, args);
environment const & env = tc.env();
@ -116,9 +106,9 @@ public:
expr const & lhs = cnstr_lhs_expr(c);
expr const & rhs = cnstr_rhs_expr(c);
justification const & j = c.get_justification();
if (is_elim_meta_app(tc, lhs))
if (inductive::is_elim_meta_app(tc, lhs))
return process_elim_meta_core(tc, ngen, lhs, rhs, j);
else if (is_elim_meta_app(tc, rhs))
else if (inductive::is_elim_meta_app(tc, rhs))
return process_elim_meta_core(tc, ngen, rhs, lhs, j);
else
return lazy_list<constraints>();

63
src/library/unifier.cpp
View file

@ -190,55 +190,6 @@ std::pair<unify_status, substitution> unify_simple(substitution const & s, const
return mk_pair(unify_status::Unsupported, s);
}
/** \brief Given \c type of the form <tt>(Pi ctx, r)</tt>, return <tt>(Pi ctx, new_range)</tt> */
static expr replace_range(expr const & type, expr const & new_range) {
if (is_pi(type))
return update_binding(type, binding_domain(type), replace_range(binding_body(type), new_range));
else
return new_range;
}
/** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */
static unsigned get_arity(expr type) {
unsigned r = 0;
while (is_pi(type)) {
type = binding_body(type);
r++;
}
return r;
}
/**
\brief Given a type \c t of the form
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
return a new metavariable \c m1 with type
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u}</tt>
where \c u is a new universe metavariable.
*/
expr mk_aux_type_metavar_for(name_generator & ngen, expr const & t) {
expr new_type = replace_range(t, mk_sort(mk_meta_univ(ngen.next())));
name n = ngen.next();
return mk_metavar(n, new_type);
}
/**
\brief Given a type \c t of the form
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
return a new metavariable \c m1 with type
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), (m2 x_1 ... x_n)</tt>
where \c m2 is a new metavariable with type
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u}</tt>
where \c u is a new universe metavariable.
*/
expr mk_aux_metavar_for(name_generator & ngen, expr const & t) {
unsigned num = get_arity(t);
expr r = mk_app_vars(mk_aux_type_metavar_for(ngen, t), num);
expr new_type = replace_range(t, r);
name n = ngen.next();
return mk_metavar(n, new_type);
}
static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification());
/**
@ -740,11 +691,15 @@ struct unifier_fn {
}
}
void pop_case_split() {
m_tc->pop();
m_case_splits.pop_back();
}
bool resolve_conflict() {
lean_assert(in_conflict());
// Remark: we must save the value of m_conflict because d->next(*this) may change it.
justification conflict = *m_conflict;
while (!m_case_splits.empty()) {
justification conflict = *m_conflict;
std::unique_ptr<case_split> & d = m_case_splits.back();
if (depends_on(conflict, d->m_assumption_idx)) {
d->m_failed_justifications = mk_composite1(d->m_failed_justifications, conflict);
@ -752,9 +707,9 @@ struct unifier_fn {
reset_conflict();
return true;
}
} else {
pop_case_split();
}
m_tc->pop();
m_case_splits.pop_back();
}
return false;
}
@ -784,6 +739,7 @@ struct unifier_fn {
} else {
// update conflict
update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications));
pop_case_split();
return false;
}
}
@ -830,6 +786,7 @@ struct unifier_fn {
} else {
// update conflict
update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications));
pop_case_split();
return false;
}
}

4
tests/lean/run/group.lean
View file

@ -29,8 +29,8 @@ definition group_to_struct [instance] (g : group) : group_struct (carrier g)
check group_struct
definition mul {A : Type} {s : group_struct A} : A → A → A
:= group_struct_rec (λ mul one inv h1 h2 h3, mul) s
definition mul {A : Type} {s : group_struct A} (a b : A) : A
:= group_struct_rec (λ mul one inv h1 h2 h3, mul) s a b
infixl `*`:75 := mul