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