Main.lean

@@ -3,39 +3,46 @@ def String.words (s : String) :=
 def String.lines (s : String) :=
   s.splitOn "\n" |>.filter (¬·.isEmpty) |>.toArray
 
-def Array.unlines (xs : Array String) : String :=
-  xs.foldl (· ++ · ++ "\n") ""
+-- TODO: remove trailing
+def Array.unlines (xs : Array String) : String := Id.run do
+  let mut out := ""
+  for line in xs do
+    out := out ++ line ++ "\n"
+  return out
 
 def String.replicate : Nat → Char → String
 | 0,   _ => ""
 | n+1, x => replicate n x |>.push x
 
-def sep (xs : Array String) (space : Fin (xs.size-1) → String)
+def sep (xs space : Array String)
   : String := Id.run do
   let mut out := ""
   let mut i := 0
   while h : i < xs.size do
     out := out ++ xs[i]
-    if h : i < xs.size - 1 then
-      out := out ++ space ⟨i, h⟩
+    if let some space := space[i]?
+    then out := out ++ space
     i := i + 1
   return out
 
-def justify (width : Nat) (words : Array String) : String :=
-  sep words space
-  where
-  space i := if i.val ≤ largeSpaces then largeSpace else smallSpace
-  largeSpace    := smallSpace.push ' '
-  smallSpace    := String.replicate smallSpaceLen ' '
-  smallSpaceLen := spacesNeeded / numSpaces
-  largeSpaces   := spacesNeeded % numSpaces
-  numSpaces     := words.size - 1
-  spacesNeeded  := width - wordsLength
-  wordsLength   := words.foldr (·.length + ·) 0
+def justify : Nat → Array String → String
+| _,   #[word] => word
+| width, words =>
+    let wordsLength   := words.foldr (·.length + ·) 0
+    let spacesNeeded  := width - wordsLength
+    let numSpaces     := words.size - 1
+    let smallSpaceLen := spacesNeeded / numSpaces
+    let smallSpace    := String.replicate smallSpaceLen ' '
+    let largeSpaces   := spacesNeeded % numSpaces
+    let smallSpaces   := numSpaces - largeSpaces
+    let largeSpace    := smallSpace.push ' '
+    let spaces := Array.mkArray largeSpaces largeSpace
+               ++ Array.mkArray smallSpaces smallSpace
+    sep words spaces
 
 def breakUp (width : Nat) (words : Array String) : Array (Array String) :=
   let (_, line, lines) := words.foldl
-    (fun (left, line, lines) word =>
+    (λ(left, line, lines) word ↦
       if word.length < left
       then (left - (word.length + 1), line.push word, lines)
       else (width - word.length, #[word], lines.push line))
@@ -49,20 +56,20 @@ def usage := "Usage: justify WIDTH"
 def fail : IO UInt32 := do IO.println usage; return 1
 
 def main : List String → IO UInt32
-| [width] => do
+| [width] =>
   if let some width := width.toNat?
-  then
+  then do
     let stdin ← IO.getStdin
     let mut remainder : Array String := #[]
-    repeat
+    while true do
       let line ← stdin.getLine
       if line.isEmpty then break
       let lines := breakUp width (remainder ++ line.words)
       if h : lines.size > 0 then
         remainder := lines[lines.size-1]
         for line in lines[0:lines.size-1] do
-          IO.println <| justify width line
-    IO.println <| sep remainder (fun _ => " ")
+          IO.println $ justify width line
+    IO.println $ String.intercalate " " remainder.toList
     return 0
   else fail
 | _ => fail

lakefile.toml

@@ -5,8 +5,3 @@ defaultTargets = ["justify"]
 [[lean_exe]]
 name = "justify"
 root = "Main"
-
-[[require]]
-name = "batteries"
-scope = "leanprover-community"
-rev = "main"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.17.0-rc1
+leanprover/lean4:4.15.0