Language.Lean.Internal.IOS

Internal declarations for IOState.

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)

withIOState :: IOState tp -> (Ptr SomeIOState -> IO a) -> IO a

Run a computation with an io state.

someIOS :: IOState tp -> SomeIOState

Lift an arbitray IOState to SomeIOState

data IOStateType

This describes the type of the IOState.

Constructors

Standard

A standard IOState

Buffered

A buffered IOState

data SomeIOState

Internal state used for bindings

Instances

IsLeanValue (IOState tp) (Ptr SomeIOState)

type SomeIOStatePtr = Ptr SomeIOState

Haskell type for lean_ios FFI parameters.

type OutSomeIOStatePtr = Ptr SomeIOStatePtr

Haskell type for lean_ios* FFI parameters.

withSomeIOState :: SomeIOState -> (Ptr SomeIOState -> IO a) -> IO a

Function c2hs uses to pass SomeIOState values to Lean

type BufferedIOState = IOState Buffered

Type synonym for c2hs to use specifically for functions that expected buffered IO state.

withBufferedIOState :: IOState Buffered -> (Ptr SomeIOState -> IO a) -> IO a

Function c2hs uses to pass BufferedIOState values to Lean