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.
325 lines
7 KiB
Text
325 lines
7 KiB
Text
import Lean
|
||
/-!
|
||
# Tests of the `letToHave` transformation
|
||
-/
|
||
|
||
set_option pp.letVarTypes true
|
||
set_option pp.mvars.anonymous false
|
||
|
||
open Lean Elab Command in
|
||
/--
|
||
`#let_to_have t` elaborates `t` then applies let-to-have. It typechecks `t` before and after.
|
||
-/
|
||
elab "#let_to_have " t:term : command => runTermElabM fun _ => do
|
||
let e ← Term.elabTermAndSynthesize t none
|
||
Meta.check e
|
||
let e' ← Meta.letToHave e
|
||
Meta.check e'
|
||
unless ← Meta.isDefEq e e' do
|
||
throwError "result is not definitionally equal"
|
||
if e == e' then
|
||
logInfo m!"no change"
|
||
else
|
||
logInfo m!"{e'}"
|
||
|
||
set_option linter.unusedVariables false
|
||
|
||
/-!
|
||
Very basic tests where there are no lets.
|
||
-/
|
||
/-- info: no change -/
|
||
#guard_msgs in #let_to_have true
|
||
/-- info: no change -/
|
||
#guard_msgs in #let_to_have fun (x : Nat) => x + 1
|
||
/-- info: no change -/
|
||
#guard_msgs in #let_to_have ∀ (x : Nat), x = x
|
||
/-- info: no change -/
|
||
#guard_msgs in #let_to_have have x := 1; x + 1
|
||
|
||
/-!
|
||
Basic tests of nondependent `let`s.
|
||
-/
|
||
/--
|
||
info: have x : Nat := 1;
|
||
true
|
||
-/
|
||
#guard_msgs in #let_to_have let x := 1; true
|
||
/--
|
||
info: have x : Nat := 1;
|
||
x + 1
|
||
-/
|
||
#guard_msgs in #let_to_have let x := 1; x + 1
|
||
/--
|
||
info: have x : Nat := 1;
|
||
have x' : Nat := x;
|
||
have x'' : Nat := x + x';
|
||
have x''' : Nat := x + x' + x'';
|
||
x + x' + x'' + x'''
|
||
-/
|
||
#guard_msgs in #let_to_have
|
||
let x : Nat := 1; let x' := x; let x'' := x + x'; let x''' := x + x' + x''; x + x' + x'' + x'''
|
||
/--
|
||
info: fun x =>
|
||
have x' : Nat := x;
|
||
have x'' : Nat := x + x';
|
||
have x''' : Nat := x + x' + x'';
|
||
x + x' + x'' + x'''
|
||
-/
|
||
#guard_msgs in #let_to_have
|
||
fun x : Nat => let x' := x; let x'' := x + x'; let x''' := x + x' + x''; x + x' + x'' + x'''
|
||
/--
|
||
info: (x : Nat) →
|
||
have x' : Nat := x;
|
||
have x'' : Nat := x + x';
|
||
have x''' : Nat := x + x' + x'';
|
||
Fin (x + x' + x'' + x''')
|
||
-/
|
||
#guard_msgs in #let_to_have
|
||
∀ x : Nat, let x' := x; let x'' := x + x'; let x''' := x + x' + x''; Fin (x + x' + x'' + x''')
|
||
|
||
/-!
|
||
Testing the cache. Reports one expression transformed.
|
||
-/
|
||
/--
|
||
info: (have x : Nat := 1;
|
||
x + 1) +
|
||
have x : Nat := 1;
|
||
x + 1
|
||
---
|
||
trace: [Meta.letToHave] ✅️ transformed 1 `let` expressions into `have` expressions
|
||
[Meta.letToHave] result:
|
||
(have x : Nat := 1;
|
||
x + 1) +
|
||
have x : Nat := 1;
|
||
x + 1
|
||
-/
|
||
#guard_msgs in
|
||
set_option trace.Meta.letToHave true in
|
||
#let_to_have (let x := 1; x + 1) + (let x := 1; x + 1)
|
||
|
||
/-!
|
||
Cache uses strict equality. Preserves binder names.
|
||
-/
|
||
/--
|
||
info: (have x : Nat := 1;
|
||
x + 1) +
|
||
have y : Nat := 1;
|
||
y + 1
|
||
-/
|
||
#guard_msgs in
|
||
#let_to_have (let x := 1; x + 1) + (let y := 1; y + 1)
|
||
|
||
/-!
|
||
The expression `(1 + 2 + 3 + 4 + 5 + 6)` enters the cache first without a type,
|
||
but then a type needs to be computed under the `let`.
|
||
-/
|
||
/--
|
||
info: 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 +
|
||
have y : Nat := 1;
|
||
1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + y
|
||
-/
|
||
#guard_msgs in
|
||
#let_to_have (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8) + (let y := 1; (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8) + y)
|
||
|
||
/-!
|
||
Dependence in a let value.
|
||
-/
|
||
/--
|
||
info: let x : Nat := 1;
|
||
have h : x = 1 := ⋯;
|
||
x
|
||
-/
|
||
#guard_msgs in #let_to_have let x := 1; let h : x = 1 := rfl; x
|
||
|
||
/-!
|
||
Dependence in a let type.
|
||
-/
|
||
/--
|
||
info: let x : Nat := 1;
|
||
have h : 0 = 0 := ⋯;
|
||
x
|
||
-/
|
||
#guard_msgs in #let_to_have let x := 1; let h : (0 : Fin x) = (0 : Fin x) := rfl; x
|
||
|
||
/-!
|
||
No dependence from the let type.
|
||
-/
|
||
/--
|
||
info: have x : Nat := 1;
|
||
have h : 0 = 0 := ⋯;
|
||
x
|
||
-/
|
||
#guard_msgs in #let_to_have let x := 1; let h : (0 : Fin (x + 1)) = (0 : Fin (x + 1)) := rfl; x
|
||
/-!
|
||
Another dependence in the let type.
|
||
-/
|
||
/--
|
||
info: let x : Nat := 1;
|
||
have h : 0 = 0 := ⋯;
|
||
x
|
||
-/
|
||
#guard_msgs in #let_to_have let x := 1; let h : (0 : Fin (x + 1)) = (0 : Fin (1 + 1)) := rfl; x
|
||
|
||
/-!
|
||
Dependence in a forall type
|
||
-/
|
||
/--
|
||
info: let U : Type 1 := Type;
|
||
have α : U := Nat;
|
||
∀ (n : α), n = n
|
||
-/
|
||
#guard_msgs in #let_to_have let U := Type; let α : U := Nat; ∀ (n : α), n = n
|
||
|
||
/-!
|
||
Dependence in a forall body
|
||
-/
|
||
/--
|
||
info: let U : Type 1 := Type;
|
||
have α : U := Nat;
|
||
Bool → α
|
||
-/
|
||
#guard_msgs in #let_to_have let U := Type; let α : U := Nat; Bool → α
|
||
|
||
/-!
|
||
Dependence in a lambda type
|
||
-/
|
||
/--
|
||
info: let U : Type 1 := Type;
|
||
have α : U := Nat;
|
||
fun n => n
|
||
-/
|
||
#guard_msgs in #let_to_have let U := Type; let α : U := Nat; fun (n : α) => n
|
||
|
||
/-!
|
||
Metavariable under binder, might be dependent, doesn't change.
|
||
-/
|
||
/-- info: no change -/
|
||
#guard_msgs in #let_to_have let x := 1; ?m
|
||
/-!
|
||
Metavariable has a context that doesn't include `x`, so it doesn't depend on it.
|
||
-/
|
||
/--
|
||
info: have x : ?_ := ?m;
|
||
?m
|
||
-/
|
||
#guard_msgs in #let_to_have let x := ?m; ?m
|
||
/-!
|
||
Similar, but we see that the outer `let` remains dependent.
|
||
-/
|
||
/--
|
||
info: let x : Nat := 1;
|
||
have y : ?_ := ?m;
|
||
?m
|
||
-/
|
||
#guard_msgs in #let_to_have let x := 1; let y := ?m; ?m
|
||
|
||
/-!
|
||
Test with a deep let expression.
|
||
-/
|
||
syntax "deepLets% " num term:arg term:arg : term
|
||
macro_rules
|
||
| `(deepLets% 0 $b $e) => `(if $b then $e else 0)
|
||
| `(deepLets% $n $b $e) =>
|
||
let n' : Lean.Syntax.NumLit := Lean.quote (n.getNat - 1)
|
||
`(let b' : Bool := !$b; let x : Nat := 1*$e; deepLets% $n' b' x)
|
||
/--
|
||
info: fun a =>
|
||
let b' : Bool := !true;
|
||
let x : Nat := 1 * (0 + a);
|
||
let b' : Bool := !b';
|
||
let x : Nat := 1 * x;
|
||
let b' : Bool := !b';
|
||
let x : Nat := 1 * x;
|
||
let b' : Bool := !b';
|
||
let x : Nat := 1 * x;
|
||
let b' : Bool := !b';
|
||
let x : Nat := 1 * x;
|
||
if b' = true then x else 0 : Nat → Nat
|
||
-/
|
||
#guard_msgs in #check fun a => deepLets% 5 true (0 + a)
|
||
/--
|
||
info: fun a =>
|
||
have b' : Bool := !true;
|
||
have x : Nat := 1 * (0 + a);
|
||
have b' : Bool := !b';
|
||
have x : Nat := 1 * x;
|
||
have b' : Bool := !b';
|
||
have x : Nat := 1 * x;
|
||
have b' : Bool := !b';
|
||
have x : Nat := 1 * x;
|
||
have b' : Bool := !b';
|
||
have x : Nat := 1 * x;
|
||
if b' = true then x else 0
|
||
-/
|
||
#guard_msgs in #let_to_have fun a => deepLets% 5 true (0 + a)
|
||
|
||
/--
|
||
info: fun a =>
|
||
have b' : Bool := !true;
|
||
have x : Nat := 1 * (0 + a);
|
||
have b' : Bool := !b';
|
||
have x : Nat := 1 * x;
|
||
have b' : Bool := !b';
|
||
have x : Nat := 1 * x;
|
||
have b' : Bool := !b';
|
||
have x : Nat := 1 * x;
|
||
have b' : Bool := !b';
|
||
have x : Nat := ⋯;
|
||
⋯
|
||
-/
|
||
#guard_msgs in set_option pp.deepTerms.threshold 10 in #let_to_have fun a => deepLets% 33 true (0 + a)
|
||
/--
|
||
info: fun a =>
|
||
have b' : Bool := !true;
|
||
have x : Nat := 1 * (0 + a);
|
||
have b' : Bool := !b';
|
||
have x : Nat := 1 * x;
|
||
have b' : Bool := !b';
|
||
have x : Nat := 1 * x;
|
||
have b' : Bool := !b';
|
||
have x : Nat := 1 * x;
|
||
have b' : Bool := !b';
|
||
have x : Nat := ⋯;
|
||
⋯
|
||
-/
|
||
#guard_msgs in set_option pp.deepTerms.threshold 10 in #let_to_have fun a => deepLets% 150 true (0 + a)
|
||
|
||
/-!
|
||
Tests of the `let_to_have` tactic.
|
||
-/
|
||
/--
|
||
trace: h :
|
||
have x : Nat := 1;
|
||
x = x
|
||
⊢ have y : Nat := 1;
|
||
y = y
|
||
-/
|
||
#guard_msgs in
|
||
example (h : let x := 1; x = x) : let y := 1; y = y := by
|
||
let_to_have at *
|
||
trace_state
|
||
rfl
|
||
/--
|
||
trace: h :
|
||
let x : Nat := 1;
|
||
x = x
|
||
⊢ have y : Nat := 1;
|
||
y = y
|
||
-/
|
||
#guard_msgs in
|
||
example (h : let x := 1; x = x) : let y := 1; y = y := by
|
||
let_to_have
|
||
trace_state
|
||
rfl
|
||
/--
|
||
trace: h :
|
||
have x : Nat := 1;
|
||
x = x
|
||
⊢ let y : Nat := 1;
|
||
y = y
|
||
-/
|
||
#guard_msgs in
|
||
example (h : let x := 1; x = x) : let y := 1; y = y := by
|
||
let_to_have at h
|
||
trace_state
|
||
rfl
|