chore: basic tests for LCNF ElimDeadBranches
This commit is contained in:
Henrik Böving
Leonardo de Moura
parent
66009a5cd3
commit
e0d619e3ee
2 changed files with 146 additions and 0 deletions
37
tests/lean/CompilerElimDeadBranches.lean
Normal file
37
tests/lean/CompilerElimDeadBranches.lean
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
def someVal (_x : Nat) : Option Nat := some 0
|
||||
|
||||
/-
|
||||
This test demonstrates two things:
|
||||
1. We eliminate all branches except the some, some one
|
||||
2. We communicate correctly to the constant folder that the `n` and `m`
|
||||
are always 0 and can thus collapse the computation.
|
||||
-/
|
||||
set_option trace.Compiler.elimDeadBranches true in
|
||||
set_option trace.Compiler.result true in
|
||||
def addSomeVal (x : Nat) :=
|
||||
match someVal x, someVal x with
|
||||
| some n, some m => some (n + m)
|
||||
| _, _ => none
|
||||
|
||||
|
||||
def throwMyError (m n : Nat) : Except String Unit :=
|
||||
throw s!"Ahhhh {m + n}"
|
||||
|
||||
/-
|
||||
This demonstrates that the optimization does do good things to monadic
|
||||
code. In this snippet Lean would usually perform a cases on the result
|
||||
of `throwMyError` in order to figure out whether it has to:
|
||||
- raise an error and exit right now
|
||||
- jump to the the `return x + y` continuation
|
||||
Since the abstract interpreter knows that `throwMyError` always returns
|
||||
an `Except.error` it will drop the branch where we jump to the continuation.
|
||||
This will in turn allow the simplifier to drop the join point that represents
|
||||
the continuation, saving us more code size.
|
||||
-/
|
||||
set_option trace.Compiler.elimDeadBranches true in
|
||||
set_option trace.Compiler.result true in
|
||||
def monadic (x y : Nat) : Except String Nat := do
|
||||
if let some m := addSomeVal x then
|
||||
if let some n := addSomeVal y then
|
||||
throwMyError m n
|
||||
return x + y
|
||||
109
tests/lean/CompilerElimDeadBranches.lean.expected.out
Normal file
109
tests/lean/CompilerElimDeadBranches.lean.expected.out
Normal file
|
|
@ -0,0 +1,109 @@
|
|||
[Compiler.elimDeadBranches] Eliminating addSomeVal._redArg with #[("_x.37",
|
||||
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor
|
||||
`Option.some
|
||||
#[Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]]),
|
||||
("val.20", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
|
||||
("val.16", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
|
||||
("_x.35", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
|
||||
("_x.36",
|
||||
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
|
||||
[Compiler.elimDeadBranches] Threw away cases _x.37 branch Option.none
|
||||
[Compiler.elimDeadBranches] Threw away cases _x.37 branch Option.none
|
||||
[Compiler.elimDeadBranches] Eliminating addSomeVal with #[("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
|
||||
("_x.38",
|
||||
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
|
||||
[Compiler.elimDeadBranches] size: 11
|
||||
def addSomeVal._redArg : Option Nat :=
|
||||
let _x.1 := someVal._redArg;
|
||||
cases _x.1 : Option Nat
|
||||
| Option.none =>
|
||||
⊥
|
||||
| Option.some val.2 =>
|
||||
let _x.3 := 0;
|
||||
cases _x.1 : Option Nat
|
||||
| Option.none =>
|
||||
⊥
|
||||
| Option.some val.4 =>
|
||||
let _x.5 := 0;
|
||||
let _x.6 := Nat.add _x.3 _x.5;
|
||||
let _x.7 := some _ _x.6;
|
||||
return _x.7
|
||||
[Compiler.elimDeadBranches] size: 1
|
||||
def addSomeVal x : Option Nat :=
|
||||
let _x.1 := addSomeVal._redArg;
|
||||
return _x.1
|
||||
[Compiler.result] size: 9
|
||||
def addSomeVal._redArg : Option Nat :=
|
||||
let _x.1 := someVal._redArg;
|
||||
cases _x.1 : Option Nat
|
||||
| Option.none =>
|
||||
⊥
|
||||
| Option.some val.2 =>
|
||||
cases _x.1 : Option Nat
|
||||
| Option.none =>
|
||||
⊥
|
||||
| Option.some val.3 =>
|
||||
let _x.4 := 0;
|
||||
let _x.5 := some _ _x.4;
|
||||
return _x.5
|
||||
[Compiler.result] size: 1 def addSomeVal x : Option Nat := let _x.1 := addSomeVal._redArg; return _x.1
|
||||
[Compiler.elimDeadBranches] Eliminating monadic with #[("_x.205",
|
||||
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
|
||||
("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
|
||||
("_x.211",
|
||||
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
|
||||
("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
|
||||
("_x.212",
|
||||
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
|
||||
("_x.91",
|
||||
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.ok #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
|
||||
("_x.207",
|
||||
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
|
||||
("_x.88", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
|
||||
("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
|
||||
("val.200", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
|
||||
("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top)]
|
||||
[Compiler.elimDeadBranches] Threw away cases _x.211 branch Option.none
|
||||
[Compiler.elimDeadBranches] Threw away cases _x.212 branch Option.none
|
||||
[Compiler.elimDeadBranches] Threw away cases _x.205 branch Except.ok
|
||||
[Compiler.elimDeadBranches] size: 15
|
||||
def monadic x y : Except String Nat :=
|
||||
jp _jp.1 : Except String Nat :=
|
||||
let _x.2 := Nat.add x y;
|
||||
let _x.3 := Except.ok _ _ _x.2;
|
||||
return _x.3;
|
||||
let _x.4 := addSomeVal._redArg;
|
||||
cases _x.4 : Except String Nat
|
||||
| Option.none =>
|
||||
⊥
|
||||
| Option.some val.5 =>
|
||||
let _x.6 := addSomeVal._redArg;
|
||||
cases _x.6 : Except String Nat
|
||||
| Option.none =>
|
||||
⊥
|
||||
| Option.some val.7 =>
|
||||
let _x.8 := throwMyError val.5 val.7;
|
||||
cases _x.8 : Except String Nat
|
||||
| Except.error a.9 =>
|
||||
let _x.10 := Except.error _ _ a.9;
|
||||
return _x.10
|
||||
| Except.ok a.11 =>
|
||||
⊥
|
||||
[Compiler.result] size: 12
|
||||
def monadic x y : Except String Nat :=
|
||||
let _x.1 := addSomeVal._redArg;
|
||||
cases _x.1 : Except String Nat
|
||||
| Option.none =>
|
||||
⊥
|
||||
| Option.some val.2 =>
|
||||
cases _x.1 : Except String Nat
|
||||
| Option.none =>
|
||||
⊥
|
||||
| Option.some val.3 =>
|
||||
let _x.4 := throwMyError val.2 val.3;
|
||||
cases _x.4 : Except String Nat
|
||||
| Except.error a.5 =>
|
||||
let _x.6 := Except.error _ _ a.5;
|
||||
return _x.6
|
||||
| Except.ok a.7 =>
|
||||
⊥
|
||||
Loading…
Add table
Reference in a new issue