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