Hets - the Heterogeneous Tool Set

Copyright(c) Klaus Luettich Rainer Grabbe Uni Bremen 2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (regex-base needs MPTC+FD)
Safe HaskellNone

Interfaces.GenericATPState

Contents

Description

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

Synopsis

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

Eq proof_tree => Eq (GenericConfig proof_tree) Source # 

Methods

(==) :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool

(/=) :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool

Ord proof_tree => Ord (GenericConfig proof_tree) Source # 

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 # 

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

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

Eq ATPRetval Source # 

Methods

(==) :: ATPRetval -> ATPRetval -> Bool

(/=) :: ATPRetval -> ATPRetval -> Bool

Show ATPRetval Source # 

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

data FileExtensions Source #

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

Constructors

FileExtensions 

Fields

data ATPTacticScript Source #

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

Constructors

ATPTacticScript 

Fields

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