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

fix(library/compiler/erase_irrelevant): minor issues

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-02 13:36:48 -07:00
parent 20e7edd4ac
commit fd46adb7b3
1 changed files with 12 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -103,6 +103,12 @@ 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));
@ -256,7 +262,7 @@ class erase_irrelevant_fn {
if (optional<unsigned> fidx = has_trivial_structure(I_name)) {
unsigned nparams = c_val.get_nparams();
lean_assert(nparams + *fidx < args.size());
return args[nparams + *fidx];
return visit(args[nparams + *fidx]);
} else {
return visit_app_default(fn, args);
}
@ -264,11 +270,13 @@ class erase_irrelevant_fn {
expr visit_app(expr const & e) {
buffer<expr> args;
expr f = visit(get_app_args(e, args));
expr f = get_app_args(e, args);
if (is_constant(f)) {
name const & fn = const_name(f);
if (fn == get_lc_proof_name()) {
return mk_enf_neutral();
} else if (fn == get_lc_unreachable_name()) {
return mk_enf_unreachable();
} else if (is_constructor(env(), fn)) {
return visit_constructor(f, args);
} else if (is_cases_on_recursor(env(), fn)) {
@ -279,6 +287,7 @@ class erase_irrelevant_fn {
return visit_quot_lift(args);
}
}
f = visit(f);
return visit_app_default(f, args);
}
@ -287,7 +296,7 @@ class erase_irrelevant_fn {
if (*fidx != proj_idx(e).get_small_value())
return mk_enf_neutral();
else
return proj_expr(e);
return visit(proj_expr(e));
} else {
return e;
}