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

fix(kernel/converter): use type_checker::scope to make sure we restore the cache, and remove constraints when is_def_eq fails in the converter

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-22 14:08:54 -07:00
parent a1d94d71ec
commit 25cb1bf6a1
2 changed files with 23 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/kernel/converter.cpp
View file

@ -404,6 +404,7 @@ struct default_converter : public converter {
// At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
if (is_app(t_n) && is_app(s_n)) {
type_checker::scope scope(c);
buffer<expr> t_args;
buffer<expr> s_args;
expr t_fn = get_app_args(t_n, t_args);
@ -414,26 +415,34 @@ struct default_converter : public converter {
if (!is_def_eq(t_args[i], s_args[i], c, jst))
break;
}
if (i == t_args.size())
if (i == t_args.size()) {
scope.keep();
return true;
}
}
}
if (m_env.prop_proof_irrel()) {
// Proof irrelevance support for Prop/Bool (aka Type.{0})
type_checker::scope scope(c);
expr t_type = infer_type(c, t);
if (is_prop(t_type, c) && is_def_eq(t_type, infer_type(c, s), c, jst))
if (is_prop(t_type, c) && is_def_eq(t_type, infer_type(c, s), c, jst)) {
scope.keep();
return true;
}
}
list<name> const & cls_proof_irrel = m_env.cls_proof_irrel();
if (!is_nil(cls_proof_irrel)) {
// Proof irrelevance support for classes
type_checker::scope scope(c);
expr t_type = whnf(infer_type(c, t), c);
if (std::any_of(cls_proof_irrel.begin(), cls_proof_irrel.end(),
[&](name const & cls_name) { return is_app_of(t_type, cls_name); }) &&
is_def_eq(t_type, infer_type(c, s), c, jst))
is_def_eq(t_type, infer_type(c, s), c, jst)) {
scope.keep();
return true;
}
}
if (has_metavar(t_n) || has_metavar(s_n)) {

21
src/kernel/type_checker.h
View file

@ -67,16 +67,6 @@ class type_checker {
buffer<constraint> m_cs; // temporary cache of constraints
bool m_cache_cs; // true if we should cache the constraints; false if we should send to m_add_cnstr_fn
struct scope {
type_checker & m_tc;
unsigned m_old_cs_size;
bool m_old_cache_cs;
bool m_keep;
scope(type_checker & tc);
~scope();
void keep();
};
friend class converter; // allow converter to access the following methods
name mk_fresh_name() { return m_gen.next(); }
optional<expr> expand_macro(expr const & m);
@ -93,6 +83,17 @@ class type_checker {
expr infer_type(expr const & e);
bool is_def_eq(expr const & t, expr const & s, delayed_justification & jst);
extension_context & get_extension() { return m_tc_ctx; }
public:
class scope {
type_checker & m_tc;
unsigned m_old_cs_size;
bool m_old_cache_cs;
bool m_keep;
public:
scope(type_checker & tc);
~scope();
void keep();
};
public:
/**