| Copyright | (c) Rene Wagner, Heng Jiang, Uni Bremen 2007 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | luecke@informatik.uni-bremen.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
SoftFOL.Sign
Contents
Description
Data structures representing SPASS signatures. Refer to http://spass.mpi-sb.mpg.de/webspass/help/syntax/dfgsyntax.html for the SPASS syntax documentation.
- type SoftFOLMorphism = DefaultMorphism Sign
- type SortMap = Map SPIdentifier (Maybe Generated)
- type FuncMap = Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
- type PredMap = Map SPIdentifier (Set [SPIdentifier])
- data Sign = Sign {}
- data Generated = Generated {
- freely :: Bool
- byFunctions :: [SPIdentifier]
- emptySign :: Sign
- type Sentence = SPTerm
- type SPIdentifier = Token
- singleSortNotGen :: Sign -> Bool
- data SFSymbol = SFSymbol {}
- data SFSymbType
- data SPProblem = SPProblem {}
- data SPLogicalPart = SPLogicalPart {}
- emptySPLogicalPart :: SPLogicalPart
- data SPSymbolList = SPSymbolList {}
- emptySymbolList :: SPSymbolList
- data SPSignSym
- = SPSignSym {
- sym :: SPIdentifier
- arity :: Int
- | SPSimpleSignSym SPIdentifier
- = SPSignSym {
- data SPSortSym = SPSortSym SPIdentifier
- data SPDeclaration
- = SPSubsortDecl { }
- | SPTermDecl {
- termDeclTermList :: [SPTerm]
- termDeclTerm :: SPTerm
- | SPSimpleTermDecl SPTerm
- | SPPredDecl {
- predSym :: SPIdentifier
- sortSyms :: [SPIdentifier]
- | SPGenDecl { }
- data SPFormulaList = SPFormulaList {
- originType :: SPOriginType
- formulae :: [SPFormula]
- isAxiomFormula :: SPFormulaList -> Bool
- data SPClauseList = SPClauseList {}
- data SPOriginType
- data SPClauseType
- type SPClause = Named NSPClause
- data NSPClause
- data NSPClauseBody = NSPClauseBody SPClauseType [SPLiteral]
- data TermWsList = TWL [SPTerm] Bool
- data SPTerm
- = SPQuantTerm {
- quantSym :: SPQuantSym
- variableList :: [SPTerm]
- qFormula :: SPTerm
- | SPComplexTerm { }
- = SPQuantTerm {
- data FileName = FileName String
- data FormKind
- data Role
- data Name = Name String
- data Annos = Annos Source (Maybe Info)
- data Source = Source GenTerm
- data AWord = AWord String
- data GenTerm
- data GenData
- data FormData = FormData FormKind SPTerm
- data Info = Info [GenTerm]
- data TPTP
- data SPLiteral = SPLiteral Bool SPSymbol
- toLiteral :: Monad m => SPTerm -> m SPLiteral
- data SPQuantSym
- data SPSymbol
- mkSPCustomSymbol :: String -> SPSymbol
- showSPSymbol :: SPSymbol -> String
- data SPProofList = SPProofList {}
- type SPProofType = SPIdentifier
- data SPProofStep = SPProofStep {}
- data SPReference = PRefTerm SPTerm
- data SPResult = PResTerm SPTerm
- data SPRuleAppl
- data SPUserRuleAppl
- data SPParent = PParTerm SPTerm
- type SPAssocList = Map SPKey SPValue
- data SPKey = PKeyTerm SPTerm
- data SPValue = PValTerm SPTerm
- type SPFormula = Named SPTerm
- typedVarTerm :: SPIdentifier -> SPIdentifier -> SPTerm
- spTerms :: [SPIdentifier] -> [SPTerm]
- spSym :: SPIdentifier -> SPSymbol
- compTerm :: SPSymbol -> [SPTerm] -> SPTerm
- simpTerm :: SPSymbol -> SPTerm
- mkConj :: SPTerm -> SPTerm -> SPTerm
- mkDisj :: SPTerm -> SPTerm -> SPTerm
- mkEq :: SPTerm -> SPTerm -> SPTerm
- data SPDescription = SPDescription {}
- data SPLogState
- data SPSetting
- = SPGeneralSettings {
- entries :: [SPHypothesis]
- | SPSettings { }
- = SPGeneralSettings {
- data SPSettingBody
- = SPClauseRelation [SPCRBIND]
- | SPFlag String [String]
- data SPHypothesis = SPHypothesis [SPIdentifier]
- data SPSettingLabel
- showSettingLabel :: SPSettingLabel -> String
- data SPCRBIND = SPCRBIND {
- clauseSPR :: String
- formulaSPR :: String
- negateSentence :: SPTerm -> Maybe SPTerm
Externally used data structures
type SoftFOLMorphism = DefaultMorphism Sign
We use the DefaultMorphism for SPASS.
type SortMap = Map SPIdentifier (Maybe Generated)
type FuncMap = Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
type PredMap = Map SPIdentifier (Set [SPIdentifier])
data Sign
This Signature data type will be translated to the SoftFOL data types internally.
sortRel contains the sorts relation. For each sort we need to know if it is a generated sort and if so by which functions it is possibly freely generated (sortMap).
For each function the types of all arguments and the return type must be known (funcMap). The same goes for the arguments of a predicate (predMap).
Constructors
| Sign | |
Instances
data Generated
Sorts can be (freely) generated by a set of functions.
Constructors
| Generated | |
Fields
| |
type SPIdentifier = Token
A SPASS Identifier is a String for now.
singleSortNotGen :: Sign -> Bool
Check a Sign if it is single sorted (and the sort is non-generated).
Symbol related datatypes
data SFSymbol
Symbols of SoftFOL.
Constructors
| SFSymbol | |
Fields | |
Instances
data SFSymbType
Symbol types of SoftFOL. (not related to CASL)
Constructors
| SFOpType [SPIdentifier] SPIdentifier | |
| SFPredType [SPIdentifier] | |
| SFSortType |
Internal data structures
SPASS Problems
data SPProblem
A SPASS problem consists of a description and a logical part. The optional settings part hasn't been implemented yet.
Constructors
| SPProblem | |
Fields
| |
SPASS Logical Parts
data SPLogicalPart
A SPASS logical part consists of a symbol list, a declaration list, and a set of formula lists. Support for clause lists and proof lists hasn't been implemented yet.
Constructors
| SPLogicalPart | |
Fields
| |
Instances
| Eq SPLogicalPart | |
| Data SPLogicalPart | |
| Ord SPLogicalPart | |
| Show SPLogicalPart | |
| ShATermConvertible SPLogicalPart | |
| Pretty SPLogicalPart | Creates a Doc from a SPASS Logical Part. |
| PrintTPTP SPLogicalPart | Creates a Doc from a SoftFOL Logical Part. |
| Typeable * SPLogicalPart |
Symbol Lists
data SPSymbolList
All non-predefined signature symbols must be declared as part of a SPASS symbol list.
Constructors
| SPSymbolList | |
Instances
| Eq SPSymbolList | |
| Data SPSymbolList | |
| Ord SPSymbolList | |
| Show SPSymbolList | |
| ShATermConvertible SPSymbolList | |
| Pretty SPSymbolList | Creates a Doc from a SPASS Symbol List. |
| Typeable * SPSymbolList |
emptySymbolList :: SPSymbolList
Creates an empty SPASS Symbol List.
data SPSignSym
A common data type used for all signature symbols.
Constructors
| SPSignSym | |
Fields
| |
| SPSimpleSignSym SPIdentifier | |
data SPSortSym
Constructors
| SPSortSym SPIdentifier |
Declarations
data SPDeclaration
SPASS Declarations allow the introduction of sorts.
Constructors
| SPSubsortDecl | |
Fields | |
| SPTermDecl | |
Fields
| |
| SPSimpleTermDecl SPTerm | |
| SPPredDecl | |
Fields
| |
| SPGenDecl | |
Fields
| |
Instances
| Eq SPDeclaration | |
| Data SPDeclaration | |
| Ord SPDeclaration | |
| Show SPDeclaration | |
| ShATermConvertible SPDeclaration | |
| Pretty SPDeclaration | Creates a Doc from a SPASS Declaration |
| PrintTPTP SPDeclaration | Creates a Doc from a SoftFOL Declaration. A subsort declaration will be rewritten as a special SPQuantTerm. |
| Typeable * SPDeclaration |
Formula List
data SPFormulaList
SPASS Formula List
Constructors
| SPFormulaList | |
Fields
| |
Instances
| Eq SPFormulaList | |
| Data SPFormulaList | |
| Ord SPFormulaList | |
| Show SPFormulaList | |
| ShATermConvertible SPFormulaList | |
| Pretty SPFormulaList | Creates a Doc from a SPASS Formula List |
| PrintTPTP SPFormulaList | Creates a Doc from a SoftFOL Formula List. |
| Typeable * SPFormulaList |
isAxiomFormula :: SPFormulaList -> Bool
test the origin type of the formula list
Clause List
data SPClauseList
SPASS Clause List
Constructors
| SPClauseList | |
Fields
| |
data SPOriginType
There are axiom formulae and conjecture formulae.
Constructors
| SPOriginAxioms | |
| SPOriginConjectures |
Instances
| Eq SPOriginType | |
| Data SPOriginType | |
| Ord SPOriginType | |
| Show SPOriginType | |
| ShATermConvertible SPOriginType | |
| Pretty SPOriginType | Creates a Doc from a SPASS Origin Type |
| PrintTPTP SPOriginType | Creates a Doc from a SoftFOL Origin Type. |
| Typeable * SPOriginType |
data SPClauseType
Formulae can be in cnf or dnf
data NSPClause
data NSPClauseBody
a true boolean indicates the cnf
Constructors
| NSPClauseBody SPClauseType [SPLiteral] |
data TermWsList
data SPTerm
A SPASS Term.
Constructors
| SPQuantTerm | |
Fields
| |
| SPComplexTerm | |
Instances
| Eq SPTerm | |
| Data SPTerm | |
| Ord SPTerm | |
| Show SPTerm | |
| ShATermConvertible SPTerm | |
| GetRange SPTerm | |
| Pretty SPTerm | Creates a Doc from a SPASS Term. |
| PrintTPTP SPTerm | Creates a Doc from a SoftFOL Term. |
| Typeable * SPTerm | |
| Sentences SoftFOL Sentence Sign SoftFOLMorphism SFSymbol | |
| Comorphism SoftFOL2CommonLogic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree | |
| Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree | |
| StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () |
data FileName
data FormKind
data Role
data Name
data Annos
data Source
data AWord
data GenTerm
data GenData
Constructors
| GenData AWord [GenTerm] | |
| OtherGenData String | |
| GenFormData FormData |
data FormData
data Info
data TPTP
Constructors
| FormAnno FormKind Name Role SPTerm (Maybe Annos) | |
| Include FileName [Name] | |
| CommentLine String | |
| EmptyLine |
Instances
data SPLiteral
Literals for SPASS CNF and DNF (the boolean indicates a negated literal).
data SPQuantSym
SPASS Quantifier Symbols.
Constructors
| SPForall | |
| SPExists | |
| SPCustomQuantSym SPIdentifier |
Instances
| Eq SPQuantSym | |
| Data SPQuantSym | |
| Ord SPQuantSym | |
| Show SPQuantSym | |
| ShATermConvertible SPQuantSym | |
| Pretty SPQuantSym | Creates a Doc from a SPASS Quantifier Symbol. |
| PrintTPTP SPQuantSym | Creates a Doc from a SoftFOL Quantifier Symbol. |
| Typeable * SPQuantSym |
data SPSymbol
SPASS Symbols.
mkSPCustomSymbol :: String -> SPSymbol
showSPSymbol :: SPSymbol -> String
Proof List
data SPProofList
SPASS Proof List
Constructors
| SPProofList | |
Fields
| |
type SPProofType = SPIdentifier
data SPProofStep
Constructors
| SPProofStep | |
Fields
| |
data SPReference
data SPResult
data SPRuleAppl
Constructors
| PRuleTerm SPTerm | |
| PRuleUser SPUserRuleAppl |
data SPUserRuleAppl
data SPParent
type SPAssocList = Map SPKey SPValue
data SPKey
data SPValue
Formulae And Terms
A SPASS Formula is modelled as a Named SPTerm for now. This doesn't reflect the fact that the SPASS syntax lists both term and label as optional.
helpers for generating SoftFOL formulas
Arguments
| :: SPIdentifier | Variable symbol: v |
| -> SPIdentifier | Sort symbol: s |
| -> SPTerm | Term: s(v) |
spTerms :: [SPIdentifier] -> [SPTerm]
spSym :: SPIdentifier -> SPSymbol
SPASS Desciptions
data SPDescription
A description is mandatory for a SPASS problem. It has to specify
at least a name, the name of the author, the status (see also
SPLogState below), and a (verbose) description.
Constructors
| SPDescription | |
Instances
| Eq SPDescription | |
| Data SPDescription | |
| Ord SPDescription | |
| Show SPDescription | |
| ShATermConvertible SPDescription | |
| Pretty SPDescription | Creates a Doc from a SPASS description. |
| PrintTPTP SPDescription | Creates a Doc from a SoftFOL description. |
| Typeable * SPDescription |
data SPLogState
The state of a SPASS problem can be satisfiable, unsatisfiable, or unknown.
Constructors
| SPStateSatisfiable | |
| SPStateUnsatisfiable | |
| SPStateUnknown |
Instances
| Eq SPLogState | |
| Data SPLogState | |
| Ord SPLogState | |
| Show SPLogState | |
| ShATermConvertible SPLogState | |
| Pretty SPLogState | Creates a Doc from an |
| PrintTPTP SPLogState | Creates a Doc from an |
| Typeable * SPLogState |
SPASS Settings
data SPSetting
New impelmentation of Settings. See spass input syntax Version 1.5.
Constructors
| SPGeneralSettings | |
Fields
| |
| SPSettings | |
Fields | |
data SPSettingBody
Constructors
| SPClauseRelation [SPCRBIND] | |
| SPFlag String [String] |
data SPHypothesis
Constructors
| SPHypothesis [SPIdentifier] |
data SPSettingLabel
data SPCRBIND
A Tupel of the Clause Relation
Constructors
| SPCRBIND | |
Fields
| |
negateSentence :: SPTerm -> Maybe SPTerm
negate a sentence