fix: mod 0

Author: hargoniX

src/Init/Data/SInt/Basic.lean

@@ -87,7 +87,7 @@ def Int8.mul (a b : Int8) : Int8 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
 @[extern "lean_int8_div"]
 def Int8.div (a b : Int8) : Int8 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 @[extern "lean_int8_mod"]
-def Int8.mod (a b : Int8) : Int8 := ⟨⟨BitVec.smod a.toBitVec b.toBitVec⟩⟩
+def Int8.mod (a b : Int8) : Int8 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
 @[extern "lean_int8_land"]
 def Int8.land (a b : Int8) : Int8 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
 @[extern "lean_int8_lor"]
@@ -184,7 +184,7 @@ def Int16.mul (a b : Int16) : Int16 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
 @[extern "lean_int16_div"]
 def Int16.div (a b : Int16) : Int16 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 @[extern "lean_int16_mod"]
-def Int16.mod (a b : Int16) : Int16 := ⟨⟨BitVec.smod a.toBitVec b.toBitVec⟩⟩
+def Int16.mod (a b : Int16) : Int16 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
 @[extern "lean_int16_land"]
 def Int16.land (a b : Int16) : Int16 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
 @[extern "lean_int16_lor"]
@@ -285,7 +285,7 @@ def Int32.mul (a b : Int32) : Int32 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
 @[extern "lean_int32_div"]
 def Int32.div (a b : Int32) : Int32 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 @[extern "lean_int32_mod"]
-def Int32.mod (a b : Int32) : Int32 := ⟨⟨BitVec.smod a.toBitVec b.toBitVec⟩⟩
+def Int32.mod (a b : Int32) : Int32 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
 @[extern "lean_int32_land"]
 def Int32.land (a b : Int32) : Int32 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
 @[extern "lean_int32_lor"]
@@ -390,7 +390,7 @@ def Int64.mul (a b : Int64) : Int64 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
 @[extern "lean_int64_div"]
 def Int64.div (a b : Int64) : Int64 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 @[extern "lean_int64_mod"]
-def Int64.mod (a b : Int64) : Int64 := ⟨⟨BitVec.smod a.toBitVec b.toBitVec⟩⟩
+def Int64.mod (a b : Int64) : Int64 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
 @[extern "lean_int64_land"]
 def Int64.land (a b : Int64) : Int64 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
 @[extern "lean_int64_lor"]

src/include/lean/lean.h

@@ -1928,7 +1928,7 @@ static inline uint8_t lean_int8_mod(uint8_t a1, uint8_t a2) {
     int8_t lhs = (int8_t) a1;
     int8_t rhs = (int8_t) a2;
 
-    return (uint8_t)(rhs == 0 ? 0 : lhs % rhs);
+    return (uint8_t)(rhs == 0 ? lhs : lhs % rhs);
 }
 
 static inline uint8_t lean_int8_land(uint8_t a1, uint8_t a2) {
@@ -2068,7 +2068,7 @@ static inline uint16_t lean_int16_mod(uint16_t a1, uint16_t a2) {
     int16_t lhs = (int16_t) a1;
     int16_t rhs = (int16_t) a2;
 
-    return (uint16_t)(rhs == 0 ? 0 : lhs % rhs);
+    return (uint16_t)(rhs == 0 ? lhs : lhs % rhs);
 }
 
 static inline uint16_t lean_int16_land(uint16_t a1, uint16_t a2) {
@@ -2207,7 +2207,7 @@ static inline uint32_t lean_int32_mod(uint32_t a1, uint32_t a2) {
     int32_t lhs = (int32_t) a1;
     int32_t rhs = (int32_t) a2;
 
-    return (uint32_t)(rhs == 0 ? 0 : lhs % rhs);
+    return (uint32_t)(rhs == 0 ? lhs : lhs % rhs);
 }
 
 static inline uint32_t lean_int32_land(uint32_t a1, uint32_t a2) {
@@ -2346,7 +2346,7 @@ static inline uint64_t lean_int64_mod(uint64_t a1, uint64_t a2) {
     int64_t lhs = (int64_t) a1;
     int64_t rhs = (int64_t) a2;
 
-    return (uint64_t)(rhs == 0 ? 0 : lhs % rhs);
+    return (uint64_t)(rhs == 0 ? lhs : lhs % rhs);
 }
 
 static inline uint64_t lean_int64_land(uint64_t a1, uint64_t a2) {

tests/lean/sint_basic.lean

@@ -34,7 +34,8 @@
 #eval (10 : Int8) / -2 = -5
 #eval (10 : Int8) / 0 = 0
 #eval (10 : Int8) % 1 = 0
-#eval (10 : Int8) % 0 = 0
+#eval (10 : Int8) % 0 = 10
+#eval (-10 : Int8) % 0 = -10
 #eval (10 : Int8) % 3 = 1
 #eval (-10 : Int8) % 3 = -1
 #eval (-10 : Int8) % -3 = -1
@@ -139,7 +140,8 @@ def myId8 (x : Int8) : Int8 := x
 #eval (10 : Int16) / -2 = -5
 #eval (10 : Int16) / 0 = 0
 #eval (10 : Int16) % 1 = 0
-#eval (10 : Int16) % 0 = 0
+#eval (10 : Int16) % 0 = 10
+#eval (-10 : Int16) % 0 = -10
 #eval (10 : Int16) % 3 = 1
 #eval (-10 : Int16) % 3 = -1
 #eval (-10 : Int16) % -3 = -1
@@ -220,7 +222,8 @@ def myId16 (x : Int16) : Int16 := x
 #eval (10 : Int32) / -2 = -5
 #eval (10 : Int32) / 0 = 0
 #eval (10 : Int32) % 1 = 0
-#eval (10 : Int32) % 0 = 0
+#eval (10 : Int32) % 0 = 10
+#eval (-10 : Int32) % 0 = -10
 #eval (10 : Int32) % 3 = 1
 #eval (-10 : Int32) % 3 = -1
 #eval (-10 : Int32) % -3 = -1
@@ -300,7 +303,8 @@ def myId32 (x : Int32) : Int32 := x
 #eval (10 : Int64) / -2 = -5
 #eval (10 : Int64) / 0 = 0
 #eval (10 : Int64) % 1 = 0
-#eval (10 : Int64) % 0 = 0
+#eval (10 : Int64) % 0 = 10
+#eval (-10 : Int64) % 0 = -10
 #eval (10 : Int64) % 3 = 1
 #eval (-10 : Int64) % 3 = -1
 #eval (-10 : Int64) % -3 = -1

tests/lean/sint_basic.lean.expected.out

@@ -71,6 +71,7 @@ true
 true
 true
 true
+true
 
 [result]
 def myId8 (x_1 : u8) : u8 :=
@@ -154,6 +155,7 @@ true
 true
 true
 true
+true
 
 [result]
 def myId16 (x_1 : u16) : u16 :=
@@ -237,6 +239,7 @@ true
 true
 true
 true
+true
 
 [result]
 def myId32 (x_1 : u32) : u32 :=
@@ -320,6 +323,7 @@ true
 true
 true
 true
+true
 
 [result]
 def myId64 (x_1 : u64) : u64 :=