How to Read from Stdin🔗

To read from stdin, you can use the IO.FS.Stream.getLine function, which reads a line of input from the standard input stream and returns it as a IO String.

def readFromStdin : IO Unit := do
  IO.print "Please enter some input: "
  (← IO.getStdout).flush
  let input ← (← IO.getStdin).getLine
  IO.println s!"You entered: {input.trimAscii}"

For more complex input handling, you can use IO.getStdin directly to read characters or the entire content until EOF.

def readAllFromStdin : IO String := do
  let stdin ← IO.getStdin
  stdin.readToEnd

Fun Example: Interactive Player Input🔗

A common pattern in CLI tools is to request specific types of data (like numbers) and re-prompt the user if the input is invalid.

/-- Repeatedly prompts the user until a valid natural number
within range is provided. -/
partial def getBoundedNat (prompt : String)
    (low high : Nat) : IO Nat := do
  IO.print s!"{prompt} ({low}-{high}): "
  (← IO.getStdout).flush
  let input ← (← IO.getStdin).getLine
  match input.trimAscii.toNat? with
  | some n =>
    if n >= low && n <= high then return n
    else
      IO.println s!"Error: {n} is out of range."
      getBoundedNat prompt low high
  | none =>
    IO.println "Error: Please enter a valid number."
    getBoundedNat prompt low high

def playerInput : IO Unit := do
  IO.print "Enter character name: "
  (← IO.getStdout).flush
  let name ← (← IO.getStdin).getLine
  
  let age ← getBoundedNat "Enter age" 1 150
  let level ← getBoundedNat "Enter starting level" 1 99
  
  IO.println s!"\nWelcome, {name.trimAscii}!"
  IO.println s!"Stats: Age {age}, Level {level}"

In this example, we use partial for getBoundedNat because it is a recursive function that might theoretically run forever if the user never provides valid input.