CarneadesIntoDung 1.0 → 2.0.0.0

raw patch · 14 files changed

+709/−506 lines, 14 filesdep +CarneadesIntoDungdep +optparse-applicativedep +tastydep −cmdargsdep ~CarneadesDSLdep ~Dungdep ~basesetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies added: CarneadesIntoDung, optparse-applicative, tasty, tasty-hunit

Dependencies removed: cmdargs

Dependency ranges changed: CarneadesDSL, Dung, base, containers, fgl

API changes (from Hackage documentation)

Files

CHANGELOG +0/−7
CHANGELOG.md +29/−0
CarneadesIntoDung.cabal +74/−36
LICENSE +1/−1
README.md +42/−0
Setup.hs +0/−2
app/Main.hs +108/−0
exampleaf.txt +15/−0
examplecaes.txt +25/−25
src/Language/CarneadesIntoDung/Examples.hs +105/−106
src/Language/CarneadesIntoDung/Translation.hs +229/−229
src/Main.hs +0/−100
test/Main.hs +10/−0
test/Test/Language/CarneadesIntoDung/Translation.hs +71/−0

− CHANGELOG

@@ -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.

+ CHANGELOG.md view

@@ -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.

CarneadesIntoDung.cabal view

@@ -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 <bmv@cs.nott.ac.uk>+maintainer:    Bas van Gijzel <nenekotan+git@gmail.com>+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 -               (<http://hackage.haskell.org/package/CarneadesDSL>) into Dung's -               argumentation frameworks (<http://hackage.haskell.org/package/Dung>). -               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 <http://www.cs.nott.ac.uk/~bmv/CarneadesIntoDung/>.+description:+  A translation from the Carneades argumentation model+  (<http://hackage.haskell.org/package/CarneadesDSL>) into Dung's+  argumentation frameworks (<http://hackage.haskell.org/package/Dung>).+  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+  <https://scholar.google.com/citations?user=Xu4yjvwAAAAJ&hl>. 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

LICENSE view

@@ -1,4 +1,4 @@-Copyright (c)2014, Bas van Gijzel+Copyright (c) 2014-2026, Bas van Gijzel  All rights reserved.

+ README.md view

@@ -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 <https://scholar.google.com/citations?user=Xu4yjvwAAAAJ&hl>.++## 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.

− Setup.hs

@@ -1,2 +0,0 @@-import Distribution.Simple
-main = defaultMain

+ app/Main.hs view

@@ -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."

+ exampleaf.txt view

@@ -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).

examplecaes.txt view

@@ -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++

src/Language/CarneadesIntoDung/Examples.hs view

@@ -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

src/Language/CarneadesIntoDung/Translation.hs view

@@ -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

− src/Main.hs

@@ -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."

+ test/Main.hs view

@@ -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+  ]

+ test/Test/Language/CarneadesIntoDung/Translation.hs view

@@ -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+  ]