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

fix(library/unifier): tolerate exceptions in the type_checker::infer method. This can happen since when we try projections we don't check whether they are type correct

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-16 02:53:54 +01:00
parent dfe48e6abe
commit c8849d42e9
1 changed files with 21 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/unifier.cpp
View file

@ -16,6 +16,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h" #include "kernel/abstract.h"
#include "kernel/instantiate.h" #include "kernel/instantiate.h"
#include "kernel/type_checker.h" #include "kernel/type_checker.h"
#include "kernel/kernel_exception.h"
#include "library/occurs.h" #include "library/occurs.h"
#include "library/unifier.h" #include "library/unifier.h"
#include "library/opaque_hints.h" #include "library/opaque_hints.h"
@ -404,7 +405,13 @@ struct unifier_fn {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
m_subst.d_assign(m, v, j); m_subst.d_assign(m, v, j);
expr m_type = mlocal_type(m); expr m_type = mlocal_type(m);
expr v_type = m_tc->infer(v); expr v_type;
try {
v_type = m_tc->infer(v);
} catch (kernel_exception & e) {
set_conflict(j);
return false;
}
if (in_conflict()) if (in_conflict())
return false; return false;
if (!is_def_eq(m_type, v_type, j)) if (!is_def_eq(m_type, v_type, j))
@ -801,7 +808,14 @@ struct unifier_fn {
lean_assert(is_choice_cnstr(c)); lean_assert(is_choice_cnstr(c));
expr const & m = cnstr_expr(c); expr const & m = cnstr_expr(c);
choice_fn const & fn = cnstr_choice_fn(c); choice_fn const & fn = cnstr_choice_fn(c);
auto m_type_jst = m_subst.d_instantiate_metavars(m_tc->infer(m)); expr m_type;
try {
m_type = m_tc->infer(m);
} catch (kernel_exception &) {
set_conflict(c.get_justification());
return false;
}
auto m_type_jst = m_subst.d_instantiate_metavars(m_type);
lazy_list<constraints> alts = fn(m, m_type_jst.first, m_subst, m_ngen.mk_child()); lazy_list<constraints> alts = fn(m, m_type_jst.first, m_subst, m_ngen.mk_child());
return process_lazy_constraints(alts, mk_composite1(c.get_justification(), m_type_jst.second)); return process_lazy_constraints(alts, mk_composite1(c.get_justification(), m_type_jst.second));
} }
@ -911,8 +925,12 @@ struct unifier_fn {
if (i == margs.size()) if (i == margs.size())
return some_expr(mtype); return some_expr(mtype);
mtype = m_tc->ensure_pi(mtype); mtype = m_tc->ensure_pi(mtype);
if (!m_tc->is_def_eq(binding_domain(mtype), m_tc->infer(margs[i]))) try {
if (!m_tc->is_def_eq(binding_domain(mtype), m_tc->infer(margs[i])))
return none_expr();
} catch (kernel_exception &) {
return none_expr(); return none_expr();
}
expr local = mk_local_for(mtype); expr local = mk_local_for(mtype);
expr body = instantiate(binding_body(mtype), local); expr body = instantiate(binding_body(mtype), local);
auto new_body = ensure_sufficient_args_core(body, i+1, margs); auto new_body = ensure_sufficient_args_core(body, i+1, margs);