PrintTPTPTests.hs revision 127a36cba0c92b465681ec55ad366aca423735eb
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) C. Maeder, DFKI GmbH 2010
81ec673ac5ab1493568d9ef7798b752ab8ee0e61Felix Gabriel ManceLicense : GPLv2 or higher, see LICENSE.txt
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceMaintainer : Christian.Maeder@dfki.de
80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskiStability : experimental
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancePortability : portable
aa0ca44e856c87db27e61687cbb630f270976da1Felix Gabriel Mancemodule Main where
090c663fcc1593c66f39a0972326799a672760d5Christian Maeder-- | a more pretty alternative for shows using PrintTPTP
80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskishowPretty2 :: PrintTPTP a => a -> ShowS
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian MaedershowPretty2 = shows . printTPTP
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance putStrLn "--- Term-Tests ---"
b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder putStrLn $ showPretty2 spSimpleTermTest1 "\n"
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder putStrLn $ showPretty2 spQuantTermTest1 "\n"
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance putStrLn $ showPretty2 spQuantTermTest2 "\n"
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance putStrLn $ showPretty2 spQuantTermTest3 "\n"
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance putStrLn $ showPretty2 spQuantTermTest4 "\n"
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder putStrLn $ showPretty2 spQuantTermTest5 "\n"
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance putStrLn "--- Formula-Test ---"
1b1144abf7f95a4b23405b8d5604813cfe7b036aFelix Gabriel Mance print $ printFormula SPOriginAxioms spFormulaTest
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski putStrLn "\n"
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance putStrLn "--- FormulaList-Tests ---"
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance putStrLn $ showPretty2 spFormulaListTest1 "\n"
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance putStrLn $ showPretty2 spFormulaListTest2 "\n"
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance putStrLn $ showPretty2 spFormulaListTest3 "\n"
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance putStrLn $ showPretty2 spFormulaListTest4 "\n"
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance putStrLn "--- Description-Tests ---"
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance putStrLn $ showPretty2 spDescTest1 "\n"
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance putStrLn $ showPretty2 spDescTest2 "\n"
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance putStrLn "--- Problem-Test ---"
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance putStrLn $ showPretty2 spProblemTest "\n"
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance putStrLn "--- Declaration-Test ---"
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance putStrLn $ showPretty2 spDeclTest "\n"
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancespSimpleTermTest1 :: SPSymbol
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancespSimpleTermTest1 = mkSPCustomSymbol "testsymbol"
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancespQuantTermTest1 :: SPTerm
9cb6af1a7632f12b60f592ce5eb2ac51e6bd33bbFelix Gabriel MancespQuantTermTest1 = SPQuantTerm {quantSym= SPForall, variableList= [simpTerm (mkSPCustomSymbol "a")], qFormula= SPComplexTerm {symbol= SPEqual, arguments= [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespQuantTermTest2 :: SPTerm
1a38107941725211e7c3f051f7a8f5e12199f03acmaederspQuantTermTest2 = SPQuantTerm {quantSym= SPForall, variableList= [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b")], qFormula= SPComplexTerm {symbol= SPEqual, arguments= [
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "a")]},
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "b")]}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespQuantTermTest3 :: SPTerm
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespQuantTermTest3 = SPQuantTerm {quantSym= SPExists, variableList= [SPComplexTerm {symbol=mkSPCustomSymbol "Klein", arguments=[simpTerm (mkSPCustomSymbol "pi")]}, SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "y")]}],
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceqFormula= SPComplexTerm {symbol= SPEqual, arguments= [simpTerm (mkSPCustomSymbol "pi"), simpTerm (mkSPCustomSymbol "y")]}}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespQuantTermTest4 :: SPTerm
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespQuantTermTest4 = SPQuantTerm {quantSym= SPForall, variableList= [
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "y")]},
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceqFormula= SPComplexTerm {symbol= SPOr, arguments= [
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "y")]},
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]}
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancespQuantTermTest5 :: SPTerm
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancespQuantTermTest5 = SPQuantTerm {quantSym= SPCustomQuantSym $ mkSimpleId "T", variableList = [
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "y")]},
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]},
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance SPComplexTerm {symbol=SPNot, arguments=[simpTerm (mkSPCustomSymbol "blue")]}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceSPComplexTerm {symbol=SPEqual, arguments=[
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance SPComplexTerm {symbol= SPOr, arguments=[
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "y")]},
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance SPComplexTerm {symbol=SPNot, arguments=[simpTerm (mkSPCustomSymbol "blue")]}
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancetoTestFormula :: SPTerm -> SPFormula
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancetoTestFormula = makeNamed "testFormula"
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespFormulaTest :: SPFormula
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespFormulaTest = toTestFormula SPComplexTerm {symbol= SPEqual, arguments= [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespFormulaListTest1 :: SPFormulaList
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespFormulaListTest1 = SPFormulaList {originType= SPOriginAxioms, formulae= [toTestFormula SPComplexTerm {symbol= SPEqual, arguments= [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}]}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespFormulaListTest2 :: SPFormulaList
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespFormulaListTest2 = SPFormulaList {originType= SPOriginConjectures, formulae= [toTestFormula SPComplexTerm {symbol= SPEqual, arguments= [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}]}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespFormulaListTest3 :: SPFormulaList
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel MancespFormulaListTest3 = 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")]}]}
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancespFormulaListTest4 :: SPFormulaList
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancespFormulaListTest4 = 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")]}]}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespDescTest1 :: SPDescription
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespDescTest1 = SPDescription {name="testdesc", author="testauthor", version=Nothing, logic=Nothing, status=SPStateUnknown, desc="Just a test.", date=Nothing}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespDescTest2 :: SPDescription
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancespDescTest2 = SPDescription {name="testdesc", author="testauthor", version=Just "0.1", logic=Just "logic description", status=SPStateUnknown, desc="Just a test.", date=Just "today"}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespProblemTest :: SPProblem
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespProblemTest = SPProblem {identifier= "testproblem", description= descr, logicalPart= logical_part, settings= []}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance descr = SPDescription {name="testdesc", author="testauthor", version=Nothing, logic=Nothing, status=SPStateUnknown, desc="Just a test.", date=Nothing}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance logical_part = emptySPLogicalPart {
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance declarationList= Just [spDeclTest, spDeclTest2],
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance 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")]}]}]}
1a38107941725211e7c3f051f7a8f5e12199f03acmaederspDeclTest :: SPDeclaration
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancespDeclTest = SPSubsortDecl
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance { sortSymA = mkSimpleId "sortSymA"
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , sortSymB = mkSimpleId "sortSymB" }
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancespDeclTest2 :: SPDeclaration
1a38107941725211e7c3f051f7a8f5e12199f03acmaederspDeclTest2 = SPTermDecl {termDeclTermList = [
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "y")]},
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancetermDeclTerm= SPComplexTerm {symbol= SPOr, arguments= [
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "y")]},
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance SPComplexTerm {symbol=mkSPCustomSymbol "Elem", arguments=[simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b"), simpTerm (mkSPCustomSymbol "c")]}