Normalizer.lean

def normalize (s : String) : String := Id.run do
  let s := s.dropWhile (·.isWhitespace) |>.dropRightWhile (·.isWhitespace)
  let lines := s.splitOn "\n" 
    |>.map (fun s => s.dropWhile (·.isWhitespace) |>.dropRightWhile (·.isWhitespace))
  let mut r := ""
  for i in [0:lines.length-1] do
    let line := lines[i]!
    if line.endsWith "." || line.endsWith ":" then
      r := r ++ line ++ "\\n"
    else if line == "" then
      r := r ++ "\\n"
    else
      r := r ++ line ++ " "
  r := r ++ lines[lines.length-1]!
  return s!"\"description\": \"{r}\""

def printNormalized (s : String) : IO Unit := do
  IO.println <| normalize s


def s := "

"

#eval printNormalized s