chore: rename UIntX.mk -> UIntX.ofBitVec (#7046)

This PR renames `UIntX.mk` to `UIntX.ofBitVec` and adds deprecations.

src/Init/Data/UInt/Basic.lean

@@ -9,6 +9,10 @@ import Init.Data.BitVec.Basic
 
 open Nat
 
+@[deprecated UInt8.ofBitVec (since := "2025-02-12"), inherit_doc UInt8.ofBitVec]
+def UInt8.mk (bitVec : BitVec 8) : UInt8 :=
+  UInt8.ofBitVec bitVec
+
 @[extern "lean_uint8_add"]
 def UInt8.add (a b : UInt8) : UInt8 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint8_sub"]
@@ -72,6 +76,10 @@ instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
 instance : Max UInt8 := maxOfLe
 instance : Min UInt8 := minOfLe
 
+@[deprecated UInt16.ofBitVec (since := "2025-02-12"), inherit_doc UInt16.ofBitVec]
+def UInt16.mk (bitVec : BitVec 16) : UInt16 :=
+  UInt16.ofBitVec bitVec
+
 @[extern "lean_uint16_add"]
 def UInt16.add (a b : UInt16) : UInt16 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint16_sub"]
@@ -137,6 +145,10 @@ instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
 instance : Max UInt16 := maxOfLe
 instance : Min UInt16 := minOfLe
 
+@[deprecated UInt32.ofBitVec (since := "2025-02-12"), inherit_doc UInt32.ofBitVec]
+def UInt32.mk (bitVec : BitVec 32) : UInt32 :=
+  UInt32.ofBitVec bitVec
+
 @[extern "lean_uint32_add"]
 def UInt32.add (a b : UInt32) : UInt32 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint32_sub"]
@@ -187,6 +199,10 @@ instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
 @[extern "lean_bool_to_uint32"]
 def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
 
+@[deprecated UInt64.ofBitVec (since := "2025-02-12"), inherit_doc UInt64.ofBitVec]
+def UInt64.mk (bitVec : BitVec 64) : UInt64 :=
+  UInt64.ofBitVec bitVec
+
 @[extern "lean_uint64_add"]
 def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint64_sub"]
@@ -250,6 +266,10 @@ instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 instance : Max UInt64 := maxOfLe
 instance : Min UInt64 := minOfLe
 
+@[deprecated USize.ofBitVec (since := "2025-02-12"), inherit_doc USize.ofBitVec]
+def USize.mk (bitVec : BitVec System.Platform.numBits) : USize :=
+  USize.ofBitVec bitVec
+
 theorem usize_size_le : USize.size ≤ 18446744073709551616 := by
   cases usize_size_eq <;> next h => rw [h]; decide
 

src/Init/Data/UInt/Lemmas.lean

@@ -22,7 +22,10 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   theorem mod_def (a b : $typeName) : a % b = ⟨a.toBitVec % b.toBitVec⟩ := rfl
   theorem add_def (a b : $typeName) : a + b = ⟨a.toBitVec + b.toBitVec⟩ := rfl
 
-  @[simp] theorem toNat_mk : (mk a).toNat = a.toNat := rfl
+  @[simp] theorem toNat_ofBitVec : (ofBitVec a).toNat = a.toNat := rfl
+
+  @[deprecated toNat_ofBitVec (since := "2025-02-12")]
+  theorem toNat_mk : (ofBitVec a).toNat = a.toNat := rfl
 
   @[simp] theorem toNat_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ $bits := BitVec.toNat_ofNat ..
 
@@ -32,7 +35,11 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
 
   theorem toNat_toBitVec_eq_toNat (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
 
-  @[simp] theorem mk_toBitVec_eq : ∀ (a : $typeName), mk a.toBitVec = a
+  @[simp] theorem ofBitVec_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
+    | ⟨_, _⟩ => rfl
+
+  @[deprecated ofBitVec_toBitVec_eq (since := "2025-02-12")]
+  theorem mk_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
     | ⟨_, _⟩ => rfl
 
   theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
@@ -177,7 +184,10 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
 
   @[simp]
-  theorem mk_ofNat (n : Nat) : mk (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
+  theorem ofBitVec_ofNat (n : Nat) : ofBitVec (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
+
+  @[deprecated ofBitVec_ofNat (since := "2025-02-12")]
+  theorem mk_ofNat (n : Nat) : ofBitVec (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
 
   )
   if let some nbits := bits.raw.isNatLit? then

src/Init/Prelude.lean

@@ -1927,11 +1927,16 @@ The type of unsigned 8-bit integers. This type has special support in the
 compiler to make it actually 8 bits rather than wrapping a `Nat`.
 -/
 structure UInt8 where
-  /-- Unpack a `UInt8` as a `BitVec 8`.
-  This function is overridden with a native implementation. -/
+  /--
+  Create a `UInt8` from a `BitVec 8`. This function is overridden with a native implementation.
+  -/
+  ofBitVec ::
+  /--
+  Unpack a `UInt8` as a `BitVec 8`. This function is overridden with a native implementation.
+  -/
   toBitVec : BitVec 8
 
-attribute [extern "lean_uint8_of_nat_mk"] UInt8.mk
+attribute [extern "lean_uint8_of_nat_mk"] UInt8.ofBitVec
 attribute [extern "lean_uint8_to_nat"] UInt8.toBitVec
 
 /--
@@ -1976,11 +1981,16 @@ The type of unsigned 16-bit integers. This type has special support in the
 compiler to make it actually 16 bits rather than wrapping a `Nat`.
 -/
 structure UInt16 where
-  /-- Unpack a `UInt16` as a `BitVec 16`.
-  This function is overridden with a native implementation. -/
+  /--
+  Create a `UInt16` from a `BitVec 16`. This function is overridden with a native implementation.
+  -/
+  ofBitVec ::
+  /--
+  Unpack a `UInt16` as a `BitVec 16`. This function is overridden with a native implementation.
+  -/
   toBitVec : BitVec 16
 
-attribute [extern "lean_uint16_of_nat_mk"] UInt16.mk
+attribute [extern "lean_uint16_of_nat_mk"] UInt16.ofBitVec
 attribute [extern "lean_uint16_to_nat"] UInt16.toBitVec
 
 /--
@@ -2025,11 +2035,16 @@ The type of unsigned 32-bit integers. This type has special support in the
 compiler to make it actually 32 bits rather than wrapping a `Nat`.
 -/
 structure UInt32 where
-  /-- Unpack a `UInt32` as a `BitVec 32.
-  This function is overridden with a native implementation. -/
+  /--
+  Create a `UInt32` from a `BitVec 32`. This function is overridden with a native implementation.
+  -/
+  ofBitVec ::
+  /--
+  Unpack a `UInt32` as a `BitVec 32`. This function is overridden with a native implementation.
+  -/
   toBitVec : BitVec 32
 
-attribute [extern "lean_uint32_of_nat_mk"] UInt32.mk
+attribute [extern "lean_uint32_of_nat_mk"] UInt32.ofBitVec
 attribute [extern "lean_uint32_to_nat"] UInt32.toBitVec
 
 /--
@@ -2105,11 +2120,16 @@ The type of unsigned 64-bit integers. This type has special support in the
 compiler to make it actually 64 bits rather than wrapping a `Nat`.
 -/
 structure UInt64 where
-  /-- Unpack a `UInt64` as a `BitVec 64`.
-  This function is overridden with a native implementation. -/
+  /--
+  Create a `UInt64` from a `BitVec 64`. This function is overridden with a native implementation.
+  -/
+  ofBitVec ::
+  /--
+  Unpack a `UInt64` as a `BitVec 64`. This function is overridden with a native implementation.
+  -/
   toBitVec: BitVec 64
 
-attribute [extern "lean_uint64_of_nat_mk"] UInt64.mk
+attribute [extern "lean_uint64_of_nat_mk"] UInt64.ofBitVec
 attribute [extern "lean_uint64_to_nat"] UInt64.toBitVec
 
 /--
@@ -2168,11 +2188,18 @@ For example, if running on a 32-bit machine, USize is equivalent to UInt32.
 Or on a 64-bit machine, UInt64.
 -/
 structure USize where
-  /-- Unpack a `USize` as a `BitVec System.Platform.numBits`.
-  This function is overridden with a native implementation. -/
+  /--
+  Create a `USize` from a `BitVec System.Platform.numBits`. This function is overridden with a
+  native implementation.
+  -/
+  ofBitVec ::
+  /--
+  Unpack a `USize` as a `BitVec System.Platform.numBits`. This function is overridden with a native
+  implementation.
+  -/
   toBitVec : BitVec System.Platform.numBits
 
-attribute [extern "lean_usize_of_nat_mk"] USize.mk
+attribute [extern "lean_usize_of_nat_mk"] USize.ofBitVec
 attribute [extern "lean_usize_to_nat"] USize.toBitVec
 
 /--
@@ -2208,6 +2235,7 @@ instance : DecidableEq USize := USize.decEq
 
 instance : Inhabited USize where
   default := USize.ofNatCore 0 usize_size_pos
+
 /--
 A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and
 it is also not a "surrogate" character (the range `0xd800` to `0xdfff` inclusive).

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -172,22 +172,22 @@ where
         return (x, toExpr <| value.bv == 1)
       | UInt8.toBitVec x =>
         if h : value.w = 8 then
-          return (x, toExpr <| UInt8.mk (h ▸ value.bv))
+          return (x, toExpr <| UInt8.ofBitVec (h ▸ value.bv))
         else
           throwError m!"Value for UInt8 was not 8 bit but {value.w} bit"
       | UInt16.toBitVec x =>
         if h : value.w = 16 then
-          return (x, toExpr <| UInt16.mk (h ▸ value.bv))
+          return (x, toExpr <| UInt16.ofBitVec (h ▸ value.bv))
         else
           throwError m!"Value for UInt16 was not 16 bit but {value.w} bit"
       | UInt32.toBitVec x =>
         if h : value.w = 32 then
-          return (x, toExpr <| UInt32.mk (h ▸ value.bv))
+          return (x, toExpr <| UInt32.ofBitVec (h ▸ value.bv))
         else
           throwError m!"Value for UInt32 was not 32 bit but {value.w} bit"
       | UInt64.toBitVec x =>
         if h : value.w = 64 then
-          return (x, toExpr <| UInt64.mk (h ▸ value.bv))
+          return (x, toExpr <| UInt64.ofBitVec (h ▸ value.bv))
         else
           throwError m!"Value for UInt64 was not 64 bit but {value.w} bit"
       | _ =>

tests/lean/run/trivial_uint.lean

@@ -8,8 +8,8 @@ example : UInt16.toBitVec 42 = 42 := by simp
 example : UInt32.toBitVec 42 = 42 := by simp
 example : UInt64.toBitVec 42 = 42 := by simp
 example : USize.toBitVec 42 = 42 := by simp
-example : UInt8.mk 42 = 42 := by simp
-example : UInt16.mk 42 = 42 := by simp
-example : UInt32.mk 42 = 42 := by simp
-example : UInt64.mk 42 = 42 := by simp
-example : USize.mk 42 = 42 := by simp
+example : UInt8.ofBitVec 42 = 42 := by simp
+example : UInt16.ofBitVec 42 = 42 := by simp
+example : UInt32.ofBitVec 42 = 42 := by simp
+example : UInt64.ofBitVec 42 = 42 := by simp
+example : USize.ofBitVec 42 = 42 := by simp