Sign.hs revision e886f76655ea805ae1410610cddce301f930b87a
{- |
Module : $Header$
Description : Data structures representing SPASS signatures.
Copyright : (c) Rene Wagner, Heng Jiang, Uni Bremen 2007
License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
Maintainer : luecke@informatik.uni-bremen.de
Stability : provisional
Portability : portable
Data structures representing SPASS signatures.
for the SPASS syntax documentation.
-}
module SoftFOL.Sign where
import Data.Char
import Common.AS_Annotation
import Common.DefaultMorphism
import Common.Doc
import Common.DocUtils
import SoftFOL.Utils
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Lib.Rel as Rel
-- import qualified Common.Id as Id
-- * Externally used data structures
type SortMap = Map.Map SPIdentifier (Maybe Generated)
{- |
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).
-}
data Sign = Sign { sortRel :: Rel.Rel SPIdentifier
, sortMap :: SortMap
, funcMap :: FuncMap
, predMap :: PredMap
, singleSorted :: Bool
} deriving (Eq, Show)
{- |
Sorts can be (freely) generated by a set of functions.
-}
data Generated = Generated { freely :: Bool
, byFunctions :: [SPIdentifier]
} deriving (Eq, Ord, Show)
{- |
Creates an empty Signature.
-}
emptySign :: Sign
emptySign = Sign { sortRel = Rel.empty
, sortMap = Map.empty
, funcMap = Map.empty
, predMap = Map.empty
, singleSorted = True
}
{- |
'checkArities'
checks if the signature has only overloaded symbols with the same arity
-}
checkArities :: Sign -> Bool
checkArities s =
checkPredArities (predMap s) && checkFuncArities (funcMap s)
checkPredArities :: PredMap -> Bool
checkPredArities = Map.fold checkSet True
where checkSet s bv = bv && not (Set.null s) &&
all (\ x -> length x == length hd) tl
where hd : tl = Set.toList s
checkFuncArities :: FuncMap -> Bool
checkFuncArities = checkPredArities . mapToPredMap
{- |
A Sentence is a SoftFOL Term.
-}
type Sentence = SPTerm
{- |
We use the DefaultMorphism for SPASS.
-}
type SoftFOLMorphism = DefaultMorphism Sign
{- |
A SPASS Identifier is a String for now. See also 'checkIdentifier' function
below. Might need conversion functions as well.
-}
type SPIdentifier = String
{- |
SPASS Identifiers may contain letters, digits, and underscores only; but
for TPTP the allowed starting letters are different for each sort of
identifier.
-}
checkIdentifier :: CType -> String -> Bool
checkIdentifier _ "" = False
checkIdentifier t xs@(x:_) = and ((checkFirstChar t x) : map checkSPChar xs)
{- |
important for TPTP format
-}
checkFirstChar :: CType -> Char -> Bool
checkFirstChar t = case t of
CVar _ -> isUpper
_ -> isLower
{- |
Allowed SPASS characters are letters, digits, and underscores.
-}
-- Warning:
-- Data.Char.isAlphaNum includes all kinds of isolatin1 characters!!
checkSPChar :: Char -> Bool
checkSPChar c = (isAlphaNum c && isAscii c )|| '_' == c
{- |
Check a Sign if it is single sorted (and the sort is non-generated).
-}
singleSortNotGen :: Sign -> Bool
singleSortNotGen spSig = singleSorted spSig &&
(head . Map.elems $ sortMap spSig) == Nothing
-- ** Symbol related datatypes
{- |
Symbols of SoftFOL.
-}
data SFSymbol = SFSymbol { sym_ident :: SPIdentifier
, sym_type :: SFSymbType}
deriving (Show,Eq,Ord)
{- |
Symbol types of SoftFOL. (not related to CASL)
-}
data SFSymbType = SFOpType [SPIdentifier] SPIdentifier
| SFPredType [SPIdentifier]
| SFSortType
deriving (Show,Eq,Ord)
instance Pretty SFSymbol where
pretty sy = cat [text (sym_ident sy) , pretty (sym_type sy)]
instance Pretty SFSymbType where
pretty st = case st of
SFOpType args res -> sep [text ":" <+> pr args, text "->" <+> text res]
SFPredType args -> text ":" <+> pr args
SFSortType -> empty
where pr = sep . punctuate (text "* ") . map text
-- * Internal data structures
-- ** SPASS Problems
{- |
A SPASS problem consists of a description and a logical part. The optional
settings part hasn't been implemented yet.
-}
data SPProblem =
SPProblem { identifier :: SPIdentifier,
description :: SPDescription,
logicalPart :: SPLogicalPart,
settings :: [SPSetting]
}
deriving (Eq, Ord, Show)
-- ** SPASS Logical Parts
{- |
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.
-}
data SPLogicalPart =
SPLogicalPart { symbolList :: Maybe SPSymbolList,
declarationList :: Maybe [SPDeclaration],
formulaLists :: [SPFormulaList],
clauseLists :: [SPClauseList],
proofLists :: [SPProofList]
}
deriving (Eq, Ord, Show)
emptySPLogicalPart :: SPLogicalPart
emptySPLogicalPart = SPLogicalPart { symbolList = Nothing,
declarationList = Nothing,
formulaLists = [],
clauseLists = [],
proofLists = []
}
-- *** Symbol Lists
{- |
All non-predefined signature symbols must be declared as part of a SPASS
symbol list.
-}
data SPSymbolList =
SPSymbolList { functions :: [SPSignSym],
predicates :: [SPSignSym],
sorts :: [SPSignSym],
operators :: [SPSignSym],
quantifiers :: [SPSignSym] }
deriving (Eq, Ord, Show)
{- |
Creates an empty SPASS Symbol List.
-}
emptySymbolList :: SPSymbolList
emptySymbolList =
SPSymbolList { functions = [],
predicates = [],
sorts = [],
operators = [],
quantifiers = [] }
{- |
A common data type used for all signature symbols.
-}
data SPSignSym =
SPSignSym { sym :: SPIdentifier,
arity :: Int }
| SPSimpleSignSym SPIdentifier
deriving (Eq, Ord, Show)
-- *** Declarations
{- |
SPASS Declarations allow the introduction of sorts.
-}
data SPDeclaration =
SPSubsortDecl { sortSymA :: SPIdentifier,
sortSymB :: SPIdentifier }
| SPTermDecl { termDeclTermList :: [SPTerm],
termDeclTerm :: SPTerm }
| SPSimpleTermDecl SPTerm
| SPPredDecl { predSym :: SPIdentifier,
sortSyms :: [SPIdentifier] }
| SPGenDecl { sortSym :: SPIdentifier,
freelyGenerated :: Bool,
funcList :: [SPIdentifier]}
deriving (Eq, Ord, Show)
-- *** Formula List
{- |
SPASS Formula List
-}
data SPFormulaList =
SPFormulaList { originType :: SPOriginType,
formulae :: [SPFormula] }
deriving (Eq, Ord, Show)
-- *** Clause List
{- |
SPASS Clause List
-}
data SPClauseList =
SPClauseList { coriginType :: SPOriginType,
clauseType :: SPClauseType,
clauses :: [SPClause] }
deriving (Eq, Ord, Show)
{- |
There are axiom formulae and conjecture formulae.
-}
data SPOriginType =
SPOriginAxioms
| SPOriginConjectures
deriving (Eq, Ord, Show)
isAxiomFormula :: SPFormulaList -> Bool
isAxiomFormula fl =
case originType fl of
SPOriginAxioms -> True
_ -> False
isAxiomClause :: SPClauseList -> Bool
isAxiomClause cl =
case coriginType cl of
SPOriginAxioms -> True
_ -> False
{- |
Formulae can be in cnf or dnf
-}
data SPClauseType = SPCNF
| SPDNF
deriving (Eq, Ord, Show)
type SPClause = Named NSPClause
data NSPClause = QuanClause [SPTerm] NSPClauseBody
| SimpleClause NSPClauseBody
| BriefClause TermWsList TermWsList TermWsList
deriving (Eq, Ord, Show)
data NSPClauseBody = NSPCNF [SPLiteral]
| NSPDNF [SPLiteral]
deriving (Eq, Ord, Show)
data TermWsList = TWL [SPTerm] Bool -- maybe plus.
deriving (Eq, Ord, Show)
{- |
A SPASS Term.
-}
data SPTerm =
SPQuantTerm { quantSym :: SPQuantSym,
variableList :: [SPTerm],
qFormula :: SPTerm }
| SPSimpleTerm SPSymbol
| SPComplexTerm { symbol :: SPSymbol,
arguments :: [SPTerm]}
deriving (Eq, Ord, Show)
{- | Literals for SPASS CNF and DNF -}
data SPLiteral = NSPFalse
| NSPTrue
{-
| NSPId SPIdentifier -- Simple literals for propositional logic
| NSPNotId SPIdentifier
-}
| NSPPLit SPTerm -- More complex literals for FOL
| NSPNotPLit SPTerm
deriving (Eq, Ord, Show)
{- |
SPASS Quantifier Symbols.
-}
data SPQuantSym =
SPForall
| SPExists
| SPCustomQuantSym SPIdentifier
deriving (Eq, Ord, Show)
{- |
SPASS Symbols.
-}
data SPSymbol =
SPEqual
| SPTrue
| SPFalse
| SPOr
| SPAnd
| SPNot
| SPImplies
| SPImplied
| SPEquiv
| SPID
| SPDiv
| SPComp
| SPSum
| SPConv
| SPCustomSymbol SPIdentifier
deriving (Eq, Ord, Show)
-- *** Proof List
{- |
SPASS Proof List
-}
data SPProofList =
SPProofList {proofType :: Maybe SPProofType,
plAssocList :: Maybe SPAssocList,
step :: [SPProofStep]}
deriving (Eq, Ord, Show)
type SPProofType = SPIdentifier
data SPProofStep = SPProofStep { reference :: SPReference,
result :: SPResult,
ruleAppl :: SPRuleAppl,
parentList :: [SPParent],
stepAssocList :: Maybe SPAssocList}
deriving (Eq, Ord, Show)
data SPReference = PRefTerm SPTerm | PRefId SPIdentifier | PRefUser Integer
deriving (Eq, Ord, Show)
data SPResult = PResTerm SPTerm | PResUser NSPClause
deriving (Eq, Ord, Show)
data SPRuleAppl = PRuleTerm SPTerm
| PRuleId SPIdentifier
| PRuleUser SPUserRuleAppl
deriving (Eq, Ord, Show)
data SPUserRuleAppl = GeR | SpL | SpR | EqF | Rew | Obv | EmS | SoR | EqR
| Mpm | SPm | OPm | SHy | OHy | URR | Fac | Spt | Inp
| Con | RRE | SSi | ClR | UnC | Ter
deriving (Eq, Ord, Show)
data SPParent = PParTerm SPTerm | PParId SPIdentifier | PParUser Integer
deriving (Eq, Ord, Show)
type SPAssocList = Map.Map SPKey SPValue
data SPKey = PKeyTerm SPTerm | PKeyId SPIdentifier
deriving (Eq, Ord, Show)
data SPValue = PValTerm SPTerm | PValId SPIdentifier | PValUser Integer
deriving (Eq, Ord, Show)
-- *** 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.
-}
type SPFormula = Named SPTerm
-- ** helpers for generating SoftFOL formulas
typedVarTerm :: SPIdentifier -- ^ Variable symbol: v
-> SPIdentifier -- ^ Sort symbol: s
-> SPTerm -- ^ Term: s(v)
typedVarTerm spVar spSort = compTerm (spSym spSort) [simpTerm (spSym spVar)]
spTerms :: [SPIdentifier] -> [SPTerm]
spTerms = map (simpTerm . spSym)
spSym :: SPIdentifier -> SPSymbol
spSym = SPCustomSymbol
compTerm :: SPSymbol -> [SPTerm] -> SPTerm
compTerm = SPComplexTerm
simpTerm :: SPSymbol -> SPTerm
simpTerm = SPSimpleTerm
mkConj :: SPTerm -> SPTerm -> SPTerm
mkConj t1 t2 = compTerm SPAnd [t1,t2]
mkDisj :: SPTerm -> SPTerm -> SPTerm
mkDisj t1 t2 = compTerm SPOr [t1,t2]
mkEq :: SPTerm -> SPTerm -> SPTerm
mkEq t1 t2 = compTerm SPEqual [t1,t2]
-- ** SPASS Desciptions
{- |
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.
-}
data SPDescription =
SPDescription { name :: String,
author :: String,
version :: Maybe String,
logic :: Maybe String,
status :: SPLogState,
desc :: String,
date :: Maybe String}
deriving (Eq, Ord, Show)
{- |
The state of a SPASS problem can be satisfiable, unsatisfiable, or unknown.
-}
data SPLogState =
SPStateSatisfiable
| SPStateUnsatisfiable
| SPStateUnknown
deriving (Eq, Ord, Show)
-- ** SPASS Settings
{- |
We only support one of the three types mentioned here:
data SPSetting = SPFlag String String
| SPClauseRelation [SPCRBIND]
deriving (Eq,Ord,Show)
-}
{- |
New impelmentation of Settings. See spass input syntax Version 1.5.
-}
data SPSetting = SPGeneralSettings {entries :: [SPHypothesis]}
| SPSettings {settingName :: SPSettingLabel,
settingBody :: [SPSettingBody]}
deriving (Eq,Ord,Show)
data SPSettingBody = SPClauseRelation [SPCRBIND] -- clauseFormulaRelation
| SPFlag SPIdentifier [String] -- set_pred(x,y,...)
deriving (Eq,Ord,Show)
data SPHypothesis = SPHypothesis [SPIdentifier]
deriving (Eq,Ord,Show)
data SPSettingLabel = KIV | LEM | OTTER | PROTEIN | SATURATE
| ThreeTAP | SETHEO | SPASS
deriving (Eq,Ord,Show)
{- |
A Tupel of the Clause Relation
-}
data SPCRBIND = SPCRBIND {clauseSPR::String, formulaSPR::String}
deriving (Eq,Ord,Show)
-- ** SoftFOL proof tree
{- |
Datatype for storing of the proof tree. The Show class is instantiated.
-}
data ATP_ProofTree = ATP_ProofTree String
deriving (Eq, Ord)
instance Show ATP_ProofTree where
show (ATP_ProofTree st) = st