{- |

Module : $Header$

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")]}

]}}