fix: expose Int* definitions for simprocs and decide (fixes leanprover#10546) (leanprover#10631)

This PR exposes the definitions about `Int*`. The main reason is that
the `SInt` simprocs require many of them to be exposed. Furthermore,
`decide` now works with `Int*` operations. This fixes leanprover#10631.

Author: datokrat

src/Init/Data/SInt/Basic.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Data.UInt.Basic
 
-public section
+@[expose] public section
 
 set_option linter.missingDocs true
 
@@ -23,7 +23,7 @@ Signed 8-bit integers.
 This type has special support in the compiler so it can be represented by an unboxed 8-bit value.
 -/
 structure Int8 where
-  private ofUInt8 ::
+  ofUInt8 ::
   /--
   Converts an 8-bit signed integer into the 8-bit unsigned integer that is its two's complement
   encoding.
@@ -36,7 +36,7 @@ Signed 16-bit integers.
 This type has special support in the compiler so it can be represented by an unboxed 16-bit value.
 -/
 structure Int16 where
-  private ofUInt16 ::
+  ofUInt16 ::
   /--
   Converts an 16-bit signed integer into the 16-bit unsigned integer that is its two's complement
   encoding.
@@ -49,7 +49,7 @@ Signed 32-bit integers.
 This type has special support in the compiler so it can be represented by an unboxed 32-bit value.
 -/
 structure Int32 where
-  private ofUInt32 ::
+  ofUInt32 ::
   /--
   Converts an 32-bit signed integer into the 32-bit unsigned integer that is its two's complement
   encoding.
@@ -62,7 +62,7 @@ Signed 64-bit integers.
 This type has special support in the compiler so it can be represented by an unboxed 64-bit value.
 -/
 structure Int64 where
-  private ofUInt64 ::
+  ofUInt64 ::
   /--
   Converts an 64-bit signed integer into the 64-bit unsigned integer that is its two's complement
   encoding.
@@ -76,7 +76,7 @@ On a 32-bit architecture, `ISize` is equivalent to `Int32`. On a 64-bit machine,
 `Int64`. This type has special support in the compiler so it can be represented by an unboxed value.
 -/
 structure ISize where
-  private ofUSize ::
+  ofUSize ::
   /--
   Converts a word-sized signed integer into the word-sized unsigned integer that is its two's
   complement encoding.

tests/lean/run/simpSInt.lean

@@ -1,3 +1,5 @@
+module
+
 #check_simp (-64 : Int8).toBitVec ~> 192#8
 #check_simp (-64 : Int16).toBitVec ~> 65472#16
 #check_simp (-64 : Int32).toBitVec ~> 4294967232#32

tests/lean/run/simprocSInt.lean

@@ -1,3 +1,5 @@
+module
+
 section
 
 variable (x : Int)
@@ -30,6 +32,9 @@ section
 
 variable (x : Int8)
 
+example : (5 : Int8) = 5 := by decide
+example : (5 : Int8) ≤ 5 := by decide
+example : (5 : Int8) < 6 := by decide
 example : Int8.toInt (-(-(-8))) + 8 = 0 := by simp +ground only
 example : Int8.toInt (-8) + 8 = 0 := by simp +ground only
 #check_simp (-5 : Int8).toNatClampNeg ~> 0
@@ -73,6 +78,9 @@ section
 
 variable (x : Int16)
 
+example : (5 : Int16) = 5 := by decide
+example : (5 : Int16) ≤ 5 := by decide
+example : (5 : Int16) < 6 := by decide
 example : Int16.toInt (-(-(-16))) + 16 = 0 := by simp +ground only
 example : Int16.toInt (-16) + 16 = 0 := by simp +ground only
 #check_simp (-5 : Int16).toNatClampNeg ~> 0
@@ -111,6 +119,9 @@ section
 
 variable (x : Int32)
 
+example : (5 : Int32) = 5 := by decide
+example : (5 : Int32) ≤ 5 := by decide
+example : (5 : Int32) < 6 := by decide
 example : Int32.toInt (-(-(-32))) + 32 = 0 := by simp +ground only
 example : Int32.toInt (-32) + 32 = 0 := by simp +ground only
 #check_simp (-5 : Int32).toNatClampNeg ~> 0
@@ -149,6 +160,9 @@ section
 
 variable (x : Int64)
 
+example : (5 : Int64) = 5 := by decide
+example : (5 : Int64) ≤ 5 := by decide
+example : (5 : Int64) < 6 := by decide
 example : Int64.toInt (-(-(-64))) + 64 = 0 := by simp +ground only
 example : Int64.toInt (-64) + 64 = 0 := by simp +ground only
 #check_simp (-5 : Int64).toNatClampNeg ~> 0

tests/lean/run/simprocUInt.lean

@@ -1,3 +1,5 @@
+module
+
 section
 
 variable (x : Nat)
@@ -17,6 +19,9 @@ section
 
 variable (x : UInt8)
 
+example : (5 : UInt8) = 5 := by decide
+example : (5 : UInt8) ≤ 5 := by decide
+example : (5 : UInt8) < 6 := by decide
 #check_simp x = 2 + 3 ~> x = 5
 #check_simp x = 2 * 3 ~> x = 6
 #check_simp x = 2 - 3 ~> x = 255
@@ -40,6 +45,9 @@ section
 
 variable (x : UInt16)
 
+example : (5 : UInt16) = 5 := by decide
+example : (5 : UInt16) ≤ 5 := by decide
+example : (5 : UInt16) < 6 := by decide
 #check_simp x = 2 + 3 ~> x = 5
 #check_simp x = 2 * 3 ~> x = 6
 #check_simp x = 2 - 3 ~> x = 65535
@@ -63,6 +71,9 @@ section
 
 variable (x : UInt32)
 
+example : (5 : UInt32) = 5 := by decide
+example : (5 : UInt32) ≤ 5 := by decide
+example : (5 : UInt32) < 6 := by decide
 #check_simp x = 2 + 3 ~> x = 5
 #check_simp x = 2 * 3 ~> x = 6
 #check_simp x = 2 - 3 ~> x = 4294967295
@@ -86,6 +97,9 @@ section
 
 variable (x : UInt64)
 
+example : (5 : UInt64) = 5 := by decide
+example : (5 : UInt64) ≤ 5 := by decide
+example : (5 : UInt64) < 6 := by decide
 #check_simp x = 2 + 3 ~> x = 5
 #check_simp x = 2 * 3 ~> x = 6
 #check_simp x = 2 - 3 ~> x = 18446744073709551615

tests/lean/sint_basic.lean

@@ -1,3 +1,5 @@
+module
+
 #check Int8
 #eval Int8.ofInt 20
 #eval Int8.ofInt (-20)

tests/lean/sint_basic.lean.expected.out

@@ -73,11 +73,11 @@ true
 true
 true
 [Compiler.IR] [result]
-    def myId8 (x_1 : u8) : u8 :=
+    def _private.sint_basic.0.myId8 (x_1 : u8) : u8 :=
       ret x_1
-    def myId8._boxed (x_1 : tagged) : tagged :=
+    def _private.sint_basic.0.myId8._boxed (x_1 : tagged) : tagged :=
       let x_2 : u8 := unbox x_1;
-      let x_3 : u8 := myId8 x_2;
+      let x_3 : u8 := _private.sint_basic.0.myId8 x_2;
       let x_4 : tobj := box x_3;
       ret x_4
 Int16 : Type
@@ -155,11 +155,11 @@ true
 true
 true
 [Compiler.IR] [result]
-    def myId16 (x_1 : u16) : u16 :=
+    def _private.sint_basic.0.myId16 (x_1 : u16) : u16 :=
       ret x_1
-    def myId16._boxed (x_1 : tagged) : tagged :=
+    def _private.sint_basic.0.myId16._boxed (x_1 : tagged) : tagged :=
       let x_2 : u16 := unbox x_1;
-      let x_3 : u16 := myId16 x_2;
+      let x_3 : u16 := _private.sint_basic.0.myId16 x_2;
       let x_4 : tobj := box x_3;
       ret x_4
 Int32 : Type
@@ -237,12 +237,12 @@ true
 true
 true
 [Compiler.IR] [result]
-    def myId32 (x_1 : u32) : u32 :=
+    def _private.sint_basic.0.myId32 (x_1 : u32) : u32 :=
       ret x_1
-    def myId32._boxed (x_1 : tobj) : tobj :=
+    def _private.sint_basic.0.myId32._boxed (x_1 : tobj) : tobj :=
       let x_2 : u32 := unbox x_1;
       dec x_1;
-      let x_3 : u32 := myId32 x_2;
+      let x_3 : u32 := _private.sint_basic.0.myId32 x_2;
       let x_4 : tobj := box x_3;
       ret x_4
 Int64 : Type
@@ -320,12 +320,12 @@ true
 true
 true
 [Compiler.IR] [result]
-    def myId64 (x_1 : u64) : u64 :=
+    def _private.sint_basic.0.myId64 (x_1 : u64) : u64 :=
       ret x_1
-    def myId64._boxed (x_1 : tobj) : tobj :=
+    def _private.sint_basic.0.myId64._boxed (x_1 : tobj) : tobj :=
       let x_2 : u64 := unbox x_1;
       dec x_1;
-      let x_3 : u64 := myId64 x_2;
+      let x_3 : u64 := _private.sint_basic.0.myId64 x_2;
       let x_4 : tobj := box x_3;
       ret x_4
 ISize : Type
@@ -403,11 +403,11 @@ true
 true
 true
 [Compiler.IR] [result]
-    def myIdSize (x_1 : usize) : usize :=
+    def _private.sint_basic.0.myIdSize (x_1 : usize) : usize :=
       ret x_1
-    def myIdSize._boxed (x_1 : tobj) : tobj :=
+    def _private.sint_basic.0.myIdSize._boxed (x_1 : tobj) : tobj :=
       let x_2 : usize := unbox x_1;
       dec x_1;
-      let x_3 : usize := myIdSize x_2;
+      let x_3 : usize := _private.sint_basic.0.myIdSize x_2;
       let x_4 : tobj := box x_3;
       ret x_4

tests/lean/test_single.sh

@@ -2,5 +2,5 @@
 source ../common.sh
 
 # these tests don't have to succeed
-exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true "$f" || true
+exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f" || true
 diff_produced