| Copyright | (c) Galois Inc, 2015 |
|---|---|
| License | Apache-2 |
| Maintainer | jhendrix@galois.com, lcasburn@galois.com |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Language.Lean.IOS
Description
Operations for creating and manipulating an IOState, an object
for controlling how Lean sends console output to the user.
- data IOState tp
- data IOStateType
- mkStandardIOState :: IO (IOState Standard)
- mkStandardIOStateWithOptions :: Options -> IO (IOState Standard)
- mkBufferedIOState :: IO (IOState Buffered)
- mkBufferedIOStateWithOptions :: Options -> IO (IOState Buffered)
- getRegularOutput :: IOState Buffered -> IO String
- getDiagnosticOutput :: IOState Buffered -> IO String
- resetRegularOutput :: IOState Buffered -> IO ()
- resetDiagnosticOutput :: IOState Buffered -> IO ()
- data IOStateTypeRepr tp where
- stateTypeRepr :: IOState tp -> IOStateTypeRepr tp
- getStateOptions :: IOState tp -> IO Options
- setStateOptions :: IOState tp -> Options -> IO ()
- ppExpr :: Env -> IOState tp -> Expr -> IO String
Documentation
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
stdoutand diagnostic output tostderr. - 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) Source |
data IOStateType Source
This describes the type of the IOState.
Standard IOState
mkStandardIOState :: IO (IOState Standard) Source
Create a standard IO state object with default options.
mkStandardIOStateWithOptions :: Options -> IO (IOState Standard) Source
Create a standard IO state object with the given options.
Buffered IOState
mkBufferedIOState :: IO (IOState Buffered) Source
Create IO state object that sends the regular and diagnostic output to string buffers with the given options.
mkBufferedIOStateWithOptions :: Options -> IO (IOState Buffered) Source
Create IO state object that sends the regular and diagnostic output to string buffers with the given options.
getRegularOutput :: IOState Buffered -> IO String Source
Return the regular output associated with a state.
getDiagnosticOutput :: IOState Buffered -> IO String Source
Return the diagnostic output associated with a state.
resetRegularOutput :: IOState Buffered -> IO () Source
Reset the regular output associated with a state.
resetDiagnosticOutput :: IOState Buffered -> IO () Source
Clear the diagnostic output associated with a state.
Operations on IO State
data IOStateTypeRepr tp where Source
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) Source |
stateTypeRepr :: IOState tp -> IOStateTypeRepr tp Source
Get the type of the channel
getStateOptions :: IOState tp -> IO Options Source
Get the options associated with the state.
setStateOptions :: IOState tp -> Options -> IO () Source
Set the options associated with the state.