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

fix(library/compiler/erase_irrelevant): add elim_array_cases

Browse source
This commit is contained in:
Leonardo de Moura 2019-09-19 10:47:05 -07:00
parent a4b860b92a
commit 0bd268fc96
4 changed files with 25 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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<expr> & 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<expr> 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 {

8
src/library/constants.cpp
View file

@ -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; }

2
src/library/constants.h
View file

@ -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();

2
src/library/constants.txt
View file

@ -6,6 +6,8 @@ And.intro
And.rec
And.casesOn
Array
Array.sz
Array.data
autoParam
bit0
bit1