From cc7d7422db923dede9eb2cc8007fc3fb1f0ef0c2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 14 Nov 2020 12:50:32 -0800
Subject: [PATCH] fix: UInt ctors/fields in generated code

---
 src/Init/Prelude.lean                  | 15 ++++++++++++
 tests/lean/uintCtors.lean              | 34 ++++++++++++++++++++++++++
 tests/lean/uintCtors.lean.expected.out | 22 +++++++++++++++++
 3 files changed, 71 insertions(+)
 create mode 100644 tests/lean/uintCtors.lean
 create mode 100644 tests/lean/uintCtors.lean.expected.out

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 21f4109e1a..a9f7f93a9c 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -600,6 +600,9 @@ def UInt8.size : Nat := 256
 structure UInt8 :=
   (val : Fin UInt8.size)
 
+attribute [extern "lean_uint8_of_nat"] UInt8.mk
+attribute [extern "lean_uint8_to_nat"] UInt8.val
+
 @[extern "lean_uint8_of_nat"]
 def UInt8.ofNatCore (n : @& Nat) (h : Less n UInt8.size) : UInt8 := {
   val := { val := n, isLt := h }
@@ -622,6 +625,9 @@ def UInt16.size : Nat := 65536
 structure UInt16 :=
   (val : Fin UInt16.size)
 
+attribute [extern "lean_uint16_of_nat"] UInt16.mk
+attribute [extern "lean_uint16_to_nat"] UInt16.val
+
 @[extern "lean_uint16_of_nat"]
 def UInt16.ofNatCore (n : @& Nat) (h : Less n UInt16.size) : UInt16 := {
   val := { val := n, isLt := h }
@@ -644,6 +650,9 @@ def UInt32.size : Nat := 4294967296
 structure UInt32 :=
   (val : Fin UInt32.size)
 
+attribute [extern "lean_uint32_of_nat"] UInt32.mk
+attribute [extern "lean_uint32_to_nat"] UInt32.val
+
 @[extern "lean_uint32_of_nat"]
 def UInt32.ofNatCore (n : @& Nat) (h : Less n UInt32.size) : UInt32 := {
   val := { val := n, isLt := h }
@@ -690,6 +699,9 @@ def UInt64.size : Nat := 18446744073709551616
 structure UInt64 :=
   (val : Fin UInt64.size)
 
+attribute [extern "lean_uint64_of_nat"] UInt64.mk
+attribute [extern "lean_uint64_to_nat"] UInt64.val
+
 @[extern "lean_uint64_of_nat"]
 def UInt64.ofNatCore (n : @& Nat) (h : Less n UInt64.size) : UInt64 := {
   val := { val := n, isLt := h }
@@ -719,6 +731,9 @@ theorem usizeSzEq : Or (Eq USize.size 4294967296) (Eq USize.size 184467440737095
 structure USize :=
   (val : Fin USize.size)
 
+attribute [extern "lean_usize_of_nat"] USize.mk
+attribute [extern "lean_usize_to_nat"] USize.val
+
 @[extern "lean_usize_of_nat"]
 def USize.ofNatCore (n : @& Nat) (h : Less n USize.size) : USize := {
   val := { val := n, isLt := h }
diff --git a/tests/lean/uintCtors.lean b/tests/lean/uintCtors.lean
new file mode 100644
index 0000000000..a885508cb8
--- /dev/null
+++ b/tests/lean/uintCtors.lean
@@ -0,0 +1,34 @@
+def UInt32.ofNatCore' (n : Nat) (h : Less n UInt32.size) : UInt32 := {
+  val := { val := n, isLt := h }
+}
+
+#eval UInt32.ofNatCore' 10 decide!
+
+def UInt64.ofNatCore' (n : Nat) (h : Less n UInt64.size) : UInt64 := {
+  val := { val := n, isLt := h }
+}
+
+#eval UInt64.ofNatCore' 3 decide!
+
+#eval toString $ { val := { val := 3, isLt := decide! } : UInt8 }
+#eval (3 : UInt8).val
+#eval toString $ { val := { val := 3, isLt := decide! } : UInt16 }
+#eval (3 : UInt16).val
+#eval toString $ { val := { val := 3, isLt := decide! } : UInt32 }
+#eval (3 : UInt32).val
+#eval toString $ { val := { val := 3, isLt := decide! } : UInt64 }
+#eval (3 : UInt64).val
+#eval toString $ { val := { val := 3, isLt := (match USize.size, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide!) } : USize }
+#eval (3 : USize).val
+
+
+#eval toString $ { val := { val := 4, isLt := decide! } : UInt8 }
+#eval (4 : UInt8).val
+#eval toString $ { val := { val := 4, isLt := decide! } : UInt16 }
+#eval (4 : UInt16).val
+#eval toString $ { val := { val := 4, isLt := decide! } : UInt32 }
+#eval (4 : UInt32).val
+#eval toString $ { val := { val := 4, isLt := decide! } : UInt64 }
+#eval (4 : UInt64).val
+#eval toString $ { val := { val := 4, isLt := (match USize.size, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide!) } : USize }
+#eval (4 : USize).val
diff --git a/tests/lean/uintCtors.lean.expected.out b/tests/lean/uintCtors.lean.expected.out
new file mode 100644
index 0000000000..b7a86a1ff6
--- /dev/null
+++ b/tests/lean/uintCtors.lean.expected.out
@@ -0,0 +1,22 @@
+10
+3
+"3"
+3
+"3"
+3
+"3"
+3
+"3"
+3
+"3"
+3
+"4"
+4
+"4"
+4
+"4"
+4
+"4"
+4
+"4"
+4