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

Data Structures

type ATPIdentifier = String

data GenericConfig proof_tree

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

Eq proof_tree => Eq (GenericConfig proof_tree)
Ord proof_tree => Ord (GenericConfig proof_tree)
Show proof_tree => Show (GenericConfig proof_tree)

emptyConfig

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

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)

We need to store one GenericConfig per goal.

type GenericGoalNameMap = Map String String

New goal name mapped to old goal name

data GenericState sentence proof_tree pst

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

Initialising the specific prover state containing logical part.

type TransSenName = String -> String

initialGenericState

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]

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

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

Eq ATPRetval
Show ATPRetval

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

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

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

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

Eq ATPTacticScript
Ord ATPTacticScript
Read ATPTacticScript
Show ATPTacticScript

guiDefaultTimeLimit :: Int

Default time limit for the GUI mode prover in seconds.

configTimeLimit :: GenericConfig proof_tree -> Int

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

parseTacticScript

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

Arguments

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

Pretty printing of prover configuration.

excepToATPResult

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).