sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

perf: speed up JSON serialisation (#6479)

Browse Source 
This PR speeds up JSON serialisation by using a lookup table to check
whether a string needs to be escaped.

The approach is based on
https://byroot.github.io/ruby/json/2024/12/15/optimizing-ruby-json-part-1.html.
This commit is contained in:
Henrik Böving
2025-01-08 13:06:25 +01:00
committed by GitHub
parent f01471f620
commit 48eb3084a0
1 changed files with 36 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

37
src/Lean/Data/Json/Printer.lean
View File

@@ -11,6 +11,22 @@ import Init.Data.List.Impl
namespace Lean
namespace Json
set_option maxRecDepth 1024 in
/--
This table contains for each UTF-8 byte whether we need to escape a string that contains it.
-/
private def escapeTable : { xs : ByteArray // xs.size = 256 } :=
⟨ByteArray.mk #[
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,1, 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1
], by rfl⟩
private def escapeAux (acc : String) (c : Char) : String :=
-- escape ", \, \n and \r, keep all other characters ≥ 0x20 and render characters < 0x20 with \u
if c = '"' then -- hack to prevent emacs from regarding the rest of the file as a string: "
@@ -39,8 +55,27 @@ private def escapeAux (acc : String) (c : Char) : String :=
let d4 := Nat.digitChar (n % 16)
acc ++ "\\u" |>.push d1 |>.push d2 |>.push d3 |>.push d4
private def needEscape (s : String) : Bool :=
go s 0
where
go (s : String) (i : Nat) : Bool :=
if h : i < s.utf8ByteSize then
let byte := s.getUtf8Byte i h
have h1 : byte.toNat < 256 := UInt8.toNat_lt_size byte
have h2 : escapeTable.val.size = 256 := escapeTable.property
if escapeTable.val.get byte.toNat (Nat.lt_of_lt_of_eq h1 h2.symm) == 0 then
go s (i + 1)
else
true
else
false
def escape (s : String) (acc : String := "") : String :=
s.foldl escapeAux acc
-- If we don't have any characters that need to be escaped we can just append right away.
if needEscape s then
s.foldl escapeAux acc
else
acc ++ s
def renderString (s : String) (acc : String := "") : String :=
let acc := acc ++ "\""