chore(library/init/lean/compiler): cleanup

library/init/lean/compiler/elimdead.lean

@@ -35,7 +35,7 @@ partial def FnBody.elimDead : FnBody → FnBody
   let bs         := modifyJPVals bs FnBody.elimDead in
   let term       := match term with
     | FnBody.case tid x alts :=
-      let alts := alts.hmap $ λ alt, alt.modifyBody $ λ b, FnBody.elimDead b in
+      let alts := alts.hmap $ λ alt, alt.modifyBody FnBody.elimDead in
       FnBody.case tid x alts
     | other := other in
   reshapeWithoutDead bs term

library/init/lean/compiler/ir.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.lean.name init.lean.kvmap init.lean.format init.data.array
-
 /-
 Implements (extended) λPure and λRc proposed in the article
 "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura.
@@ -581,6 +580,7 @@ partial def formatFnBody (indent : Nat := 2) : FnBody → Format
 | FnBody.unreachable         := "⊥"
 
 instance fnBodyHasFormat : HasFormat FnBody := ⟨formatFnBody⟩
+instance fnBodyHasToString : HasToString FnBody := ⟨λ b, (format b).pretty⟩
 
 def formatDecl (indent : Nat := 2) : Decl → Format
 | (Decl.fdecl f xs ty b) := "def " ++ format f ++ formatArray xs ++ format " : " ++ format ty ++ " :=" ++ Format.nest indent (Format.line ++ formatFnBody indent b)

library/init/lean/compiler/pushproj.lean

@@ -41,7 +41,7 @@ partial def FnBody.pushProj : FnBody → FnBody
   | FnBody.case tid x alts :=
     let afvs       := alts.map $ λ alt, alt.body.freeVars in
     let (bs, alts) := pushProjs bs alts afvs Array.empty {x.idx} in
-    let alts       := alts.hmap $ λ alt, alt.modifyBody $ λ b, FnBody.pushProj b in
+    let alts       := alts.hmap $ λ alt, alt.modifyBody FnBody.pushProj in
     let term       := FnBody.case tid x alts in
     reshape bs term
   | other := reshape bs term