From fc334ffbee0ff00fa61faf71d890706e752da2aa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 5 Sep 2021 19:15:59 -0700
Subject: [PATCH] fix: pattern matching on `UInt`

---
 src/library/compiler/erase_irrelevant.cpp | 12 ++++++++++++
 tests/lean/uintMatch.lean                 | 15 +++++++++++++++
 tests/lean/uintMatch.lean.expected.out    |  5 +++++
 3 files changed, 32 insertions(+)
 create mode 100644 tests/lean/uintMatch.lean
 create mode 100644 tests/lean/uintMatch.lean.expected.out

diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
index c735eb9374..c57dde090b 100644
--- a/src/library/compiler/erase_irrelevant.cpp
+++ b/src/library/compiler/erase_irrelevant.cpp
@@ -210,6 +210,16 @@ class erase_irrelevant_fn {
                            binding_body(minor));
     }
 
+    expr elim_uint_cases(name const & uint_name, buffer<expr> & args) {
+        lean_assert(args.size() == 3);
+        expr major = visit(args[1]);
+        expr minor = visit_minor(args[2]);
+        lean_assert(is_lambda(minor));
+        return
+          ::lean::mk_let(next_name(), mk_enf_object_type(), mk_app(mk_const(name(uint_name, "toNat")), major),
+                         binding_body(minor));
+    }
+
     expr decidable_to_bool_cases(buffer<expr> const & args) {
         lean_assert(args.size() == 5);
         expr const & major  = args[2];
@@ -235,6 +245,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_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()) {
             return decidable_to_bool_cases(args);
         } else {
diff --git a/tests/lean/uintMatch.lean b/tests/lean/uintMatch.lean
new file mode 100644
index 0000000000..8629d96708
--- /dev/null
+++ b/tests/lean/uintMatch.lean
@@ -0,0 +1,15 @@
+def f : UInt8 → Bool
+ | 5 => true
+ | _ => false
+
+#eval f 8
+#eval f 5
+
+def g : UInt32 → String
+ | 5    => "hello"
+ | 1555 => "world"
+ | _    => "bla"
+
+#eval g 5
+#eval g 1555
+#eval g 555
diff --git a/tests/lean/uintMatch.lean.expected.out b/tests/lean/uintMatch.lean.expected.out
new file mode 100644
index 0000000000..e128aed1b3
--- /dev/null
+++ b/tests/lean/uintMatch.lean.expected.out
@@ -0,0 +1,5 @@
+false
+true
+"hello"
+"world"
+"bla"