From 52b687cab46909afdbfdaf2b318d8ec033a6ef93 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 19 Nov 2025 14:06:27 +0100 Subject: [PATCH] perf: less allocations when using string patterns (#11255) This PR reduces the allocations when using string patterns. In particular `startsWith`, `dropPrefix?`, `endsWith`, `dropSuffix?` are optimized. --- src/Init/Data/String/Defs.lean | 4 ++-- src/Init/Data/String/Pattern/Basic.lean | 25 ++++++++++++++++++++++-- src/Init/Data/String/Pattern/String.lean | 4 ++-- src/Init/Data/String/Slice.lean | 2 +- src/include/lean/lean.h | 2 +- src/lake/Lake/Util/FilePath.lean | 9 --------- src/runtime/object.cpp | 22 ++++++++++----------- stage0/src/stdlib_flags.h | 2 +- 8 files changed, 41 insertions(+), 29 deletions(-) diff --git a/src/Init/Data/String/Defs.lean b/src/Init/Data/String/Defs.lean index 887c113d2f..27b7498285 100644 --- a/src/Init/Data/String/Defs.lean +++ b/src/Init/Data/String/Defs.lean @@ -435,7 +435,7 @@ theorem endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endValidP theorem str_toSlice {s : String} : s.toSlice.str = s := rfl /-- The number of bytes of the UTF-8 encoding of the string slice. -/ -@[expose] +@[expose, inline] def Slice.utf8ByteSize (s : Slice) : Nat := s.startInclusive.offset.byteDistance s.endExclusive.offset @@ -464,7 +464,7 @@ theorem Pos.Raw.byteIdx_sub_slice {p : Pos.Raw} {s : Slice} : (p - s).byteIdx = p.byteIdx - s.utf8ByteSize := rfl /-- The end position of a slice, as a `Pos.Raw`. -/ -@[expose] +@[expose, inline] def Slice.rawEndPos (s : Slice) : Pos.Raw where byteIdx := s.utf8ByteSize diff --git a/src/Init/Data/String/Pattern/Basic.lean b/src/Init/Data/String/Pattern/Basic.lean index 8939859194..d32f61df9e 100644 --- a/src/Init/Data/String/Pattern/Basic.lean +++ b/src/Init/Data/String/Pattern/Basic.lean @@ -74,8 +74,8 @@ class ForwardPattern (ρ : Type) where namespace Internal -@[extern "lean_slice_memcmp"] -def memcmp (lhs rhs : @& Slice) (lstart : @& String.Pos.Raw) (rstart : @& String.Pos.Raw) +@[extern "lean_string_memcmp"] +def memcmpStr (lhs rhs : @& String) (lstart : @& String.Pos.Raw) (rstart : @& String.Pos.Raw) (len : @& String.Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos) (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) : Bool := go 0 @@ -99,6 +99,27 @@ where simp [Pos.Raw.lt_iff] at h ⊢ omega +@[inline] +def memcmpSlice (lhs rhs : Slice) (lstart : String.Pos.Raw) (rstart : String.Pos.Raw) + (len : String.Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos) + (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) : Bool := + memcmpStr + lhs.str + rhs.str + (lstart.offsetBy lhs.startInclusive.offset) + (rstart.offsetBy rhs.startInclusive.offset) + len + (by + have := lhs.startInclusive_le_endExclusive + have := lhs.endExclusive.isValid.le_utf8ByteSize + simp [ValidPos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at * + omega) + (by + have := rhs.startInclusive_le_endExclusive + have := rhs.endExclusive.isValid.le_utf8ByteSize + simp [ValidPos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at * + omega) + end Internal namespace ForwardPattern diff --git a/src/Init/Data/String/Pattern/String.lean b/src/Init/Data/String/Pattern/String.lean index b8dc9ce662..8843cecfea 100644 --- a/src/Init/Data/String/Pattern/String.lean +++ b/src/Init/Data/String/Pattern/String.lean @@ -270,7 +270,7 @@ def startsWith (s : Slice) (pat : Slice) : Bool := omega have hp := by simp [Pos.Raw.le_iff] - Internal.memcmp s pat s.startPos.offset pat.startPos.offset pat.rawEndPos hs hp + Internal.memcmpSlice s pat s.startPos.offset pat.startPos.offset pat.rawEndPos hs hp else false @@ -306,7 +306,7 @@ def endsWith (s : Slice) (pat : Slice) : Bool := omega have hp := by simp [patStart, Pos.Raw.le_iff] at h ⊢ - Internal.memcmp s pat sStart patStart pat.rawEndPos hs hp + Internal.memcmpSlice s pat sStart patStart pat.rawEndPos hs hp else false diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean index 49e98818ee..bc2c2711a4 100644 --- a/src/Init/Data/String/Slice.lean +++ b/src/Init/Data/String/Slice.lean @@ -68,7 +68,7 @@ def beq (s1 s2 : Slice) : Bool := if h : s1.utf8ByteSize = s2.utf8ByteSize then have h1 := by simp [h, String.Pos.Raw.le_iff] have h2 := by simp [h, String.Pos.Raw.le_iff] - Internal.memcmp s1 s2 s1.startPos.offset s2.startPos.offset s1.rawEndPos h1 h2 + Internal.memcmpSlice s1 s2 s1.startPos.offset s2.startPos.offset s1.rawEndPos h1 h2 else false diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 5f967b0fdc..042111e75d 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1163,7 +1163,7 @@ static inline uint8_t lean_string_dec_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) { static inline uint8_t lean_string_dec_lt(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_lt(s1, s2); } LEAN_EXPORT uint64_t lean_string_hash(b_lean_obj_arg); LEAN_EXPORT lean_obj_res lean_string_of_usize(size_t); -LEAN_EXPORT uint8_t lean_slice_memcmp(b_lean_obj_arg s1, b_lean_obj_arg s2, b_lean_obj_arg lstart, b_lean_obj_arg rstart, b_lean_obj_arg len); +LEAN_EXPORT uint8_t lean_string_memcmp(b_lean_obj_arg s1, b_lean_obj_arg s2, b_lean_obj_arg lstart, b_lean_obj_arg rstart, b_lean_obj_arg len); LEAN_EXPORT uint64_t lean_slice_hash(b_lean_obj_arg); LEAN_EXPORT uint8_t lean_slice_dec_lt(b_lean_obj_arg s1, b_lean_obj_arg s2); diff --git a/src/lake/Lake/Util/FilePath.lean b/src/lake/Lake/Util/FilePath.lean index 8e41e39f78..814dd7c3f1 100644 --- a/src/lake/Lake/Util/FilePath.lean +++ b/src/lake/Lake/Util/FilePath.lean @@ -82,13 +82,4 @@ where removeExts s i' e termination_by i.1 --- sanity check -example : - modOfFilePath "Foo/Bar" = `Foo.Bar - ∧ modOfFilePath "Foo/Bar/" = `Foo.Bar - ∧ modOfFilePath "Foo/Bar.lean" = `Foo.Bar - ∧ modOfFilePath "Foo/Bar.tar.gz" = `Foo.Bar - ∧ modOfFilePath "Foo/Bar.lean/" = `Foo.«Bar.lean» -:= by native_decide - attribute [deprecated "Deprecated without replacement." (since := "2025-08-01")] modOfFilePath diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index c97ad33bb3..980725a908 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -2362,6 +2362,17 @@ extern "C" LEAN_EXPORT obj_res lean_string_of_usize(size_t n) { return mk_ascii_string_unchecked(std::to_string(n)); } +extern "C" LEAN_EXPORT uint8_t lean_string_memcmp(b_obj_arg s1, b_obj_arg s2, b_obj_arg lstart, b_obj_arg rstart, b_obj_arg len) { + // Thanks to the proof arguments we know that lstart, rstart and len are all scalars. + lean_assert(lean_is_scalar(lstart)); + lean_assert(lean_is_scalar(rstart)); + lean_assert(lean_is_scalar(len)); + + char const * lbase = lean_string_cstr(s1) + lean_unbox(lstart); + char const * rbase = lean_string_cstr(s2) + lean_unbox(rstart); + return std::memcmp(lbase, rbase, lean_unbox(len)) == 0; +} + size_t lean_slice_size(b_obj_arg slice) { b_obj_res start = lean_ctor_get(slice, 1); lean_assert(lean_is_scalar(start)); @@ -2377,17 +2388,6 @@ char const * lean_slice_base(b_obj_arg slice) { return lean_string_cstr(string) + lean_unbox(offset); } -extern "C" LEAN_EXPORT uint8_t lean_slice_memcmp(b_obj_arg s1, b_obj_arg s2, b_obj_arg lstart, b_obj_arg rstart, b_obj_arg len) { - // Thanks to the proof arguments we know that lstart, rstart and len are all scalars. - lean_assert(lean_is_scalar(lstart)); - lean_assert(lean_is_scalar(rstart)); - lean_assert(lean_is_scalar(len)); - - char const * lbase = lean_slice_base(s1) + lean_unbox(lstart); - char const * rbase = lean_slice_base(s2) + lean_unbox(rstart); - return std::memcmp(lbase, rbase, lean_unbox(len)) == 0; -} - extern "C" LEAN_EXPORT uint64_t lean_slice_hash(b_obj_arg s) { size_t sz = lean_slice_size(s); char const * str = lean_slice_base(s); diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..6b964da742 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -11,7 +11,7 @@ options get_default_options() { opts = opts.update({"debug", "terminalTacticsAsSorry"}, false); // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with