List from user input

Stream: lean4

[Florent Schaffhauser]

Hi!

The following function asks the user to input some numbers in the IO unit, then it constructs a list from it:

def main : IO Unit := do

  let stdin ← IO.getStdin
  let stdout ← IO.getStdout

  stdout.putStrLn "Please enter a list of integers in the form 1, -2, 3 (as many integers as you want, seperated by a comma)."

  let input ← stdin.getLine
  let list := input.splitOn "," |> List.map (fun s => s.trim.toInt!)

  stdout.putStrLn s!"The list you entered is {list}."

However, I am unable to make the same thing works with rationals in place of integers.

I tried to write the following function outside of main, to help parse rational numbers:

def parseRational (s : String) : Option ℚ :=
match s.splitOn "/" with
| [num, denom] =>
  let denomNat := denom.toNat!
  if denomNat = 0 then none
  else some (Rat.mk' (num.toInt!) denomNat _ _)
| _ => none

Am I on the right track? Any pointers on how to proceed?

A much minor issue is that, in the initial function, I would also like to be able to ask the user to input a list under the form [1, -2, 3], as opposed to 1, -2, 3, but I am having a hard time getting rid of the brackets when parsing the user input (I thought I could do it, but then it also suppressed the entry right next to it...). Is there a standard way to do that? I am also happy to read from a reference if somebody can point me to one :-)

[Kyle Miller]

For creating the rational, I'm not sure docs#Rat.mk' should be considered a public interface. You can instead do (num.toInt! / denomNat : ℚ), which should cause both the numerator and denominator to be coerced to a rational and then their quotient is taken in the rationals.

[Kyle Miller]

Here's an example of using Parsec for parsing your square bracket input. I had to write a combinator for doing comma-separated lists, since there's not much in the core Parsec library already. I also didn't write these definitions as tersely as possible.

import Lean

open Lean (Parsec)
open Lean.Parsec

def parseNat : Parsec Nat := do
  let num ← many1Chars digit
  return num.toNat!

def parsePosInt : Parsec Int := do
  let n ← parseNat
  return n

def parseNegInt : Parsec Int := do
  skipChar '-'
  let n ← parseNat
  return -n

def parseInt : Parsec Int := parsePosInt <|> parseNegInt

/--
Parses a comma-separated list of items parsed by `p`.
The commas can have whitespace surrounding them.
-/
partial def parseCommaSep {α : Type} (p : Parsec α) : Parsec (Array α) := do
  go #[]
where
  go (acc : Array α) : Parsec (Array α) := do
    let acc := acc.push (← p)
    ws
    if (← peek?) == ',' then
      skip
      ws
      go acc
    else
      return acc

def parseIntArray : Parsec (Array Int) := do
  skipChar '['
  ws
  let arr ← parseCommaSep parseInt
  skipChar ']'
  return arr

-- Example:
#eval parseIntArray.run "[1,2,-3]"
/- Except.ok #[1, 2, -3] -/

/--
I split this out of `main` to be able to test it with `#eval`.
-/
def processLine (input : String) : IO Unit := do
  -- Uses `eof` to guarantee the whole input is read.
  let list ← IO.ofExcept <| (parseIntArray <* eof).run input.trim

  IO.println s!"The list you entered is {list}."

#eval processLine "[1, -2, 3]"
/-
The list you entered is #[1, -2, 3].
-/

def main : IO Unit := do
  let stdin ← IO.getStdin

  IO.println "Please enter a list of integers in the form [1, -2, 3] (as many integers as you want, seperated by commas)."

  let input ← stdin.getLine
  processLine input

[Kyle Miller]

Here's a version with rational number parsing:

import Lean

open Lean (Parsec Rat)
open Lean.Parsec

def parseNat : Parsec Nat := do
  let num ← many1Chars digit
  return num.toNat!

def parsePosInt : Parsec Int := do
  let n ← parseNat
  return n

def parseNegInt : Parsec Int := do
  skipChar '-'
  let n ← parseNat
  return -n

def parseInt : Parsec Int := parsePosInt <|> parseNegInt

def parseRat : Parsec Rat := do
  let num ← parseInt
  if (← peek?) == '/' then
    skip
    let denom ← parseNat
    if denom == 0 then
      fail "Denominator is 0"
    return num / denom
  else
    return num

/--
Parses a comma-separated list of items parsed by `p`.
The commas can have whitespace surrounding them.
-/
partial def parseCommaSep {α : Type} (p : Parsec α) : Parsec (Array α) := do
  go #[]
where
  go (acc : Array α) : Parsec (Array α) := do
    let acc := acc.push (← p)
    ws
    if (← peek?) == ',' then
      skip
      ws
      go acc
    else
      return acc

def parseRatArray : Parsec (Array Rat) := do
  skipChar '['
  ws
  let arr ← parseCommaSep parseRat
  skipChar ']'
  return arr

-- Example:
#eval toString <| parseRatArray.run "[1,2/3,-3]"
/- "ok: #[1, 2/3, -3]" -/

/--
I split this out of `main` to be able to test it with `#eval`.
-/
def processLine (input : String) : IO Unit := do
  -- Uses `eof` to guarantee the whole input is read.
  let list ← IO.ofExcept <| (parseRatArray <* eof).run input.trim

  IO.println s!"The list you entered is {list}."

#eval processLine "[1, -2/3, 3]"
/-
The list you entered is #[1, -2/3, 3].
-/

def main : IO Unit := do
  let stdin ← IO.getStdin

  IO.println "Please enter a list of integers in the form [1, -2, 3] (as many integers as you want, seperated by commas)."

  let input ← stdin.getLine
  processLine input

[Florent Schaffhauser]

Wow, that's fantastic, @Kyle Miller , thanks! It will take me time to digest all of this, but I'm very grateful :pray:

Something that was not working for me in my initial code was the input of the empty list, the was not being recognized. As far as I can tell, the above code has the same issue, in spite of the brackets. I will try to fix this :sweat_smile: Thanks again!

[Kyle Miller]

@Flo (Florent Schaffhauser) Here seems to be a way to fix the logic so it handles empty lists:

partial def parseCommaSep {α : Type} (p : Parsec α) : Parsec (Array α) :=
  (do go #[← p]) <|> pure #[]
where
  go (acc : Array α) : Parsec (Array α) := do
    ws
    if (← peek?) == ',' then
      skip
      ws
      go (acc.push (← p))
    else
      return acc

The idea is

1. see if p parses, and if not that means we must be looking at an empty list
2. if p does parse, then we want to look for a sequence of , p

[Florent Schaffhauser]

Thanks @Kyle Miller :blush: I lost track of this issue somewhere along the way, but now I'm motivated to try again :+1: