mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
72 lines
2.3 KiB
Lean4
72 lines
2.3 KiB
Lean4
import Std.Internal.Parsec.String
|
|
|
|
/-!
|
|
Regression test for performance of `backward.whnf.reducibleClassField` with UInt16 bitwise operations.
|
|
|
|
The `isNonTrivialRegular` function in ExprDefEq should only classify class projections as
|
|
nontrivial at `.reducible` transparency (where `unfoldDefault`'s extra reduction applies).
|
|
At higher transparency levels, the classification causes unnecessary heuristic attempts
|
|
that cascade through BitVec reductions.
|
|
|
|
Without the fix, the `uEscape` function below took ~4.5G instructions.
|
|
With the fix, it takes ~0.94G instructions.
|
|
-/
|
|
|
|
set_option backward.whnf.reducibleClassField true
|
|
set_option maxHeartbeats 400000
|
|
|
|
open Std.Internal.Parsec
|
|
open Std.Internal.Parsec.String
|
|
|
|
def hexChar : Parser UInt16 := do
|
|
let c ← any
|
|
if '0' <= c && c <= '9' then
|
|
pure $ (c.val - '0'.val).toUInt16
|
|
else if 'a' <= c && c <= 'f' then
|
|
pure $ (c.val - 'a'.val + 10).toUInt16
|
|
else if 'A' <= c && c <= 'F' then
|
|
pure $ (c.val - 'A'.val + 10).toUInt16
|
|
else
|
|
fail "invalid hex character"
|
|
|
|
def finishSurrogatePair (low : UInt16) : Parser Char := do
|
|
let c ← any
|
|
if c != '\\' then fail ""
|
|
let c ← any
|
|
if c != 'u' then fail ""
|
|
let c ← any
|
|
if c != 'd' && c != 'D' then fail ""
|
|
let u2 ← hexChar; let u3 ← hexChar; let u4 ← hexChar
|
|
let val := (u2 <<< 8) ||| (u3 <<< 4) ||| u4
|
|
if val < 0xC00 then fail ""
|
|
let charVal := (((low.toUInt32 &&& 0x3FF) <<< 10) ||| (val.toUInt32 &&& 0x3FF)) + 0x10000
|
|
if h : charVal.isValidChar then
|
|
return ⟨charVal, h⟩
|
|
else
|
|
fail ""
|
|
|
|
def escapedChar : Parser Char := do
|
|
let c ← any
|
|
match c with
|
|
| '\\' => return '\\'
|
|
| '"' => return '"'
|
|
| '/' => return '/'
|
|
| 'b' => return '\x08'
|
|
| 'f' => return '\x0c'
|
|
| 'n' => return '\n'
|
|
| 'r' => return '\x0d'
|
|
| 't' => return '\t'
|
|
| 'u' =>
|
|
let u1 ← hexChar; let u2 ← hexChar; let u3 ← hexChar; let u4 ← hexChar
|
|
let val := (u1 <<< 12) ||| (u2 <<< 8) ||| (u3 <<< 4) ||| u4
|
|
if h : val < 0xD800 then
|
|
return ⟨val.toUInt32, Or.inl h⟩
|
|
else if h' : val < 0xE000 then
|
|
if val < 0xDC00 then
|
|
attempt (finishSurrogatePair val) <|> pure '\ufffd'
|
|
else
|
|
return '\ufffd'
|
|
else
|
|
return ⟨val.toUInt32, Or.inr ⟨Nat.not_lt.mp h', Nat.lt_trans val.toFin.isLt (by decide)⟩⟩
|
|
| _ => fail "illegal \\u escape"
|