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.
29 lines
905 B
Text
29 lines
905 B
Text
import Lean
|
|
|
|
open Lean Meta
|
|
run_meta do
|
|
let nat := mkConst ``Nat
|
|
withLocalDeclD `x nat fun x =>
|
|
withLocalDeclD `y nat fun y =>
|
|
withLocalDeclD `z nat fun z =>
|
|
withLocalDeclD `w nat fun w => do
|
|
let o := mkNatLit 0
|
|
let e1 ← mkAdd x x -- x + x
|
|
let e2 ← mkAdd x y -- x + y
|
|
let e3 ← mkAdd e2 z -- (x + y) + z
|
|
let e4 ← mkAdd e2 e2 -- (x + y) + (x + y)
|
|
let e5 ← mkAdd e4 w -- ((x + y) + (x + y)) + w
|
|
let e6 ← mkAdd e5 z -- (((x + y) + (x + y)) + w) + z
|
|
assert! o.fvarsSubset e6
|
|
assert! !e6.fvarsSubset o
|
|
assert! o.fvarsSubset e1
|
|
assert! !e1.fvarsSubset o
|
|
assert! e1.fvarsSubset e1
|
|
assert! e1.fvarsSubset e2
|
|
assert! e6.fvarsSubset e6
|
|
assert! !e2.fvarsSubset e1
|
|
assert! e1.fvarsSubset e6
|
|
assert! e4.fvarsSubset e6
|
|
assert! !e3.fvarsSubset e5
|
|
assert! !e5.fvarsSubset e3
|
|
assert! e4.fvarsSubset e6
|