ivor-0.1.11: Theorem proving library based on dependent type theorySource codeContentsIndex
Ivor.Shell
Portabilitynon-portable
Stabilityexperimental
Maintainereb@dcs.st-and.ac.uk
Description
Shell interface to theorem prover
Synopsis
data ShellState
runShell :: String -> ShellState -> IO ShellState
importFile :: FilePath -> ShellState -> IO ShellState
addModulePath :: ShellState -> FilePath -> ShellState
addStdlibPath :: ShellState -> ShellState
prefix :: FilePath
getContext :: ShellState -> Context
newShell :: Context -> ShellState
updateShell :: (Context -> TTM Context) -> ShellState -> TTM ShellState
sendCommand :: String -> ShellState -> TTM ShellState
sendCommandIO :: String -> ShellState -> IO ShellState
addTactic :: String -> (String -> Tactic) -> ShellState -> ShellState
addCommand :: String -> (String -> Context -> IO (String, Context)) -> ShellState -> ShellState
extendParser :: ShellState -> Parser ViewTerm -> ShellState
configureEq :: String -> String -> String -> ShellState -> ShellState
shellParseTerm :: ShellState -> Parser ViewTerm
showProofState :: ShellState -> String
response :: ShellState -> String
Documentation
data ShellState Source
runShellSource
:: StringPrompt string
-> ShellStateInitial state
-> IO ShellState
Run a command shell.
importFile :: FilePath -> ShellState -> IO ShellStateSource
Import a file of shell commands; fails if the module does not exist in the current directory or search path, does nothing if already loaded.
addModulePath :: ShellState -> FilePath -> ShellStateSource
Add a directory to the module search path
addStdlibPath :: ShellState -> ShellStateSource
Add the standard library path to the module search path
prefix :: FilePathSource
Get the install prefix of the library
getContext :: ShellState -> ContextSource
Get the system state from a finished shell
newShellSource
:: ContextInitial system state
-> ShellState
Create a new shell state.
updateShellSource
:: Context -> TTM ContextFunction to update context
-> ShellState
-> TTM ShellState
Update the context in a shell
sendCommand :: String -> ShellState -> TTM ShellStateSource
Send a command directly to a shell
sendCommandIO :: String -> ShellState -> IO ShellStateSource
Send a command directly to a shell, allowing commands which might do IO actions.
addTacticSource
:: StringTactic name.
-> String -> TacticTactic function. The argument is whatever was input on the shell; the function is responsible for parsing this.
-> ShellStateShell to which to add the tactic.
-> ShellState
Add a user defined tactic to the shell.
addCommandSource
:: StringCommand name.
-> String -> Context -> IO (String, Context)Command function. The argument is whatever was input on the shell; the function is responsible for parsing this. The command returns a string (the response) and a possibly updated context.
-> ShellStateShell to which to add the command.
-> ShellState
Add a user defined command to the shell.
extendParser :: ShellState -> Parser ViewTerm -> ShellStateSource
Add another parsing rule for parsing terms.
configureEq :: String -> String -> String -> ShellState -> ShellStateSource
Set up the equality type, for use by the replace tactic
shellParseTerm :: ShellState -> Parser ViewTermSource
Parse a term using the shell's current parser extensions
showProofState :: ShellState -> StringSource
Get a string representation of the current proof state
response :: ShellState -> StringSource
Get reply from last shell command
Produced by Haddock version 2.6.0