Copyright	(c) Klaus Luettich Rainer Grabbe Uni Bremen 2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (regex-base needs MPTC+FD)
Safe Haskell	None

Interfaces.GenericATPState

Contents

Data Structures

Description

Data structures and initialising functions for Prover state and configurations. Used by GUI.GenericATP.

Synopsis

type ATPIdentifier = String
data GenericConfig proof_tree = GenericConfig {
- timeLimit :: Maybe Int
- timeLimitExceeded :: Bool
- extraOpts :: [String]
- proofStatus :: ProofStatus proof_tree
- resultOutput :: [String]
- timeUsed :: TimeOfDay
}
emptyConfig :: Ord proof_tree => String -> String -> proof_tree -> GenericConfig proof_tree
getConfig :: Ord proof_tree => String -> ATPIdentifier -> proof_tree -> GenericConfigsMap proof_tree -> GenericConfig proof_tree
type GenericConfigsMap proof_tree = Map ATPIdentifier (GenericConfig proof_tree)
type GenericGoalNameMap = Map String String
data GenericState sentence proof_tree pst = GenericState {
- currentGoal :: Maybe ATPIdentifier
- currentProofTree :: proof_tree
- configsMap :: GenericConfigsMap proof_tree
- namesMap :: GenericGoalNameMap
- goalsList :: [Named sentence]
- proverState :: pst
}
type InitialProverState sign sentence morphism pst = sign -> [Named sentence] -> [FreeDefMorphism sentence morphism] -> pst
type TransSenName = String -> String
initialGenericState :: (Ord sentence, Ord proof_tree) => String -> InitialProverState sign sentence morphism pst -> TransSenName -> Theory sign sentence proof_tree -> [FreeDefMorphism sentence morphism] -> proof_tree -> GenericState sentence proof_tree pst
revertRenamingOfLabels :: (Ord sentence, Ord proof_tree) => GenericState sentence proof_tree pst -> [ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
data ATPRetval
- = ATPSuccess
- | ATPTLimitExceeded
- | ATPError String
- | ATPBatchStopped
type RunProver sentence proof_tree pst = pst -> GenericConfig proof_tree -> Bool -> String -> Named sentence -> IO (ATPRetval, GenericConfig proof_tree)
data ATPFunctions sign sentence morphism proof_tree pst = ATPFunctions {
- initialProverState :: InitialProverState sign sentence morphism pst
- atpTransSenName :: TransSenName
- atpInsertSentence :: pst -> Named sentence -> pst
- goalOutput :: pst -> Named sentence -> [String] -> IO String
- proverHelpText :: String
- batchTimeEnv :: String
- fileExtensions :: FileExtensions
- runProver :: RunProver sentence proof_tree pst
- createProverOptions :: GenericConfig proof_tree -> [String]
}
data FileExtensions = FileExtensions {
- problemOutput :: String
- proverOutput :: String
- theoryConfiguration :: String
}
data ATPTacticScript = ATPTacticScript {
- tsTimeLimit :: Int
- tsExtraOpts :: [String]
}
guiDefaultTimeLimit :: Int
configTimeLimit :: GenericConfig proof_tree -> Int
parseTacticScript :: Int -> [String] -> TacticScript -> ATPTacticScript
printCfgText :: Map ATPIdentifier (GenericConfig proof_tree) -> Doc
excepToATPResult :: String -> String -> SomeException -> IO (ATPRetval, GenericConfig ProofTree)

Data Structures

type ATPIdentifier = String Source #

data GenericConfig proof_tree Source #

Constructors

GenericConfig

Fields

timeLimit :: Maybe Int
Time limit in seconds passed to prover via extra option. Default will be used if Nothing.
timeLimitExceeded :: Bool
True if timelimit exceeded during last prover run.
extraOpts :: [String]
Extra options passed verbatimely to prover. -DocProof, -Stdin, and -TimeLimit will be overridden.
proofStatus :: ProofStatus proof_tree
Represents the result of a prover run.
resultOutput :: [String]
timeUsed :: TimeOfDay
global time used in milliseconds

Instances

Instances details

Eq proof_tree => Eq (GenericConfig proof_tree) Source #
Instance details Defined in Interfaces.GenericATPState Methods (==) :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool (/=) :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
Ord proof_tree => Ord (GenericConfig proof_tree) Source #
Instance details Defined in Interfaces.GenericATPState Methods compare :: GenericConfig proof_tree -> GenericConfig proof_tree -> Ordering (<) :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool (<=) :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool (>) :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool (>=) :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool max :: GenericConfig proof_tree -> GenericConfig proof_tree -> GenericConfig proof_tree min :: GenericConfig proof_tree -> GenericConfig proof_tree -> GenericConfig proof_tree
Show proof_tree => Show (GenericConfig proof_tree) Source #
Instance details Defined in Interfaces.GenericATPState Methods showsPrec :: Int -> GenericConfig proof_tree -> ShowS show :: GenericConfig proof_tree -> String showList :: [GenericConfig proof_tree] -> ShowS

emptyConfig Source #

Arguments

:: Ord proof_tree
=> String	name of the prover
-> String	name of the goal
-> proof_tree	initial empty proof_tree
-> GenericConfig proof_tree

Creates an empty GenericConfig with a given goal name. Default time limit, no resultOutput and no extra options.

getConfig Source #

Arguments

:: Ord proof_tree
=> String	name of the prover
-> ATPIdentifier	name of the goal
-> proof_tree	initial empty proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfig proof_tree

Performs a lookup on the ConfigsMap. Returns the config for the goal or an empty config if none is set yet.

type GenericConfigsMap proof_tree = Map ATPIdentifier (GenericConfig proof_tree) Source #

We need to store one GenericConfig per goal.

type GenericGoalNameMap = Map String String Source #

New goal name mapped to old goal name

data GenericState sentence proof_tree pst Source #

Represents the global state of the prover GUI.

Constructors

GenericState

Fields

currentGoal :: Maybe ATPIdentifier
currently selected goal or Nothing
currentProofTree :: proof_tree
initial empty proof_tree
configsMap :: GenericConfigsMap proof_tree
stores the prover configurations for each goal and the results retrieved by running prover for each goal
namesMap :: GenericGoalNameMap
stores a mapping from the ATP compliant labels to the original labels for all goals
goalsList :: [Named sentence]
list of all goals
proverState :: pst
logical part without theorems

type InitialProverState sign sentence morphism pst = sign -> [Named sentence] -> [FreeDefMorphism sentence morphism] -> pst Source #

Initialising the specific prover state containing logical part.

type TransSenName = String -> String Source #

initialGenericState Source #

Arguments

:: (Ord sentence, Ord proof_tree)
=> String	name of the prover
-> InitialProverState sign sentence morphism pst
-> TransSenName
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]	freeness constraints
-> proof_tree	initial empty proof_tree
-> GenericState sentence proof_tree pst

