{- |
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 ()
