d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederModule : $Header$

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederDescription : To be replaced by SoftFOL.Sign

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederCopyright : (c) Immanuel Normann, Uni Bremen 2007

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederLicense : GPLv2 or higher

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederMaintainer : inormann@jacobs-university.de

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedermodule Search.SPASS.Sign where

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertype SPIdentifier = String

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdata SPProblem =

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SPProblem { identifier :: SPIdentifier,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder description :: SPDescription,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder logicalPart :: SPLogicalPart,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder settings :: [SPSetting]

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder }

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder deriving (Eq, Ord, Show)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- ** SPASS Logical Parts

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder A SPASS logical part consists of a symbol list, a declaration list, and a

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder set of formula lists. Support for clause lists and proof lists hasn't

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder been implemented yet.

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdata SPLogicalPart =

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SPLogicalPart { symbolList :: Maybe SPSymbolList,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder declarationList :: [SPDeclaration],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder formulaLists :: [SPFormulaList] --,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- clauseLists :: [SPClauseList],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- proofLists :: [SPProofList]

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder }

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder deriving (Eq, Ord, Show)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- *** Symbol Lists

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder All non-predefined signature symbols must be declared as part of a SPASS

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder symbol list.

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdata SPSymbolList =

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SPSymbolList { functions :: [SPSignSym],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder predicates :: [SPSignSym],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder sorts :: [SPSignSym],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder operators :: [SPSignSym],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder quantifiers :: [SPSignSym] }

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder deriving (Eq, Ord, Show)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Creates an empty SPASS Symbol List.

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederemptySymbolList :: SPSymbolList

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederemptySymbolList =

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SPSymbolList { functions = [],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder predicates = [],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder sorts = [],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder operators = [],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder quantifiers = [] }

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder A common data type used for all signature symbols.

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdata SPSignSym =

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SPSignSym { sym :: SPIdentifier,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder arity :: Int }

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder | SPSimpleSignSym SPIdentifier

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder deriving (Eq, Ord, Show)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- *** Declarations

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SPASS Declarations allow the introduction of sorts.

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdata SPDeclaration =

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SPSubsortDecl { sortSymA :: SPIdentifier,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder sortSymB :: SPIdentifier }

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder | SPTermDecl { termDeclTermList :: [SPTerm],

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder termDeclTerm :: SPTerm }

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder | SPSimpleTermDecl SPTerm

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder | SPPredDecl { predSym :: SPIdentifier,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder sortSyms :: [SPIdentifier] }

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder | SPGenDecl { sortSym :: SPIdentifier,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder freelyGenerated :: Bool,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder funcList :: [SPIdentifier]}

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder deriving (Eq, Ord, Show)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- *** Formula List

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SPASS Formula List

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdata SPFormulaList =

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SPFormulaList { originType :: SPOriginType,

formulae :: [SPFormula] }

deriving (Eq, Ord, Show)

{- |

There are axiom formulae and conjecture formulae.

-}

data SPOriginType =

SPOriginAxioms

| SPOriginConjectures

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.

-}

data Named s = NamedSen

{ senName :: String

, isAxiom :: Bool

, isDef :: Bool

, sentence :: s } deriving (Eq, Ord, Show)

type SPFormula = Named SPTerm

{- |

A SPASS Term.

-}

data SPTerm =

SPQuantTerm { quantSym :: SPQuantSym,

variableList :: [SPTerm],

qFormula :: SPTerm }

| SPSimpleTerm SPSymbol

| SPComplexTerm { symbol :: SPSymbol,

arguments :: [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

| SPXor -- eigene Erweiterung

| SPCustomSymbol SPIdentifier

deriving (Eq, Ord, Show)

-- ** 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:

<http://spass.mpi-sb.mpg.de/webspass/help/options.html>

-}

data SPSetting = SPFlag String String

deriving (Eq,Ord,Show)

-- ** SoftFOL proof tree

{- |

Datatype for storing of the proof tree. The Show class is instantiated.

-}

data ProofTree = ProofTree String

deriving (Eq, Ord)

instance Show ProofTree where

show (ProofTree st) = st