content: {- |
  Module      :  ./SoftFOL/tests/Sokrates.hs
  Copyright   :  (c) Rene Wagner, Uni Bremen 2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  rwagner@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  unknown
  
  The Sokrates example from the SPASS tutorial at
  <http://spass.mpi-sb.mpg.de/tutorial/> as a Haskell data structure.
  -}
  
  import SoftFOL.Sign
  import SoftFOL.Print ()
  import Common.DocUtils
  import Common.AS_Annotation
  import Common.Id
  
  main :: IO ()
  main = putStrLn $ showDoc sokratesProblem ""
  
  sokratesProblem :: SPProblem
  sokratesProblem = SPProblem
    { identifier = "Sokrates1",
      description = sokratesDescription,
      logicalPart = sokratesLogicalPart,
      settings = [] }
  
  sokratesDescription :: SPDescription
  sokratesDescription = SPDescription
    { name = "Sokrates",
      author = "Christoph Weidenbach",
      version = Nothing,
      logic = Nothing,
      status = SPStateUnsatisfiable,
      desc =
      "Sokrates is mortal and since all humans are mortal, he is mortal too.",
      date = Nothing }
  
  sokratesLogicalPart :: SPLogicalPart
  sokratesLogicalPart = emptySPLogicalPart
    { symbolList = Just sokratesSymbolList,
      formulaLists = [sokratesAxiomFormulae, sokratesConjectureFormulae] }
  
  sokratesSymbolList :: SPSymbolList
  sokratesSymbolList = SPSymbolList
    { functions = [SPSignSym {sym = mkSimpleId "sokrates", arity = 0}],
      predicates = [SPSignSym {sym = mkSimpleId "Human", arity = 1}
                   , SPSignSym {sym = mkSimpleId "Mortal", arity = 1}],
      sorts = [] }
  
  sokratesAxiomFormulae :: SPFormulaList
  sokratesAxiomFormulae = SPFormulaList {originType = SPOriginAxioms,
                                         formulae = [f1, f2] }
    where
      f1 = makeNamed "f1" $ compTerm (mkSPCustomSymbol "Human")
           [ simpTerm $ mkSPCustomSymbol "sokrates"]
      f2 = makeNamed "f2" SPQuantTerm
           {quantSym = SPForall,
            variableList = [simpTerm (mkSPCustomSymbol "x")],
            qFormula = compTerm SPImplies
                   [ compTerm (mkS1PCustomSymbol "Human")
                     [simpTerm $ mkSPCustomSymbol "x"]
                   , compTerm (mkSPCustomSymbol "Mortal")
                     [simpTerm $ mkSPCustomSymbol "x"]]}
  
  sokratesConjectureFormulae :: SPFormulaList
  sokratesConjectureFormulae = SPFormulaList
    { originType = SPOriginConjectures,
      formulae = [f3 {isAxiom = False} ] }
    where
      f3 = makeNamed "f3" $ compTerm (mkSPCustomSymbol "Mortal")
           [simpTerm $ mkSPCustomSymbol "sokrates"]
  