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

feat(library/compiler/lcnf): replace eq.rec and eq.ndrec applications with lc_cast

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-12 11:00:34 -07:00
parent 9f2d543209
commit cfdc331ecb
1 changed files with 28 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/library/compiler/lcnf.cpp
View file

@ -208,6 +208,31 @@ public:
}
}
expr visit_eq_rec(expr const & fn, buffer<expr> & args, bool root) {
lean_assert(const_name(fn) == get_eq_rec_name() || const_name(fn) == get_eq_ndrec_name());
if (args.size() < 6) {
return visit(eta_expand(mk_app(fn, args), 6 - args.size()), root);
} else {
unsigned eq_rec_nargs = 6;
unsigned minor_idx = 3;
type_checker tc(m_env, m_lctx, m_tc_cache);
expr minor = args[minor_idx];
expr minor_type = tc.whnf(tc.infer(minor));
expr eq_rec_type = tc.whnf(tc.infer(mk_app(fn, eq_rec_nargs, args.data())));
expr new_e;
if (tc.is_def_eq(minor_type, eq_rec_type)) {
/* Type cast is not needed */
new_e = minor;
} else {
level minor_lvl = sort_level(tc.ensure_type(minor_type));
level eq_rec_lvl = sort_level(tc.ensure_type(eq_rec_type));
new_e = mk_app(mk_constant(get_lc_cast_name(), {eq_rec_lvl, minor_lvl}), minor_type, eq_rec_type, minor);
}
new_e = mk_app(new_e, args.size() - eq_rec_nargs, args.data() + eq_rec_nargs);
return visit(new_e, root);
}
}
expr visit_app_default(expr const & fn, buffer<expr> & args, bool root) {
for (expr & arg : args) {
arg = visit(arg, false);
@ -232,6 +257,9 @@ public:
}
} else if (is_no_confusion(m_env, const_name(fn))) {
return visit_no_confusion(fn, args, root);
} else if (const_name(fn) == get_eq_rec_name() ||
const_name(fn) == get_eq_ndrec_name()) {
return visit_eq_rec(fn, args, root);
}
}
return visit_app_default(fn, args, root);