903493799d
This removes checks in `Lean.Meta.reduceNat?` that caused it to fail on terms it could handle because they contain meta variables in arguments. This lead to those operations being reduced using their equational definitions and slow performance on large patterns: ``` set_option profiler true set_option profiler.threshold 1 def testMod (x:Nat) := match x with | 128 % 1024 => true | _ => false -- elaboration took 3.02ms def testMul (x:Nat) := match x with | 128 * 1 => true | _ => false -- type checking took 11.1ms -- compilation of testMul.match_1 took 313ms -- compilation of testMul took 65.7ms -- elaboration took 58.9ms ``` Performance is slower on `testMul` than `testMod` because `whnf` ends up evaluateing `128 * 1` using Peano arithmetic while `128 % 1024` is able to avoid that treatment since `128 < 1024`.
17 lines
423 B
Text
17 lines
423 B
Text
-- This validates that Lean is able to simplify patterns containing operations
|
|
-- on ground natural literals.
|
|
--
|
|
-- This is a regression test for #3139.
|
|
set_option maxHeartbeats 1000
|
|
|
|
-- This fails without the fix and maxHeartbeats 1000.
|
|
def testZeroAdd (x:Nat) :=
|
|
match x with
|
|
| 0 + 128 => true
|
|
| _ => false
|
|
|
|
-- This succeeds in all cases
|
|
def testAddZero (x:Nat) :=
|
|
match x with
|
|
| 128 + 0 => true
|
|
| _ => false
|