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

fix(frontends/lean/elaborator): whnf may produce assertion violation if term contains free variables

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-09 15:22:50 -07:00
parent 27fa0d0ae3
commit 38058450d4
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/elaborator.cpp
View file

@ -136,7 +136,7 @@ elaborator_context::elaborator_context(environment const & env, io_state const &
optional<name> is_ext_class(type_checker & tc, expr type) {
type = tc.whnf(type).first;
if (is_pi(type)) {
return is_ext_class(tc, binding_body(type));
return is_ext_class(tc, instantiate(binding_body(type), mk_local(tc.mk_fresh_name(), binding_domain(type))));
} else {
expr f = get_app_fn(type);
if (!is_constant(f))
@ -460,7 +460,7 @@ class elaborator {
type = m_elab.whnf(type).first;
if (!is_pi(type))
break;
type = binding_body(type);
type = instantiate(binding_body(type), ::lean::mk_local(m_elab.m_ngen.next(), binding_domain(type)));
pre = copy_tag(m_meta, ::lean::mk_app(pre, copy_tag(m_meta, mk_strict_expr_placeholder())));
}
try {

3
src/kernel/type_checker.h
View file

@ -94,7 +94,6 @@ class type_checker {
level_param_names const * m_params;
friend class converter; // allow converter to access the following methods
name mk_fresh_name() { return m_gen.next(); }
pair<expr, expr> open_binding_body(expr const & e);
pair<expr, constraint_seq> ensure_sort_core(expr e, expr const & s);
pair<expr, constraint_seq> ensure_pi_core(expr e, expr const & s);
@ -126,7 +125,7 @@ public:
environment const & env() const { return m_env; }
name_generator mk_ngen() { return m_gen.mk_child(); }
name mk_fresh_name() { return m_gen.next(); }
/**
\brief Return the type of \c t.