Creates an initial GenericState around a Theory.

revertRenamingOfLabels :: (Ord sentence, Ord proof_tree) => GenericState sentence proof_tree pst -> [ProofStatus proof_tree] -> Result [ProofStatus proof_tree] Source #

applies the recorded name mapping (in the state) of prover specific names to the original names to the list of ProofStatus (the name of the goal and the names of used axioms are translated); additionally the axioms generated from typing information are removed and warnings are generated.

data ATPRetval Source #

Represents the general return value of a prover run.

Constructors

ATPSuccess	prover completed successfully
ATPTLimitExceeded	prover did not terminate before the time limit exceeded
ATPError String	an error occured while running the prover
ATPBatchStopped	ATP batch mode was stopped with killthread

Instances

Instances details

Eq ATPRetval Source #
Instance details Defined in Interfaces.GenericATPState Methods (==) :: ATPRetval -> ATPRetval -> Bool (/=) :: ATPRetval -> ATPRetval -> Bool
Show ATPRetval Source #
Instance details Defined in Interfaces.GenericATPState Methods showsPrec :: Int -> ATPRetval -> ShowS show :: ATPRetval -> String showList :: [ATPRetval] -> ShowS

type RunProver sentence proof_tree pst = pst -> GenericConfig proof_tree -> Bool -> String -> Named sentence -> IO (ATPRetval, GenericConfig proof_tree) Source #

