ivor-0.1.8: Theorem proving library based on dependent type theory Source code Contents Index

Ivor.Shell Portability non-portable Stability experimental Maintainer eb@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 :: Monad m => (Context -> m Context) -> ShellState -> m ShellState sendCommand :: Monad m => String -> ShellState -> m 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

runShell Source

:: String Prompt string -> ShellState Initial state -> IO ShellState Run a command shell.

importFile :: FilePath -> ShellState -> IO ShellState Source

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 -> ShellState Source

Add a directory to the module search path

addStdlibPath :: ShellState -> ShellState Source

Add the standard library path to the module search path

prefix :: FilePath Source

Get the install prefix of the library

getContext :: ShellState -> Context Source

Get the system state from a finished shell

newShell Source

:: Context Initial system state -> ShellState Create a new shell state.

updateShell Source

:: Monad m => Context -> m Context Function to update context -> ShellState -> m ShellState Update the context in a shell

sendCommand :: Monad m => String -> ShellState -> m ShellState Source

Send a command directly to a shell

sendCommandIO :: String -> ShellState -> IO ShellState Source

Send a command directly to a shell, allowing commands which might do IO actions.

addTactic Source

:: String Tactic name. -> String -> Tactic Tactic function. The argument is whatever was input on the shell; the function is responsible for parsing this. -> ShellState Shell to which to add the tactic. -> ShellState Add a user defined tactic to the shell.

addCommand Source

:: String Command 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. -> ShellState Shell to which to add the command. -> ShellState Add a user defined command to the shell.

extendParser :: ShellState -> Parser ViewTerm -> ShellState Source

Add another parsing rule for parsing terms.

configureEq :: String -> String -> String -> ShellState -> ShellState Source

Set up the equality type, for use by the replace tactic

shellParseTerm :: ShellState -> Parser ViewTerm Source

Parse a term using the shell's current parser extensions

showProofState :: ShellState -> String Source

Get a string representation of the current proof state

response :: ShellState -> String Source

Get reply from last shell command

Produced by Haddock version 2.4.2