mbk/justify
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

remove Array.replicate and #evals

Browse source 
`Array.mkArray` does the same thing. couldn't remember the name!
This commit is contained in:
mehbark 2025-01-28 11:31:50 -05:00
parent 434de18e37
commit 0706170d95
1 changed files with 4 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
Main.lean
View file

@ -10,19 +10,6 @@ def Array.unlines (xs : Array String) : String := Id.run do
out := out ++ line ++ "\n" out := out ++ line ++ "\n"
return out return out
def ex := "The heat bloomed\tin December\nas the carnival season\n kicked into gear.\nNearly helpless with sun and glare, I avoided Rio's brilliant\nsidewalks\n and glittering beaches,\npanting in dark corners\nand waiting out the inverted southern summer."
#eval ex.words
#eval ex.lines
#eval IO.println ex.lines.unlines
def Array.replicate : Nat → α → Array α
| 0, _ => #[]
| n+1, x => replicate n x |>.push x
theorem Array.replicate_size_eq_n : (Array.replicate n x).size = n := by
induction n <;> simp [Array.replicate, *]
def String.replicate : Nat → Char → String def String.replicate : Nat → Char → String
| 0, _ => "" | 0, _ => ""
| n+1, x => replicate n x |>.push x | n+1, x => replicate n x |>.push x
@ -32,9 +19,9 @@ def sep (xs space : Array String)
let mut out := "" let mut out := ""
let mut i := 0 let mut i := 0
while h : i < xs.size do while h : i < xs.size do
out := out.append xs[i] out := out ++ xs[i]
if let some space := space[i]? if let some space := space[i]?
then out := out.append space then out := out ++ space
i := i + 1 i := i + 1
return out return out
@ -49,13 +36,10 @@ def justify : Nat → Array String → String
let largeSpaces := spacesNeeded % numSpaces let largeSpaces := spacesNeeded % numSpaces
let smallSpaces := numSpaces - largeSpaces let smallSpaces := numSpaces - largeSpaces
let largeSpace := smallSpace.push ' ' let largeSpace := smallSpace.push ' '
let spaces := Array.replicate largeSpaces largeSpace let spaces := Array.mkArray largeSpaces largeSpace
++ Array.replicate smallSpaces smallSpace ++ Array.mkArray smallSpaces smallSpace
sep words spaces sep words spaces
#eval justify 1 "Hello, world, how is it going?".words
#eval justify 1 "Hello, world, how is it going?".words |>.length
def breakUp (width : Nat) (words : Array String) : Array (Array String) := def breakUp (width : Nat) (words : Array String) : Array (Array String) :=
let (_, line, lines) := words.foldl let (_, line, lines) := words.foldl
(λ(left, line, lines) word ↦ (λ(left, line, lines) word ↦
@ -68,8 +52,6 @@ def breakUp (width : Nat) (words : Array String) : Array (Array String) :=
def solve (width : Nat) := def solve (width : Nat) :=
Array.unlines ∘ Array.map (justify width) ∘ breakUp width ∘ String.words Array.unlines ∘ Array.map (justify width) ∘ breakUp width ∘ String.words
#eval IO.println $ solve 40 ex
def usage := "Usage: justify WIDTH" def usage := "Usage: justify WIDTH"
def fail : IO UInt32 := do IO.println usage; return 1 def fail : IO UInt32 := do IO.println usage; return 1