max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/erase_irrelevant): visit_constant

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-02 15:51:03 -07:00
parent 49425aa80c
commit cd8dc8670d
1 changed files with 24 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

53
src/library/compiler/erase_irrelevant.cpp
View file

@ -97,35 +97,6 @@ class erase_irrelevant_fn {
}
}
expr visit_constant(expr const & e) {
lean_assert(!is_enf_neutral(e));
name const & c = const_name(e);
if (c == get_lc_unreachable_name()) {
return mk_enf_unreachable();
} else if (c == get_lc_proof_name()) {
return mk_enf_neutral();
}
try {
type_checker tc(m_st, m_lctx);
expr e_type = tc.whnf(tc.infer(e));
if (tc.is_prop(e_type) || is_sort(e_type))
return mk_enf_neutral();
else
return mk_constant(const_name(e));
} catch (kernel_exception &) {
return mk_constant(const_name(e));
}
}
bool is_atom(expr const & e) {
switch (e.kind()) {
case expr_kind::FVar: return true;
case expr_kind::Lit: return true;
case expr_kind::Const: return true;
default: return false;
}
}
bool is_irrelevant(expr const & e) {
try {
type_checker tc(m_st, m_lctx);
@ -148,6 +119,30 @@ class erase_irrelevant_fn {
}
}
expr visit_constant(expr const & e) {
lean_assert(!is_enf_neutral(e));
name const & c = const_name(e);
if (c == get_lc_unreachable_name()) {
return mk_enf_unreachable();
} else if (c == get_lc_proof_name()) {
return mk_enf_neutral();
}
if (is_irrelevant(e)) {
return mk_enf_neutral();
} else {
return mk_constant(const_name(e));
}
}
bool is_atom(expr const & e) {
switch (e.kind()) {
case expr_kind::FVar: return true;
case expr_kind::Lit: return true;
case expr_kind::Const: return true;
default: return false;
}
}
expr visit_lambda_core(expr e, bool is_minor) {
flet<local_ctx> save_lctx(m_lctx, m_lctx);
buffer<expr> bfvars;