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

fix: compiler support for FloatArray.casesOn and ByteArray.casesOn

Browse source 
closes #1311
This commit is contained in:
Leonardo de Moura 2022-07-24 12:36:08 -07:00
parent 7829be9d54
commit 5253cc6742
2 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -219,6 +219,16 @@ class erase_irrelevant_fn {
binding_body(minor));
}
expr elim_scalar_array_cases(buffer<expr> & args) {
lean_always_assert(args.size() == 3);
expr major = visit(args[1]);
expr minor = visit_minor(args[2]);
lean_always_assert(is_lambda(minor));
return
::lean::mk_let(next_name(), mk_enf_object_type(), major,
binding_body(minor));
}
expr elim_uint_cases(name const & uint_name, buffer<expr> & args) {
lean_always_assert(args.size() == 3);
expr major = visit(args[1]);
@ -254,6 +264,8 @@ class erase_irrelevant_fn {
return elim_int_cases(args);
} else if (I_name == get_array_name()) {
return elim_array_cases(args);
} else if (I_name == get_float_array_name() || I_name == get_byte_array_name()) {
return elim_scalar_array_cases(args);
} else if (I_name == get_uint8_name() || I_name == get_uint16_name() || I_name == get_uint32_name() || I_name == get_uint64_name() || I_name == get_usize_name()) {
return elim_uint_cases(I_name, args);
} else if (I_name == get_decidable_name()) {

7
tests/lean/run/1311.lean Normal file
View file

@ -0,0 +1,7 @@
instance : DecidableEq ByteArray
| ⟨a⟩, ⟨b⟩ => match decEq a b with
| isTrue h₁ => isTrue $ congrArg ByteArray.mk h₁
| isFalse h₂ => isFalse $ fun h => by cases h; cases (h₂ rfl)
#eval ByteArray.empty = ByteArray.empty
#eval ByteArray.empty != ByteArray.empty.push 5