data ATPFunctions sign sentence morphism proof_tree pst Source #

Prover specific functions

Constructors

ATPFunctions

Fields

initialProverState :: InitialProverState sign sentence morphism pst
initial prover specific state
atpTransSenName :: TransSenName
prover specific translation of goal name
atpInsertSentence :: pst -> Named sentence -> pst
inserts a goal into prover state
goalOutput :: pst -> Named sentence -> [String] -> IO String
output of a goal in a prover specific format
proverHelpText :: String
help text
batchTimeEnv :: String
environment variable containing time limit for batch time
fileExtensions :: FileExtensions
file extensions for all output formats
runProver :: RunProver sentence proof_tree pst
runs the prover
createProverOptions :: GenericConfig proof_tree -> [String]
list of all options the prover finally runs with

data FileExtensions Source #

File extensions for all prover specific output formats. Given extensions should begin with a dot.

Constructors

FileExtensions
Fields problemOutput :: String file extension for saving problem proverOutput :: String file extension for saving prover output theoryConfiguration :: String file extension for saving theory configuration

data ATPTacticScript Source #

Tactic script implementation for ATPs. Read and show functions are derived.

Constructors

ATPTacticScript
Fields tsTimeLimit :: Int used time limit tsExtraOpts :: [String] used extra options (if any)

Instances

Instances details

Eq ATPTacticScript Source #
Instance details Defined in Interfaces.GenericATPState Methods (==) :: ATPTacticScript -> ATPTacticScript -> Bool (/=) :: ATPTacticScript -> ATPTacticScript -> Bool
Ord ATPTacticScript Source #
Instance details Defined in Interfaces.GenericATPState Methods compare :: ATPTacticScript -> ATPTacticScript -> Ordering (<) :: ATPTacticScript -> ATPTacticScript -> Bool (<=) :: ATPTacticScript -> ATPTacticScript -> Bool (>) :: ATPTacticScript -> ATPTacticScript -> Bool (>=) :: ATPTacticScript -> ATPTacticScript -> Bool max :: ATPTacticScript -> ATPTacticScript -> ATPTacticScript min :: ATPTacticScript -> ATPTacticScript -> ATPTacticScript
Read ATPTacticScript Source #
Instance details Defined in Interfaces.GenericATPState Methods readsPrec :: Int -> ReadS ATPTacticScript readList :: ReadS [ATPTacticScript] readPrec :: ReadPrec ATPTacticScript readListPrec :: ReadPrec [ATPTacticScript]
Show ATPTacticScript Source #
Instance details Defined in Interfaces.GenericATPState Methods showsPrec :: Int -> ATPTacticScript -> ShowS show :: ATPTacticScript -> String showList :: [ATPTacticScript] -> ShowS

guiDefaultTimeLimit :: Int Source #

Default time limit for the GUI mode prover in seconds.

configTimeLimit :: GenericConfig proof_tree -> Int Source #

Returns the time limit from GenericConfig if available. Otherwise guiDefaultTimeLimit is returned.

parseTacticScript Source #

Arguments

:: Int	default time limit (standard: `batchTimeLimit`)
-> [String]	default extra options (prover specific)
-> TacticScript
-> ATPTacticScript

Parses a given default tactic script into a ATPTacticScript if possible. Otherwise a default prover's tactic script is returned.

printCfgText Source #

Arguments

:: Map ATPIdentifier (GenericConfig proof_tree)
-> Doc	prover configuration

Pretty printing of prover configuration.

excepToATPResult Source #

Arguments

:: String	name of running prover
-> String	goal name to prove
-> SomeException	occured exception
-> IO (ATPRetval, GenericConfig ProofTree)	(retval, configuration with proof status and complete output)

Converts a thrown exception into an ATP result (ATPRetval and proof tree).