max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: lake: introduce lowerHexUInt64 (#13455)

Browse source 
This PR adds a `lowerHexUInt64` utility to Lake which is used to
optimize `Hash.hex`.
This commit is contained in:
Mac Malone 2026-04-17 23:43:11 -04:00 • committed by GitHub
parent 592eb02bb2
commit 0fa749f71b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 39 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/lake/Lake/Build/Trace.lean
View file

@ -9,7 +9,7 @@ prelude
public import Lean.Data.Json public import Lean.Data.Json
import Init.Data.Nat.Fold import Init.Data.Nat.Fold
meta import Init.Data.Nat.Fold meta import Init.Data.Nat.Fold
import Lake.Util.String public import Lake.Util.String
public import Init.Data.String.Search public import Init.Data.String.Search
public import Init.Data.String.Extra public import Init.Data.String.Extra
import Init.Data.Option.Coe import Init.Data.Option.Coe
@ -141,8 +141,8 @@ public def ofHex? (s : String) : Option Hash :=
if s.utf8ByteSize = 16 && isHex s then ofHex s else none if s.utf8ByteSize = 16 && isHex s then ofHex s else none
/-- Returns the hash as 16-digit lowercase hex string. -/ /-- Returns the hash as 16-digit lowercase hex string. -/
public def hex (self : Hash) : String := @[inline] public def hex (self : Hash) : String :=
lpad (String.ofList <| Nat.toDigits 16 self.val.toNat) '0' 16 lowerHexUInt64 self.val
/-- Parse a hash from a string of decimal digits. -/ /-- Parse a hash from a string of decimal digits. -/
public def ofDecimal? (s : String) : Option Hash := public def ofDecimal? (s : String) : Option Hash :=

36
src/lake/Lake/Util/String.lean
View file

@ -7,6 +7,7 @@ module
prelude prelude
public import Init.Data.ToString.Basic public import Init.Data.ToString.Basic
import Init.Data.UInt.Lemmas
import Init.Data.String.Basic import Init.Data.String.Basic
import Init.Data.Nat.Fold import Init.Data.Nat.Fold
@ -33,3 +34,38 @@ public def isHex (s : String) : Bool :=
65 ≤ c -- 'A' 65 ≤ c -- 'A'
else else
false false
def lowerHexByte (n : UInt8) : UInt8 :=
if n ≤ 9 then
n + 48 -- + '0'
else
n + 87 -- + ('a' - 10)
theorem isValidChar_of_lt_256 (h : n < 256) : isValidChar n :=
Or.inl <| Nat.lt_trans h (by decide)
def lowerHexChar (n : UInt8) : Char :=
⟨lowerHexByte n |>.toUInt32, isValidChar_of_lt_256 <|
UInt32.lt_iff_toNat_lt.mpr <| (lowerHexByte n).toNat_lt⟩
public def lowerHexUInt64 (n : UInt64) : String :=
String.ofByteArray (ByteArray.emptyWithCapacity 16) ByteArray.isValidUTF8_empty
|>.push (lowerHexChar (n >>> 60 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 56 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 52 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 48 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 44 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 40 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 36 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 32 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 28 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 24 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 20 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 16 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 12 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 8 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n >>> 4 &&& 0xf).toUInt8)
|>.push (lowerHexChar (n &&& 0xf).toUInt8)
-- sanity check
example : "0123456789abcdef" = lowerHexUInt64 0x0123456789abcdef := by decide