{- |

Module : $EmptyHeader$

Description : <optional short description entry>

Copyright : (c) <Authors or Affiliations>

License : GPLv2 or higher

Maintainer : <email>

Stability : unstable | experimental | provisional | stable | frozen

Portability : portable | non-portable (<reason>)

<optional description>

-}

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" ++ descr_expected ++ "\n" ++ logical_part_expected ++ "\nend_problem."

descr_expected = "list_of_descriptions.\nname({* testdesc *}).\nauthor({* testauthor *}).\nstatus(unknown).\ndescription({* Just a test. *}).\nend_of_list."

logical_part_expected = "list_of_symbols.\nfunctions[(foo,1),\n"++ (replicate (length "functions[") ' ') ++ "bar].\nend_of_list.\nlist_of_declarations.\nsubsort(a,b).\nsort a generated by [genA].\nend_of_list.\nlist_of_formulae(axioms).\nformula(equal(a,a),testformula).\nend_of_list.\nlist_of_formulae(conjectures).\nformula(equal(a,a),testformula).\nformula(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),\n"++ (replicate (length "functions[") ' ') ++ "bar].\nend_of_list.\nlist_of_declarations.\nsubsort(a,b).\nsort a generated by [genA].\nend_of_list.\nlist_of_formulae(axioms).\nformula(equal(a,a),testformula).\nend_of_list.\nlist_of_formulae(conjectures).\nformula(equal(a,a),testformula).\nformula(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),\n"++ (replicate (length "functions[") ' ') ++ "bar].\nend_of_list.") (showDoc (SPSymbolList {functions= syms, predicates= [], sorts= []}) ""))),

TestLabel "sym_list_predicates" (TestCase (assertEqual "" ("list_of_symbols.\npredicates[(foo,1),\n"++ (replicate (length "predicates[") ' ') ++ "bar].\nend_of_list.") (showDoc (SPSymbolList {functions= [], predicates= syms, sorts= []}) ""))),

TestLabel "sym_list_sorts" (TestCase (assertEqual "" ("list_of_symbols.\nsorts[(foo,1),\n"++ (replicate (length "sorts[") ' ') ++ "bar].\nend_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).\nformula(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).\nformula(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).\nformula(equal(a,a),testformula).\nformula(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).\nformula(equal(a,a),testformula).\nformula(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 *}).\nauthor({* testauthor *}).\nstatus(unknown).\ndescription({* 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 *}).\nauthor({* testauthor *}).\nversion({* 0.1 *}).\nlogic({* logic description *}).\nstatus(unknown).\ndescription({* Just a test. *}).\ndate({* today *}).\nend_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 ()