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.
118 lines
2.4 KiB
Text
118 lines
2.4 KiB
Text
import Lean
|
||
open Lean Meta
|
||
|
||
def test1 (e : Expr) : Option Expr :=
|
||
match_expr e with
|
||
| c@Eq α a b => some (mkApp3 c α b a)
|
||
| Eq.refl _ a => some a
|
||
| _ => none
|
||
|
||
/--
|
||
info: 3 = 1
|
||
---
|
||
info: 3
|
||
---
|
||
info: 4 = 2
|
||
-/
|
||
#guard_msgs in
|
||
run_meta do
|
||
let eq ← mkEq (toExpr 1) (toExpr 3)
|
||
let eq := mkAnnotation `foo eq
|
||
let some eq := test1 eq | throwError "unexpected"
|
||
logInfo eq
|
||
let rfl ← mkEqRefl (toExpr 3)
|
||
let some n := test1 rfl | throwError "unexpected"
|
||
logInfo n
|
||
let eq := mkAnnotation `boo <| mkApp (mkAnnotation `bla (mkApp (mkAnnotation `foo eq.appFn!.appFn!) (toExpr 2))) (toExpr 4)
|
||
let some eq := test1 eq | throwError "unexpected"
|
||
logInfo eq
|
||
|
||
def test2 (e : Expr) : MetaM Expr := do
|
||
match_expr e with
|
||
| HAdd.hAdd _ _ _ _ a b => mkSub a b
|
||
| HMul.hMul _ _ _ _ a b => mkAdd b a
|
||
| _ => return e
|
||
|
||
/--
|
||
info: 2 - 5
|
||
---
|
||
info: 5 + 2
|
||
---
|
||
info: 5 - 2
|
||
-/
|
||
#guard_msgs in
|
||
run_meta do
|
||
let e ← mkAdd (toExpr 2) (toExpr 5)
|
||
let e ← test2 e
|
||
logInfo e
|
||
let e ← mkMul (toExpr 2) (toExpr 5)
|
||
let e ← test2 e
|
||
logInfo e
|
||
let m ← mkFreshExprMVar none
|
||
let m ← test2 m
|
||
assert! m.isMVar
|
||
discard <| isDefEq m e
|
||
let m ← test2 m
|
||
logInfo m
|
||
|
||
def test3 (e : Expr) : Option Expr :=
|
||
let_expr c@Eq α a b := e | none
|
||
some (mkApp3 c α b a)
|
||
|
||
def test4 (e : Expr) : Option Expr :=
|
||
let_expr Eq.refl _ a := e | none
|
||
some a
|
||
|
||
/--
|
||
info: 3 = 1
|
||
---
|
||
info: 3
|
||
---
|
||
info: 4 = 2
|
||
-/
|
||
#guard_msgs in
|
||
run_meta do
|
||
let eq ← mkEq (toExpr 1) (toExpr 3)
|
||
let eq := mkAnnotation `foo eq
|
||
let some eq := test3 eq | throwError "unexpected"
|
||
logInfo eq
|
||
let rfl ← mkEqRefl (toExpr 3)
|
||
let some n := test4 rfl | throwError "unexpected"
|
||
logInfo n
|
||
let eq := mkAnnotation `boo <| mkApp (mkAnnotation `bla (mkApp (mkAnnotation `foo eq.appFn!.appFn!) (toExpr 2))) (toExpr 4)
|
||
let some eq := test3 eq | throwError "unexpected"
|
||
logInfo eq
|
||
|
||
def test5 (e : Expr) : MetaM Expr := do
|
||
let_expr HAdd.hAdd _ _ _ _ a b ← e
|
||
| return e
|
||
mkSub a b
|
||
|
||
def test6 (e : Expr) : MetaM Expr := do
|
||
let_expr HAdd.hAdd _ _ _ _ a b := e
|
||
| return e
|
||
mkSub a b
|
||
|
||
/--
|
||
info: 2 - 5
|
||
---
|
||
info: 2 - 5
|
||
---
|
||
info: 2 - 5
|
||
-/
|
||
#guard_msgs in
|
||
run_meta do
|
||
let e ← mkAdd (toExpr 2) (toExpr 5)
|
||
let e' ← test5 e
|
||
logInfo e'
|
||
let e' ← test6 e
|
||
logInfo e'
|
||
let m ← mkFreshExprMVar none
|
||
let m ← test5 m
|
||
assert! m.isMVar
|
||
discard <| isDefEq m e
|
||
let m' ← test5 m
|
||
logInfo m'
|
||
assert! m.isMVar
|
||
let m' ← test6 m -- does not instantiate mvars
|
||
assert! m'.isMVar
|