From 3936b2ba794ea98ae6f23ec540429e66946a6ce3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 27 Mar 2019 12:59:43 -0700
Subject: [PATCH] chore(library/init/io): we don't need `fix` anymore

`partial def` are much more general
---
 library/init/io.lean                  | 9 +++------
 tests/playground/fix.lean             | 6 +++---
 tests/playground/fix_1.lean           | 8 --------
 tests/playground/fix_with_tuples.lean | 8 --------
 4 files changed, 6 insertions(+), 25 deletions(-)
 delete mode 100644 tests/playground/fix_1.lean
 delete mode 100644 tests/playground/fix_with_tuples.lean

diff --git a/library/init/io.lean b/library/init/io.lean
index 1b00e305d1..822fac7718 100644
--- a/library/init/io.lean
+++ b/library/init/io.lean
@@ -64,16 +64,13 @@ constant Fs.handle : Type := Unit
 namespace Prim
 open Fs
 
-def iterateAux {α β : Type} (f : α → IO (Sum α β)) : (α → IO β) → (α → IO β)
-| rec a :=
+@[specialize] partial def iterate {α β : Type} : α → (α → IO (Sum α β)) → IO β
+| a f :=
   do v ← f a,
   match v with
-  | Sum.inl a := rec a
+  | Sum.inl a := iterate a f
   | Sum.inr b := pure b
 
-@[specialize] def iterate {α β : Type} (a : α) (f : α → IO (Sum α β)) : IO β :=
-fixCore (λ _, throw "deep recursion") (iterateAux f) a
-
 @[extern 2 "lean_io_prim_put_str"]
 constant putStr (s: @& String) : IO Unit := default _
 @[extern 1 "lean_io_prim_get_line"]
diff --git a/tests/playground/fix.lean b/tests/playground/fix.lean
index 795b6a683e..36385a422f 100644
--- a/tests/playground/fix.lean
+++ b/tests/playground/fix.lean
@@ -1,8 +1,8 @@
-def foo (rec : Nat → Nat → Nat) : Nat → Nat → Nat
+partial def foo : Nat → Nat → Nat
 | 0     a := a
-| (n+1) a := rec n a + a + rec n (a+1)
+| (n+1) a := foo n a + a + foo n (a+1)
 
 def main (xs : List String) : IO UInt32 :=
-let v := fix2 foo (xs.head.toNat) 10 in
+let v := foo (xs.head.toNat) 10 in
 IO.println (toString v) *>
 pure 0
diff --git a/tests/playground/fix_1.lean b/tests/playground/fix_1.lean
deleted file mode 100644
index 657b5a8c98..0000000000
--- a/tests/playground/fix_1.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-def foo (rec : Nat → Nat → Nat) : Nat → Nat → Nat
-| 0     a := a
-| (n+1) a := rec n a + a + rec n (a+1)
-
-def main (xs : List String) : IO UInt32 :=
-let v := fix1 foo (xs.head.toNat) 10 in
-IO.println (toString v) *>
-pure 0
diff --git a/tests/playground/fix_with_tuples.lean b/tests/playground/fix_with_tuples.lean
deleted file mode 100644
index 9980f7efe5..0000000000
--- a/tests/playground/fix_with_tuples.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-def foo (rec : Nat × Nat → Nat) : Nat × Nat → Nat
-| (0, a)   := a
-| (n+1, a) := rec (n, a) + a + rec (n, a+1)
-
-def main (xs : List String) : IO UInt32 :=
-let v := fix foo (xs.head.toNat, 10) in
-IO.println (toString v) *>
-pure 0