content: {- |
  Module      :  ./SoftFOL/tests/PrintTests.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 Test.HUnit
  import SoftFOL.Sign
  import SoftFOL.Print
  
  import Common.AS_Annotation
  import Common.DocUtils
  import Common.Id
  
  toTestFormula :: SPTerm -> SPFormula
  toTestFormula = makeNamed "testformula"
  
  printProblemTest = TestList [
    TestLabel "problem" (TestCase (assertEqual "" expected actual))
    ]
    where
      expected = "begin_problem(testproblem).\n\n" ++ descr_expected ++ "\n\n" ++
                logical_part_expected ++ "\n\nend_problem."
      descr_expected = "list_of_descriptions.\nname({* testdesc *}).\n" ++
                      "author({* testauthor *}).\nstatus(unknown).\n" ++
                      "description({* Just a test. *}).\nend_of_list."
      logical_part_expected = "list_of_symbols.\nfunctions[(foo, 1), bar].\n" ++
                             "end_of_list.\n\nlist_of_declarations.\n" ++
                             "subsort(a, b).\nsort a generated by [genA].\n" ++
                             "end_of_list.\n\nlist_of_formulae(axioms).\n" ++
                             "formula(equal(a, a), testformula).\n" ++
                             "end_of_list.\nlist_of_formulae(conjectures).\n" ++
                             "formula(equal(a, a), testformula).\n" ++
                             "formula(equal(a, a), testformula).\nend_of_list."
      actual = showDoc SPProblem {identifier = "testproblem", description = descr,
                                  logicalPart = logical_part, settings = []} ""
      descr = SPDescription {name = "testdesc", author = "testauthor",
                             version = Nothing, logic = Nothing,
                             status = SPStateUnknown, desc = "Just a test.",
                             date = Nothing}
      logical_part = emptySPLogicalPart {symbolList = Just SPSymbolList
                      {functions = syms, predicates = [], sorts = []},
                       declarationList = Just [
                        SPSubsortDecl {sortSymA = mkSimpleId "a",
                                       sortSymB = mkSimpleId "b"},
                        SPGenDecl {sortSym = mkSimpleId "a",
                                   freelyGenerated = False,
                                   funcList = [mkSimpleId "genA"]}],
                       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")]}]}]}
      syms = [SPSignSym {sym = mkSimpleId "foo", arity = 1}
             , SPSimpleSignSym $ mkSimpleId "bar"]
  
  printLogicalPartTest = TestList [
    TestLabel "logical_part" (TestCase (assertEqual "" expected actual))
    ]
    where
      expected = "list_of_symbols.\nfunctions[(foo, 1), bar].\nend_of_list.\n" ++
                 "\nlist_of_declarations.\nsubsort(a, b).\n" ++
                 "sort a generated by [genA].\nend_of_list.\n" ++
                 "\nlist_of_formulae(axioms).\n" ++
                 "formula(equal(a, a), testformula).\nend_of_list.\n" ++
                 "list_of_formulae(conjectures).\n" ++
                 "formula(equal(a, a), testformula).\n" ++
                 "formula(equal(a, a), testformula).\nend_of_list."
      actual = showDoc (emptySPLogicalPart
        {symbolList = Just SPSymbolList {functions = syms, predicates = [],
                                           sorts = []},
         declarationList = Just [SPSubsortDecl {sortSymA = mkSimpleId "a",
                                                sortSymB = mkSimpleId "b"},
                                 SPGenDecl {sortSym = mkSimpleId "a",
                                            freelyGenerated = False,
                                            funcList = [mkSimpleId "genA"]}],
         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")]}]}]}) ""
      syms = [SPSignSym {sym = mkSimpleId "foo", arity = 1}
             , SPSimpleSignSym $ mkSimpleId "bar"]
  
  printSymbolListTest = TestList [
    TestLabel "sym_list_functions"
     (TestCase (assertEqual "" ("list_of_symbols.\nfunctions[(foo, 1), bar].\n" ++
      "end_of_list.") (showDoc SPSymbolList {functions = syms, predicates = [],
                                             sorts = []} ""))),
    TestLabel "sym_list_predicates"
     (TestCase (assertEqual "" ("list_of_symbols.\npredicates[(foo, 1), bar].\n" ++
      "end_of_list.") (showDoc SPSymbolList {functions = [], predicates = syms,
                                             sorts = []} ""))),
    TestLabel "sym_list_sorts"
     (TestCase (assertEqual "" ("list_of_symbols.\nsorts[(foo, 1), bar].\n" ++
      "end_of_list.") (showDoc SPSymbolList {functions = [], predicates = [],
                                             sorts = syms} "")))
    ]
    where
      syms = [SPSignSym {sym = mkSimpleId "foo", arity = 1}
             , SPSimpleSignSym $ mkSimpleId "bar"]
  
  printSignSymTest = TestList [
    TestLabel "sign_sym" (TestCase (assertEqual "" "(a, 1)" (showDoc SPSignSym
      {sym = mkSimpleId "a", arity = 1} ""))),
    TestLabel "simple_sign_sym" (TestCase (assertEqual "" "b"
      (showDoc (SPSimpleSignSym $ mkSimpleId "b") "")))
    ]
  
  printDeclarationTest = TestList [
    TestLabel "subsort_decl" (TestCase (assertEqual "" "subsort(a, b)."
      (showDoc SPSubsortDecl {sortSymA = mkSimpleId "a",
                              sortSymB = mkSimpleId "b"} ""))),
    TestLabel "term_decl" (TestCase (
      assertEqual "" "forall([a, b], implies(a, b))."
      (showDoc SPTermDecl {termDeclTermList = [simpTerm (mkSPCustomSymbol "a"),
        simpTerm (mkSPCustomSymbol "b")], termDeclTerm = SPComplexTerm
         {symbol = SPImplies, arguments = [simpTerm (mkSPCustomSymbol "a"),
          simpTerm (mkSPCustomSymbol "b")]}} ""))),
    TestLabel "simple_term_decl" (TestCase (assertEqual "" "asimpletestterm."
      (showDoc (SPSimpleTermDecl (simpTerm (mkSPCustomSymbol "asimpletestterm"))) ""))),
    TestLabel "pred_decl1" (TestCase (assertEqual "" "predicate(a, b)."
      (showDoc SPPredDecl {predSym = mkSimpleId "a",
                           sortSyms = [mkSimpleId "b"]} ""))),
    TestLabel "pred_decl2" (TestCase (assertEqual "" "predicate(a, b, c)."
      (showDoc SPPredDecl {predSym = mkSimpleId "a",
                           sortSyms = map mkSimpleId ["b", "c"]} ""))),
    TestLabel "gen_decl1" (TestCase (assertEqual "" "sort a generated by [genA]."
      (showDoc SPGenDecl {sortSym = mkSimpleId "a", freelyGenerated = False,
                          funcList = [mkSimpleId "genA"]} ""))),
    TestLabel "gen_decl2" (TestCase (assertEqual ""
      "sort a generated by [genA, genA2]."
      (showDoc SPGenDecl {sortSym = mkSimpleId "a", freelyGenerated = False,
                          funcList = map mkSimpleId ["genA", "genA2"]} ""))),
    TestLabel "gen_decl3" (TestCase (assertEqual ""
      "sort a freely generated by [genA]."
      (showDoc SPGenDecl {sortSym = mkSimpleId "a", freelyGenerated = True,
                          funcList = [mkSimpleId "genA"]} ""))),
    TestLabel "gen_decl4" (TestCase (assertEqual ""
      "sort a freely generated by [genA, genA2]."
      (showDoc SPGenDecl {sortSym = mkSimpleId "a", freelyGenerated = True,
                          funcList = map mkSimpleId ["genA", "genA2"]} ""))),
    TestLabel "gen_decl5" (TestCase (assertEqual ""
      "sort a freely generated by [genA, genA2, genA3]."
      (showDoc SPGenDecl {sortSym = mkSimpleId "a", freelyGenerated = True,
                          funcList = map mkSimpleId ["genA", "genA2", "genA3"]} "")))
    ]
  
  printFormulaListTest = TestList [
    TestLabel "formula_list0" (TestList [
      TestCase (assertEqual "" "list_of_formulae(axioms).\nend_of_list."
        (showDoc SPFormulaList {originType = SPOriginAxioms, formulae = []} "")),
      TestCase (assertEqual "" "list_of_formulae(conjectures).\nend_of_list."
        (showDoc SPFormulaList {originType = SPOriginConjectures,
                                formulae = []} ""))]),
    TestLabel "formula_list1" (TestList [
      TestCase (assertEqual "" ("list_of_formulae(axioms).\n" ++
        "formula(equal(a, a), testformula).\nend_of_list.")
      (showDoc SPFormulaList {originType = SPOriginAxioms,
                              formulae = [toTestFormula SPComplexTerm
                                 {symbol = SPEqual,
                                  arguments = [simpTerm (mkSPCustomSymbol "a"),
                                               simpTerm (mkSPCustomSymbol "a")]}]} "")),
      TestCase (assertEqual "" ("list_of_formulae(conjectures).\n" ++
        "formula(equal(a, a), testformula).\nend_of_list.")
      (showDoc SPFormulaList {originType = SPOriginConjectures,
                              formulae = [toTestFormula SPComplexTerm
                                {symbol = SPEqual,
                                 arguments = [simpTerm (mkSPCustomSymbol "a"),
                                              simpTerm (mkSPCustomSymbol "a")]}]} ""))]),
    TestLabel "formula_list2" (TestList [
      TestCase (assertEqual "" ("list_of_formulae(axioms).\n" ++
        "formula(equal(a, a), testformula).\n" ++
        "formula(equal(a, a), testformula).\nend_of_list.")
      (showDoc 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")]}]} "")),
      TestCase (assertEqual "" ("list_of_formulae(conjectures).\n" ++
        "formula(equal(a, a), testformula).\n" ++
        "formula(equal(a, a), testformula).\nend_of_list.")
      (showDoc SPFormulaList {originType = SPOriginConjectures,
                              formulae = [(toTestFormula SPComplexTerm
                                {symbol = SPEqual,
                                 arguments = [simpTerm (mkSPCustomSymbol "a"),
                                              simpTerm (mkSPCustomSymbol "a")]})
                               {senAttr = "testformula"},
                               toTestFormula SPComplexTerm
                                {symbol = SPEqual,
                                 arguments = [simpTerm (mkSPCustomSymbol "a"),
                                              simpTerm (mkSPCustomSymbol "a")]}]} ""))])
    ]
  
  printFormulaTest = TestList [
    TestLabel "formula" (TestCase (assertEqual "" "formula(equal(a, a), testformula)."
      (show (printFormula (toTestFormula SPComplexTerm {symbol = SPEqual,
        arguments = [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]})))))
    ]
  
  printTermTest = TestList [
    -- empty term list not allowed!
    TestLabel "quant_term1" (TestCase (assertEqual "" "forall([a], equal(a, a))"
     (showDoc SPQuantTerm {quantSym = SPForall, variableList =
      [simpTerm (mkSPCustomSymbol "a")], qFormula = SPComplexTerm
       {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "a"),
                                       simpTerm (mkSPCustomSymbol "a")]}} ""))),
    TestLabel "quant_term2" (TestCase (assertEqual "" "forall([a, a], equal(a, a))"
     (showDoc SPQuantTerm {quantSym = SPForall, variableList =
      [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")],
      qFormula = SPComplexTerm {symbol = SPEqual, arguments =
        [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "a")]}} ""))),
    TestLabel "simple_term" (TestCase (assertEqual "" "testsymbol"
      (showDoc (simpTerm (mkSPCustomSymbol "testsymbol")) ""))),
    -- empty arguments list not allowed!
    TestLabel "complex_term1" (TestCase (assertEqual "" "test(a)"
      (showDoc SPComplexTerm {symbol = mkSPCustomSymbol "test",
        arguments = [simpTerm (mkSPCustomSymbol "a")]} ""))),
    TestLabel "complex_term2" (TestCase (assertEqual "" "implies(a, b)"
      (showDoc SPComplexTerm {symbol = SPImplies, arguments =
        [simpTerm (mkSPCustomSymbol "a"), simpTerm (mkSPCustomSymbol "b")]} "")))]
  
  printQuantSymTest = TestList [
    TestLabel "forall_sym" (TestCase (assertEqual "" "forall" (showDoc SPForall ""))),
    TestLabel "exists_sym" (TestCase (assertEqual "" "exists" (showDoc SPExists ""))),
    TestLabel "custom_sym" (TestCase (assertEqual "" "custom"
      (showDoc (SPCustomQuantSym $ mkSimpleId "custom") "")))]
  
  printSymTest = TestList [
    TestLabel "equal_sym" (TestCase (assertEqual "" "equal" (showDoc SPEqual ""))),
    TestLabel "true_sym" (TestCase (assertEqual "" "true" (showDoc SPTrue ""))),
    TestLabel "false_sym" (TestCase (assertEqual "" "false" (showDoc SPFalse ""))),
    TestLabel "or_sym" (TestCase (assertEqual "" "or" (showDoc SPOr ""))),
    TestLabel "and_sym" (TestCase (assertEqual "" "and" (showDoc SPAnd ""))),
    TestLabel "not_sym" (TestCase (assertEqual "" "not" (showDoc SPNot ""))),
    TestLabel "implies_sym" (TestCase (assertEqual "" "implies" (showDoc SPImplies ""))),
    TestLabel "implied_sym" (TestCase (assertEqual "" "implied" (showDoc SPImplied ""))),
    TestLabel "equiv_sym" (TestCase (assertEqual "" "equiv" (showDoc SPEquiv ""))),
    TestLabel "custom_sym" (TestCase (assertEqual "" "custom" (showDoc (mkSPCustomSymbol "custom") "")))]
  
  printDescriptionTest = TestList [
    TestLabel "description1" (TestCase (assertEqual ""
      ("list_of_descriptions.\nname({* testdesc *}).\n" ++
      "author({* testauthor *}).\nstatus(unknown).\n" ++
      "description({* Just a test. *}).\nend_of_list.")
      (showDoc SPDescription {name = "testdesc", author = "testauthor",
        version = Nothing, logic = Nothing, status = SPStateUnknown,
        desc = "Just a test.", date = Nothing} ""))),
    TestLabel "description2" (TestCase (assertEqual ""
      ("list_of_descriptions.\nname({* testdesc *}).\n" ++
        "author({* testauthor *}).\nversion({* 0.1 *}).\n" ++
        "logic({* logic description *}).\nstatus(unknown).\n" ++
        "description({* Just a test. *}).\ndate({* today *}).\n" ++
        "end_of_list.") (showDoc SPDescription {name = "testdesc",
          author = "testauthor", version = Just "0.1",
          logic = Just "logic description", status = SPStateUnknown,
          desc = "Just a test.", date = Just "today"} "")))
    ]
  
  printLogStateTest = TestList [
    TestLabel "state_satisfiable" (TestCase (assertEqual ""
      "satisfiable" (showDoc SPStateSatisfiable ""))),
    TestLabel "state_unsatisfiable" (TestCase (assertEqual ""
      "unsatisfiable" (showDoc SPStateUnsatisfiable ""))),
    TestLabel "state_unkwown" (TestCase (assertEqual "" "unknown"
      (showDoc SPStateUnknown "")))]
  
  tests = TestList [
    printProblemTest,
    printLogicalPartTest,
    printSymbolListTest,
    printSignSymTest,
    printDeclarationTest,
    printFormulaListTest,
    printFormulaTest,
    printTermTest,
    printQuantSymTest,
    printSymTest,
    printDescriptionTest,
    printLogStateTest]
  
  main :: IO ()
  main = do
    c <- runTestTT tests
    return ()
  