{- |

Module : $Header$

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