Language.Lean.IOS

Operations for creating and manipulating an IOState, an object for controlling how Lean sends console output to the user.

Documentation

data IOState tp

The IO State object

Lean uses two channels for sending output to the user:

• A regular output channel, which consists of messages normally printed to stdout.
• A diagnostic output channel, which consists of debugging messages that are normally printed to stderr.

This module currently provides two different IOState types:

• A standard IO state that sends regular output to stdout and diagnostic output to stderr.
• A buffered IO state type that stores output internally, and provides methods for getting output as strings.

To prevent users from accidentally using the wrong type of output, the IOState has an extra type-level parameter used to indicate the type of channel. Most Lean operations support both types of channels and either can be used. Operations specific to a particular channel can use this type parameter to ensure users do not call the function on the wrong type of channel. In addition, we provide a function stateTypeRepr to allow users to determine the type of channel.

Instances

IsLeanValue (IOState tp) (Ptr SomeIOState)

data IOStateType

This describes the type of the IOState.

Constructors

Standard

A standard IOState

Buffered

A buffered IOState

Standard IOState

mkStandardIOState :: IO (IOState Standard)

Create a standard IO state object with default options.

mkStandardIOStateWithOptions :: Options -> IO (IOState Standard)

Create a standard IO state object with the given options.

Buffered IOState

mkBufferedIOState :: IO (IOState Buffered)

Create IO state object that sends the regular and diagnostic output to string buffers with the given options.

mkBufferedIOStateWithOptions :: Options -> IO (IOState Buffered)

Create IO state object that sends the regular and diagnostic output to string buffers with the given options.

getRegularOutput :: IOState Buffered -> IO String

Return the regular output associated with a state.

getDiagnosticOutput :: IOState Buffered -> IO String

Return the diagnostic output associated with a state.

resetRegularOutput :: IOState Buffered -> IO ()

Reset the regular output associated with a state.

resetDiagnosticOutput :: IOState Buffered -> IO ()

Clear the diagnostic output associated with a state.

Operations on IO State

data IOStateTypeRepr tp where

Flag indicating the type of state.

This is implemented as a GADT to allow client code to specialize an IOState to the appropriate subtype.

Constructors

StandardRepr :: IOStateTypeRepr Standard

BufferedRepr :: IOStateTypeRepr Buffered

Instances

Show (IOStateTypeRepr tp)

stateTypeRepr :: IOState tp -> IOStateTypeRepr tp

Get the type of the channel

getStateOptions :: IOState tp -> IO Options

Get the options associated with the state.

setStateOptions :: IOState tp -> Options -> IO ()

Set the options associated with the state.

Operations using IOState

ppExpr :: Env -> IOState tp -> Expr -> IO String

Pretty print an expression