diff --git a/CHANGELOG b/CHANGELOG deleted file mode 100644 --- a/CHANGELOG +++ /dev/null @@ -1,7 +0,0 @@ -0.9 => 1.0 -============= -This package version is updated with a command line utility. - -* Make use of the CarneadesDSL Input and Dung Output modules to provide a - command line interface reading a Carneades Argument Evaluation Structure - and possible give the evaluation result or output in CEGARTIX format. diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,29 @@ +# Changelog + +## 1.0 → 2.0.0.0 + +### Breaking changes + +- **CLI rewritten**: The `caell` executable now uses `optparse-applicative` + instead of `cmdargs`. Command-line flags have changed: + - Use `--cegartix` / `--lax-cegartix` for output format selection + - Use `--extension`, `--correspondence`, `--x-semantics` to select output + +### Improvements + +- Upgraded to `cabal-version: 3.0` format +- Relaxed dependency bounds to build on GHC 9.4+ +- Updated to CarneadesDSL 2.0 and Dung 2.0 +- Added test suite (tasty + HUnit) +- Added GitHub Actions CI for GHC 9.4, 9.6, 9.8, 9.10 +- Fixed all `-Wall` warnings +- Removed dependency on unmaintained `cmdargs` library +- Converted documentation to Markdown + +## 0.9 → 1.0 + +This package version is updated with a command line utility. + +- Make use of the CarneadesDSL Input and Dung Output modules to provide a + command line interface reading a Carneades Argument Evaluation Structure + and possible give the evaluation result or output in CEGARTIX format. diff --git a/CarneadesIntoDung.cabal b/CarneadesIntoDung.cabal --- a/CarneadesIntoDung.cabal +++ b/CarneadesIntoDung.cabal @@ -1,50 +1,88 @@ +cabal-version: 3.0 name: CarneadesIntoDung -category: Argumentation, Embedded, AI -version: 1.0 -license: BSD3 -cabal-version: >= 1.6 +version: 2.0.0.0 +license: BSD-3-Clause license-file: LICENSE author: Bas van Gijzel, Henrik Nilsson -maintainer: Bas van Gijzel +maintainer: Bas van Gijzel +copyright: Copyright (C) 2014-2026 Bas van Gijzel stability: experimental -homepage: http://www.cs.nott.ac.uk/~bmv/CarneadesIntoDung/ -copyright: Copyright (C) 2014 Bas van Gijzel +category: Argumentation, Embedded, AI +homepage: https://github.com/nebasuke/CarneadesIntoDung synopsis: A translation from the Carneades argumentation model into Dung's AFs. -description: A translation from the Carneades argumentation model - () into Dung's - argumentation frameworks (). - This package provides a translation function and correspondence - properties. For the papers accompanying this library see - \"Towards a framework for the implementation and verification of - translations between argumentation models\" and \"A principled - approach to the implementation of argumentation models\", - available at . +description: + A translation from the Carneades argumentation model + () into Dung's + argumentation frameworks (). + This package provides a translation function and correspondence + properties. For the papers accompanying this library see "Towards a + framework for the implementation and verification of translations + between argumentation models" and "A principled approach to the + implementation of argumentation models", available at + . build-type: Simple +tested-with: GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1 -Extra-Source-Files: - CHANGELOG - examplecaes.txt +extra-doc-files: + README.md + CHANGELOG.md -Library - build-depends: - base >= 4 && < 5, - containers >= 0.3 && < 0.6, - fgl >= 5.4.2.4, - cmdargs >= 0.10.2, - CarneadesDSL >= 1.3, - Dung >= 1.0.0.1 - - hs-source-dirs: - src +extra-source-files: + LICENSE + examplecaes.txt + exampleaf.txt +source-repository head + type: git + location: https://github.com/nebasuke/CarneadesIntoDung + +common warnings + ghc-options: + -Wall + -Wcompat + -Widentities + -Wincomplete-record-updates + -Wincomplete-uni-patterns + -Wredundant-constraints + default-language: Haskell2010 + +library + import: warnings + hs-source-dirs: src + build-depends: + base >= 4.16 && < 5, + containers >= 0.6 && < 0.8, + fgl >= 5.7 && < 5.9, + CarneadesDSL >= 2.0 && < 2.1, + Dung >= 2.0 && < 2.1 exposed-modules: Language.CarneadesIntoDung.Translation Language.CarneadesIntoDung.Examples -Executable caell - main-Is: Main.hs - hs-source-dirs: src +executable caell + import: warnings + main-is: Main.hs + hs-source-dirs: app + build-depends: + base >= 4.16 && < 5, + CarneadesIntoDung, + CarneadesDSL >= 2.0 && < 2.1, + Dung >= 2.0 && < 2.1, + optparse-applicative >= 0.17 && < 0.19 + ghc-options: -threaded -source-repository head - Type: git - Location: https://github.com/nebasuke/CarneadesIntoDung +test-suite carneadesintodung-tests + import: warnings + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test + build-depends: + base >= 4.16 && < 5, + CarneadesIntoDung, + CarneadesDSL >= 2.0 && < 2.1, + Dung >= 2.0 && < 2.1, + containers >= 0.6 && < 0.8, + tasty >= 1.4 && < 1.6, + tasty-hunit >= 0.10 && < 0.11 + other-modules: + Test.Language.CarneadesIntoDung.Translation diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c)2014, Bas van Gijzel +Copyright (c) 2014-2026, Bas van Gijzel All rights reserved. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,42 @@ +# CarneadesIntoDung + +A translation from the Carneades argumentation model +([CarneadesDSL](http://hackage.haskell.org/package/CarneadesDSL)) into Dung's +argumentation frameworks ([Dung](http://hackage.haskell.org/package/Dung)). + +This package provides a translation function and correspondence properties +showing that the translation preserves applicability and acceptability. + +For the papers accompanying this library see "Towards a framework for the +implementation and verification of translations between argumentation models" +and "A principled approach to the implementation of argumentation models", +available at . + +## Usage + +```haskell +import Language.CarneadesIntoDung.Translation +import Language.CarneadesIntoDung.Examples + +-- Translate the example CAES into a Dung AF +translate caes + +-- Verify correspondence properties +corApp caes -- True +corAcc caes -- True +``` + +## Executable + +The `caell` executable reads a Carneades Argument Evaluation Structure from a +file and translates it into a Dung argumentation framework: + +``` +caell --filename examplecaes.txt --extension +caell --filename examplecaes.txt --correspondence +caell --filename examplecaes.txt --cegartix --outputfile out.txt +``` + +## License + +BSD-3-Clause. See [LICENSE](LICENSE) for details. diff --git a/Setup.hs b/Setup.hs deleted file mode 100644 --- a/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,108 @@ +-- |This module implements a command-line interface to the implementation of +-- Carneades. CAES + Haskell = caell +{-# LANGUAGE RecordWildCards #-} +module Main + ( main + ) where + +import Language.CarneadesIntoDung.Translation +import Language.Carneades.CarneadesDSL (CAES(..), getAllArgs, applicable, + getProps, acceptable) +import Language.Carneades.Input +import Language.Dung.AF (groundedExt) +import Language.Dung.Output + +import Options.Applicative +import System.Exit +import Control.Monad (when) + +data Options = Options + { optCegartix :: Bool + , optLaxCegartix :: Bool + , optFileName :: FilePath + , optOutputFile :: Maybe FilePath + , optCorrespondence :: Bool + , optExtension :: Bool + , optXSemantics :: Bool + } deriving (Show) + +optionsParser :: Parser Options +optionsParser = Options + <$> switch + ( long "cegartix" + <> help "Output in strict CEGARTIX/PrefSat format (standard)" + ) + <*> switch + ( long "lax-cegartix" + <> help "Output in lax CEGARTIX/PrefSat format (+parentheses)" + ) + <*> strOption + ( long "filename" + <> metavar "FILE" + <> help "Name of the file to be read" + ) + <*> optional (strOption + ( long "outputfile" + <> metavar "FILE" + <> help "Name of the file to be written" + )) + <*> switch + ( long "correspondence" + <> help "Display satisfaction of correspondence result" + ) + <*> switch + ( long "extension" + <> help "Output unique complete extension for the translated CAES" + ) + <*> switch + ( long "x-semantics" + <> help "Output evaluation of the original Carneades semantics" + ) + +opts :: ParserInfo Options +opts = info (optionsParser <**> helper) + ( fullDesc + <> progDesc "An implementation of Carneades in Haskell" + <> header "caell - Carneades + Haskell argumentation tool" + ) + +main :: IO () +main = do + options@Options{..} <- execParser opts + input <- readFile optFileName + caes <- case parseCAES input of + Left err -> do + putStrLn "Parsing error: " + print err + exitWith (ExitFailure 1) + Right c -> return c + exec options caes + +-- |Execute supplied options +exec :: Options -> CAES -> IO () +exec Options{..} caes@(CAES (argSet, (assumptions, _), _)) = do + let args = getAllArgs argSet + let transCaes = translate caes + putStrLn $ "Argument set: " ++ show args + when optXSemantics $ do + putStrLn "Evaluation under original semantics:" + putStrLn "Applicable arguments:" + print (filter (`applicable` caes) args) + putStrLn "Acceptable propositions:" + print (filter (\p -> p `acceptable` caes + || p `elem` assumptions) + (getProps argSet)) + when optExtension $ + putStrLn "Extension after translation: " + >> print (groundedExt transCaes) + when optCorrespondence $ + putStrLn ("Correspondence of applicability is: " ++ show (corApp caes)) + >> putStrLn ("Correspondence of acceptability is: " ++ show (corAcc caes)) + let useStrict = optCegartix && not optLaxCegartix + case optOutputFile of + Nothing -> return () + Just fp -> do + if useStrict + then writeFile fp (toStrictCegartix transCaes) + else writeFile fp (toCegartix transCaes) + putStrLn "File outputted." diff --git a/exampleaf.txt b/exampleaf.txt new file mode 100644 --- /dev/null +++ b/exampleaf.txt @@ -0,0 +1,15 @@ +arg(a). +arg(b). +arg(c). +arg(d). +arg(e). +arg(f). +arg(g). +att(a,b). +att(c,b). +att(c,d). +att(d,c). +att(d,e). +att(e,g). +att(f,e). +att(g,f). diff --git a/examplecaes.txt b/examplecaes.txt --- a/examplecaes.txt +++ b/examplecaes.txt @@ -1,25 +1,25 @@ -argument arg1 ["kill", "intent"] [ ] "murder" -argument arg2 ["witness"] ["unreliable"] "intent" -argument arg3 ["witness2"] ["unreliable2"] "-intent" - -weight arg1 0.8 -weight arg2 0.3 -weight arg3 0.8 - -assumptions ["kill", "witness", "witness2", "unreliable2"] - - --- Comments are allowed --- also valid: standard "intent" BeyondReasonableDoubt --- Propositions either as string literals or plain identifiers -standard "kill" scintilla -standard "intent" beyond_reasonable_doubt -standard "-intent" scintilla -standard murder scintilla -standard "-murder" scintilla -standard "unreliable" scintilla -standard "unreliable2" scintilla -standard witness scintilla -standard witness2 scintilla - - +argument arg1 ["kill", "intent"] [ ] "murder" +argument arg2 ["witness"] ["unreliable"] "intent" +argument arg3 ["witness2"] ["unreliable2"] "-intent" + +weight arg1 0.8 +weight arg2 0.3 +weight arg3 0.8 + +assumptions ["kill", "witness", "witness2", "unreliable2"] + + +-- Comments are allowed +-- also valid: standard "intent" BeyondReasonableDoubt +-- Propositions either as string literals or plain identifiers +standard "kill" scintilla +standard "intent" beyond_reasonable_doubt +standard "-intent" scintilla +standard murder scintilla +standard "-murder" scintilla +standard "unreliable" scintilla +standard "unreliable2" scintilla +standard witness scintilla +standard witness2 scintilla + + diff --git a/src/Language/CarneadesIntoDung/Examples.hs b/src/Language/CarneadesIntoDung/Examples.hs --- a/src/Language/CarneadesIntoDung/Examples.hs +++ b/src/Language/CarneadesIntoDung/Examples.hs @@ -1,107 +1,106 @@ --- | This is the examples module accompanying the implementation of the --- translation from the Carneades argumentation model into Dung's --- argumentation frameworks. --- --- This module contains a collection of examples, showing how to translate --- an existing Carneades Argument Evaluation Structure (CAES) into an argumentation --- framework. --- --- To run these examples, or your own: start GHCi and do the following: --- --- @\:l Language.CarneadesIntoDung.Examples@ --- - -module Language.CarneadesIntoDung.Examples - ( - -- *Example translation - -- |We use the example CAES as defined in "Language.Carneades.ExampleCAES". - caes, - exTrans, exTrans', - -- *Correspondence properties - corProp, - ) - where -import Language.CarneadesIntoDung.Translation -import Language.Dung.AF -import Language.Carneades.CarneadesDSL -import Language.Carneades.ExampleCAES - --- |Translation of the example CAES 'caes'. --- The following is the prettified output of the translation, where --- the five propositions in the middle are the assumptions and 'defeater'. --- --- >>> translate caes --- AF [ --- Left (True,"murder"), --- Left (False,"murder"), --- Right ["kill","intent"] ~[]=>"murder", --- Left (False,"intent"), --- Left (True,"intent"), --- Right ["witness2"] ~["unreliable2"]=>"-intent", --- Right ["witness"] ~["unreliable"]=>"intent", --- Left (True,"unreliable"), --- Left (False,"unreliable") --- , --- Left (True,"defeater"), --- Left (True,"kill"), --- Left (True,"witness"), --- Left (True,"witness2"), --- Left (True,"unreliable2")] --- [ --- (Left (True,"defeater"), Left (True,"murder")), --- (Left (True,"defeater"), Left (False,"murder")), --- (Left (True,"defeater"), Right ["kill","intent"] ~[]=>"murder"), --- (Left (True,"defeater"), Left (False,"intent")), --- (Left (True,"defeater"),Left (True,"intent")), --- (Left (True,"unreliable2"),Right ["witness2"] ~["unreliable2"]=>"-intent"), --- (Left (True,"defeater"),Left (True,"unreliable")), --- (Left (True,"defeater"),Left (False,"unreliable")) --- ] -exTrans :: ConcreteAF -exTrans = translate caes - - - --- |Translation of the example CAES 'caes', keeping labels. --- The following is the prettified output of the translation, where --- the five propositions in the middle are the assumptions and 'defeater'. --- --- >>> translate' caes --- AF [ --- (False,Left (True,"murder")), --- (False,Left (False,"murder")), --- (False,Right ["kill","intent"] ~[]=>"murder"), --- (False,Left (False,"intent")), --- (False,Left (True,"intent")), --- (False,Right ["witness2"] ~["unreliable2"]=>"-intent"), --- (True,Right ["witness"] ~["unreliable"]=>"intent"), --- (False,Left (True,"unreliable")), --- (False,Left (False,"unreliable")) --- , --- (True,Left (True,"defeater")), --- (True,Left (True,"kill")), --- (True,Left (True,"witness")), --- (True,Left (True,"witness2")), --- (True,Left (True,"unreliable2"))] --- [ --- ((True,Left (True,"defeater")),(False,Left (True,"murder"))), --- ((True,Left (True,"defeater")),(False,Left (False,"murder"))), --- ((True,Left (True,"defeater")), (False,Right ["kill","intent"] ~[]=>"murder")), --- ((True,Left (True,"defeater")),(False,Left (False,"intent"))), --- ((True,Left (True,"defeater")),(False,Left (True,"intent"))), --- ((True,Left (True,"unreliable2")),(False,Right ["witness2"] ~["unreliable2"]=>"-intent")), --- ((True,Left (True,"defeater")),(False,Left (True,"unreliable"))), --- ((True,Left (True,"defeater")),(False,Left (False,"unreliable"))) -exTrans' :: LConcreteAF -exTrans' = translate' caes - - - --- |Combining the correspondence properties. --- --- And as expected: --- --- >>> corApp caes && corAcc caes --- True -corProp :: CAES -> Bool +-- | This is the examples module accompanying the implementation of the +-- translation from the Carneades argumentation model into Dung's +-- argumentation frameworks. +-- +-- This module contains a collection of examples, showing how to translate +-- an existing Carneades Argument Evaluation Structure (CAES) into an argumentation +-- framework. +-- +-- To run these examples, or your own: start GHCi and do the following: +-- +-- @\:l Language.CarneadesIntoDung.Examples@ +-- + +module Language.CarneadesIntoDung.Examples + ( + -- *Example translation + -- |We use the example CAES as defined in "Language.Carneades.ExampleCAES". + caes, + exTrans, exTrans', + -- *Correspondence properties + corProp, + ) + where +import Language.CarneadesIntoDung.Translation +import Language.Carneades.CarneadesDSL (CAES) +import Language.Carneades.ExampleCAES + +-- |Translation of the example CAES 'caes'. +-- The following is the prettified output of the translation, where +-- the five propositions in the middle are the assumptions and 'defeater'. +-- +-- >>> translate caes +-- AF [ +-- Left (True,"murder"), +-- Left (False,"murder"), +-- Right ["kill","intent"] ~[]=>"murder", +-- Left (False,"intent"), +-- Left (True,"intent"), +-- Right ["witness2"] ~["unreliable2"]=>"-intent", +-- Right ["witness"] ~["unreliable"]=>"intent", +-- Left (True,"unreliable"), +-- Left (False,"unreliable") +-- , +-- Left (True,"defeater"), +-- Left (True,"kill"), +-- Left (True,"witness"), +-- Left (True,"witness2"), +-- Left (True,"unreliable2")] +-- [ +-- (Left (True,"defeater"), Left (True,"murder")), +-- (Left (True,"defeater"), Left (False,"murder")), +-- (Left (True,"defeater"), Right ["kill","intent"] ~[]=>"murder"), +-- (Left (True,"defeater"), Left (False,"intent")), +-- (Left (True,"defeater"),Left (True,"intent")), +-- (Left (True,"unreliable2"),Right ["witness2"] ~["unreliable2"]=>"-intent"), +-- (Left (True,"defeater"),Left (True,"unreliable")), +-- (Left (True,"defeater"),Left (False,"unreliable")) +-- ] +exTrans :: ConcreteAF +exTrans = translate caes + + + +-- |Translation of the example CAES 'caes', keeping labels. +-- The following is the prettified output of the translation, where +-- the five propositions in the middle are the assumptions and 'defeater'. +-- +-- >>> translate' caes +-- AF [ +-- (False,Left (True,"murder")), +-- (False,Left (False,"murder")), +-- (False,Right ["kill","intent"] ~[]=>"murder"), +-- (False,Left (False,"intent")), +-- (False,Left (True,"intent")), +-- (False,Right ["witness2"] ~["unreliable2"]=>"-intent"), +-- (True,Right ["witness"] ~["unreliable"]=>"intent"), +-- (False,Left (True,"unreliable")), +-- (False,Left (False,"unreliable")) +-- , +-- (True,Left (True,"defeater")), +-- (True,Left (True,"kill")), +-- (True,Left (True,"witness")), +-- (True,Left (True,"witness2")), +-- (True,Left (True,"unreliable2"))] +-- [ +-- ((True,Left (True,"defeater")),(False,Left (True,"murder"))), +-- ((True,Left (True,"defeater")),(False,Left (False,"murder"))), +-- ((True,Left (True,"defeater")), (False,Right ["kill","intent"] ~[]=>"murder")), +-- ((True,Left (True,"defeater")),(False,Left (False,"intent"))), +-- ((True,Left (True,"defeater")),(False,Left (True,"intent"))), +-- ((True,Left (True,"unreliable2")),(False,Right ["witness2"] ~["unreliable2"]=>"-intent")), +-- ((True,Left (True,"defeater")),(False,Left (True,"unreliable"))), +-- ((True,Left (True,"defeater")),(False,Left (False,"unreliable"))) +exTrans' :: LConcreteAF +exTrans' = translate' caes + + + +-- |Combining the correspondence properties. +-- +-- And as expected: +-- +-- >>> corApp caes && corAcc caes +-- True +corProp :: CAES -> Bool corProp caes = corApp caes && corAcc caes diff --git a/src/Language/CarneadesIntoDung/Translation.hs b/src/Language/CarneadesIntoDung/Translation.hs --- a/src/Language/CarneadesIntoDung/Translation.hs +++ b/src/Language/CarneadesIntoDung/Translation.hs @@ -1,230 +1,230 @@ --- |This module implements a translation from the Carneades argumentation model --- into Dung's argumentation frameworks. Any cycle-free Carneades Argument --- Evaluation Structure (CAES) is handled. We also give a Haskell implementation of --- correspondence properties. --- --- Translation is done according to the following algorithm (see also \"Towards a --- framework for the implementation and verification of translations between --- argumentation models\" by Bas van Gijzel and Henrik Nilsson) --- --- 1. generatedArgs = /emptyset/. --- --- 2. sortedArgs = Topological sort of arguments on its dependency graph. --- --- 3. while sortedArgs != /emptyset/: --- --- * Pick the first argument in sortedArgs. --- Remove all arguments from sortedArgs that have the same conclusion, --- c, and put them in argSet. --- --- * Translate applicability part of arguments argSet, building on previously --- generatedArgs and put the generated arguments in tempArgs. --- --- * argSet = /emptyset/ --- --- * Repeat the above three steps for the arguments for the opposite conclusion. --- --- * Translate the acceptability part of c and the opposite conclusion based on --- arguments in tempArgs. Add the results and tempArgs to generatedArgs. --- --- * tempArgs = /emptyset/ -module Language.CarneadesIntoDung.Translation - ( - -- * Basic types - ConcreteArg, LConcreteArg, - ConcreteAF, LConcreteAF, - -- * Translation functions - translate, translate', - -- * Correspondence properties - -- | Informally, the correspondence properties below state that every - -- argument and proposition in a CAES, after translation, will have a - -- corresponding argument and keep the same acceptability status. - -- - -- If the translation function is a correct implementation, the Haskell - -- implementation of the correspondence properties should always return - -- 'True'. However to constitute an actual (mechanised) proof we would - -- need to convert the translation and the implementation of the - -- correspondence properties in Haskell to a theorem prover like Agda. - -- - -- See Section 4.4 of the paper for the formally stated properties. - - - corApp, corAcc) - where -import Language.Dung.AF hiding (acceptable) -import Language.Carneades.CarneadesDSL -import Language.Carneades.Cyclic -import Data.Graph.Inductive -import Data.List(find, delete, intersect) -import Data.Maybe(fromMaybe) -import Data.Either(lefts, rights) -import Data.Set(fromList) -import Prelude hiding (negate) - --- |A concrete argument (in an argumentation framework) is either a Carneades --- propositional literal, or a Carneades argument. -type ConcreteArg = Either PropLiteral Argument - --- |A labelled version of the concrete argument allowing a more efficient --- translation by keeping track of the translation status. -type LConcreteArg = (Bool, ConcreteArg) - --- |An argumentation framework (AF) instantiated with 'ConcreteArg'. -type ConcreteAF = DungAF ConcreteArg - --- |An argumentation framework (AF) instantiated with 'LConcreteArg'. -type LConcreteAF = DungAF LConcreteArg - --- |Assumed true argument in the translated AF. It is used to attack arguments --- that do not uphold their proof standard or have unacceptable premises. -defeater :: LConcreteArg -defeater = (True, Left $ mkProp "defeater") - - --- | Topological sort of the dependency graph --- The result is a list, pairing a proposition with all its pro arguments -topSort :: ArgSet -> [(PropLiteral, [Argument])] -topSort g | cyclic g = error "Argumentation graph is cyclic!" - | otherwise = reverse $ topsort' g - --- |Transforms a Carneades proposition into a Dung argument and labels it 'True'. -propToLArg :: PropLiteral -> LConcreteArg -propToLArg p = (True, Left p) - --- |Strips the label of both the 'LConcreteArg's in the attack. -stripAttack :: (LConcreteArg, LConcreteArg) -> (ConcreteArg, ConcreteArg) -stripAttack (a, b) = (snd a, snd b) - --- |Translation function. It translate an arbitrary /cycle-free/ Carneades argument --- Evaluation Structure (CAES) into a Dung argumentation framework (instantiated --- with a ConcreteArg) -translate :: CAES -> ConcreteAF -translate caes@(CAES (argSet, (assumptions, _), _)) - = AF (map snd args) (map stripAttack attacks) - where AF args attacks = argsToAF (topSort argSet) - caes - (AF (defeater : map propToLArg assumptions) []) - - --- |Mainly, for testing purposes. This function behaves exactly like 'translate', --- but retains the labels. -translate' :: CAES -> LConcreteAF -translate' caes@(CAES (argSet, (assumptions, _), _)) - = AF args attacks - where AF args attacks = argsToAF (topSort argSet) - caes - (AF (defeater : map propToLArg assumptions) []) - - --- |Retrieves the arguments con the given proposition 'p'. -conArgs :: PropLiteral -> [(PropLiteral, [Argument])] -> (PropLiteral, [Argument]) -conArgs p argList = fromMaybe (negate p, []) (find ((== negate p) . fst) argList) - --- |Corresponds to the whole of 3. of the above algorithm (or Algorithm 4.1 in --- the paper) --- --- If there are no more arguments to process, the translated AF is returned. - --- If there is a propositional literal left, but it is an assumption, it has --- already been translated and does not need to be considered. --- --- Otherwise, collect all pro and con arguments for p (con arguments are obtained --- by calling 'conArgs') and remove them from @argList@. The translation is then --- done in four steps. 'transApps' is called to translate the applicability part of --- the pro and con arguments. 'transAcc' is called to translate the acceptability of --- p and the opposite of p (note that the order of applicable arguments is switched --- for translating the acceptability of the opposite of p). The results of these --- four calls are collected and used in the recursive step of 'argsToAF'. -argsToAF :: [(PropLiteral, [Argument])] -> CAES -> LConcreteAF -> LConcreteAF -argsToAF [] _ transAF = transAF -argsToAF (pro@(p, proArgs) : argList) caes@(CAES (_, (assumptions, _), _)) (AF args defs) - | p `elem` assumptions = argsToAF argList caes (AF args defs) - | otherwise = - let con = conArgs p argList - (proAppArgs, proDefs) = transApps args pro - (conAppArgs, conDefs) = transApps args con - (newArgPro, proDefs') = transAcc p proAppArgs conAppArgs caes - (newArgCon, conDefs') = transAcc (negate p) conAppArgs proAppArgs caes - argList' = delete con argList - in argsToAF argList' caes - (AF (newArgPro : newArgCon : proAppArgs ++ conAppArgs ++ args) - (proDefs' ++ conDefs' ++ proDefs ++ conDefs ++ defs)) - --- |Filters out propositional literals that have been labelled 'True'. -accProps :: [LConcreteArg] -> [PropLiteral] -accProps [] = [] -accProps ((True, Left p) : ls) = p : accProps ls -accProps ((True, Right _) : ls) = accProps ls -accProps ((False, _) : ls) = accProps ls - --- |This function takes two arguments, a list of already translated arguments --- (including the translated premises and exceptions) and a proposition --- paired with its to be translated arguments. It collects the results --- of the transApp function, which does the main work. -transApps :: [LConcreteArg] -> (PropLiteral, [Argument]) -> ([LConcreteArg], [(LConcreteArg, LConcreteArg)]) -transApps tArgs (p, args) = - let tr = map (transApp tArgs p) args - in (map fst tr, concatMap snd tr) - --- |Given a list of already translated arguments and a propositional literal, --- an argument (pro the propositional literal) is translated into a Dung argument --- and a possibly empty list of attackers. -transApp :: [LConcreteArg] -> PropLiteral -> Argument -> (LConcreteArg, [(LConcreteArg, LConcreteArg)]) -transApp tArgs p a@(Arg (prems, excs, c)) - | accProps tArgs `intersect` prems /= prems = ((False, Right a), [(defeater, (False, Right a))]) - | otherwise = - let acceptableExceptions = filter (\ (b, arg) -> b && either (`elem` excs) (const False) arg) tArgs - applicableArg = (null acceptableExceptions, Right a) - defeats = map (\ argExc -> (argExc, applicableArg)) acceptableExceptions - in (applicableArg, defeats) - --- |Determines the maximum weight of a list of applicable arguments (assumed --- to have the same conclusion). -maxWeight :: [LConcreteArg] -> CAES -> Double -maxWeight as caes@(CAES (_, (_, argWeight), _)) - = foldl max 0 [argWeight a | (True, Right a) <- as] - - --- |This function expects the following arguments: a propositional literal at --- question, a list of pro arguments (labelled 'True', and thus acceptable in --- the current AF), a list of con arguments (acceptable in the current AF) and --- a CAES. The result will be an argument corresponding to the proposition and --- a list of attacks. -transAcc :: PropLiteral -> [LConcreteArg] -> [LConcreteArg] -> CAES -> (LConcreteArg, [(LConcreteArg, LConcreteArg)]) -transAcc c [] conArgs caes = ((False, Left c), [(defeater, (False, Left c))]) -- no applicable argument for p -transAcc c ((_, Left _): proArgs) conArgs caes = error "Proposition in the list of applicable arguments" -transAcc c ((False, _) : proArgs) conArgs caes = transAcc c proArgs conArgs caes -transAcc c proArgs@((True, _) : proArgs') conArgs caes@(CAES (_, _, standard)) - | standard c == Scintilla = ((True, Left c), []) -- there is an applicable argument for p, thus acceptable under Scintilla - | standard c == Preponderance && - maxWeight proArgs caes > maxWeight conArgs caes = ((True, Left c), []) - | standard c == ClearAndConvincing && - maxWeight proArgs caes > alpha && - maxWeight proArgs caes > maxWeight conArgs caes + beta = ((True, Left c), []) - | standard c == BeyondReasonableDoubt && - maxWeight proArgs caes > alpha && - maxWeight proArgs caes > maxWeight conArgs caes + beta && - maxWeight conArgs caes < gamma = ((True, Left c), []) - | standard c == DialecticalValidity && null conArgs = ((True, Left c), []) - | otherwise = ((False, Left c), [(defeater, (False, Left c))]) - --- |Correspondence of the applicability of arguments. -corApp :: CAES -> Bool -corApp caes@(CAES (argSet, _, _)) = - let translatedCAES = translate caes - applicableArgs = filter (`applicable` caes) - (getAllArgs argSet) - transArgs = rights $ groundedExt translatedCAES - in fromList applicableArgs == fromList transArgs - --- |Correspondence of the acceptability of propositional literals, including --- assumptions. -corAcc :: CAES -> Bool -corAcc caes@(CAES (argSet, (assumptions, _), _)) = - let translatedCAES = translate caes - acceptableProps = filter (\ p -> p `acceptable` caes || - p `elem` assumptions) - (getProps argSet) - transProps = lefts $ delete (Left $ mkProp "defeater") - (groundedExt translatedCAES ) +-- |This module implements a translation from the Carneades argumentation model +-- into Dung's argumentation frameworks. Any cycle-free Carneades Argument +-- Evaluation Structure (CAES) is handled. We also give a Haskell implementation of +-- correspondence properties. +-- +-- Translation is done according to the following algorithm (see also \"Towards a +-- framework for the implementation and verification of translations between +-- argumentation models\" by Bas van Gijzel and Henrik Nilsson) +-- +-- 1. generatedArgs = /emptyset/. +-- +-- 2. sortedArgs = Topological sort of arguments on its dependency graph. +-- +-- 3. while sortedArgs != /emptyset/: +-- +-- * Pick the first argument in sortedArgs. +-- Remove all arguments from sortedArgs that have the same conclusion, +-- c, and put them in argSet. +-- +-- * Translate applicability part of arguments argSet, building on previously +-- generatedArgs and put the generated arguments in tempArgs. +-- +-- * argSet = /emptyset/ +-- +-- * Repeat the above three steps for the arguments for the opposite conclusion. +-- +-- * Translate the acceptability part of c and the opposite conclusion based on +-- arguments in tempArgs. Add the results and tempArgs to generatedArgs. +-- +-- * tempArgs = /emptyset/ +module Language.CarneadesIntoDung.Translation + ( + -- * Basic types + ConcreteArg, LConcreteArg, + ConcreteAF, LConcreteAF, + -- * Translation functions + translate, translate', + -- * Correspondence properties + -- | Informally, the correspondence properties below state that every + -- argument and proposition in a CAES, after translation, will have a + -- corresponding argument and keep the same acceptability status. + -- + -- If the translation function is a correct implementation, the Haskell + -- implementation of the correspondence properties should always return + -- 'True'. However to constitute an actual (mechanised) proof we would + -- need to convert the translation and the implementation of the + -- correspondence properties in Haskell to a theorem prover like Agda. + -- + -- See Section 4.4 of the paper for the formally stated properties. + + + corApp, corAcc) + where +import Language.Dung.AF (DungAF(..), groundedExt) +import Language.Carneades.CarneadesDSL +import Language.Carneades.Cyclic +import Data.Graph.Inductive +import Data.List (find, delete, intersect) +import Data.Maybe (fromMaybe) +import Data.Either (lefts, rights) +import Data.Set (fromList) +import Prelude hiding (negate) + +-- |A concrete argument (in an argumentation framework) is either a Carneades +-- propositional literal, or a Carneades argument. +type ConcreteArg = Either PropLiteral Argument + +-- |A labelled version of the concrete argument allowing a more efficient +-- translation by keeping track of the translation status. +type LConcreteArg = (Bool, ConcreteArg) + +-- |An argumentation framework (AF) instantiated with 'ConcreteArg'. +type ConcreteAF = DungAF ConcreteArg + +-- |An argumentation framework (AF) instantiated with 'LConcreteArg'. +type LConcreteAF = DungAF LConcreteArg + +-- |Assumed true argument in the translated AF. It is used to attack arguments +-- that do not uphold their proof standard or have unacceptable premises. +defeater :: LConcreteArg +defeater = (True, Left $ mkProp "defeater") + + +-- | Topological sort of the dependency graph +-- The result is a list, pairing a proposition with all its pro arguments +topSort :: ArgSet -> [(PropLiteral, [Argument])] +topSort g | cyclic g = error "Argumentation graph is cyclic!" + | otherwise = reverse $ topsort' g + +-- |Transforms a Carneades proposition into a Dung argument and labels it 'True'. +propToLArg :: PropLiteral -> LConcreteArg +propToLArg p = (True, Left p) + +-- |Strips the label of both the 'LConcreteArg's in the attack. +stripAttack :: (LConcreteArg, LConcreteArg) -> (ConcreteArg, ConcreteArg) +stripAttack (a, b) = (snd a, snd b) + +-- |Translation function. It translate an arbitrary /cycle-free/ Carneades argument +-- Evaluation Structure (CAES) into a Dung argumentation framework (instantiated +-- with a ConcreteArg) +translate :: CAES -> ConcreteAF +translate caes@(CAES (argSet, (assumptions, _), _)) + = AF (map snd args) (map stripAttack attacks) + where AF args attacks = argsToAF (topSort argSet) + caes + (AF (defeater : map propToLArg assumptions) []) + + +-- |Mainly, for testing purposes. This function behaves exactly like 'translate', +-- but retains the labels. +translate' :: CAES -> LConcreteAF +translate' caes@(CAES (argSet, (assumptions, _), _)) + = AF args attacks + where AF args attacks = argsToAF (topSort argSet) + caes + (AF (defeater : map propToLArg assumptions) []) + + +-- |Retrieves the arguments con the given proposition 'p'. +conArgs :: PropLiteral -> [(PropLiteral, [Argument])] -> (PropLiteral, [Argument]) +conArgs p argList = fromMaybe (negate p, []) (find ((== negate p) . fst) argList) + +-- |Corresponds to the whole of 3. of the above algorithm (or Algorithm 4.1 in +-- the paper) +-- +-- If there are no more arguments to process, the translated AF is returned. + +-- If there is a propositional literal left, but it is an assumption, it has +-- already been translated and does not need to be considered. +-- +-- Otherwise, collect all pro and con arguments for p (con arguments are obtained +-- by calling 'conArgs') and remove them from @argList@. The translation is then +-- done in four steps. 'transApps' is called to translate the applicability part of +-- the pro and con arguments. 'transAcc' is called to translate the acceptability of +-- p and the opposite of p (note that the order of applicable arguments is switched +-- for translating the acceptability of the opposite of p). The results of these +-- four calls are collected and used in the recursive step of 'argsToAF'. +argsToAF :: [(PropLiteral, [Argument])] -> CAES -> LConcreteAF -> LConcreteAF +argsToAF [] _ transAF = transAF +argsToAF (pro@(p, _proArgs) : argList) caes@(CAES (_, (assumptions, _), _)) (AF args defs) + | p `elem` assumptions = argsToAF argList caes (AF args defs) + | otherwise = + let con = conArgs p argList + (proAppArgs, proDefs) = transApps args pro + (conAppArgs, conDefs) = transApps args con + (newArgPro, proDefs') = transAcc p proAppArgs conAppArgs caes + (newArgCon, conDefs') = transAcc (negate p) conAppArgs proAppArgs caes + argList' = delete con argList + in argsToAF argList' caes + (AF (newArgPro : newArgCon : proAppArgs ++ conAppArgs ++ args) + (proDefs' ++ conDefs' ++ proDefs ++ conDefs ++ defs)) + +-- |Filters out propositional literals that have been labelled 'True'. +accProps :: [LConcreteArg] -> [PropLiteral] +accProps [] = [] +accProps ((True, Left p) : ls) = p : accProps ls +accProps ((True, Right _) : ls) = accProps ls +accProps ((False, _) : ls) = accProps ls + +-- |This function takes two arguments, a list of already translated arguments +-- (including the translated premises and exceptions) and a proposition +-- paired with its to be translated arguments. It collects the results +-- of the transApp function, which does the main work. +transApps :: [LConcreteArg] -> (PropLiteral, [Argument]) -> ([LConcreteArg], [(LConcreteArg, LConcreteArg)]) +transApps tArgs (p, args) = + let tr = map (transApp tArgs p) args + in (map fst tr, concatMap snd tr) + +-- |Given a list of already translated arguments and a propositional literal, +-- an argument (pro the propositional literal) is translated into a Dung argument +-- and a possibly empty list of attackers. +transApp :: [LConcreteArg] -> PropLiteral -> Argument -> (LConcreteArg, [(LConcreteArg, LConcreteArg)]) +transApp tArgs _p a@(Arg (prems, excs, _c)) + | accProps tArgs `intersect` prems /= prems = ((False, Right a), [(defeater, (False, Right a))]) + | otherwise = + let acceptableExceptions = filter (\ (b, arg) -> b && either (`elem` excs) (const False) arg) tArgs + applicableArg = (null acceptableExceptions, Right a) + defeats = map (\ argExc -> (argExc, applicableArg)) acceptableExceptions + in (applicableArg, defeats) + +-- |Determines the maximum weight of a list of applicable arguments (assumed +-- to have the same conclusion). +maxWeight :: [LConcreteArg] -> CAES -> Double +maxWeight args (CAES (_, (_, argWeight), _)) + = foldl max 0 [argWeight a | (True, Right a) <- args] + + +-- |This function expects the following arguments: a propositional literal at +-- question, a list of pro arguments (labelled 'True', and thus acceptable in +-- the current AF), a list of con arguments (acceptable in the current AF) and +-- a CAES. The result will be an argument corresponding to the proposition and +-- a list of attacks. +transAcc :: PropLiteral -> [LConcreteArg] -> [LConcreteArg] -> CAES -> (LConcreteArg, [(LConcreteArg, LConcreteArg)]) +transAcc c [] _conArgs _caes = ((False, Left c), [(defeater, (False, Left c))]) -- no applicable argument for p +transAcc _c ((_, Left _): _proArgs) _conArgs _caes = error "Proposition in the list of applicable arguments" +transAcc c ((False, _) : proArgs) conArgs caes = transAcc c proArgs conArgs caes +transAcc c proArgs@((True, _) : _) conArgs caes@(CAES (_, _, standard)) + | standard c == Scintilla = ((True, Left c), []) -- there is an applicable argument for p, thus acceptable under Scintilla + | standard c == Preponderance && + maxWeight proArgs caes > maxWeight conArgs caes = ((True, Left c), []) + | standard c == ClearAndConvincing && + maxWeight proArgs caes > alpha && + maxWeight proArgs caes > maxWeight conArgs caes + beta = ((True, Left c), []) + | standard c == BeyondReasonableDoubt && + maxWeight proArgs caes > alpha && + maxWeight proArgs caes > maxWeight conArgs caes + beta && + maxWeight conArgs caes < gamma = ((True, Left c), []) + | standard c == DialecticalValidity && null conArgs = ((True, Left c), []) + | otherwise = ((False, Left c), [(defeater, (False, Left c))]) + +-- |Correspondence of the applicability of arguments. +corApp :: CAES -> Bool +corApp caes@(CAES (argSet, _, _)) = + let translatedCAES = translate caes + applicableArgs = filter (`applicable` caes) + (getAllArgs argSet) + transArgs = rights $ groundedExt translatedCAES + in fromList applicableArgs == fromList transArgs + +-- |Correspondence of the acceptability of propositional literals, including +-- assumptions. +corAcc :: CAES -> Bool +corAcc caes@(CAES (argSet, (assumptions, _), _)) = + let translatedCAES = translate caes + acceptableProps = filter (\p -> p `acceptable` caes || + p `elem` assumptions) + (getProps argSet) + transProps = lefts $ delete (Left $ mkProp "defeater") + (groundedExt translatedCAES) in fromList acceptableProps == fromList transProps diff --git a/src/Main.hs b/src/Main.hs deleted file mode 100644 --- a/src/Main.hs +++ /dev/null @@ -1,100 +0,0 @@ --- |This module implements a command-line interface to the implementation of --- Carneades. CAES + Haskell = caell --- --- Code in this module partly taken from/inspired by Shinobu --- See: http://zuttobenkyou.wordpress.com/2011/04/19/haskell-using-cmdargs-single-and-multi-mode/ --- and http://listx.github.com/ -{-# LANGUAGE DeriveDataTypeable, RecordWildCards #-} -module Main - ( - main - ) - where -import Language.CarneadesIntoDung.Translation -import Language.Carneades.CarneadesDSL(CAES(..), getAllArgs, applicable, - getProps, acceptable) -import Language.Carneades.Input -import Language.Dung.AF(groundedExt, preferredExt, stableExt, semiStableExt, - DungAF(..)) -import Language.Dung.Output - -import System.Console.CmdArgs -import System.Environment (getArgs, withArgs) -import System.Exit -import Control.Monad (when, unless) - -data MyOptions = MyOptions { - cegartix :: Bool, - laxCegartix :: Bool, - fileName :: String, - outputFile :: String, - correspondence :: Bool, - extension :: Bool, - xSemantics :: Bool - } deriving (Show, Data, Typeable) - -myProgOpts :: MyOptions -myProgOpts = MyOptions - { cegartix = True &= help "Output in strict CEGARTIX/PrefSat format (standard)" - , laxCegartix = False &= help "Output in lax CEGARTIX/PrefSat format (+parentheses)" - , fileName = def &= typFile &= help "Name of the file to be read" - , outputFile = def &= typFile &= help "Name of the file to be written" - , extension = True &= help "Output unique complete extension for the translated CAES (standard)" - , correspondence = False &= help "Display satisfaction of correspondence result" - , xSemantics = False &= help "Output evaluation of the original Carneades semantics" - } - -getOpts :: IO MyOptions -getOpts = cmdArgs $ myProgOpts - &= versionArg [explicit, name "version", name "v", summary _PROGRAM_INFO] - &= summary (_PROGRAM_INFO ++ ", " ++ _COPYRIGHT) - &= help _PROGRAM_ABOUT - &= helpArg [explicit, name "help", name "h"] - &= program _PROGRAM_NAME - -_PROGRAM_NAME = "caell" -_PROGRAM_VERSION = "1.0" -_PROGRAM_INFO = _PROGRAM_NAME ++ " version " ++ _PROGRAM_VERSION -_PROGRAM_ABOUT = "An implementation of Carneades in Haskell" -_COPYRIGHT = "(C) Bas van Gijzel 2014" - - -main :: IO () -main = do - args <- getArgs - opts <- (if null args then withArgs ["--help"] else id) getOpts - optionHandler opts - --- |Check any malformed arguments/missing arguments. -optionHandler :: MyOptions -> IO () -optionHandler opts@MyOptions{..} = do - when (null fileName) $ putStrLn "--fileName is blank!" >> exitWith (ExitFailure 1) - input <- readFile fileName - let opts' = opts {cegartix = not laxCegartix} - caes <- case parseCAES input of - Left err -> putStrLn "Parsing error: " >> print err >> exitWith (ExitFailure 1) - Right caes -> return caes - exec opts' caes - --- |Execute supplied options -exec :: MyOptions -> CAES -> IO () -exec opts@MyOptions{..} caes@(CAES (argSet, (assumptions, _), _)) = do - let args = getAllArgs argSet - let transCaes = translate caes - putStrLn $ "Argument set: " ++ show args - when xSemantics $ - putStrLn "Evaluation under original semantics:" >> - putStrLn "Applicable arguments:" >> - print (filter (`applicable` caes) args) >> - putStrLn "Acceptable propositions:" >> - print (filter (\ p -> p `acceptable` caes - || p `elem` assumptions) - (getProps argSet)) - when extension $ putStrLn "Extension after translation: " - >> print (groundedExt transCaes) - when correspondence $ putStrLn ("Correspondence of applicability is: " ++ show (corApp caes)) - >> putStrLn ("Correspondence of acceptability is: " ++ show (corAcc caes)) - unless (null outputFile) - $ if cegartix - then writeFile outputFile (toStrictCegartix transCaes) >> putStrLn "File outputted." - else writeFile outputFile (toCegartix transCaes) >> putStrLn "File outputted." diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,10 @@ +module Main (main) where + +import Test.Tasty + +import qualified Test.Language.CarneadesIntoDung.Translation as Translation + +main :: IO () +main = defaultMain $ testGroup "CarneadesIntoDung" + [ Translation.tests + ] diff --git a/test/Test/Language/CarneadesIntoDung/Translation.hs b/test/Test/Language/CarneadesIntoDung/Translation.hs new file mode 100644 --- /dev/null +++ b/test/Test/Language/CarneadesIntoDung/Translation.hs @@ -0,0 +1,71 @@ +module Test.Language.CarneadesIntoDung.Translation (tests) where + +import Data.Either (lefts, rights) +import Data.Set (fromList) +import Test.Tasty +import Test.Tasty.HUnit + +import Language.Dung.AF (DungAF(..), groundedExt) +import Language.Carneades.CarneadesDSL (CAES(..), mkProp, getAllArgs, applicable, + getProps, acceptable) +import Language.Carneades.ExampleCAES (caes) +import Language.CarneadesIntoDung.Translation + +tests :: TestTree +tests = testGroup "Language.CarneadesIntoDung.Translation" + [ translateTests + , groundedExtTests + , correspondenceTests + ] + +translateTests :: TestTree +translateTests = testGroup "translate" + [ testCase "translate produces a non-empty AF" $ do + let AF args attacks = translate caes + assertBool "AF should have arguments" (not (null args)) + assertBool "AF should have attacks" (not (null attacks)) + , testCase "translate' produces a non-empty labelled AF" $ do + let AF args attacks = translate' caes + assertBool "labelled AF should have arguments" (not (null args)) + assertBool "labelled AF should have attacks" (not (null attacks)) + , testCase "defeater is in the grounded extension" $ do + let ext = groundedExt (translate caes) + assertBool "defeater should be in grounded extension" + (Left (mkProp "defeater") `elem` ext) + , testCase "assumptions are in the grounded extension" $ do + let CAES (_, (assumptions, _), _) = caes + let ext = lefts $ groundedExt (translate caes) + mapM_ (\a -> assertBool ("assumption " ++ show a ++ " should be in extension") + (a `elem` ext)) + assumptions + ] + +groundedExtTests :: TestTree +groundedExtTests = testGroup "groundedExt" + [ testCase "grounded extension contains applicable arguments" $ do + let CAES (argSet, _, _) = caes + let appArgs = filter (`applicable` caes) (getAllArgs argSet) + let ext = rights $ groundedExt (translate caes) + mapM_ (\a -> assertBool ("applicable arg " ++ show a ++ " should be in extension") + (a `elem` ext)) + appArgs + , testCase "grounded extension contains acceptable propositions" $ do + let CAES (argSet, (assumptions, _), _) = caes + let accProps = filter (\p -> p `acceptable` caes || p `elem` assumptions) + (getProps argSet) + let ext = lefts $ filter (/= Left (mkProp "defeater")) + (groundedExt (translate caes)) + assertEqual "acceptable propositions should match" + (fromList accProps) (fromList ext) + ] + +correspondenceTests :: TestTree +correspondenceTests = testGroup "correspondence" + [ testCase "corApp caes returns True" $ + corApp caes @?= True + , testCase "corAcc caes returns True" $ + corAcc caes @?= True + , testCase "corProp (combined) returns True" $ do + let result = corApp caes && corAcc caes + result @?= True + ]