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

fix(library/unifier): more bugs in the unifier

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-25 19:26:32 -07:00
parent cf44c80ffb
commit 01cec1e1f1
4 changed files with 60 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/kernel/type_checker.cpp
View file

@ -355,12 +355,16 @@ expr type_checker::infer_type(expr const & e) {
return r;
}
void type_checker::copy_constraints(unsigned qhead, buffer<constraint> & new_cnstrs) {
for (unsigned i = qhead; i < m_cs.size(); i++)
new_cnstrs.push_back(m_cs[i]);
}
expr type_checker::infer(expr const & e, buffer<constraint> & new_cnstrs) {
scope mk_scope(*this);
unsigned cs_qhead = m_cs_qhead;
unsigned cs_qhead = m_cs.size();
expr r = infer_type_core(e, true);
for (unsigned i = cs_qhead; i < m_cs_qhead; i++)
new_cnstrs.push_back(m_cs[i]);
copy_constraints(cs_qhead, new_cnstrs);
return r;
}
@ -406,14 +410,26 @@ bool type_checker::is_def_eq(expr const & t, expr const & s, justification const
return is_def_eq(t, s, djst);
}
bool type_checker::is_def_eq(expr const & t, expr const & s, justification const & j, buffer<constraint> & new_cnstrs) {
unsigned cs_qhead = m_cs.size();
scope mk_scope(*this);
as_delayed_justification djst(j);
if (m_conv->is_def_eq(t, s, *this, djst)) {
copy_constraints(cs_qhead, new_cnstrs);
return true;
} else {
return false;
}
}
bool type_checker::is_def_eq_types(expr const & t, expr const & s, justification const & j, buffer<constraint> & new_cnstrs) {
scope mk_scope(*this);
unsigned cs_qhead = m_cs_qhead;
unsigned cs_qhead = m_cs.size();
expr r1 = infer_type_core(t, true);
expr r2 = infer_type_core(s, true);
if (is_def_eq(r1, r2, j)) {
for (unsigned i = cs_qhead; i < m_cs_qhead; i++)
new_cnstrs.push_back(m_cs[i]);
as_delayed_justification djst(j);
if (m_conv->is_def_eq(r1, r2, *this, djst)) {
copy_constraints(cs_qhead, new_cnstrs);
return true;
} else {
return false;
@ -432,6 +448,14 @@ expr type_checker::whnf(expr const & t) {
return m_conv->whnf(t, *this);
}
expr type_checker::whnf(expr const & t, buffer<constraint> & new_cnstrs) {
scope mk_scope(*this);
unsigned cs_qhead = m_cs.size();
expr r = m_conv->whnf(t, *this);
copy_constraints(cs_qhead, new_cnstrs);
return r;
}
void type_checker::push() {
m_infer_type_cache[0].push();
m_infer_type_cache[1].push();

9
src/kernel/type_checker.h
View file

@ -103,6 +103,7 @@ class type_checker {
expr infer_app(expr const & e, bool infer_only);
expr infer_type_core(expr const & e, bool infer_only);
expr infer_type(expr const & e);
void copy_constraints(unsigned qhead, buffer<constraint> & new_cnstrs);
extension_context & get_extension() { return m_tc_ctx; }
public:
/**
@ -147,7 +148,11 @@ public:
bool is_def_eq(expr const & t, expr const & s);
bool is_def_eq(expr const & t, expr const & s, justification const & j);
bool is_def_eq(expr const & t, expr const & s, delayed_justification & jst);
/** \brief Return true iff \c t and \c s (may b) definitionally equal (modulo constraints)
/** \brief Return true iff \c t and \c s are (may be) definitionally equal (module constraints)
New constraints associated with test are store in \c new_cnstrs.
*/
bool is_def_eq(expr const & t, expr const & s, justification const & j, buffer<constraint> & new_cnstrs);
/** \brief Return true iff types of \c t and \c s are (may be) definitionally equal (modulo constraints)
New constraints associated with test are store in \c new_cnstrs.
*/
bool is_def_eq_types(expr const & t, expr const & s, justification const & j, buffer<constraint> & new_cnstrs);
@ -155,6 +160,8 @@ public:
bool is_prop(expr const & t);
/** \brief Return the weak head normal form of \c t. */
expr whnf(expr const & t);
/** \brief Similar to the previous method, but it also returns the new constraints created in the process. */
expr whnf(expr const & t, buffer<constraint> & new_cnstrs);
/** \brief Return a Pi if \c t is convertible to a Pi type. Throw an exception otherwise.
The argument \c s is used when reporting errors */
expr ensure_pi(expr const & t, expr const & s);

17
src/library/inductive_unifier_plugin.cpp
View file

@ -56,9 +56,11 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
buffer<expr> margs;
expr const & m = get_app_args(meta, margs);
expr mtype = tc.infer(m, tc_cnstr_buffer);
list<constraint> tc_cnstrs = to_list(tc_cnstr_buffer.begin(), tc_cnstr_buffer.end());
lean_assert(!tc.next_cnstr());
unsigned buff_sz = tc_cnstr_buffer.size();
buffer<constraints> alts;
for (auto const & intro : inductive::inductive_decl_intros(decl)) {
tc_cnstr_buffer.shrink(buff_sz);
name const & intro_name = inductive::intro_rule_name(intro);
declaration intro_decl = env.get(intro_name);
levels intro_lvls;
@ -70,17 +72,22 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
}
expr intro_fn = mk_constant(inductive::intro_rule_name(intro), intro_lvls);
expr hint = intro_fn;
expr intro_type = tc.whnf(inductive::intro_rule_type(intro));
expr intro_type = tc.whnf(inductive::intro_rule_type(intro), tc_cnstr_buffer);
while (is_pi(intro_type)) {
hint = mk_app(hint, mk_app(mk_aux_metavar_for(ngen, mtype), margs));
intro_type = tc.whnf(binding_body(intro_type));
intro_type = tc.whnf(binding_body(intro_type), tc_cnstr_buffer);
lean_assert(!tc.next_cnstr());
}
constraint c1 = mk_eq_cnstr(meta, hint, j);
args[major_idx] = hint;
expr reduce_elim = tc.whnf(mk_app(elim, args));
lean_assert(!tc.next_cnstr());
expr reduce_elim = tc.whnf(mk_app(elim, args), tc_cnstr_buffer);
lean_assert(!tc.next_cnstr());
constraint c2 = mk_eq_cnstr(reduce_elim, t, j);
list<constraint> tc_cnstrs = to_list(tc_cnstr_buffer.begin(), tc_cnstr_buffer.end());
alts.push_back(cons(c1, cons(c2, tc_cnstrs)));
}
lean_assert(!tc.next_cnstr());
return to_lazy(to_list(alts.begin(), alts.end()));
}
@ -88,8 +95,10 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
expr const & lhs, expr const & rhs, justification const & j) const {
lean_assert(inductive::is_elim_meta_app(tc, lhs));
buffer<constraint> tc_cnstr_buffer;
lean_assert(!tc.next_cnstr());
if (!tc.is_def_eq_types(lhs, rhs, j, tc_cnstr_buffer))
return lazy_list<constraints>();
lean_assert(!tc.next_cnstr());
buffer<expr> args;
expr const & elim = get_app_args(lhs, args);
environment const & env = tc.env();

28
src/library/unifier.cpp
View file

@ -413,22 +413,6 @@ struct unifier_fn {
}
}
/** \brief Check if \c t1 and \c t2 are definitionally, and accumulate constraints in \c new_cs
\pre m_tc must not have pending constraints
*/
bool is_def_eq(expr const & t1, expr const & t2, justification const & j, buffer<constraint> & new_cs) {
type_checker::scope s(*m_tc);
lean_assert(!m_tc->next_cnstr());
if (m_tc->is_def_eq(t1, t2, j)) {
while (auto c = m_tc->next_cnstr())
new_cs.push_back(*c);
return true;
} else {
return false;
}
}
/**
\brief Assign \c v to metavariable \c m with justification \c j.
The type of v and m are inferred, and is_def_eq is invoked.
@ -855,22 +839,26 @@ struct unifier_fn {
return lazy_list<constraints>();
justification const & j = c.get_justification();
buffer<constraint> cs;
if (!is_def_eq(f_lhs, f_rhs, j, cs))
lean_assert(!m_tc->next_cnstr());
if (!m_tc->is_def_eq(f_lhs, f_rhs, j, cs))
return lazy_list<constraints>();
buffer<expr> args_lhs, args_rhs;
get_app_args(lhs, args_lhs);
get_app_args(rhs, args_rhs);
if (args_lhs.size() != args_rhs.size())
return lazy_list<constraints>();
lean_assert(!m_tc->next_cnstr());
for (unsigned i = 0; i < args_lhs.size(); i++)
if (!is_def_eq(args_lhs[i], args_rhs[i], j, cs))
if (!m_tc->is_def_eq(args_lhs[i], args_rhs[i], j, cs))
return lazy_list<constraints>();
return lazy_list<constraints>(to_list(cs.begin(), cs.end()));
}
bool process_plugin_constraint(constraint const & c) {
lean_assert(!is_choice_cnstr(c));
lean_assert(!m_tc->next_cnstr());
lazy_list<constraints> alts = m_plugin->solve(*m_tc, c, m_ngen.mk_child());
lean_assert(!m_tc->next_cnstr());
alts = append(alts, process_const_const_cnstr(c));
return process_lazy_constraints(alts, c.get_justification());
}
@ -937,7 +925,7 @@ struct unifier_fn {
expr t = apply_beta(lhs_fn_val, lhs_args.size(), lhs_args.data());
expr s = apply_beta(rhs_fn_val, rhs_args.size(), rhs_args.data());
buffer<constraint> cs2;
if (is_def_eq(t, s, j, cs2)) {
if (m_tc->is_def_eq(t, s, j, cs2)) {
// create a case split
a = mk_assumption_justification(m_next_assumption_idx);
add_case_split(std::unique_ptr<case_split>(new simple_case_split(*this, j, to_list(cs2.begin(), cs2.end()))));
@ -1223,7 +1211,7 @@ struct unifier_fn {
if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j)) {
// Remark: we should not use mk_eq_cnstr(marg, rhs, j) since is_def_eq may be able to reduce them.
// The unifier assumes the eq constraints are reduced.
if (is_def_eq(marg, rhs, j, cs)) {
if (m_tc->is_def_eq(marg, rhs, j, cs)) {
expr v = mk_lambda_for(*new_mtype, mk_var(vidx));
cs.push_back(mk_eq_cnstr(m, v, j));
alts.push_back(to_list(cs.begin(), cs.end()));