PrintTPTPTests.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
{- |
Module : ./SoftFOL/tests/PrintTPTPTests.hs
Copyright : (c) C. Maeder, DFKI GmbH 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : experimental
Portability : portable
-}
module Main where
import SoftFOL.Sign
import SoftFOL.PrintTPTP
import Common.AS_Annotation
import Common.Id
-- | a more pretty alternative for shows using PrintTPTP
showPretty2 :: PrintTPTP a => a -> ShowS
showPretty2 = shows . printTPTP
main :: IO ()
main = do
putStrLn "--- Term-Tests ---"
putStrLn $ showPretty2 spSimpleTermTest1 "\n"
putStrLn $ showPretty2 spQuantTermTest1 "\n"
putStrLn $ showPretty2 spQuantTermTest2 "\n"
putStrLn $ showPretty2 spQuantTermTest3 "\n"
putStrLn $ showPretty2 spQuantTermTest4 "\n"
putStrLn $ showPretty2 spQuantTermTest5 "\n"
putStrLn "--- Formula-Test ---"
print $ printFormula SPOriginAxioms spFormulaTest
putStrLn "\n"
putStrLn "--- FormulaList-Tests ---"
putStrLn $ showPretty2 spFormulaListTest1 "\n"
putStrLn $ showPretty2 spFormulaListTest2 "\n"
putStrLn $ showPretty2 spFormulaListTest3 "\n"
putStrLn $ showPretty2 spFormulaListTest4 "\n"
putStrLn "--- Description-Tests ---"
putStrLn $ showPretty2 spDescTest1 "\n"
putStrLn $ showPretty2 spDescTest2 "\n"
putStrLn "--- Problem-Test ---"
putStrLn $ showPretty2 spProblemTest "\n"
putStrLn "--- Declaration-Test ---"
putStrLn $ showPretty2 spDeclTest "\n"
spSimpleTermTest1 :: SPSymbol
spSimpleTermTest1 = mkSPCustomSymbol "testsymbol"
spQuantTermTest1 :: SPTerm
spQuantTermTest1 = SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "a")], qFormula = SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}}
spQuantTermTest2 :: SPTerm
spQuantTermTest2 = SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b")], qFormula = SPComplexTerm {symbol = SPEqual, arguments = [
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "a")]},
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "b")]}
]}}
spQuantTermTest3 :: SPTerm
spQuantTermTest3 = SPQuantTerm {quantSym = SPExists, variableList = [SPComplexTerm {symbol = mkSPCustomSymbol "Klein", arguments = [simpTerm (mkSPCustomSymbol "pi")]}, SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "y")]}],
qFormula = SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "pi"), simpTerm (mkSPCustomSymbol "y")]}}
spQuantTermTest4 :: SPTerm
spQuantTermTest4 = SPQuantTerm {quantSym = SPForall, variableList = [
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "y")]},
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]}
],
qFormula = SPComplexTerm {symbol = SPOr, arguments = [
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "y")]},
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]}
]}}
spQuantTermTest5 :: SPTerm
spQuantTermTest5 = SPQuantTerm {quantSym = SPCustomQuantSym $ mkSimpleId "T", variableList = [
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "y")]},
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]},
SPComplexTerm {symbol = SPNot, arguments = [simpTerm (mkSPCustomSymbol "blue")]}
],
qFormula =
SPComplexTerm {symbol = SPEqual, arguments = [
SPComplexTerm {symbol = SPOr, arguments = [
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "y")]},
SPComplexTerm {symbol = SPNot, arguments = [simpTerm (mkSPCustomSymbol "blue")]}
]},
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]}
]}}
toTestFormula :: SPTerm -> SPFormula
toTestFormula = makeNamed "testFormula"
spFormulaTest :: SPFormula
spFormulaTest = toTestFormula SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}
spFormulaListTest1 :: SPFormulaList
spFormulaListTest1 = SPFormulaList {originType = SPOriginAxioms, formulae = [toTestFormula SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}]}
spFormulaListTest2 :: SPFormulaList
spFormulaListTest2 = SPFormulaList {originType = SPOriginConjectures, formulae = [toTestFormula SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}]}
spFormulaListTest3 :: SPFormulaList
spFormulaListTest3 = SPFormulaList {originType = SPOriginAxioms, formulae = [toTestFormula SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}, toTestFormula SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}]}
spFormulaListTest4 :: SPFormulaList
spFormulaListTest4 = SPFormulaList {originType = SPOriginConjectures, formulae = [toTestFormula SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}, toTestFormula SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}]}
spDescTest1 :: SPDescription
spDescTest1 = SPDescription {name = "testdesc", author = "testauthor", version = Nothing, logic = Nothing, status = SPStateUnknown, desc = "Just a test.", date = Nothing}
spDescTest2 :: SPDescription
spDescTest2 = SPDescription {name = "testdesc", author = "testauthor", version = Just "0.1", logic = Just "logic description", status = SPStateUnknown, desc = "Just a test.", date = Just "today"}
spProblemTest :: SPProblem
spProblemTest = SPProblem {identifier = "testproblem", description = descr, logicalPart = logical_part, settings = []}
where
descr = SPDescription {name = "testdesc", author = "testauthor", version = Nothing, logic = Nothing, status = SPStateUnknown, desc = "Just a test.", date = Nothing}
logical_part = emptySPLogicalPart {
declarationList = Just [spDeclTest, spDeclTest2],
formulaLists = [SPFormulaList {originType = SPOriginAxioms, formulae = [toTestFormula SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}]}, SPFormulaList {originType = SPOriginConjectures, formulae = [toTestFormula SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}, toTestFormula SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}]}]}
spDeclTest :: SPDeclaration
spDeclTest = SPSubsortDecl
{ sortSymA = mkSimpleId "sortSymA"
, sortSymB = mkSimpleId "sortSymB" }
spDeclTest2 :: SPDeclaration
spDeclTest2 = SPTermDecl {termDeclTermList = [
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "y")]},
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]}
],
termDeclTerm = SPComplexTerm {symbol = SPOr, arguments = [
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "y")]},
SPComplexTerm {symbol = mkSPCustomSymbol "Elem", arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]}
]}}