From 0bd268fc96addfda0d9903efff120340a2589298 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Sep 2019 10:47:05 -0700 Subject: [PATCH] fix(library/compiler/erase_irrelevant): add `elim_array_cases` --- src/library/compiler/erase_irrelevant.cpp | 13 +++++++++++++ src/library/constants.cpp | 8 ++++++++ src/library/constants.h | 2 ++ src/library/constants.txt | 2 ++ 4 files changed, 25 insertions(+) diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index bcb634e2b6..03e0a016b8 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -200,6 +200,17 @@ class erase_irrelevant_fn { return mk_app(mk_constant(get_bool_cases_on_name()), c, minor_p, minor_n); } + expr elim_array_cases(buffer & args) { + lean_assert(args.size() == 4); + expr major = visit(args[2]); + expr minor = visit_minor(args[3]); + lean_assert(is_lambda(minor)); + return + ::lean::mk_let(next_name(), mk_enf_object_type(), mk_app(mk_constant(get_array_sz_name()), mk_enf_neutral(), major), + ::lean::mk_let(next_name(), mk_enf_object_type(), mk_app(mk_constant(get_array_data_name()), mk_enf_neutral(), major), + binding_body(binding_body(minor)))); + } + expr decidable_to_bool_cases(buffer const & args) { lean_assert(args.size() == 5); expr const & major = args[2]; @@ -223,6 +234,8 @@ class erase_irrelevant_fn { return elim_nat_cases(args); } else if (I_name == get_int_name()) { return elim_int_cases(args); + } else if (I_name == get_array_name()) { + return elim_array_cases(args); } else if (I_name == get_decidable_name()) { return decidable_to_bool_cases(args); } else { diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 7ac76d40fb..5d27e42e58 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -11,6 +11,8 @@ name const * g_and_intro = nullptr; name const * g_and_rec = nullptr; name const * g_and_cases_on = nullptr; name const * g_array = nullptr; +name const * g_array_sz = nullptr; +name const * g_array_data = nullptr; name const * g_auto_param = nullptr; name const * g_bit0 = nullptr; name const * g_bit1 = nullptr; @@ -193,6 +195,8 @@ void initialize_constants() { g_and_rec = new name{"And", "rec"}; g_and_cases_on = new name{"And", "casesOn"}; g_array = new name{"Array"}; + g_array_sz = new name{"Array", "sz"}; + g_array_data = new name{"Array", "data"}; g_auto_param = new name{"autoParam"}; g_bit0 = new name{"bit0"}; g_bit1 = new name{"bit1"}; @@ -376,6 +380,8 @@ void finalize_constants() { delete g_and_rec; delete g_and_cases_on; delete g_array; + delete g_array_sz; + delete g_array_data; delete g_auto_param; delete g_bit0; delete g_bit1; @@ -558,6 +564,8 @@ name const & get_and_intro_name() { return *g_and_intro; } name const & get_and_rec_name() { return *g_and_rec; } name const & get_and_cases_on_name() { return *g_and_cases_on; } name const & get_array_name() { return *g_array; } +name const & get_array_sz_name() { return *g_array_sz; } +name const & get_array_data_name() { return *g_array_data; } name const & get_auto_param_name() { return *g_auto_param; } name const & get_bit0_name() { return *g_bit0; } name const & get_bit1_name() { return *g_bit1; } diff --git a/src/library/constants.h b/src/library/constants.h index 569e0bc653..97b481523f 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -13,6 +13,8 @@ name const & get_and_intro_name(); name const & get_and_rec_name(); name const & get_and_cases_on_name(); name const & get_array_name(); +name const & get_array_sz_name(); +name const & get_array_data_name(); name const & get_auto_param_name(); name const & get_bit0_name(); name const & get_bit1_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index fa59593d8b..ffe7c98937 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -6,6 +6,8 @@ And.intro And.rec And.casesOn Array +Array.sz +Array.data autoParam bit0 bit1