test(tests/playground/badreset): add test that exposes a bad reset/reuse placement
The generated code is safe, but the `reset/reuse` optimization will never be applicable at runtime. The issue is that `insert_reset_reuse_fn` is not checking the joint points. I will fix the bug only at `resetreuse.lean`.
This commit is contained in:
parent
80e9c4706f
commit
cae5ee075e
1 changed files with 12 additions and 0 deletions
12
tests/playground/badreset.lean
Normal file
12
tests/playground/badreset.lean
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
@[noinline] def g (x : Nat × Nat) := x
|
||||
|
||||
set_option trace.compiler.boxed true
|
||||
|
||||
@[noinline] def f (b : Bool) (x : Nat × Nat) : (Nat × Nat) × (Nat × Nat) :=
|
||||
let done (y : Nat × Nat) := (g (g (g y)), x) in
|
||||
match b with
|
||||
| true := match x with | (a, b) := done (a, 0)
|
||||
| false := match x with | (a, b) := done (0, b)
|
||||
|
||||
def main (xs : List String) : IO Unit :=
|
||||
IO.println $ f true (xs.head.toNat, xs.tail.head.toNat)
|
||||
Loading…
Add table
Reference in a new issue