From cae5ee075e5f9bc7393687a5eeca563c2f24293a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 May 2019 17:13:29 -0700 Subject: [PATCH] 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`. --- tests/playground/badreset.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/playground/badreset.lean diff --git a/tests/playground/badreset.lean b/tests/playground/badreset.lean new file mode 100644 index 0000000000..461278d7ec --- /dev/null +++ b/tests/playground/badreset.lean @@ -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)