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

feat(library/compiler/lcnf): eliminate false.cases_on and eq.cases_on

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-12 14:26:29 -07:00
parent 1e5f0a91f1
commit 112f183be4
4 changed files with 19 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -213,12 +213,18 @@ 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());
lean_assert(const_name(fn) == get_eq_rec_name() ||
const_name(fn) == get_eq_ndrec_name() ||
const_name(fn) == get_eq_cases_on_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;
unsigned minor_idx;
if (const_name(fn) == get_eq_cases_on_name())
minor_idx = 5;
else
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));
@ -241,7 +247,8 @@ public:
if (args.size() < 2) {
return visit(eta_expand(mk_app(fn, args), 2 - args.size()), root);
} else {
/* Remark: args.size() may be greater than 2, but (lc_unreachable a_1 ... a_n) is equivalent to (lc_unreachable) */
/* Remark: args.size() may be greater than 2, but
(lc_unreachable a_1 ... a_n) is equivalent to (lc_unreachable) */
type_checker tc(m_env, m_lctx, m_tc_cache);
expr type = tc.whnf(tc.infer(mk_app(fn, args)));
level lvl = sort_level(tc.ensure_type(type));
@ -289,9 +296,10 @@ public:
if (is_constant(fn)) {
if (const_name(fn) == get_and_rec_name() || const_name(fn) == get_and_cases_on_name()) {
return visit_and_rec(fn, args, root);
} else if (const_name(fn) == get_eq_rec_name() || const_name(fn) == get_eq_ndrec_name()) {
} else if (const_name(fn) == get_eq_rec_name() || const_name(fn) == get_eq_ndrec_name() ||
const_name(fn) == get_eq_cases_on_name()) {
return visit_eq_rec(fn, args, root);
} else if (const_name(fn) == get_false_rec_name()) {
} else if (const_name(fn) == get_false_rec_name() || const_name(fn) == get_false_cases_on_name()) {
return visit_false_rec(fn, args, root);
} else if (is_cases_on_recursor(m_env, const_name(fn))) {
return visit_cases_on(fn, args, root);

4
src/library/constants.cpp
View file

@ -62,6 +62,7 @@ name const * g_false = nullptr;
name const * g_false_of_true_iff_false = nullptr;
name const * g_false_of_true_eq_false = nullptr;
name const * g_false_rec = nullptr;
name const * g_false_cases_on = nullptr;
name const * g_fin_mk = nullptr;
name const * g_fin_ne_of_vne = nullptr;
name const * g_forall_congr = nullptr;
@ -318,6 +319,7 @@ void initialize_constants() {
g_false_of_true_iff_false = new name{"false_of_true_iff_false"};
g_false_of_true_eq_false = new name{"false_of_true_eq_false"};
g_false_rec = new name{"false", "rec"};
g_false_cases_on = new name{"false", "cases_on"};
g_fin_mk = new name{"fin", "mk"};
g_fin_ne_of_vne = new name{"fin", "ne_of_vne"};
g_forall_congr = new name{"forall_congr"};
@ -575,6 +577,7 @@ void finalize_constants() {
delete g_false_of_true_iff_false;
delete g_false_of_true_eq_false;
delete g_false_rec;
delete g_false_cases_on;
delete g_fin_mk;
delete g_fin_ne_of_vne;
delete g_forall_congr;
@ -831,6 +834,7 @@ name const & get_false_name() { return *g_false; }
name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; }
name const & get_false_of_true_eq_false_name() { return *g_false_of_true_eq_false; }
name const & get_false_rec_name() { return *g_false_rec; }
name const & get_false_cases_on_name() { return *g_false_cases_on; }
name const & get_fin_mk_name() { return *g_fin_mk; }
name const & get_fin_ne_of_vne_name() { return *g_fin_ne_of_vne; }
name const & get_forall_congr_name() { return *g_forall_congr; }

1
src/library/constants.h
View file

@ -64,6 +64,7 @@ name const & get_false_name();
name const & get_false_of_true_iff_false_name();
name const & get_false_of_true_eq_false_name();
name const & get_false_rec_name();
name const & get_false_cases_on_name();
name const & get_fin_mk_name();
name const & get_fin_ne_of_vne_name();
name const & get_forall_congr_name();

1
src/library/constants.txt
View file

@ -57,6 +57,7 @@ false
false_of_true_iff_false
false_of_true_eq_false
false.rec
false.cases_on
fin.mk
fin.ne_of_vne
forall_congr