chore: rename UIntX.val -> UIntX.toFin (#7050)
This PR renames the functions `UIntX.val` to `UIntX.toFin`.
This commit is contained in:
Markus Himmel
GitHub
parent
ae9d12aeaa
commit
1ecb4a43ae
7 changed files with 57 additions and 30 deletions
|
|
@ -56,7 +56,7 @@ def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem
|
|||
instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
|
||||
getElem xs i h := xs.get i
|
||||
|
||||
instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
|
||||
instance : GetElem ByteArray USize UInt8 fun xs i => i.toFin < xs.size where
|
||||
getElem xs i h := xs.uget i h
|
||||
|
||||
@[extern "lean_byte_array_set"]
|
||||
|
|
|
|||
|
|
@ -62,7 +62,7 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
|
|||
instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
|
||||
getElem xs i h := xs.get i h
|
||||
|
||||
instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
|
||||
instance : GetElem FloatArray USize Float fun xs i => i.toNat < xs.size where
|
||||
getElem xs i h := xs.uget i h
|
||||
|
||||
@[extern "lean_float_array_uset"]
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
|
|||
@[extern "lean_uint8_mod"]
|
||||
def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
|
||||
@[deprecated UInt8.mod (since := "2024-09-23")]
|
||||
def UInt8.modn (a : UInt8) (n : Nat) : UInt8 := ⟨Fin.modn a.val n⟩
|
||||
def UInt8.modn (a : UInt8) (n : Nat) : UInt8 := ⟨Fin.modn a.toFin n⟩
|
||||
@[extern "lean_uint8_land"]
|
||||
def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩
|
||||
@[extern "lean_uint8_lor"]
|
||||
|
|
@ -91,7 +91,7 @@ def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec
|
|||
@[extern "lean_uint16_mod"]
|
||||
def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
|
||||
@[deprecated UInt16.mod (since := "2024-09-23")]
|
||||
def UInt16.modn (a : UInt16) (n : Nat) : UInt16 := ⟨Fin.modn a.val n⟩
|
||||
def UInt16.modn (a : UInt16) (n : Nat) : UInt16 := ⟨Fin.modn a.toFin n⟩
|
||||
@[extern "lean_uint16_land"]
|
||||
def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩
|
||||
@[extern "lean_uint16_lor"]
|
||||
|
|
@ -160,7 +160,7 @@ def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec
|
|||
@[extern "lean_uint32_mod"]
|
||||
def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
|
||||
@[deprecated UInt32.mod (since := "2024-09-23")]
|
||||
def UInt32.modn (a : UInt32) (n : Nat) : UInt32 := ⟨Fin.modn a.val n⟩
|
||||
def UInt32.modn (a : UInt32) (n : Nat) : UInt32 := ⟨Fin.modn a.toFin n⟩
|
||||
@[extern "lean_uint32_land"]
|
||||
def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩
|
||||
@[extern "lean_uint32_lor"]
|
||||
|
|
@ -214,7 +214,7 @@ def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec
|
|||
@[extern "lean_uint64_mod"]
|
||||
def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
|
||||
@[deprecated UInt64.mod (since := "2024-09-23")]
|
||||
def UInt64.modn (a : UInt64) (n : Nat) : UInt64 := ⟨Fin.modn a.val n⟩
|
||||
def UInt64.modn (a : UInt64) (n : Nat) : UInt64 := ⟨Fin.modn a.toFin n⟩
|
||||
@[extern "lean_uint64_land"]
|
||||
def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩
|
||||
@[extern "lean_uint64_lor"]
|
||||
|
|
@ -283,7 +283,7 @@ def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
|
|||
@[extern "lean_usize_mod"]
|
||||
def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
|
||||
@[deprecated USize.mod (since := "2024-09-23")]
|
||||
def USize.modn (a : USize) (n : Nat) : USize := ⟨Fin.modn a.val n⟩
|
||||
def USize.modn (a : USize) (n : Nat) : USize := ⟨Fin.modn a.toFin n⟩
|
||||
@[extern "lean_usize_land"]
|
||||
def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩
|
||||
@[extern "lean_usize_lor"]
|
||||
|
|
|
|||
|
|
@ -16,7 +16,10 @@ This file thus breaks the import cycle that would be created by this dependency.
|
|||
|
||||
open Nat
|
||||
|
||||
def UInt8.val (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
|
||||
/-- Converts a `UInt8` into the corresponding `Fin UInt8.size`. -/
|
||||
def UInt8.toFin (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
|
||||
@[deprecated UInt8.toFin (since := "2025-02-12"), inherit_doc UInt8.toFin]
|
||||
def UInt8.val (x : UInt8) : Fin UInt8.size := x.toFin
|
||||
@[extern "lean_uint8_of_nat"]
|
||||
def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩
|
||||
abbrev Nat.toUInt8 := UInt8.ofNat
|
||||
|
|
@ -25,7 +28,10 @@ def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat
|
|||
|
||||
instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
|
||||
|
||||
def UInt16.val (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin
|
||||
/-- Converts a `UInt16` into the corresponding `Fin UInt16.size`. -/
|
||||
def UInt16.toFin (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin
|
||||
@[deprecated UInt16.toFin (since := "2025-02-12"), inherit_doc UInt16.toFin]
|
||||
def UInt16.val (x : UInt16) : Fin UInt16.size := x.toFin
|
||||
@[extern "lean_uint16_of_nat"]
|
||||
def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨BitVec.ofNat 16 n⟩
|
||||
abbrev Nat.toUInt16 := UInt16.ofNat
|
||||
|
|
@ -38,7 +44,10 @@ def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVe
|
|||
|
||||
instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
|
||||
|
||||
def UInt32.val (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin
|
||||
/-- Converts a `UInt32` into the corresponding `Fin UInt32.size`. -/
|
||||
def UInt32.toFin (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin
|
||||
@[deprecated UInt32.toFin (since := "2025-02-12"), inherit_doc UInt32.toFin]
|
||||
def UInt32.val (x : UInt32) : Fin UInt32.size := x.toFin
|
||||
@[extern "lean_uint32_of_nat"]
|
||||
def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩
|
||||
@[extern "lean_uint32_of_nat"]
|
||||
|
|
@ -73,7 +82,10 @@ theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt
|
|||
simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
|
||||
Nat.mod_eq_of_lt h2, imp_self]
|
||||
|
||||
def UInt64.val (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin
|
||||
/-- Converts a `UInt64` into the corresponding `Fin UInt64.size`. -/
|
||||
def UInt64.toFin (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin
|
||||
@[deprecated UInt64.toFin (since := "2025-02-12"), inherit_doc UInt64.toFin]
|
||||
def UInt64.val (x : UInt64) : Fin UInt64.size := x.toFin
|
||||
@[extern "lean_uint64_of_nat"]
|
||||
def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨BitVec.ofNat 64 n⟩
|
||||
abbrev Nat.toUInt64 := UInt64.ofNat
|
||||
|
|
@ -97,7 +109,10 @@ instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
|
|||
@[deprecated usize_size_pos (since := "2024-11-24")] theorem usize_size_gt_zero : USize.size > 0 :=
|
||||
usize_size_pos
|
||||
|
||||
def USize.val (x : USize) : Fin USize.size := x.toBitVec.toFin
|
||||
/-- Converts a `USize` into the corresponding `Fin USize.size`. -/
|
||||
def USize.toFin (x : USize) : Fin USize.size := x.toBitVec.toFin
|
||||
@[deprecated USize.toFin (since := "2025-02-12"), inherit_doc USize.toFin]
|
||||
def USize.val (x : USize) : Fin USize.size := x.toFin
|
||||
@[extern "lean_usize_of_nat"]
|
||||
def USize.ofNat (n : @& Nat) : USize := ⟨BitVec.ofNat _ n⟩
|
||||
abbrev Nat.toUSize := USize.ofNat
|
||||
|
|
|
|||
|
|
@ -31,7 +31,9 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
|
|||
|
||||
@[simp] theorem toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatCore n h).toNat = n := BitVec.toNat_ofNatLt ..
|
||||
|
||||
@[simp] theorem val_val_eq_toNat (x : $typeName) : x.val.val = x.toNat := rfl
|
||||
@[simp] theorem toFin_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := rfl
|
||||
@[deprecated toFin_val_eq_toNat (since := "2025-02-12")]
|
||||
theorem val_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := rfl
|
||||
|
||||
theorem toNat_toBitVec_eq_toNat (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
|
||||
|
||||
|
|
@ -86,13 +88,21 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
|
|||
protected theorem eq_iff_toBitVec_eq {a b : $typeName} : a = b ↔ a.toBitVec = b.toBitVec :=
|
||||
Iff.intro toBitVec_eq_of_eq eq_of_toBitVec_eq
|
||||
|
||||
open $typeName (eq_of_toBitVec_eq) in
|
||||
protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by
|
||||
rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [val]
|
||||
open $typeName (eq_of_toBitVec_eq toFin) in
|
||||
protected theorem eq_of_toFin_eq {a b : $typeName} (h : a.toFin = b.toFin) : a = b := by
|
||||
rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [toFin]
|
||||
open $typeName (eq_of_toFin_eq) in
|
||||
@[deprecated eq_of_toFin_eq (since := "2025-02-12")]
|
||||
protected theorem eq_of_val_eq {a b : $typeName} (h : a.toFin = b.toFin) : a = b :=
|
||||
eq_of_toFin_eq h
|
||||
|
||||
open $typeName (eq_of_val_eq) in
|
||||
protected theorem val_inj {a b : $typeName} : a.val = b.val ↔ a = b :=
|
||||
Iff.intro eq_of_val_eq (congrArg val)
|
||||
open $typeName (eq_of_toFin_eq) in
|
||||
protected theorem toFin_inj {a b : $typeName} : a.toFin = b.toFin ↔ a = b :=
|
||||
Iff.intro eq_of_toFin_eq (congrArg toFin)
|
||||
open $typeName (toFin_inj) in
|
||||
@[deprecated toFin_inj (since := "2025-02-12")]
|
||||
protected theorem val_inj {a b : $typeName} : a.toFin = b.toFin ↔ a = b :=
|
||||
toFin_inj
|
||||
|
||||
open $typeName (eq_of_toBitVec_eq) in
|
||||
protected theorem toBitVec_ne_of_ne {a b : $typeName} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec :=
|
||||
|
|
@ -178,7 +188,9 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
|
|||
simp [Nat.mod_eq_of_lt x.toNat_lt_size]
|
||||
|
||||
@[simp]
|
||||
theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
|
||||
theorem toFin_ofNat (n : Nat) : toFin (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
|
||||
@[deprecated toFin_ofNat (since := "2025-02-12")]
|
||||
theorem val_ofNat (n : Nat) : toFin (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
|
||||
|
||||
@[simp, int_toBitVec]
|
||||
theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
|
||||
|
|
|
|||
|
|
@ -7,16 +7,16 @@ prelude
|
|||
import Init.Data.Fin.Log2
|
||||
|
||||
@[extern "lean_uint8_log2"]
|
||||
def UInt8.log2 (a : UInt8) : UInt8 := ⟨⟨Fin.log2 a.val⟩⟩
|
||||
def UInt8.log2 (a : UInt8) : UInt8 := ⟨⟨Fin.log2 a.toFin⟩⟩
|
||||
|
||||
@[extern "lean_uint16_log2"]
|
||||
def UInt16.log2 (a : UInt16) : UInt16 := ⟨⟨Fin.log2 a.val⟩⟩
|
||||
def UInt16.log2 (a : UInt16) : UInt16 := ⟨⟨Fin.log2 a.toFin⟩⟩
|
||||
|
||||
@[extern "lean_uint32_log2"]
|
||||
def UInt32.log2 (a : UInt32) : UInt32 := ⟨⟨Fin.log2 a.val⟩⟩
|
||||
def UInt32.log2 (a : UInt32) : UInt32 := ⟨⟨Fin.log2 a.toFin⟩⟩
|
||||
|
||||
@[extern "lean_uint64_log2"]
|
||||
def UInt64.log2 (a : UInt64) : UInt64 := ⟨⟨Fin.log2 a.val⟩⟩
|
||||
def UInt64.log2 (a : UInt64) : UInt64 := ⟨⟨Fin.log2 a.toFin⟩⟩
|
||||
|
||||
@[extern "lean_usize_log2"]
|
||||
def USize.log2 (a : USize) : USize := ⟨⟨Fin.log2 a.val⟩⟩
|
||||
def USize.log2 (a : USize) : USize := ⟨⟨Fin.log2 a.toFin⟩⟩
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
example : UInt8.val 42 = 42 := by simp
|
||||
example : UInt16.val 42 = 42 := by simp
|
||||
example : UInt32.val 42 = 42 := by simp
|
||||
example : UInt64.val 42 = 42 := by simp
|
||||
example : USize.val 42 = 42 := by simp
|
||||
example : UInt8.toFin 42 = 42 := by simp
|
||||
example : UInt16.toFin 42 = 42 := by simp
|
||||
example : UInt32.toFin 42 = 42 := by simp
|
||||
example : UInt64.toFin 42 = 42 := by simp
|
||||
example : USize.toFin 42 = 42 := by simp
|
||||
example : UInt8.toBitVec 42 = 42 := by simp
|
||||
example : UInt16.toBitVec 42 = 42 := by simp
|
||||
example : UInt32.toBitVec 42 = 42 := by simp
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue