inductive System.SysIO.IOMode : Type

IO mode for opening files.

$$\text{IOMode} ::= \text{readMode} \mid \text{writeMode} \mid \text{appendMode} \mid \text{readWriteMode}$$

• readMode : IOMode

  Open for reading.

• writeMode : IOMode

  Open for writing (truncates existing content).

• appendMode : IOMode

  Open for appending.

• readWriteMode : IOMode

  Open for both reading and writing.

@[implicit_reducible]

instance System.SysIO.instBEqIOMode : BEq IOMode

Equations

• System.SysIO.instBEqIOMode = { beq := System.SysIO.instBEqIOMode.beq }

def System.SysIO.instBEqIOMode.beq : IOMode → IOMode → Bool

Equations

• System.SysIO.instBEqIOMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def System.SysIO.instReprIOMode.repr : IOMode → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance System.SysIO.instReprIOMode : Repr IOMode

Equations

• System.SysIO.instReprIOMode = { reprPrec := System.SysIO.instReprIOMode.repr }

@[reducible, inline]

abbrev System.SysIO.Handle : Type

Handle is an alias for Lean's IO.FS.Handle.

$$\text{Handle} \triangleq \text{IO.FS.Handle}$$

Equations

• System.SysIO.Handle = IO.FS.Handle

def System.SysIO.stdin : IO IO.FS.Stream

Standard input stream.

$$\text{stdin} : \text{IO}\ \text{IO.FS.Stream}$$

Equations

• System.SysIO.stdin = liftM IO.getStdin

def System.SysIO.stdout : IO IO.FS.Stream

Standard output stream.

$$\text{stdout} : \text{IO}\ \text{IO.FS.Stream}$$

Equations

• System.SysIO.stdout = liftM IO.getStdout

def System.SysIO.stderr : IO IO.FS.Stream

Standard error stream.

$$\text{stderr} : \text{IO}\ \text{IO.FS.Stream}$$

Equations

• System.SysIO.stderr = liftM IO.getStderr

@[inline]

def System.SysIO.hPutStr (h : Handle) (s : String) : IO Unit

Write a string to a handle.

$$\text{hPutStr} : \text{Handle} \to \text{String} \to \text{IO}\ \text{Unit}$$

Equations

• System.SysIO.hPutStr h s = IO.FS.Handle.putStr h s

def System.SysIO.hPutStrLn (h : Handle) (s : String) : IO Unit

Write a string followed by a newline to a handle.

$$\text{hPutStrLn} : \text{Handle} \to \text{String} \to \text{IO}\ \text{Unit}$$

Equations

• System.SysIO.hPutStrLn h s = do IO.FS.Handle.putStr h s IO.FS.Handle.putStr h "\n"

@[inline]

def System.SysIO.hGetLine (h : Handle) : IO String

Read a line from a handle.

$$\text{hGetLine} : \text{Handle} \to \text{IO}\ \text{String}$$

Equations

• System.SysIO.hGetLine h = IO.FS.Handle.getLine h

@[inline]

def System.SysIO.hFlush (h : Handle) : IO Unit

Flush a handle's output buffer.

$$\text{hFlush} : \text{Handle} \to \text{IO}\ \text{Unit}$$

Equations

• System.SysIO.hFlush h = IO.FS.Handle.flush h

@[inline]

def System.SysIO.hGetContents (h : Handle) : IO String

Read all remaining contents from a handle.

$$\text{hGetContents} : \text{Handle} \to \text{IO}\ \text{String}$$

Uses Lean's readToEnd which reads until EOF.

Equations

• System.SysIO.hGetContents h = IO.FS.Handle.readToEnd h

def System.SysIO.toFSMode : IOMode → IO.FS.Mode

Convert an IOMode to Lean's IO.FS.Mode.

$$\text{toFSMode} : \text{IOMode} \to \text{IO.FS.Mode}$$

Equations

• System.SysIO.toFSMode System.SysIO.IOMode.readMode = IO.FS.Mode.read
• System.SysIO.toFSMode System.SysIO.IOMode.writeMode = IO.FS.Mode.write
• System.SysIO.toFSMode System.SysIO.IOMode.appendMode = IO.FS.Mode.append
• System.SysIO.toFSMode System.SysIO.IOMode.readWriteMode = IO.FS.Mode.readWrite

def System.SysIO.withFile {α : Type} (path : FilePath) (mode : IOMode) (f : Handle → IO α) : IO α

Open a file with the given mode, use it via the callback, then return.

$$\text{withFile} : \text{FilePath} \to \text{IOMode} \to (\text{Handle} \to \text{IO}\ \alpha) \to \text{IO}\ \alpha$$

The handle is scoped to the callback f.

Equations

• System.SysIO.withFile path mode f = do let h ← IO.FS.Handle.mk path (System.SysIO.toFSMode mode) f h

@[inline]

def System.SysIO.putStr (s : String) : IO Unit

Convenience: write a string to stdout.

$$\text{putStr} : \text{String} \to \text{IO}\ \text{Unit}$$

Equations

• System.SysIO.putStr s = IO.print s

@[inline]

def System.SysIO.putStrLn (s : String) : IO Unit

Convenience: write a string with newline to stdout.

$$\text{putStrLn} : \text{String} \to \text{IO}\ \text{Unit}$$

Equations

• System.SysIO.putStrLn s = IO.println s

def System.SysIO.getLine : IO String

Convenience: read a line from stdin.

$$\text{getLine} : \text{IO}\ \text{String}$$

Equations

• System.SysIO.getLine = do let __do_lift ← liftM IO.getStdin __do_lift.getLine