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

fix(kernel/type_checker): bug in whnf method, and missing call to max_sharing in is_conv and is_def_eq methods

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-28 12:09:23 -07:00
parent 4e893d3902
commit 6c3a796119
1 changed files with 13 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/kernel/type_checker.cpp
View file

@ -174,9 +174,9 @@ struct type_checker::imp {
} }
lean_assert(m <= num_args); lean_assert(m <= num_args);
r = whnf_core(mk_rev_app(instantiate(binder_body(f), m, args.data() + (num_args - m)), num_args - m, args.data())); r = whnf_core(mk_rev_app(instantiate(binder_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()));
break; } else {
r = is_eqp(f, *it) ? e : mk_rev_app(f, args.size(), args.data());
} }
r = is_eqp(f, *it) ? e : mk_rev_app(f, args.size(), args.data());
break; break;
}} }}
@ -309,7 +309,7 @@ struct type_checker::imp {
expr t = e; expr t = e;
while (true) { while (true) {
expr t1 = unfold_names(whnf_core(t), 0); expr t1 = whnf_core(t, 0);
auto new_t = norm_ext(t1); auto new_t = norm_ext(t1);
if (new_t) { if (new_t) {
t = *new_t; t = *new_t;
@ -521,12 +521,12 @@ struct type_checker::imp {
/** \brief Return true iff \c t is convertible to s */ /** \brief Return true iff \c t is convertible to s */
bool is_conv(expr const & t, expr const & s, delayed_justification & jst) { bool is_conv(expr const & t, expr const & s, delayed_justification & jst) {
return is_conv(t, s, false, jst); return is_conv(max_sharing(t), max_sharing(s), false, jst);
} }
/** \brief Return true iff \c t and \c s are definitionally equal */ /** \brief Return true iff \c t and \c s are definitionally equal */
bool is_def_eq(expr const & t, expr const & s, delayed_justification & jst) { bool is_def_eq(expr const & t, expr const & s, delayed_justification & jst) {
return is_conv(t, s, true, jst); return is_conv(max_sharing(t), max_sharing(s), true, jst);
} }
/** \brief Return true iff \c e is a proposition */ /** \brief Return true iff \c e is a proposition */
@ -894,6 +894,14 @@ certified_definition check(environment const & env, name_generator const & g, de
} }
// TODO(Leo): solve universe level constraints // TODO(Leo): solve universe level constraints
#if 1
// temporary code
for (auto c : chandler.m_cnstrs) {
std::cout << c << "\n";
}
if (!chandler.m_cnstrs.empty())
throw_kernel_exception(env, "invalid declaration, unsatisfied level constraints");
#endif
return certified_definition(env.get_id(), d); return certified_definition(env.get_id(), d);
} }