From 112f183be4dc789e709f2fccdab25b9e9428840c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Sep 2018 14:26:29 -0700 Subject: [PATCH] feat(library/compiler/lcnf): eliminate `false.cases_on` and `eq.cases_on` --- src/library/compiler/lcnf.cpp | 18 +++++++++++++----- src/library/constants.cpp | 4 ++++ src/library/constants.h | 1 + src/library/constants.txt | 1 + 4 files changed, 19 insertions(+), 5 deletions(-) diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index ae4484ed5e..39a73d14ab 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -213,12 +213,18 @@ public: } expr visit_eq_rec(expr const & fn, buffer & 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); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 1340762354..518935f7af 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -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; } diff --git a/src/library/constants.h b/src/library/constants.h index 13fe64f34f..d227513f7b 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index efe996e5a8..d44aba757a 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -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