CarneadesDSL 1.3 → 2.0.0.0

raw patch · 20 files changed

+1733/−1033 lines, 20 filesdep +CarneadesDSLdep +tastydep +tasty-hunitdep ~basedep ~containersdep ~fglsetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies added: CarneadesDSL, tasty, tasty-hunit

Dependency ranges changed: base, containers, fgl, parsec

API changes (from Hackage documentation)

Files

• CHANGELOG +0/−17
• CHANGELOG.md +30/−0
• CarneadesDSL.cabal +62/−28
• LICENSE +1/−1
• Language/Carneades/CarneadesDSL.lhs +0/−550
• Language/Carneades/Cyclic.hs +0/−11
• Language/Carneades/ExampleCAES.lhs +0/−181
• Language/Carneades/Input.hs +0/−224
• README.md +54/−0
• Setup.hs +0/−2
• doc/CarneadesDSL.lhs +550/−0
• doc/ExampleCAES.lhs +181/−0
• examplecaes.txt +19/−19
• src/Language/Carneades/CarneadesDSL.hs +307/−0
• src/Language/Carneades/Cyclic.hs +11/−0
• src/Language/Carneades/ExampleCAES.hs +95/−0
• src/Language/Carneades/Input.hs +219/−0
• test/Main.hs +12/−0
• test/Test/Language/Carneades/CarneadesDSL.hs +96/−0
• test/Test/Language/Carneades/Input.hs +96/−0

@@ -1,17 +0,0 @@-1.2 => 1.3-=============-This package has been extended and now includes:--* An Input module, allowing files to be parsed.- -* An example of the usage of this module.--1.1.0.1 => 1.2-=============-This package version is now compatible with the translation package CarneadesIntoDung. -See http://hackage.haskell.org/package/CarneadesIntoDung/--* Change the use of proof standards to rely on the definition of |PSName|-  to allow for an easier translation.--* Fix the definition of applicability to include all three conditions.

@@ -0,0 +1,30 @@+# Changelog++## 2.0.0.0++* Modernise build: require `cabal-version: 3.0`, GHC 9.4++* Move sources under `src/` layout+* Convert literate Haskell (`.lhs`) to plain Haskell (`.hs`); originals+  preserved in `doc/`+* Add `-Wall`-clean compilation+* Add test suite (tasty + HUnit)+* Add GitHub Actions CI (GHC 9.4 / 9.6 / 9.8 / 9.10)+* Remove `Setup.hs`+* Update maintainer email, copyright years, and homepage URL++## 1.3++* An Input module, allowing files to be parsed.+* An example of the usage of this module.++## 1.2++* This package version is now compatible with the translation package+  CarneadesIntoDung.+* Change the use of proof standards to rely on the definition of `PSName`+  to allow for an easier translation.+* Fix the definition of applicability to include all three conditions.++## 1.1.0.1++* Initial Hackage release.

@@ -1,43 +1,77 @@+cabal-version: 3.0 name:          CarneadesDSL-category:      Argumentation, Embedded, AI-version:       1.3-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/CarneadesDSL/-copyright:     Copyright (C) 2014 Bas van Gijzel+category:      Argumentation, Embedded, AI+homepage:      https://github.com/nebasuke/CarneadesDSL synopsis:      An implementation and DSL for the Carneades argumentation model.-description:   An implementation and domain specific language for the Carneades-               argumentation model. See "Haskell Gets Argumentative" in the -               Proceedings of Symposium on Trends in Functional Programming -               (TFP 2012) by Bas van Gijzel and Henrik Nilsson or the -               package's homepage. Thanks to Stefan Sabev for providing initial-               code for the cyclicity check. +description:+  An implementation and domain specific language for the Carneades+  argumentation model. See "Haskell Gets Argumentative" in the+  Proceedings of Symposium on Trends in Functional Programming+  (TFP 2012) by Bas van Gijzel and Henrik Nilsson. Thanks to Stefan+  Sabev for providing initial code for the cyclicity check.+  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,-    parsec                 >= 3+extra-source-files:+  LICENSE+  examplecaes.txt+  doc/CarneadesDSL.lhs+  doc/ExampleCAES.lhs +source-repository head+  type:     git+  location: https://github.com/nebasuke/CarneadesDSL++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,+    parsec     >= 3.1  && < 3.2   exposed-modules:     Language.Carneades.CarneadesDSL     Language.Carneades.ExampleCAES     Language.Carneades.Cyclic     Language.Carneades.Input-     -source-repository head-  Type:     git-  Location: https://github.com/nebasuke/CarneadesDSL--       +test-suite carneadesdsl-tests+  import:           warnings+  type:             exitcode-stdio-1.0+  main-is:          Main.hs+  hs-source-dirs:   test+  build-depends:+    base              >= 4.16 && < 5,+    CarneadesDSL,+    containers        >= 0.6  && < 0.8,+    tasty             >= 1.4  && < 1.6,+    tasty-hunit       >= 0.10 && < 0.11+  other-modules:+    Test.Language.Carneades.CarneadesDSL+    Test.Language.Carneades.Input

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

@@ -1,550 +0,0 @@-%include arg-preamble.fmt--\begin{code}-module Language.Carneades.CarneadesDSL where--import Language.Carneades.Cyclic--import Prelude hiding (negate)--import Data.Graph.Inductive-import Data.Map (Map)-import Data.List(nub)-import qualified Data.Set as Set-import qualified Data.Map as Map-import Data.Maybe (fromJust)-\end{code}---\subsection{Arguments}-As our ultimate goal is a DSL for argumentation theory, we strive for a-realisation in Haskell that mirrors the mathematical model of Carneades-argumentation framework as closely as possible. Ideally, there would be little-more to a realisation than a transliteration. We will thus proceed by-stating the central definitions of Carneades along with our realisation-of them in Haskell. --\begin{definition}[Arguments]-\label{def:carneadesargs}-Let $\mathcal{L}$ be a propositional language. An \emph{argument} is a-tuple $\langle P, E, c \rangle$ where $P \subset \mathcal{L}$ are its-\emph{premises}, $E \subset \mathcal{L}$ with $P \cap E = \emptyset$-are its \emph{exceptions} and $c \in \mathcal{L}$ is its-\emph{conclusion}. For simplicity, all members of $\mathcal{L}$ -must be literals, i.e. either an atomic proposition or a negated-atomic proposition.  -An argument is said to be \emph{pro} its conclusion $c$ (which may be-a negative atomic proposition) and \emph{con} the negation of $c$.-\end{definition}--In Carneades all logical formulae are literals in propositional logic;-i.e., all propositions are either positive or negative atoms. Taking-atoms to be strings suffice in the following, and propositional literals can-then be formed by pairing this atom with a Boolean to denote whether-it is negated or not: -\begin{code} -type PropLiteral = (Bool, String)-\end{code}-We write $\overline{p}$ for the negation of a literal $p$. The realisation-is immediate:-\begin{code}-negate :: PropLiteral -> PropLiteral -negate (b, x) = (not b, x)-\end{code}--We chose to realise an \emph{argument} as a newtype (to allow a manual Eq instance)-containing a tuple of two lists of propositions, its \emph{premises} and its -\emph{exceptions}, and a proposition that denotes the \emph{conclusion}: -\begin{code}-newtype Argument = Arg ([PropLiteral], [PropLiteral], PropLiteral)- deriving Ord -\end{code}--Arguments are considered equal if their premises, exceptions and-conclusion are equal; thus arguments are identified by their logical-content. The equality instance for |Argument| (omitted for brevity) takes-this into account by comparing the lists as sets.--\begin{code}---Manual Eq instance for set equality on premises and exceptions-instance Eq Argument where- (Arg (prems, excs, c)) == (Arg (prems', excs', c')) -    =  Set.fromList prems == Set.fromList prems'  && -       Set.fromList excs == Set.fromList excs'    && -       c == c'--showProp :: PropLiteral -> String-showProp (True, c)   = c-showProp (_    , c)  = '-' : c--instance Show Argument where - show (Arg (prems, excs, (True, c)))   = show (map showProp prems) ++ ' ' : '~' : show (map showProp excs) ++ "=>" ++ show c- show (Arg (prems, excs, (_    , c)))  = show (map showProp prems) ++ ' ' : '~' : show (map showProp excs) ++ "=>" ++ show ('-' : c)-\end{code}---A set of arguments determines how propositions depend on each other.-Carneades requires that there are no cycles among these dependencies. -Following Brewka and Gordon~\cite{Brewka10a}, we use a dependency-graph to determine acyclicity of a set of arguments.--\begin{definition}[Acyclic set of arguments]-\label{def:carneadesacyclic}-A set of \emph{arguments} is \emph{acyclic} iff its corresponding-dependency graph is acyclic. The corresponding dependency graph has a-node for every literal appearing in the set of arguments. A node $p$-has a link to node $q$ whenever $p$ depends on $q$ in the sense that-there is an argument pro or con $p$ that has $q$ or $\overline{q}$ in-its set of premises or exceptions.-\end{definition}--Our realisation of a set of arguments is considered abstract for DSL-purposes, only providing a check for acyclicity and a function to-retrieve arguments pro a proposition. We use FGL \cite{Erwig2001} to-implement the dependency graph, forming nodes for propositions and edges-for the dependencies. For simplicity, we opt to keep the graph-also as the representation of a set of arguments.---\begin{code}--- Note that for practical purposes we do not need to know the following --- implementation but can use the abstraction further below-type ArgSet = Gr (PropLiteral, [Argument]) ()-\end{code}---\begin{spec}--- abstraction of ArgSet and the operating functions on it-type ArgSet = ...--getArgs     :: PropLiteral -> ArgSet -> [Argument]  -checkCycle  :: ArgSet -> Bool-\end{spec}---\subsection{Carneades Argument Evaluation Structure}--The main structure of the argumentation model is called a Carneades-Argument Evaluation Structure (CAES):-\begin{definition}[Carneades Argument Evaluation Structure (CAES)] A-\emph{Carneades Argument Evaluation Structure} (CAES) is a triple-\[-\langle arguments, audience, standard \rangle-\]-where $arguments$ is an acyclic set of arguments, $audience$ is an audience as-defined below (Def.~\ref{def:carneadesaudience}), and \emph{standard} is a-total function mapping each proposition to to its specific proof standard. -\end{definition}-Note that propositions may be associated with \emph{different} proof-standards. This is considered a particular strength of the Carneades-framework. The transliteration into Haskell is almost immediate%-\footnote{Note that we use a newtype to prevent a cycle in the type-definitions.}:-\begin{code}-newtype CAES = CAES (ArgSet, Audience, PropStandard)-\end{code}--\begin{definition}[Audience]-\label{def:carneadesaudience}-Let $\mathcal{L}$ be a propositional language. An \emph{audience} is a-tuple $\langle$\emph{assumptions}, \emph{weight}$\rangle$, where-$assumptions \subset \mathcal{L}$ is a propositionally consistent set of-literals (i.e., not containing both a literal and its negation) assumed-to be acceptable by the audience and \emph{weight} is a function mapping-arguments to a real-valued weight in the range $[0,1]$.-\end{definition}-This definition is captured by the following Haskell definitions:-\begin{code}-type Audience = (Assumptions, ArgWeight)-type Assumptions = [PropLiteral]-type ArgWeight = Argument -> Weight-type Weight = Double-\end{code}--Further, as each proposition is associated with a specific proof standard,-we need a mapping from propositions to proof standards:-\begin{code}-type PropStandard = PropLiteral -> PSName--data PSName = Scintilla -  | Preponderance | ClearAndConvincing -  | BeyondReasonableDoubt | DialecticalValidity- deriving (Show, Eq)-\end{code}--\begin{spec}-psMap :: PSName -> ProofStandard -\end{spec}--A proof standard is a function that given a proposition $p$, aggregates-arguments pro and con $p$ and decides whether it is acceptable or not:-\begin{code}-type ProofStandard = PropLiteral -> CAES -> Bool--newtype ProofStandardNamed = P (String, PropLiteral -> CAES -> Bool)-instance Eq ProofStandardNamed where- P (l1, _) == P (l2, _) = l1 == l2-\end{code}-This aggregation process will be defined in detail in the next section,-but note that it is done relative to a specific CAES, and note the-cyclic dependence at the type level between |CAES| and |ProofStandard|.--The above definition of proof standard also demonstrates that-implementation in a typed language such as Haskell is a useful way of-verifying definitions from argumentation theoretic models. Our-implementation effort revealed that the original definition as given-in~\cite{Gordon09a} could not be realised as stated, because proof standards-in general not only depend on a set of arguments and the audience,-but may need the whole CAES.--\subsection{Evaluation}--Two concepts central to the evaluation of a CAES are-\emph{applicability of arguments}, which arguments should be-taken into account, and \emph{acceptability of propositions}, which-conclusions can be reached under the relevant proof standards, given-the beliefs of a specific audience.-\begin{definition}[Applicability of arguments]-Given a set of arguments and a set of assumptions (in an audience) in a CAES-$C$, then an argument $a = \langle P, E, c \rangle$ is-\emph{applicable} iff-\begin{itemize}-\item-    $p \in P$ implies $p$ is an assumption or [\,$\overline{p}$ is-    not an assumption and $p$ is acceptable in $C$\,] and-\item-    $e \in E$ implies $e$ is not an assumption and [\,$\overline{e}$-    is an assumption or $e$ is not acceptable in $C$\,].-\end{itemize}-\end{definition}-\begin{definition}[Acceptability of propositions]-Given a CAES $C$, a proposition $p$ is \emph{acceptable} in $C$ iff-$(s \; p \; C)$ is $true$, where $s$ is the proof standard for $p$.-\end{definition}--Note that these two definitions in general are mutually dependent-because acceptability depends on proof standards, and most sensible-proof standards depend on the applicability of arguments. This is the-reason that Carneades restricts the set of arguments to be acyclic. -(Specific proof standards are considered in the next section.)-The realisation of applicability and acceptability in Haskell is-straightforward:--- \begin{code}--- applicable :: Argument -> CAES -> Bool--- applicable (Arg (prems, excns, _)) caes@(CAES (_, (assumptions, _), _)) -  -- = and  $  [(p `elem` assumptions)  ||     (p `acceptable` caes)  |  p <- prems  ]-            -- ++-            -- [(e `elem` assumptions)  `nor`  (e `acceptable` caes)  |  e <- excns  ]-      -- where-          -- x `nor` y = not (x || y)--- acceptable :: PropLiteral -> CAES -> Bool--- acceptable c caes@(CAES (_, _, standard))  -  -- = c `s` caes -  -- where P (_, s) = standard c--- \end{code}-\begin{code}-applicable :: Argument -> CAES -> Bool-applicable  (Arg (prems, excns, _)) -            caes@(CAES (_, (assumptions, _), _)) -  = and  $  [  p `elem` assumptions ||     -             (  negate p `notElem` assumptions &&-                p `acceptable` caes)  |  p <- prems  ]-            ++-            [  (e `notElem` assumptions) &&-             (  negate e `elem` assumptions ||-                not (e `acceptable` caes))  |  e <- excns  ]--acceptable :: PropLiteral -> CAES -> Bool-acceptable c caes@(CAES (_, _, standard))  -  = c `s` caes -  where s = psMap $ standard c- --\end{code}---\subsection{Proof standards}--Carneades predefines five proof standards, originating from the work of-Freeman and Farley \cite{Freeman96,Farley95}: \emph{scintilla of-evidence}, \emph{preponderance of the evidence}, \emph{clear and convincing-evidence}, \emph{beyond reasonable doubt} and \emph{dialectical-validity}. Some proof standards depend on constants such as $\alpha$, -$\beta$, $\gamma$; these are assumed to be defined once and globally.-This time, we proceed to give the definitions directly in Haskell,-as they really only are translitarations of the original definitions.--For a proposition $p$ to satisfy the weakest proof standard, scintilla of-evidence, there should be at least one applicable argument pro $p$ in the CAES:-\begin{code}-scintilla :: ProofStandard-scintilla p caes@(CAES (g, _, _))- = any (`applicable` caes) (getArgs p g)-\end{code}--Preponderance of the evidence additionally requires the maximum weight of-the applicable arguments pro $p$ to be greater than the maximum weight of the-applicable arguments con $p$. The weight of zero arguments is taken to-be 0. As the maximal weight of applicable arguments pro and con is a recurring-theme in the definitions of several of the proof standards, we start by-defining those notions:---\begin{code}-maxWeightApplicable :: [Argument] -> CAES -> Weight-maxWeightApplicable as caes@(CAES (_, (_, argWeight), _))- = foldl max 0 [argWeight a | a <- as, a `applicable` caes] --maxWeightPro :: PropLiteral -> CAES -> Weight-maxWeightPro p caes@(CAES (g, _, _))- = maxWeightApplicable (getArgs p g) caes--maxWeightCon :: PropLiteral -> CAES -> Weight-maxWeightCon p caes@(CAES (g, _, _))- = maxWeightApplicable (getArgs (negate p) g) caes-\end{code}-%-We can then define the proof standard preponderance:-%-\begin{code}-preponderance :: ProofStandard -preponderance p caes = maxWeightPro p caes > maxWeightCon p caes   -\end{code}---Clear and convincing evidence strengthen the preponderance constraints by-insisting that the difference between the maximal weights of the pro and con-arguments must be greater than a given positive constant $\beta$, and there-should furthermore be at least one applicable argument pro $p$ that is-stronger than a given positive constant $\alpha$:---\begin{code}-clear_and_convincing :: ProofStandard -clear_and_convincing p caes- =  (mwp > alpha) && (mwp - mwc > beta)-  where -    mwp  =  maxWeightPro p caes-    mwc  =  maxWeightCon p caes-\end{code}--Beyond reasonable doubt has one further requirement: the maximal-strength of an argument con $p$ must be less than a given positive-constant $\gamma$; i.e., there must be no reasonable doubt:-\begin{code}-beyond_reasonable_doubt :: ProofStandard -beyond_reasonable_doubt p caes- = clear_and_convincing p caes && (maxWeightCon p caes < gamma)-\end{code}--Finally dialectical validity requires at least one applicable argument pro $p$-and no applicable arguments con $p$:-\begin{code}-dialectical_validity :: ProofStandard -dialectical_validity p caes   -  = scintilla p caes && not (scintilla (negate p) caes)-\end{code}--%if False-Proof standard names can then be mapped to their according proof standard. --\begin{code}-psMap :: PSName -> ProofStandard -psMap Scintilla = scintilla-psMap Preponderance = preponderance-psMap ClearAndConvincing = clear_and_convincing-psMap BeyondReasonableDoubt = beyond_reasonable_doubt-psMap DialecticalValidity = dialectical_validity-\end{code}-%endif---\subsection{Convenience functions}-We provide a set of functions to facilitate construction of propositions,-arguments, argument sets and sets of assumptions. Together with the definitions-covered so far, this constitute our DSL for constructing Carneades-argumentation models.-\begin{spec}-mkProp         :: String -> PropLiteral                        -mkArg          :: [String] -> [String] -> String -> Argument   -mkArgSet       :: [Argument] -> ArgSet-mkAssumptions  :: [String] -> [PropLiteral]-\end{spec}-A string starting with a |'-'| is taken to denote a negative atomic-proposition.--To construct an audience, native Haskell tupling is used to combine-a set of assumptions and a weight function, exactly as it would be-done in the Carneades model:-\begin{spec}-audience :: Audience-audience = (assumptions, weight) -\end{spec}-Carneades Argument Evaluation Structures and weight functions are defined in-a similar way, as will be shown in the next subsection.--Finally, we provide a function for retrieving the arguments for a-specific proposition from an argument set, a couple of functions to-retrieve all arguments and propositions respectively from an argument-set, and functions to retrieve the (not) applicable arguments or (not)-acceptable propositions from a CAES:-\begin{spec}-getArgs             :: PropLiteral  -> ArgSet  ->  [Argument]-getAllArgs          :: ArgSet                  ->  [Argument]-getProps            :: ArgSet                  ->  [PropLiteral]-applicableArgs      :: CAES                    ->  [Argument]-nonApplicableArgs   :: CAES                    ->  [Argument]-acceptableProps     :: CAES                    ->  [PropLiteral]-nonAcceptableProps  :: CAES                    ->  [PropLiteral]-\end{spec}--\begin{code}-getAllArgs :: ArgSet -> [Argument]-getAllArgs g = nub $ concatMap (snd . snd) (labNodes g)--getProps :: ArgSet -> [PropLiteral]-getProps g = map (fst . snd) (labNodes g)--applicableArgs :: CAES -> [Argument]-applicableArgs c@(CAES (argSet, _, _)) = filter (`applicable` c) (getAllArgs argSet)  --nonApplicableArgs :: CAES -> [Argument]-nonApplicableArgs c@(CAES (argSet, _, _)) = filter (not . (`applicable` c)) (getAllArgs argSet)--acceptableProps :: CAES  -> [PropLiteral]-acceptableProps c@(CAES (argSet, _, _)) = filter (`acceptable` c) (getProps argSet)--nonAcceptableProps :: CAES  -> [PropLiteral]-nonAcceptableProps c@(CAES (argSet, _, _)) = filter (not . (`acceptable` c)) (getProps argSet)-\end{code}---\begin{code}-contextP :: PropLiteral -> AGraph -> [Context (PropLiteral, [Argument]) ()]-contextP p = gsel (\ (_, _, a, _) -> fst a == p) -     -getArgs :: PropLiteral -> AGraph -> [Argument]  -getArgs p g -  =  case contextP p g of-       []                          -> []-       ((_, _, (_, args), _) : _)  -> args-\end{code}----\subsection{Graph construction}-We associate a graph along with a |Map| that stores the node number for every |PropLiteral| to make construction of the |AGraph| easier.--\begin{code}-type AGraph = ArgSet-type PropNode = LNode (PropLiteral, [Argument])-type AssociatedGraph = (AGraph, Map PropLiteral Node)-\end{code}--An argument graph is then constructed as following:-\begin{code}-mkArgSet :: [Argument] -> ArgSet-mkArgSet = mkArgGraph--mkArgGraph :: [Argument] -> AGraph-mkArgGraph = fst . foldr addArgument (empty, Map.empty)-\end{code}--Carneades uses the following definition for acyclicity:-\begin{definition}[Acyclic set of arguments]-\label{def:carneadesacyclic}-A list of arguments is acyclic iff its corresponding dependency graph is acyclic. The corresponding dependency graph has nodes for every literal appearing in the list of arguments. A node $p$ has a directed link to node $q$ whenever $p$ depends on $q$ in the sense that there is an argument pro or con $p$ that has $q$ or $\overline{q}$ in its list of premises or exceptions.-\end{definition}--So when we add an argument |(Arg premises exceptions conclusion)| to our graph, we need to add both the conclusion and its negate to the graph, adding edges for both to all premises and exceptions while adding the argument to the list of arguments for |conclusion| as well. --\begin{code}-addArgument :: Argument -> AssociatedGraph -> AssociatedGraph-addArgument arg@(Arg (prem, exc, c)) gr  = -  let  deps             =  prem ++ exc-       (gr',  nodeNr)   =  addArgument' arg gr-       (gr'', nodeNr')  =  addNode (negate c) gr'-  in addEdges nodeNr' deps $ addEdges nodeNr deps gr'' -\end{code}---\begin{code}-addToContext :: Argument -> (Context (PropLiteral, [Argument]) (), AGraph) -> AGraph-addToContext arg ((adjb, n, (p, args), adja), g') = (adjb, n, (p, arg:args), adja) & g'--unsafeMatch :: Graph gr => Node -> gr a b -> (Context a b, gr a b)-unsafeMatch n g = mapFst fromJust $ match n g-\end{code}--Add an argument to the graph. If there is no node present yet for the conclusion insert it, in both cases add the argument to the context of the conclusion.-\begin{code}-addArgument' :: Argument -> AssociatedGraph -> (AssociatedGraph, Node)-addArgument' arg@(Arg (_, _, c)) (g, m) - = case Map.lookup c m of -       Nothing  ->  ((insNode (nodeNr, (c, [arg])) g, -                       Map.insert c nodeNr m), -                         nodeNr)-       Just n   ->  ((addToContext arg (unsafeMatch n g), -                       m), -                         n) -  where nodeNr = Map.size m + 1-\end{code}--Add a proposition to the graph.-\begin{code}-addNode :: PropLiteral -> AssociatedGraph -> (AssociatedGraph, Node)-addNode p gr@(g,m) - =  case Map.lookup p m of -       Nothing -> ((insNode (nodeNr, (p, [])) g, Map.insert p nodeNr m), nodeNr)-       Just n  -> (gr, n)-    where nodeNr = Map.size m + 1-\end{code}--For a specific node, add an edge for every |PropLiteral| in the list for the given graph.-\begin{code}-addEdges :: Node -> [PropLiteral] -> AssociatedGraph -> AssociatedGraph-addEdges n ps (g, m) = addEdges' n (map (fromJust . flip Map.lookup m') ps)  (g', m')-- addEdges' c n ps (g', m')- where  nodeNr    = Map.size m + 1 -        newProps  = filter ( (== Nothing) . flip Map.lookup m) ps  -        g'        = insNodes (propsToNodes newProps nodeNr) g-        m'        = Map.union m . Map.fromList $ zip newProps [nodeNr..]-\end{code}---Generate unlabelled edges from a |Node| to a list of |Node|s and add it to the graph.-\begin{code}-addEdges' :: Node -> [Node] -> AssociatedGraph -> AssociatedGraph-addEdges' c ps (g, m) = (insEdges edges' g, m)- where  edges' = map (genEdge c) ps-        genEdge k l = (k, l, ())--\end{code}--Some useful functions.-\begin{code}-propsToNodes :: [PropLiteral] -> Node -> [PropNode]-propsToNodes ps n = zip [n..] (map (\ p -> (p, [])) ps)--checkCycle :: AGraph -> Bool-checkCycle = cyclic--- Old definition using Graphalyze--- not . null . cyclesIn--mkProp :: String -> PropLiteral-mkProp ('-':s)  = mapFst not (mkProp s)-mkProp s        = (True, s)--mkAssumptions :: [String] -> [PropLiteral]-mkAssumptions = map mkProp--mkArg :: [String] -> [String] -> String -> Argument-mkArg ps es c = Arg (map mkProp ps, map mkProp es, mkProp c)-\end{code}--Globally predefined alpha, beta and gamma. -\begin{code}-alpha, beta, gamma :: Double-alpha  =  0.4-beta   =  0.3-gamma  =  0.2-\end{code}

@@ -1,11 +0,0 @@--- Based on initial code provided by Stefan Sabev-module Language.Carneades.Cyclic(cyclic) where-import Data.Graph.Inductive--cyclic :: (DynGraph g) => g a b -> Bool-cyclic g | not (null leafs) = cyclic (delNodes leafs g)-         | otherwise        = not (isEmpty g)-  where leafs = filter (isLeaf g) (nodes g)--isLeaf :: (DynGraph g) => g a b -> Node -> Bool-isLeaf g n = n `notElem` map fst (edges g)

@@ -1,181 +0,0 @@-%include arg-preamble.fmt--\begin{code}-module Language.Carneades.ExampleCAES where--import Prelude hiding (negate)-import Language.Carneades.CarneadesDSL-import Language.Carneades.Input-import System.Exit-import Control.Monad (when)-\end{code}----\subsection{Implementing a CAES}--This subsection shows how an argumentation theorist given the-Carneades DSL developed in this section quickly and at a high level of-abstraction can implement a Carneades argument evaluation structure-and evaluate it as well. We revisit the arguments from Section-\ref{sec:background} and assume the following:--\begin{align*}-\mathit{arguments} &= \{\mathit{arg1}, \mathit{arg2}, \mathit{arg3} \}, \\-\mathit{assumptions} &= \{\mathit{kill}, \mathit{witness}, \mathit{witness2}, \mathit{unreliable2} \},\\-\mathit{standard(intent)} &= \mathit{beyond}\textit{-}\mathit{reasonable}\textit{-}\mathit{doubt}, \\-\mathit{standard(x)} &= \mathit{scintilla},\ \textrm{for any other proposition x}, \\-\alpha &= 0.4,\ \beta = 0.3,\ \gamma = 0.2.-\end{align*}--Note that since alpha, beta and gamma are assumed they are global, they are predefined in |CarneadesDSL.lhs|.-----%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%Start example code%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%-\begin{spec}-alpha, beta, gamma :: Double-alpha  =  0.4-beta   =  0.3-gamma  =  0.2-\end{spec}---Arguments and the argument graph are constructed by calling |mkArg| and-|mkArgSet| respectively:-\begin{code}-arg1, arg2, arg3 :: Argument -arg1 = mkArg ["kill", "intent"] [] "murder"-arg2 = mkArg ["witness"] ["unreliable"] "intent"-arg3 = mkArg ["witness2"] ["unreliable2"] "-intent"--argSet :: ArgSet-argSet = mkArgSet [arg1, arg2, arg3]-\end{code}--The audience is implemented by defining the |weight| function and calling-|mkAssumptions| on the propositions which are to be assumed. The audience is-just a pair of these:---\begin{code}-weight :: ArgWeight-weight  arg  |  arg == arg1  = 0.8-weight  arg  |  arg == arg2  = 0.3-weight  arg  |  arg == arg3  = 0.8-weight  _                    = error "no weight assigned"--assumptions :: [PropLiteral]-assumptions = mkAssumptions ["kill", "witness", "witness2","unreliable2"] --audience :: Audience-audience = (assumptions, weight) -\end{code}--Finally, after assigning proof standards in the |standard| function, we form-the CAES from the argument graph, audience and function |standard|:-\begin{code}-standard :: PropStandard -standard  (_, "intent")  = BeyondReasonableDoubt -standard  _              = Scintilla --caes :: CAES -caes = CAES (argSet, audience, standard)-\end{code}--We can now try out the argumentation structure. --\begin{spec}-getAllArgs argSet- > [  ["witness2"]       ~["unreliable2"]   =>  "-intent",-      ["witness"]        ~["unreliable"]    =>  "intent",-      ["kill","intent"]  ~[]                =>  "murder"]-\end{spec}--Then, as expected, there are no applicable arguments for $\mathit{-intent}$, -since $\mathit{unreliable2}$ is an exception, but there is an applicable -argument for $\mathit{intent}$, namely $\mathit{arg2}$:---\begin{spec}-filter (`applicable` caes) $ getArgs (mkProp "intent") argSet- > [["witness"]=>"intent"]--filter (`applicable` caes) $ getArgs (mkProp "-intent") argSet- >  []-\end{spec}--Despite the applicable argument $\mathit{arg2}$ for $\mathit{intent}$,-$\mathit{murder}$ should not be acceptable, because the weight of-$\mathit{arg2} < \alpha$. However, note that we can't reach the opposite-conclusion either:--\begin{spec}-acceptable (mkProp "murder") caes- > False-acceptable (mkProp "-murder") caes- > False-\end{spec}--As a further extension, one could for example imagine giving an-argumentation theorist the means to see a trace of the derivation of-acceptability. It would be straightforward to add further primitives-to the DSL and keeping track of intermediate results for-acceptability and applicability to achieve this.--\begin{code}-testAppIntent :: [Argument]-testAppIntent = filter (`applicable` caes) $ getArgs (mkProp "intent") argSet        --testAppNotIntent :: [Argument]-testAppNotIntent = filter (`applicable` caes) $ getArgs (mkProp "-intent") argSet        --testAppMurder :: [Argument]-testAppMurder = filter (`applicable` caes) $ getArgs (mkProp "murder") argSet        --testAppNotMurder :: [Argument]-testAppNotMurder = filter (`applicable` caes) $ getArgs (mkProp "-murder") argSet        --testMurder  :: Bool-testMurder  = acceptable (mkProp "murder") caes--testNotMurder  :: Bool-testNotMurder  = acceptable (mkProp "-murder") caes-\end{code}--Assuming a file examplecaes.txt with the following input:---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"]---- Haskell style commments are allowed.--{- also valid for standards: -   standard "intent" BeyondReasonableDoubt -}--standard "kill" scintilla-standard "intent" beyond_reasonable_doubt---\begin{code}-parse :: IO ()-parse = do -           input <- readFile "examplecaes.txt"-           (CAES (argSet, (assumps, weight), standard)) <- case parseCAES input of -               Left err -> putStrLn "Parsing error: " >> print err >> exitWith (ExitFailure 1)-               Right caes -> return caes-           print $ getAllArgs argSet-           print assumps-           print $ standard (mkProp "intent")-\end{code}-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%End example code%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%-

@@ -1,224 +0,0 @@--- | This is the input module accompanying the implementation of Carneades.
---  It defines a simple parser for a Carneades Argument Evaluation Structure
--- (CAES). 
---
--- Files are assumed to have the following order of content:
--- one argument or attack on each line, ending
--- in a dot. (Our parser is slightly more relaxed than this and 
--- doesn't care about whitespace.)
---
--- @att(a1,a2).@ or @arg(a1).@
---
--- Argument names are assumed to consist only of letters and numbers.
--- Arguments used in attacks should be declared separately as well. 
---
--- For a complete example see <http://www.cs.nott.ac.uk/~bmv/Code/examplecaes.txt>
--- (also included as an additional source file) or see the accompanying 
--- ExampleCAES module.
-module Language.Carneades.Input
-  (
-   -- * Parsing functions
-   parseCAES, pCAES
-   )
- where
-import Language.Carneades.CarneadesDSL
-import Text.Parsec
-import Text.Parsec.String (Parser)
-import Text.Parsec.Char (char, string)
-import qualified Text.Parsec.Token as P
-import Text.Parsec.Language(haskellStyle)
-import Text.Parsec.Error(errorMessages, messageString)
-import Data.Either (partitionEithers)
-import Debug.Trace
-import Data.Maybe(fromMaybe)    
-
--- This allows the parsing of a CAES to have comments,
--- arguments consisting of a letter followed by alphanumerical characters, etc.
-lexer :: P.TokenParser ()
-lexer = P.makeTokenParser 
- (haskellStyle 
-    { P.reservedNames = ["Scintilla", "Preponderance", "ClearAndConvincing",
-                         "BeyondReasonableDoubt", "DialecticalValidity",
-                         "scintilla", "preponderance", "clear_and_convincing",
-                         "beyond_reasonable_doubt", "dialectical_validity"]
-    }
- )
-
-whiteSpace :: Parser ()
-whiteSpace = P.whiteSpace lexer
-
-identifier :: Parser String
-identifier = P.identifier lexer
-
-stringLiteral :: Parser String
-stringLiteral = P.stringLiteral lexer
-
-symbol :: String -> Parser String
-symbol = P.symbol lexer
-
-float :: Parser Double
-float = P.float lexer
-
--- A named Carneades argument.
-data Argument' = Arg' String ([PropLiteral], [PropLiteral], PropLiteral)
- deriving (Eq, Show)
-
--- A weight to a name of a Carneades argument.
-type Weight' = (String, Double)
-
--- A proof standard to a name of a Carneades argument.
-type Standard' = (String, PSName)
-
--- |An argument name consists of a letter followed by one or more letters and digits,
--- underscore or \'. Alternatively, a string literal.
-argName :: Parser String
-argName = try identifier <|> stringLiteral
-
--- |Parses a proposition by parsing an identifier and using 'mkProp' from the 
--- CarneadesDSL package. 
-pProposition :: Parser PropLiteral
-pProposition = do 
-                  p <- argName
-                  whiteSpace
-                  return (mkProp p)
-
--- |Parses a list of propositions. Propositions are separated by commas.
--- Optional whitespace is allowed in the list.
-pPropositions :: Parser [PropLiteral]
-pPropositions = do 
-                   char '[' >> whiteSpace
-                   ps <- pProposition `sepBy` (symbol "," >> whiteSpace)
-                   char ']' >> whiteSpace
-                   return ps
-
--- |Parses a complete argument consists of @arg@ or @argument@ followed by an
- -- @argName@, two lists of propositions, and a conclusion. 
-pArgument :: Parser Argument'
-pArgument = do 
-               try (string "argument") <|> string "arg"
-               whiteSpace
-               name <- argName
-               prems <- pPropositions
-               excs <- pPropositions
-               c <- pProposition
-               return (Arg' name (prems, excs, c))
-
--- |Parses one declaration of a weight. A weight is declared by the string 
--- @weight@ followed by the name of a previously declared argument,
--- and a 'Double' assigned to that argument.
-pWeight :: Parser Weight'
-pWeight = do
-             string "weight" >> whiteSpace
-             name <- argName
-             weight <- float
-             return (name, weight)
-
--- |Parses a list of assumptions. A list of assumptions is just the keyword 
--- @assumptions@ followed by a list of propositions.
-pAssumptions :: Parser Assumptions
-pAssumptions = do 
-                  string "assumptions" >> whiteSpace
-                  pPropositions
-
--- |Parses the name of a proof standard allowing both the names as given in 
--- the original paper and the constructors of PSName. 
-pPSName :: Parser PSName
-pPSName =  try ((try (string "Scintilla") <|> 
-                      string "scintilla") 
-                 >> return Scintilla) 
-       <|> try ((try (string "Preponderance") <|> 
-                      string "preponderance") 
-                 >> return Preponderance) 
-       <|> try ((try (string "ClearAndConvincing") <|> 
-                      string "clear_and_convincing") 
-                 >> return ClearAndConvincing) 
-       <|> try ((try (string "BeyondReasonableDoubt") <|> 
-                      string "beyond_reasonable_doubt") 
-                 >> return BeyondReasonableDoubt) 
-       <|> try ((try (string "DialecticalValidity") <|> 
-                      string "dialectical_validity") 
-                 >> return DialecticalValidity)
-       
--- |Parses one declaration of a proof standard.  A proof standard is declared 
--- by the string @standard@ followed by a proposition and the name of a proof 
--- standard.
-pStandard :: Parser Standard'
-pStandard = do 
-                string "standard"
-                whiteSpace
-                name <- argName
-                psName <- pPSName
-                whiteSpace
-                return (name, psName)
-
--- |Converts a named argument to the definition used in the implementation 
--- (and the paper).
-argToArg :: Argument' -> Argument
-argToArg (Arg' _ a) = Arg a
-
--- |Looks up a normal argument in a list of named argument and returns its name.
-lookupArg :: Argument -> [Argument'] -> Maybe String
-lookupArg a [] = Nothing 
-lookupArg a (Arg' name a' : args) 
- | a == Arg a' = Just name
- | otherwise = lookupArg a args
-
--- |Converts a list of named 'Argument\''s and named 'Weight\''s to a weight 
--- function. Arguments not assigned a weight will raise an error.
-weightToWeight :: [Argument'] -> [Weight'] -> ArgWeight
-weightToWeight args ws arg = 
- fromMaybe (error $ "no weight assigned to" ++ show arg)
-          (lookupArg arg args >>= \name -> lookup name ws) 
-
--- |Converts a list of named 'Standard\''s to a standard function.
--- Propositions not assigned a weight will raise an error.
-standardToStandard :: [Standard'] -> PropStandard
-standardToStandard [] p = error $ "no standard assigned to" ++ show p
-standardToStandard ((name, st) : sts) p 
- | mkProp name == p = st
- | otherwise        = standardToStandard sts p
-
--- |Parses the definition of a complete Carneades Argument Evaluation Structure
--- (CAES). 
--- 
--- A CAES is parsed in multiple stages: 
--- 
--- First parsing zero or more arguments: 
--- where a complete argument consists of @arg@ or @argument@ followed by an
--- @argName@ (a letter followed by one or more letters and digits,
--- underscore or \'; alternatively, a string literal), two lists of propositions,
--- and a conclusion. 
--- 
--- Then, zero or more weights, 
--- where a weight is declared by the string 
--- @weight@ followed by the name of a previously declared argument,
--- and a 'Double' assigned to that argument.
--- 
--- Then, a list of assumptions, 
--- where a list of assumptions is just the keyword 
--- @assumptions@ followed by a list of propositions.
---
--- Then a list of proof standard declarations,
--- where a proof standard is declared 
--- by the string @standard@ followed by a proposition and the name of a proof 
--- standard.
---
--- This is followed by an end of file token.
-pCAES :: Parser CAES
-pCAES = do 
-           whiteSpace
-           args <- many pArgument
-           weights <- many pWeight
-           assumps <- pAssumptions
-           standards <- many pStandard
-           eof
-           let weight = weightToWeight args weights
-           let audience = (assumps, weight) 
-           let standard = standardToStandard standards
-           let argSet = mkArgSet (map argToArg args)
-           return (CAES (argSet, audience, standard))
-
--- |Parses a 'String' containing a CAES. 
--- If parsing fails, it propagates the parse error.
-parseCAES :: String -> Either ParseError CAES
-parseCAES = parse pCAES ""

@@ -0,0 +1,54 @@+# CarneadesDSL++An implementation and domain-specific language for the+[Carneades argumentation model](https://carneades.github.io/).++## Synopsis++CarneadesDSL provides a Haskell DSL for constructing and evaluating+Carneades Argument Evaluation Structures (CAES). It supports five+predefined proof standards and includes a parser for external CAES+definitions.++## Usage++```haskell+import Language.Carneades.CarneadesDSL+import Language.Carneades.ExampleCAES (caes, argSet)++-- Construct propositions and arguments+let p = mkProp "intent"+let a = mkArg ["witness"] ["unreliable"] "intent"++-- Query a CAES+acceptable (mkProp "murder") caes   -- False+applicableArgs caes                 -- [applicable arguments]+```++## Parsing++CAES definitions can be parsed from text files:++```haskell+import Language.Carneades.Input (parseCAES)++main :: IO ()+main = do+  input <- readFile "examplecaes.txt"+  case parseCAES input of+    Left err   -> print err+    Right caes -> print (acceptableProps caes)+```++## References++See "Haskell Gets Argumentative" in the Proceedings of Symposium on+Trends in Functional Programming (TFP 2012) by Bas van Gijzel and+Henrik Nilsson.++For the papers accompanying this library see+[Google Scholar](https://scholar.google.com/citations?user=Xu4yjvwAAAAJ&hl).++## License++BSD-3-Clause (see [LICENSE](LICENSE))

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

@@ -0,0 +1,550 @@+%include arg-preamble.fmt++\begin{code}+module Language.Carneades.CarneadesDSL where++import Language.Carneades.Cyclic++import Prelude hiding (negate)++import Data.Graph.Inductive+import Data.Map (Map)+import Data.List(nub)+import qualified Data.Set as Set+import qualified Data.Map as Map+import Data.Maybe (fromJust)+\end{code}+++\subsection{Arguments}+As our ultimate goal is a DSL for argumentation theory, we strive for a+realisation in Haskell that mirrors the mathematical model of Carneades+argumentation framework as closely as possible. Ideally, there would be little+more to a realisation than a transliteration. We will thus proceed by+stating the central definitions of Carneades along with our realisation+of them in Haskell. ++\begin{definition}[Arguments]+\label{def:carneadesargs}+Let $\mathcal{L}$ be a propositional language. An \emph{argument} is a+tuple $\langle P, E, c \rangle$ where $P \subset \mathcal{L}$ are its+\emph{premises}, $E \subset \mathcal{L}$ with $P \cap E = \emptyset$+are its \emph{exceptions} and $c \in \mathcal{L}$ is its+\emph{conclusion}. For simplicity, all members of $\mathcal{L}$ +must be literals, i.e. either an atomic proposition or a negated+atomic proposition.  +An argument is said to be \emph{pro} its conclusion $c$ (which may be+a negative atomic proposition) and \emph{con} the negation of $c$.+\end{definition}++In Carneades all logical formulae are literals in propositional logic;+i.e., all propositions are either positive or negative atoms. Taking+atoms to be strings suffice in the following, and propositional literals can+then be formed by pairing this atom with a Boolean to denote whether+it is negated or not: +\begin{code} +type PropLiteral = (Bool, String)+\end{code}+We write $\overline{p}$ for the negation of a literal $p$. The realisation+is immediate:+\begin{code}+negate :: PropLiteral -> PropLiteral +negate (b, x) = (not b, x)+\end{code}++We chose to realise an \emph{argument} as a newtype (to allow a manual Eq instance)+containing a tuple of two lists of propositions, its \emph{premises} and its +\emph{exceptions}, and a proposition that denotes the \emph{conclusion}: +\begin{code}+newtype Argument = Arg ([PropLiteral], [PropLiteral], PropLiteral)+ deriving Ord +\end{code}++Arguments are considered equal if their premises, exceptions and+conclusion are equal; thus arguments are identified by their logical+content. The equality instance for |Argument| (omitted for brevity) takes+this into account by comparing the lists as sets.++\begin{code}+--Manual Eq instance for set equality on premises and exceptions+instance Eq Argument where+ (Arg (prems, excs, c)) == (Arg (prems', excs', c')) +    =  Set.fromList prems == Set.fromList prems'  && +       Set.fromList excs == Set.fromList excs'    && +       c == c'++showProp :: PropLiteral -> String+showProp (True, c)   = c+showProp (_    , c)  = '-' : c++instance Show Argument where + show (Arg (prems, excs, (True, c)))   = show (map showProp prems) ++ ' ' : '~' : show (map showProp excs) ++ "=>" ++ show c+ show (Arg (prems, excs, (_    , c)))  = show (map showProp prems) ++ ' ' : '~' : show (map showProp excs) ++ "=>" ++ show ('-' : c)+\end{code}+++A set of arguments determines how propositions depend on each other.+Carneades requires that there are no cycles among these dependencies. +Following Brewka and Gordon~\cite{Brewka10a}, we use a dependency+graph to determine acyclicity of a set of arguments.++\begin{definition}[Acyclic set of arguments]+\label{def:carneadesacyclic}+A set of \emph{arguments} is \emph{acyclic} iff its corresponding+dependency graph is acyclic. The corresponding dependency graph has a+node for every literal appearing in the set of arguments. A node $p$+has a link to node $q$ whenever $p$ depends on $q$ in the sense that+there is an argument pro or con $p$ that has $q$ or $\overline{q}$ in+its set of premises or exceptions.+\end{definition}++Our realisation of a set of arguments is considered abstract for DSL+purposes, only providing a check for acyclicity and a function to+retrieve arguments pro a proposition. We use FGL \cite{Erwig2001} to+implement the dependency graph, forming nodes for propositions and edges+for the dependencies. For simplicity, we opt to keep the graph+also as the representation of a set of arguments.+++\begin{code}+-- Note that for practical purposes we do not need to know the following +-- implementation but can use the abstraction further below+type ArgSet = Gr (PropLiteral, [Argument]) ()+\end{code}+++\begin{spec}+-- abstraction of ArgSet and the operating functions on it+type ArgSet = ...++getArgs     :: PropLiteral -> ArgSet -> [Argument]  +checkCycle  :: ArgSet -> Bool+\end{spec}+++\subsection{Carneades Argument Evaluation Structure}++The main structure of the argumentation model is called a Carneades+Argument Evaluation Structure (CAES):+\begin{definition}[Carneades Argument Evaluation Structure (CAES)] A+\emph{Carneades Argument Evaluation Structure} (CAES) is a triple+\[+\langle arguments, audience, standard \rangle+\]+where $arguments$ is an acyclic set of arguments, $audience$ is an audience as+defined below (Def.~\ref{def:carneadesaudience}), and \emph{standard} is a+total function mapping each proposition to to its specific proof standard. +\end{definition}+Note that propositions may be associated with \emph{different} proof+standards. This is considered a particular strength of the Carneades+framework. The transliteration into Haskell is almost immediate%+\footnote{Note that we use a newtype to prevent a cycle in the type+definitions.}:+\begin{code}+newtype CAES = CAES (ArgSet, Audience, PropStandard)+\end{code}++\begin{definition}[Audience]+\label{def:carneadesaudience}+Let $\mathcal{L}$ be a propositional language. An \emph{audience} is a+tuple $\langle$\emph{assumptions}, \emph{weight}$\rangle$, where+$assumptions \subset \mathcal{L}$ is a propositionally consistent set of+literals (i.e., not containing both a literal and its negation) assumed+to be acceptable by the audience and \emph{weight} is a function mapping+arguments to a real-valued weight in the range $[0,1]$.+\end{definition}+This definition is captured by the following Haskell definitions:+\begin{code}+type Audience = (Assumptions, ArgWeight)+type Assumptions = [PropLiteral]+type ArgWeight = Argument -> Weight+type Weight = Double+\end{code}++Further, as each proposition is associated with a specific proof standard,+we need a mapping from propositions to proof standards:+\begin{code}+type PropStandard = PropLiteral -> PSName++data PSName = Scintilla +  | Preponderance | ClearAndConvincing +  | BeyondReasonableDoubt | DialecticalValidity+ deriving (Show, Eq)+\end{code}++\begin{spec}+psMap :: PSName -> ProofStandard +\end{spec}++A proof standard is a function that given a proposition $p$, aggregates+arguments pro and con $p$ and decides whether it is acceptable or not:+\begin{code}+type ProofStandard = PropLiteral -> CAES -> Bool++newtype ProofStandardNamed = P (String, PropLiteral -> CAES -> Bool)+instance Eq ProofStandardNamed where+ P (l1, _) == P (l2, _) = l1 == l2+\end{code}+This aggregation process will be defined in detail in the next section,+but note that it is done relative to a specific CAES, and note the+cyclic dependence at the type level between |CAES| and |ProofStandard|.++The above definition of proof standard also demonstrates that+implementation in a typed language such as Haskell is a useful way of+verifying definitions from argumentation theoretic models. Our+implementation effort revealed that the original definition as given+in~\cite{Gordon09a} could not be realised as stated, because proof standards+in general not only depend on a set of arguments and the audience,+but may need the whole CAES.++\subsection{Evaluation}++Two concepts central to the evaluation of a CAES are+\emph{applicability of arguments}, which arguments should be+taken into account, and \emph{acceptability of propositions}, which+conclusions can be reached under the relevant proof standards, given+the beliefs of a specific audience.+\begin{definition}[Applicability of arguments]+Given a set of arguments and a set of assumptions (in an audience) in a CAES+$C$, then an argument $a = \langle P, E, c \rangle$ is+\emph{applicable} iff+\begin{itemize}+\item+    $p \in P$ implies $p$ is an assumption or [\,$\overline{p}$ is+    not an assumption and $p$ is acceptable in $C$\,] and+\item+    $e \in E$ implies $e$ is not an assumption and [\,$\overline{e}$+    is an assumption or $e$ is not acceptable in $C$\,].+\end{itemize}+\end{definition}+\begin{definition}[Acceptability of propositions]+Given a CAES $C$, a proposition $p$ is \emph{acceptable} in $C$ iff+$(s \; p \; C)$ is $true$, where $s$ is the proof standard for $p$.+\end{definition}++Note that these two definitions in general are mutually dependent+because acceptability depends on proof standards, and most sensible+proof standards depend on the applicability of arguments. This is the+reason that Carneades restricts the set of arguments to be acyclic. +(Specific proof standards are considered in the next section.)+The realisation of applicability and acceptability in Haskell is+straightforward:+-- \begin{code}+-- applicable :: Argument -> CAES -> Bool+-- applicable (Arg (prems, excns, _)) caes@(CAES (_, (assumptions, _), _)) +  -- = and  $  [(p `elem` assumptions)  ||     (p `acceptable` caes)  |  p <- prems  ]+            -- +++            -- [(e `elem` assumptions)  `nor`  (e `acceptable` caes)  |  e <- excns  ]+      -- where+          -- x `nor` y = not (x || y)+-- acceptable :: PropLiteral -> CAES -> Bool+-- acceptable c caes@(CAES (_, _, standard))  +  -- = c `s` caes +  -- where P (_, s) = standard c+-- \end{code}+\begin{code}+applicable :: Argument -> CAES -> Bool+applicable  (Arg (prems, excns, _)) +            caes@(CAES (_, (assumptions, _), _)) +  = and  $  [  p `elem` assumptions ||     +             (  negate p `notElem` assumptions &&+                p `acceptable` caes)  |  p <- prems  ]+            +++            [  (e `notElem` assumptions) &&+             (  negate e `elem` assumptions ||+                not (e `acceptable` caes))  |  e <- excns  ]++acceptable :: PropLiteral -> CAES -> Bool+acceptable c caes@(CAES (_, _, standard))  +  = c `s` caes +  where s = psMap $ standard c+ ++\end{code}+++\subsection{Proof standards}++Carneades predefines five proof standards, originating from the work of+Freeman and Farley \cite{Freeman96,Farley95}: \emph{scintilla of+evidence}, \emph{preponderance of the evidence}, \emph{clear and convincing+evidence}, \emph{beyond reasonable doubt} and \emph{dialectical+validity}. Some proof standards depend on constants such as $\alpha$, +$\beta$, $\gamma$; these are assumed to be defined once and globally.+This time, we proceed to give the definitions directly in Haskell,+as they really only are translitarations of the original definitions.++For a proposition $p$ to satisfy the weakest proof standard, scintilla of+evidence, there should be at least one applicable argument pro $p$ in the CAES:+\begin{code}+scintilla :: ProofStandard+scintilla p caes@(CAES (g, _, _))+ = any (`applicable` caes) (getArgs p g)+\end{code}++Preponderance of the evidence additionally requires the maximum weight of+the applicable arguments pro $p$ to be greater than the maximum weight of the+applicable arguments con $p$. The weight of zero arguments is taken to+be 0. As the maximal weight of applicable arguments pro and con is a recurring+theme in the definitions of several of the proof standards, we start by+defining those notions:+++\begin{code}+maxWeightApplicable :: [Argument] -> CAES -> Weight+maxWeightApplicable as caes@(CAES (_, (_, argWeight), _))+ = foldl max 0 [argWeight a | a <- as, a `applicable` caes] ++maxWeightPro :: PropLiteral -> CAES -> Weight+maxWeightPro p caes@(CAES (g, _, _))+ = maxWeightApplicable (getArgs p g) caes++maxWeightCon :: PropLiteral -> CAES -> Weight+maxWeightCon p caes@(CAES (g, _, _))+ = maxWeightApplicable (getArgs (negate p) g) caes+\end{code}+%+We can then define the proof standard preponderance:+%+\begin{code}+preponderance :: ProofStandard +preponderance p caes = maxWeightPro p caes > maxWeightCon p caes   +\end{code}+++Clear and convincing evidence strengthen the preponderance constraints by+insisting that the difference between the maximal weights of the pro and con+arguments must be greater than a given positive constant $\beta$, and there+should furthermore be at least one applicable argument pro $p$ that is+stronger than a given positive constant $\alpha$:+++\begin{code}+clear_and_convincing :: ProofStandard +clear_and_convincing p caes+ =  (mwp > alpha) && (mwp - mwc > beta)+  where +    mwp  =  maxWeightPro p caes+    mwc  =  maxWeightCon p caes+\end{code}++Beyond reasonable doubt has one further requirement: the maximal+strength of an argument con $p$ must be less than a given positive+constant $\gamma$; i.e., there must be no reasonable doubt:+\begin{code}+beyond_reasonable_doubt :: ProofStandard +beyond_reasonable_doubt p caes+ = clear_and_convincing p caes && (maxWeightCon p caes < gamma)+\end{code}++Finally dialectical validity requires at least one applicable argument pro $p$+and no applicable arguments con $p$:+\begin{code}+dialectical_validity :: ProofStandard +dialectical_validity p caes   +  = scintilla p caes && not (scintilla (negate p) caes)+\end{code}++%if False+Proof standard names can then be mapped to their according proof standard. ++\begin{code}+psMap :: PSName -> ProofStandard +psMap Scintilla = scintilla+psMap Preponderance = preponderance+psMap ClearAndConvincing = clear_and_convincing+psMap BeyondReasonableDoubt = beyond_reasonable_doubt+psMap DialecticalValidity = dialectical_validity+\end{code}+%endif+++\subsection{Convenience functions}+We provide a set of functions to facilitate construction of propositions,+arguments, argument sets and sets of assumptions. Together with the definitions+covered so far, this constitute our DSL for constructing Carneades+argumentation models.+\begin{spec}+mkProp         :: String -> PropLiteral                        +mkArg          :: [String] -> [String] -> String -> Argument   +mkArgSet       :: [Argument] -> ArgSet+mkAssumptions  :: [String] -> [PropLiteral]+\end{spec}+A string starting with a |'-'| is taken to denote a negative atomic+proposition.++To construct an audience, native Haskell tupling is used to combine+a set of assumptions and a weight function, exactly as it would be+done in the Carneades model:+\begin{spec}+audience :: Audience+audience = (assumptions, weight) +\end{spec}+Carneades Argument Evaluation Structures and weight functions are defined in+a similar way, as will be shown in the next subsection.++Finally, we provide a function for retrieving the arguments for a+specific proposition from an argument set, a couple of functions to+retrieve all arguments and propositions respectively from an argument+set, and functions to retrieve the (not) applicable arguments or (not)+acceptable propositions from a CAES:+\begin{spec}+getArgs             :: PropLiteral  -> ArgSet  ->  [Argument]+getAllArgs          :: ArgSet                  ->  [Argument]+getProps            :: ArgSet                  ->  [PropLiteral]+applicableArgs      :: CAES                    ->  [Argument]+nonApplicableArgs   :: CAES                    ->  [Argument]+acceptableProps     :: CAES                    ->  [PropLiteral]+nonAcceptableProps  :: CAES                    ->  [PropLiteral]+\end{spec}++\begin{code}+getAllArgs :: ArgSet -> [Argument]+getAllArgs g = nub $ concatMap (snd . snd) (labNodes g)++getProps :: ArgSet -> [PropLiteral]+getProps g = map (fst . snd) (labNodes g)++applicableArgs :: CAES -> [Argument]+applicableArgs c@(CAES (argSet, _, _)) = filter (`applicable` c) (getAllArgs argSet)  ++nonApplicableArgs :: CAES -> [Argument]+nonApplicableArgs c@(CAES (argSet, _, _)) = filter (not . (`applicable` c)) (getAllArgs argSet)++acceptableProps :: CAES  -> [PropLiteral]+acceptableProps c@(CAES (argSet, _, _)) = filter (`acceptable` c) (getProps argSet)++nonAcceptableProps :: CAES  -> [PropLiteral]+nonAcceptableProps c@(CAES (argSet, _, _)) = filter (not . (`acceptable` c)) (getProps argSet)+\end{code}+++\begin{code}+contextP :: PropLiteral -> AGraph -> [Context (PropLiteral, [Argument]) ()]+contextP p = gsel (\ (_, _, a, _) -> fst a == p) +     +getArgs :: PropLiteral -> AGraph -> [Argument]  +getArgs p g +  =  case contextP p g of+       []                          -> []+       ((_, _, (_, args), _) : _)  -> args+\end{code}++++\subsection{Graph construction}+We associate a graph along with a |Map| that stores the node number for every |PropLiteral| to make construction of the |AGraph| easier.++\begin{code}+type AGraph = ArgSet+type PropNode = LNode (PropLiteral, [Argument])+type AssociatedGraph = (AGraph, Map PropLiteral Node)+\end{code}++An argument graph is then constructed as following:+\begin{code}+mkArgSet :: [Argument] -> ArgSet+mkArgSet = mkArgGraph++mkArgGraph :: [Argument] -> AGraph+mkArgGraph = fst . foldr addArgument (empty, Map.empty)+\end{code}++Carneades uses the following definition for acyclicity:+\begin{definition}[Acyclic set of arguments]+\label{def:carneadesacyclic}+A list of arguments is acyclic iff its corresponding dependency graph is acyclic. The corresponding dependency graph has nodes for every literal appearing in the list of arguments. A node $p$ has a directed link to node $q$ whenever $p$ depends on $q$ in the sense that there is an argument pro or con $p$ that has $q$ or $\overline{q}$ in its list of premises or exceptions.+\end{definition}++So when we add an argument |(Arg premises exceptions conclusion)| to our graph, we need to add both the conclusion and its negate to the graph, adding edges for both to all premises and exceptions while adding the argument to the list of arguments for |conclusion| as well. ++\begin{code}+addArgument :: Argument -> AssociatedGraph -> AssociatedGraph+addArgument arg@(Arg (prem, exc, c)) gr  = +  let  deps             =  prem ++ exc+       (gr',  nodeNr)   =  addArgument' arg gr+       (gr'', nodeNr')  =  addNode (negate c) gr'+  in addEdges nodeNr' deps $ addEdges nodeNr deps gr'' +\end{code}+++\begin{code}+addToContext :: Argument -> (Context (PropLiteral, [Argument]) (), AGraph) -> AGraph+addToContext arg ((adjb, n, (p, args), adja), g') = (adjb, n, (p, arg:args), adja) & g'++unsafeMatch :: Graph gr => Node -> gr a b -> (Context a b, gr a b)+unsafeMatch n g = mapFst fromJust $ match n g+\end{code}++Add an argument to the graph. If there is no node present yet for the conclusion insert it, in both cases add the argument to the context of the conclusion.+\begin{code}+addArgument' :: Argument -> AssociatedGraph -> (AssociatedGraph, Node)+addArgument' arg@(Arg (_, _, c)) (g, m) + = case Map.lookup c m of +       Nothing  ->  ((insNode (nodeNr, (c, [arg])) g, +                       Map.insert c nodeNr m), +                         nodeNr)+       Just n   ->  ((addToContext arg (unsafeMatch n g), +                       m), +                         n) +  where nodeNr = Map.size m + 1+\end{code}++Add a proposition to the graph.+\begin{code}+addNode :: PropLiteral -> AssociatedGraph -> (AssociatedGraph, Node)+addNode p gr@(g,m) + =  case Map.lookup p m of +       Nothing -> ((insNode (nodeNr, (p, [])) g, Map.insert p nodeNr m), nodeNr)+       Just n  -> (gr, n)+    where nodeNr = Map.size m + 1+\end{code}++For a specific node, add an edge for every |PropLiteral| in the list for the given graph.+\begin{code}+addEdges :: Node -> [PropLiteral] -> AssociatedGraph -> AssociatedGraph+addEdges n ps (g, m) = addEdges' n (map (fromJust . flip Map.lookup m') ps)  (g', m')-- addEdges' c n ps (g', m')+ where  nodeNr    = Map.size m + 1 +        newProps  = filter ( (== Nothing) . flip Map.lookup m) ps  +        g'        = insNodes (propsToNodes newProps nodeNr) g+        m'        = Map.union m . Map.fromList $ zip newProps [nodeNr..]+\end{code}+++Generate unlabelled edges from a |Node| to a list of |Node|s and add it to the graph.+\begin{code}+addEdges' :: Node -> [Node] -> AssociatedGraph -> AssociatedGraph+addEdges' c ps (g, m) = (insEdges edges' g, m)+ where  edges' = map (genEdge c) ps+        genEdge k l = (k, l, ())++\end{code}++Some useful functions.+\begin{code}+propsToNodes :: [PropLiteral] -> Node -> [PropNode]+propsToNodes ps n = zip [n..] (map (\ p -> (p, [])) ps)++checkCycle :: AGraph -> Bool+checkCycle = cyclic+-- Old definition using Graphalyze+-- not . null . cyclesIn++mkProp :: String -> PropLiteral+mkProp ('-':s)  = mapFst not (mkProp s)+mkProp s        = (True, s)++mkAssumptions :: [String] -> [PropLiteral]+mkAssumptions = map mkProp++mkArg :: [String] -> [String] -> String -> Argument+mkArg ps es c = Arg (map mkProp ps, map mkProp es, mkProp c)+\end{code}++Globally predefined alpha, beta and gamma. +\begin{code}+alpha, beta, gamma :: Double+alpha  =  0.4+beta   =  0.3+gamma  =  0.2+\end{code}

@@ -0,0 +1,181 @@+%include arg-preamble.fmt++\begin{code}+module Language.Carneades.ExampleCAES where++import Prelude hiding (negate)+import Language.Carneades.CarneadesDSL+import Language.Carneades.Input+import System.Exit+import Control.Monad (when)+\end{code}++++\subsection{Implementing a CAES}++This subsection shows how an argumentation theorist given the+Carneades DSL developed in this section quickly and at a high level of+abstraction can implement a Carneades argument evaluation structure+and evaluate it as well. We revisit the arguments from Section+\ref{sec:background} and assume the following:++\begin{align*}+\mathit{arguments} &= \{\mathit{arg1}, \mathit{arg2}, \mathit{arg3} \}, \\+\mathit{assumptions} &= \{\mathit{kill}, \mathit{witness}, \mathit{witness2}, \mathit{unreliable2} \},\\+\mathit{standard(intent)} &= \mathit{beyond}\textit{-}\mathit{reasonable}\textit{-}\mathit{doubt}, \\+\mathit{standard(x)} &= \mathit{scintilla},\ \textrm{for any other proposition x}, \\+\alpha &= 0.4,\ \beta = 0.3,\ \gamma = 0.2.+\end{align*}++Note that since alpha, beta and gamma are assumed they are global, they are predefined in |CarneadesDSL.lhs|.+++++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%Start example code%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+\begin{spec}+alpha, beta, gamma :: Double+alpha  =  0.4+beta   =  0.3+gamma  =  0.2+\end{spec}+++Arguments and the argument graph are constructed by calling |mkArg| and+|mkArgSet| respectively:+\begin{code}+arg1, arg2, arg3 :: Argument +arg1 = mkArg ["kill", "intent"] [] "murder"+arg2 = mkArg ["witness"] ["unreliable"] "intent"+arg3 = mkArg ["witness2"] ["unreliable2"] "-intent"++argSet :: ArgSet+argSet = mkArgSet [arg1, arg2, arg3]+\end{code}++The audience is implemented by defining the |weight| function and calling+|mkAssumptions| on the propositions which are to be assumed. The audience is+just a pair of these:+++\begin{code}+weight :: ArgWeight+weight  arg  |  arg == arg1  = 0.8+weight  arg  |  arg == arg2  = 0.3+weight  arg  |  arg == arg3  = 0.8+weight  _                    = error "no weight assigned"++assumptions :: [PropLiteral]+assumptions = mkAssumptions ["kill", "witness", "witness2","unreliable2"] ++audience :: Audience+audience = (assumptions, weight) +\end{code}++Finally, after assigning proof standards in the |standard| function, we form+the CAES from the argument graph, audience and function |standard|:+\begin{code}+standard :: PropStandard +standard  (_, "intent")  = BeyondReasonableDoubt +standard  _              = Scintilla ++caes :: CAES +caes = CAES (argSet, audience, standard)+\end{code}++We can now try out the argumentation structure. ++\begin{spec}+getAllArgs argSet+ > [  ["witness2"]       ~["unreliable2"]   =>  "-intent",+      ["witness"]        ~["unreliable"]    =>  "intent",+      ["kill","intent"]  ~[]                =>  "murder"]+\end{spec}++Then, as expected, there are no applicable arguments for $\mathit{-intent}$, +since $\mathit{unreliable2}$ is an exception, but there is an applicable +argument for $\mathit{intent}$, namely $\mathit{arg2}$:+++\begin{spec}+filter (`applicable` caes) $ getArgs (mkProp "intent") argSet+ > [["witness"]=>"intent"]++filter (`applicable` caes) $ getArgs (mkProp "-intent") argSet+ >  []+\end{spec}++Despite the applicable argument $\mathit{arg2}$ for $\mathit{intent}$,+$\mathit{murder}$ should not be acceptable, because the weight of+$\mathit{arg2} < \alpha$. However, note that we can't reach the opposite+conclusion either:++\begin{spec}+acceptable (mkProp "murder") caes+ > False+acceptable (mkProp "-murder") caes+ > False+\end{spec}++As a further extension, one could for example imagine giving an+argumentation theorist the means to see a trace of the derivation of+acceptability. It would be straightforward to add further primitives+to the DSL and keeping track of intermediate results for+acceptability and applicability to achieve this.++\begin{code}+testAppIntent :: [Argument]+testAppIntent = filter (`applicable` caes) $ getArgs (mkProp "intent") argSet        ++testAppNotIntent :: [Argument]+testAppNotIntent = filter (`applicable` caes) $ getArgs (mkProp "-intent") argSet        ++testAppMurder :: [Argument]+testAppMurder = filter (`applicable` caes) $ getArgs (mkProp "murder") argSet        ++testAppNotMurder :: [Argument]+testAppNotMurder = filter (`applicable` caes) $ getArgs (mkProp "-murder") argSet        ++testMurder  :: Bool+testMurder  = acceptable (mkProp "murder") caes++testNotMurder  :: Bool+testNotMurder  = acceptable (mkProp "-murder") caes+\end{code}++Assuming a file examplecaes.txt with the following input:+++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"]++-- Haskell style commments are allowed.++{- also valid for standards: +   standard "intent" BeyondReasonableDoubt -}++standard "kill" scintilla+standard "intent" beyond_reasonable_doubt+++\begin{code}+parse :: IO ()+parse = do +           input <- readFile "examplecaes.txt"+           (CAES (argSet, (assumps, weight), standard)) <- case parseCAES input of +               Left err -> putStrLn "Parsing error: " >> print err >> exitWith (ExitFailure 1)+               Right caes -> return caes+           print $ getAllArgs argSet+           print assumps+           print $ standard (mkProp "intent")+\end{code}+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%End example code%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+

@@ -1,19 +1,19 @@-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"]
-
--- Haskell style commments are allowed.
-
-{- also valid for standards: 
-   standard "intent" BeyondReasonableDoubt -}
-
-standard "kill" scintilla
-standard "intent" beyond_reasonable_doubt
-
-
+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"]++-- Haskell style commments are allowed.++{- also valid for standards: +   standard "intent" BeyondReasonableDoubt -}++standard "kill" scintilla+standard "intent" beyond_reasonable_doubt++

@@ -0,0 +1,307 @@+-- | An implementation and DSL for the Carneades argumentation model.+--+-- See \"Haskell Gets Argumentative\" in the Proceedings of Symposium on+-- Trends in Functional Programming (TFP 2012) by Bas van Gijzel and+-- Henrik Nilsson.+--+-- For the literate Haskell source with full definitions, see+-- @doc\/CarneadesDSL.lhs@.+module Language.Carneades.CarneadesDSL where++import Language.Carneades.Cyclic++import Prelude hiding (negate)++import Data.Graph.Inductive+import Data.Map (Map)+import Data.List (nub)+import qualified Data.Set as Set+import qualified Data.Map as Map+import Data.Maybe (fromJust)++-- $arguments+-- In Carneades all logical formulae are literals in propositional logic;+-- i.e., all propositions are either positive or negative atoms. Taking+-- atoms to be strings suffices, and propositional literals can then be+-- formed by pairing this atom with a 'Bool' to denote whether it is+-- negated or not.++-- | A propositional literal is a pair of a polarity and a name.+type PropLiteral = (Bool, String)++-- | Negate a propositional literal.+negate :: PropLiteral -> PropLiteral+negate (b, x) = (not b, x)++-- | An argument is a tuple of premises, exceptions, and a conclusion.+-- Arguments are considered equal if their premises, exceptions and+-- conclusion are equal (comparing lists as sets).+newtype Argument = Arg ([PropLiteral], [PropLiteral], PropLiteral)+ deriving Ord++-- Manual Eq instance for set equality on premises and exceptions+instance Eq Argument where+ (Arg (prems, excs, c)) == (Arg (prems', excs', c'))+    =  Set.fromList prems == Set.fromList prems'  &&+       Set.fromList excs == Set.fromList excs'    &&+       c == c'++-- | Show a propositional literal as a string, prefixing negative+-- literals with @-@.+showProp :: PropLiteral -> String+showProp (True, c)   = c+showProp (_    , c)  = '-' : c++instance Show Argument where+ show (Arg (prems, excs, (True, c)))   = show (map showProp prems) ++ ' ' : '~' : show (map showProp excs) ++ "=>" ++ show c+ show (Arg (prems, excs, (_    , c)))  = show (map showProp prems) ++ ' ' : '~' : show (map showProp excs) ++ "=>" ++ show ('-' : c)++-- $caes+-- A Carneades Argument Evaluation Structure ('CAES') is a triple of an+-- acyclic set of arguments, an audience, and a mapping from propositions+-- to proof standards.++-- | An acyclic set of arguments represented as an FGL graph.+type ArgSet = Gr (PropLiteral, [Argument]) ()++-- | A Carneades Argument Evaluation Structure.+newtype CAES = CAES (ArgSet, Audience, PropStandard)++-- | An audience is a pair of assumptions and a weight function.+type Audience = (Assumptions, ArgWeight)++-- | A list of assumed propositional literals.+type Assumptions = [PropLiteral]++-- | A function mapping arguments to weights in the range @[0,1]@.+type ArgWeight = Argument -> Weight++-- | A weight is a 'Double'.+type Weight = Double++-- | A mapping from propositions to proof standard names.+type PropStandard = PropLiteral -> PSName++-- | Names of the five predefined proof standards.+data PSName = Scintilla+  | Preponderance | ClearAndConvincing+  | BeyondReasonableDoubt | DialecticalValidity+ deriving (Show, Eq)++-- | A proof standard decides, given a proposition and a CAES, whether the+-- proposition is acceptable.+type ProofStandard = PropLiteral -> CAES -> Bool++-- | A named proof standard, with equality based on the name.+newtype ProofStandardNamed = P (String, PropLiteral -> CAES -> Bool)+instance Eq ProofStandardNamed where+ P (l1, _) == P (l2, _) = l1 == l2++-- $evaluation+-- Two concepts central to evaluation: /applicability/ of arguments and+-- /acceptability/ of propositions.++-- | An argument is applicable in a CAES when all premises are assumed or+-- acceptable, and all exceptions are neither assumed nor acceptable.+applicable :: Argument -> CAES -> Bool+applicable  (Arg (prems, excns, _))+            caes@(CAES (_, (assumptions, _), _))+  = and  $  [  p `elem` assumptions ||+             (  negate p `notElem` assumptions &&+                p `acceptable` caes)  |  p <- prems  ]+            +++            [  (e `notElem` assumptions) &&+             (  negate e `elem` assumptions ||+                not (e `acceptable` caes))  |  e <- excns  ]++-- | A proposition is acceptable in a CAES when it satisfies its+-- associated proof standard.+acceptable :: PropLiteral -> CAES -> Bool+acceptable c caes@(CAES (_, _, standard))+  = c `s` caes+  where s = psMap $ standard c++-- $proofstandards+-- Carneades predefines five proof standards.++-- | Scintilla of evidence: at least one applicable argument pro.+scintilla :: ProofStandard+scintilla p caes@(CAES (g, _, _))+ = any (`applicable` caes) (getArgs p g)++-- | Maximum weight among applicable arguments.+maxWeightApplicable :: [Argument] -> CAES -> Weight+maxWeightApplicable as caes@(CAES (_, (_, argWeight), _))+ = foldl max 0 [argWeight a | a <- as, a `applicable` caes]++-- | Maximum weight of applicable arguments pro a proposition.+maxWeightPro :: PropLiteral -> CAES -> Weight+maxWeightPro p caes@(CAES (g, _, _))+ = maxWeightApplicable (getArgs p g) caes++-- | Maximum weight of applicable arguments con a proposition.+maxWeightCon :: PropLiteral -> CAES -> Weight+maxWeightCon p caes@(CAES (g, _, _))+ = maxWeightApplicable (getArgs (negate p) g) caes++-- | Preponderance: max weight pro exceeds max weight con.+preponderance :: ProofStandard+preponderance p caes = maxWeightPro p caes > maxWeightCon p caes++-- | Clear and convincing evidence: preponderance plus minimum+-- thresholds on weight and difference.+clear_and_convincing :: ProofStandard+clear_and_convincing p caes+ =  (mwp > alpha) && (mwp - mwc > beta)+  where+    mwp  =  maxWeightPro p caes+    mwc  =  maxWeightCon p caes++-- | Beyond reasonable doubt: clear and convincing plus max weight+-- con must be below gamma.+beyond_reasonable_doubt :: ProofStandard+beyond_reasonable_doubt p caes+ = clear_and_convincing p caes && (maxWeightCon p caes < gamma)++-- | Dialectical validity: at least one applicable argument pro and+-- no applicable arguments con.+dialectical_validity :: ProofStandard+dialectical_validity p caes+  = scintilla p caes && not (scintilla (negate p) caes)++-- | Map proof standard names to their implementation.+psMap :: PSName -> ProofStandard+psMap Scintilla = scintilla+psMap Preponderance = preponderance+psMap ClearAndConvincing = clear_and_convincing+psMap BeyondReasonableDoubt = beyond_reasonable_doubt+psMap DialecticalValidity = dialectical_validity++-- $convenience+-- Functions to facilitate construction of propositions, arguments,+-- argument sets and assumptions.++-- | Retrieve all arguments from an argument set.+getAllArgs :: ArgSet -> [Argument]+getAllArgs g = nub $ concatMap (snd . snd) (labNodes g)++-- | Retrieve all propositions from an argument set.+getProps :: ArgSet -> [PropLiteral]+getProps g = map (fst . snd) (labNodes g)++-- | Retrieve all applicable arguments from a CAES.+applicableArgs :: CAES -> [Argument]+applicableArgs c@(CAES (argSet, _, _)) = filter (`applicable` c) (getAllArgs argSet)++-- | Retrieve all non-applicable arguments from a CAES.+nonApplicableArgs :: CAES -> [Argument]+nonApplicableArgs c@(CAES (argSet, _, _)) = filter (not . (`applicable` c)) (getAllArgs argSet)++-- | Retrieve all acceptable propositions from a CAES.+acceptableProps :: CAES  -> [PropLiteral]+acceptableProps c@(CAES (argSet, _, _)) = filter (`acceptable` c) (getProps argSet)++-- | Retrieve all non-acceptable propositions from a CAES.+nonAcceptableProps :: CAES  -> [PropLiteral]+nonAcceptableProps c@(CAES (argSet, _, _)) = filter (not . (`acceptable` c)) (getProps argSet)++contextP :: PropLiteral -> AGraph -> [Context (PropLiteral, [Argument]) ()]+contextP p = gsel (\ (_, _, a, _) -> fst a == p)++-- | Retrieve the arguments for a specific proposition from an argument set.+getArgs :: PropLiteral -> AGraph -> [Argument]+getArgs p g+  =  case contextP p g of+       []                          -> []+       ((_, _, (_, args), _) : _)  -> args++-- $graph+-- Graph construction internals.++-- | Synonym for 'ArgSet'.+type AGraph = ArgSet++-- | A labelled node in the argument graph.+type PropNode = LNode (PropLiteral, [Argument])++-- | An argument graph paired with a map from propositions to node numbers.+type AssociatedGraph = (AGraph, Map PropLiteral Node)++-- | Construct an acyclic argument set from a list of arguments.+mkArgSet :: [Argument] -> ArgSet+mkArgSet = mkArgGraph++mkArgGraph :: [Argument] -> AGraph+mkArgGraph = fst . foldr addArgument (empty, Map.empty)++addArgument :: Argument -> AssociatedGraph -> AssociatedGraph+addArgument arg@(Arg (prem, exc, c)) gr  =+  let  deps             =  prem ++ exc+       (gr',  nodeNr)   =  addArgument' arg gr+       (gr'', nodeNr')  =  addNode (negate c) gr'+  in addEdges nodeNr' deps $ addEdges nodeNr deps gr''++addToContext :: Argument -> (Context (PropLiteral, [Argument]) (), AGraph) -> AGraph+addToContext arg ((adjb, n, (p, args), adja), g') = (adjb, n, (p, arg:args), adja) & g'++unsafeMatch :: Graph gr => Node -> gr a b -> (Context a b, gr a b)+unsafeMatch n g = mapFst fromJust $ match n g++addArgument' :: Argument -> AssociatedGraph -> (AssociatedGraph, Node)+addArgument' arg@(Arg (_, _, c)) (g, m)+ = case Map.lookup c m of+       Nothing  ->  ((insNode (nodeNr, (c, [arg])) g,+                       Map.insert c nodeNr m),+                         nodeNr)+       Just n   ->  ((addToContext arg (unsafeMatch n g),+                       m),+                         n)+  where nodeNr = Map.size m + 1++addNode :: PropLiteral -> AssociatedGraph -> (AssociatedGraph, Node)+addNode p gr@(g,m)+ =  case Map.lookup p m of+       Nothing -> ((insNode (nodeNr, (p, [])) g, Map.insert p nodeNr m), nodeNr)+       Just n  -> (gr, n)+    where nodeNr = Map.size m + 1++addEdges :: Node -> [PropLiteral] -> AssociatedGraph -> AssociatedGraph+addEdges n ps (g, m) = addEdges' n (map (fromJust . flip Map.lookup m') ps)  (g', m')+ where  nodeNr    = Map.size m + 1+        newProps  = filter ( (== Nothing) . flip Map.lookup m) ps+        g'        = insNodes (propsToNodes newProps nodeNr) g+        m'        = Map.union m . Map.fromList $ zip newProps [nodeNr..]++addEdges' :: Node -> [Node] -> AssociatedGraph -> AssociatedGraph+addEdges' c ps (g, m) = (insEdges edges' g, m)+ where  edges' = map (genEdge c) ps+        genEdge k l = (k, l, ())++propsToNodes :: [PropLiteral] -> Node -> [PropNode]+propsToNodes ps n = zip [n..] (map (\ p -> (p, [])) ps)++-- | Check whether an argument graph is cyclic.+checkCycle :: AGraph -> Bool+checkCycle = cyclic++-- | Construct a 'PropLiteral' from a string. A leading @-@ denotes+-- a negative literal.+mkProp :: String -> PropLiteral+mkProp ('-':s)  = mapFst not (mkProp s)+mkProp s        = (True, s)++-- | Construct a list of assumptions from a list of strings.+mkAssumptions :: [String] -> [PropLiteral]+mkAssumptions = map mkProp++-- | Construct an 'Argument' from lists of premise, exception, and+-- conclusion strings.+mkArg :: [String] -> [String] -> String -> Argument+mkArg ps es c = Arg (map mkProp ps, map mkProp es, mkProp c)++-- | Globally predefined alpha, beta and gamma thresholds for proof+-- standards.+alpha, beta, gamma :: Double+alpha  =  0.4+beta   =  0.3+gamma  =  0.2

@@ -0,0 +1,11 @@+-- Based on initial code provided by Stefan Sabev+module Language.Carneades.Cyclic(cyclic) where+import Data.Graph.Inductive++cyclic :: (DynGraph g) => g a b -> Bool+cyclic g | not (null leafs) = cyclic (delNodes leafs g)+         | otherwise        = not (isEmpty g)+  where leafs = filter (isLeaf g) (nodes g)++isLeaf :: (DynGraph g) => g a b -> Node -> Bool+isLeaf g n = n `notElem` map fst (edges g)

@@ -0,0 +1,95 @@+-- | Example Carneades Argument Evaluation Structure.+--+-- Demonstrates how to construct and evaluate a CAES using the DSL.+-- For the literate Haskell source with full definitions, see+-- @doc\/ExampleCAES.lhs@.+module Language.Carneades.ExampleCAES where++import Prelude hiding (negate)+import Language.Carneades.CarneadesDSL+import Language.Carneades.Input++-- $example+-- We revisit the murder example from the paper and assume the following:+--+-- * @arguments = {arg1, arg2, arg3}@+-- * @assumptions = {kill, witness, witness2, unreliable2}@+-- * @standard(intent) = beyond-reasonable-doubt@+-- * @standard(x) = scintilla@ for any other proposition @x@+-- * @alpha = 0.4, beta = 0.3, gamma = 0.2@++-- | Argument: kill and intent imply murder.+arg1 :: Argument+arg1 = mkArg ["kill", "intent"] [] "murder"++-- | Argument: witness testimony supports intent (exception: unreliable).+arg2 :: Argument+arg2 = mkArg ["witness"] ["unreliable"] "intent"++-- | Argument: second witness testimony opposes intent (exception: unreliable2).+arg3 :: Argument+arg3 = mkArg ["witness2"] ["unreliable2"] "-intent"++-- | The argument set containing all three arguments.+argSet :: ArgSet+argSet = mkArgSet [arg1, arg2, arg3]++-- | Weight function assigning weights to arguments.+weight :: ArgWeight+weight  arg  |  arg == arg1  = 0.8+weight  arg  |  arg == arg2  = 0.3+weight  arg  |  arg == arg3  = 0.8+weight  _                    = error "no weight assigned"++-- | The assumed propositions.+assumptions :: [PropLiteral]+assumptions = mkAssumptions ["kill", "witness", "witness2","unreliable2"]++-- | The audience combining assumptions and weight function.+audience :: Audience+audience = (assumptions, weight)++-- | Proof standard mapping: intent requires beyond reasonable doubt,+-- everything else requires scintilla.+standard :: PropStandard+standard  (_, "intent")  = BeyondReasonableDoubt+standard  _              = Scintilla++-- | The complete CAES.+caes :: CAES+caes = CAES (argSet, audience, standard)++-- | Applicable arguments for intent.+testAppIntent :: [Argument]+testAppIntent = filter (`applicable` caes) $ getArgs (mkProp "intent") argSet++-- | Applicable arguments for -intent.+testAppNotIntent :: [Argument]+testAppNotIntent = filter (`applicable` caes) $ getArgs (mkProp "-intent") argSet++-- | Applicable arguments for murder.+testAppMurder :: [Argument]+testAppMurder = filter (`applicable` caes) $ getArgs (mkProp "murder") argSet++-- | Applicable arguments for -murder.+testAppNotMurder :: [Argument]+testAppNotMurder = filter (`applicable` caes) $ getArgs (mkProp "-murder") argSet++-- | Whether murder is acceptable.+testMurder  :: Bool+testMurder  = acceptable (mkProp "murder") caes++-- | Whether -murder is acceptable.+testNotMurder  :: Bool+testNotMurder  = acceptable (mkProp "-murder") caes++-- | Parse and display the example CAES file.+parse :: IO ()+parse = do+           input <- readFile "examplecaes.txt"+           (CAES (argSet', (assumps, _weight), standard')) <- case parseCAES input of+               Left err -> fail $ "Parsing error: " ++ show err+               Right res -> return res+           print $ getAllArgs argSet'+           print assumps+           print $ standard' (mkProp "intent")

@@ -0,0 +1,219 @@+-- | This is the input module accompanying the implementation of Carneades.+--  It defines a simple parser for a Carneades Argument Evaluation Structure+-- (CAES). +--+-- Files are assumed to have the following order of content:+-- one argument or attack on each line, ending+-- in a dot. (Our parser is slightly more relaxed than this and +-- doesn't care about whitespace.)+--+-- @att(a1,a2).@ or @arg(a1).@+--+-- Argument names are assumed to consist only of letters and numbers.+-- Arguments used in attacks should be declared separately as well. +--+-- For a complete example see the included @examplecaes.txt@ file or+-- the accompanying ExampleCAES module.+module Language.Carneades.Input+  (+   -- * Parsing functions+   parseCAES, pCAES+   )+ where+import Language.Carneades.CarneadesDSL+import Text.Parsec+import Text.Parsec.String (Parser)+import qualified Text.Parsec.Token as P+import Text.Parsec.Language (haskellStyle)+import Data.Maybe(fromMaybe)++-- This allows the parsing of a CAES to have comments,+-- arguments consisting of a letter followed by alphanumerical characters, etc.+lexer :: P.TokenParser ()+lexer = P.makeTokenParser + (haskellStyle +    { P.reservedNames = ["Scintilla", "Preponderance", "ClearAndConvincing",+                         "BeyondReasonableDoubt", "DialecticalValidity",+                         "scintilla", "preponderance", "clear_and_convincing",+                         "beyond_reasonable_doubt", "dialectical_validity"]+    }+ )++whiteSpace :: Parser ()+whiteSpace = P.whiteSpace lexer++identifier :: Parser String+identifier = P.identifier lexer++stringLiteral :: Parser String+stringLiteral = P.stringLiteral lexer++symbol :: String -> Parser String+symbol = P.symbol lexer++float :: Parser Double+float = P.float lexer++-- A named Carneades argument.+data Argument' = Arg' String ([PropLiteral], [PropLiteral], PropLiteral)+ deriving (Eq, Show)++-- A weight to a name of a Carneades argument.+type Weight' = (String, Double)++-- A proof standard to a name of a Carneades argument.+type Standard' = (String, PSName)++-- |An argument name consists of a letter followed by one or more letters and digits,+-- underscore or \'. Alternatively, a string literal.+argName :: Parser String+argName = try identifier <|> stringLiteral++-- |Parses a proposition by parsing an identifier and using 'mkProp' from the +-- CarneadesDSL package. +pProposition :: Parser PropLiteral+pProposition = do +                  p <- argName+                  whiteSpace+                  return (mkProp p)++-- |Parses a list of propositions. Propositions are separated by commas.+-- Optional whitespace is allowed in the list.+pPropositions :: Parser [PropLiteral]+pPropositions = do+                   _ <- char '[' >> whiteSpace+                   ps <- pProposition `sepBy` (symbol "," >> whiteSpace)+                   _ <- char ']' >> whiteSpace+                   return ps++-- |Parses a complete argument consists of @arg@ or @argument@ followed by an+ -- @argName@, two lists of propositions, and a conclusion. +pArgument :: Parser Argument'+pArgument = do+               _ <- try (string "argument") <|> string "arg"+               whiteSpace+               name <- argName+               prems <- pPropositions+               excs <- pPropositions+               c <- pProposition+               return (Arg' name (prems, excs, c))++-- |Parses one declaration of a weight. A weight is declared by the string +-- @weight@ followed by the name of a previously declared argument,+-- and a 'Double' assigned to that argument.+pWeight :: Parser Weight'+pWeight = do+             _ <- string "weight" >> whiteSpace+             name <- argName+             weight <- float+             return (name, weight)++-- |Parses a list of assumptions. A list of assumptions is just the keyword +-- @assumptions@ followed by a list of propositions.+pAssumptions :: Parser Assumptions+pAssumptions = do+                  _ <- string "assumptions" >> whiteSpace+                  pPropositions++-- |Parses the name of a proof standard allowing both the names as given in +-- the original paper and the constructors of PSName. +pPSName :: Parser PSName+pPSName =  try ((try (string "Scintilla") <|> +                      string "scintilla") +                 >> return Scintilla) +       <|> try ((try (string "Preponderance") <|> +                      string "preponderance") +                 >> return Preponderance) +       <|> try ((try (string "ClearAndConvincing") <|> +                      string "clear_and_convincing") +                 >> return ClearAndConvincing) +       <|> try ((try (string "BeyondReasonableDoubt") <|> +                      string "beyond_reasonable_doubt") +                 >> return BeyondReasonableDoubt) +       <|> try ((try (string "DialecticalValidity") <|> +                      string "dialectical_validity") +                 >> return DialecticalValidity)+       +-- |Parses one declaration of a proof standard.  A proof standard is declared +-- by the string @standard@ followed by a proposition and the name of a proof +-- standard.+pStandard :: Parser Standard'+pStandard = do+                _ <- string "standard"+                whiteSpace+                name <- argName+                psName <- pPSName+                whiteSpace+                return (name, psName)++-- |Converts a named argument to the definition used in the implementation +-- (and the paper).+argToArg :: Argument' -> Argument+argToArg (Arg' _ a) = Arg a++-- |Looks up a normal argument in a list of named argument and returns its name.+lookupArg :: Argument -> [Argument'] -> Maybe String+lookupArg _ [] = Nothing+lookupArg a (Arg' name a' : args)+ | a == Arg a' = Just name+ | otherwise = lookupArg a args++-- |Converts a list of named 'Argument\''s and named 'Weight\''s to a weight +-- function. Arguments not assigned a weight will raise an error.+weightToWeight :: [Argument'] -> [Weight'] -> ArgWeight+weightToWeight args ws arg = + fromMaybe (error $ "no weight assigned to" ++ show arg)+          (lookupArg arg args >>= \name -> lookup name ws) ++-- |Converts a list of named 'Standard\''s to a standard function.+-- Propositions not assigned a weight will raise an error.+standardToStandard :: [Standard'] -> PropStandard+standardToStandard [] p = error $ "no standard assigned to" ++ show p+standardToStandard ((name, st) : sts) p + | mkProp name == p = st+ | otherwise        = standardToStandard sts p++-- |Parses the definition of a complete Carneades Argument Evaluation Structure+-- (CAES). +-- +-- A CAES is parsed in multiple stages: +-- +-- First parsing zero or more arguments: +-- where a complete argument consists of @arg@ or @argument@ followed by an+-- @argName@ (a letter followed by one or more letters and digits,+-- underscore or \'; alternatively, a string literal), two lists of propositions,+-- and a conclusion. +-- +-- Then, zero or more weights, +-- where a weight is declared by the string +-- @weight@ followed by the name of a previously declared argument,+-- and a 'Double' assigned to that argument.+-- +-- Then, a list of assumptions, +-- where a list of assumptions is just the keyword +-- @assumptions@ followed by a list of propositions.+--+-- Then a list of proof standard declarations,+-- where a proof standard is declared +-- by the string @standard@ followed by a proposition and the name of a proof +-- standard.+--+-- This is followed by an end of file token.+pCAES :: Parser CAES+pCAES = do +           whiteSpace+           args <- many pArgument+           weights <- many pWeight+           assumps <- pAssumptions+           standards <- many pStandard+           eof+           let weight = weightToWeight args weights+           let audience = (assumps, weight) +           let standard = standardToStandard standards+           let argSet = mkArgSet (map argToArg args)+           return (CAES (argSet, audience, standard))++-- |Parses a 'String' containing a CAES. +-- If parsing fails, it propagates the parse error.+parseCAES :: String -> Either ParseError CAES+parseCAES = parse pCAES ""

@@ -0,0 +1,12 @@+module Main (main) where++import Test.Tasty++import qualified Test.Language.Carneades.CarneadesDSL+import qualified Test.Language.Carneades.Input++main :: IO ()+main = defaultMain $ testGroup "CarneadesDSL"+  [ Test.Language.Carneades.CarneadesDSL.tests+  , Test.Language.Carneades.Input.tests+  ]

@@ -0,0 +1,96 @@+module Test.Language.Carneades.CarneadesDSL (tests) where++import Prelude hiding (negate)+import Test.Tasty+import Test.Tasty.HUnit++import Language.Carneades.CarneadesDSL+import Language.Carneades.ExampleCAES++tests :: TestTree+tests = testGroup "CarneadesDSL"+  [ testGroup "mkProp"+      [ testCase "positive literal" $+          mkProp "kill" @?= (True, "kill")+      , testCase "negative literal" $+          mkProp "-intent" @?= (False, "intent")+      , testCase "double negation" $+          mkProp "--x" @?= (True, "x")+      ]+  , testGroup "negate"+      [ testCase "negate positive" $+          negate (True, "p") @?= (False, "p")+      , testCase "negate negative" $+          negate (False, "p") @?= (True, "p")+      ]+  , testGroup "mkArg"+      [ testCase "constructs argument" $ do+          let a = mkArg ["kill", "intent"] [] "murder"+          let Arg (prems, excs, c) = a+          length prems @?= 2+          excs @?= []+          c @?= (True, "murder")+      , testCase "negative conclusion" $ do+          let a = mkArg ["witness2"] ["unreliable2"] "-intent"+          let Arg (_, _, c) = a+          c @?= (False, "intent")+      ]+  , testGroup "mkArgSet"+      [ testCase "acyclic set is not cyclic" $+          checkCycle argSet @?= False+      , testCase "retrieves arguments for prop" $ do+          let args = getArgs (mkProp "murder") argSet+          length args @?= 1+      , testCase "no arguments for unknown prop" $ do+          let args = getArgs (mkProp "unknown") argSet+          args @?= []+      ]+  , testGroup "applicability (ExampleCAES)"+      [ testCase "arg2 is applicable for intent" $+          testAppIntent @?= [arg2]+      , testCase "no applicable args for -intent" $+          testAppNotIntent @?= []+      , testCase "no applicable args for murder (intent not accepted)" $+          testAppMurder @?= []+      , testCase "no applicable args for -murder" $+          testAppNotMurder @?= []+      ]+  , testGroup "acceptability (ExampleCAES)"+      [ testCase "murder is not acceptable" $+          testMurder @?= False+      , testCase "-murder is not acceptable" $+          testNotMurder @?= False+      ]+  , testGroup "proof standards"+      [ testCase "scintilla: at least one applicable arg" $ do+          -- intent has applicable arg2, so scintilla should pass+          let result = scintilla (mkProp "intent") caes+          result @?= True+      , testCase "scintilla: no applicable arg fails" $ do+          -- -intent has no applicable args (unreliable2 is an exception)+          let result = scintilla (mkProp "-intent") caes+          result @?= False+      , testCase "beyond reasonable doubt: weight too low" $ do+          -- intent's arg2 has weight 0.3 < alpha=0.4+          let result = beyond_reasonable_doubt (mkProp "intent") caes+          result @?= False+      ]+  , testGroup "convenience functions"+      [ testCase "getAllArgs returns all arguments" $ do+          let allArgs = getAllArgs argSet+          length allArgs @?= 3+      , testCase "getProps returns all propositions" $ do+          let props = getProps argSet+          -- Should have murder, -murder, intent, -intent, kill, witness, witness2, unreliable, unreliable2+          assertBool "at least 5 props" (length props >= 5)+      , testCase "applicableArgs" $ do+          let appArgs = applicableArgs caes+          -- Only arg2 (witness -> intent) is applicable+          appArgs @?= [arg2]+      , testCase "acceptableProps returns empty for this CAES" $ do+          let accProps = acceptableProps caes+          -- kill and witness are assumptions but not in the graph as conclusions+          -- intent fails BeyondReasonableDoubt, murder fails since intent not acceptable+          accProps @?= []+      ]+  ]

@@ -0,0 +1,96 @@+module Test.Language.Carneades.Input (tests) where++import Prelude hiding (negate)+import Test.Tasty+import Test.Tasty.HUnit++import Language.Carneades.CarneadesDSL+import Language.Carneades.Input++tests :: TestTree+tests = testGroup "Input"+  [ testGroup "parseCAES"+      [ testCase "parses valid input" $ do+          let input = unlines+                [ "argument arg1 [\"kill\", \"intent\"] [] \"murder\""+                , "weight arg1 0.8"+                , "assumptions [\"kill\", \"intent\"]"+                , "standard \"kill\" scintilla"+                , "standard \"intent\" scintilla"+                ]+          case parseCAES input of+            Left err -> assertFailure $ "Parse error: " ++ show err+            Right (CAES (argSet, (assumps, _), _)) -> do+              length (getAllArgs argSet) @?= 1+              length assumps @?= 2++      , testCase "parses multiple arguments" $ do+          let input = unlines+                [ "argument a1 [\"p\"] [] \"q\""+                , "argument a2 [\"r\"] [\"s\"] \"-q\""+                , "weight a1 0.5"+                , "weight a2 0.6"+                , "assumptions [\"p\", \"r\"]"+                , "standard \"q\" preponderance"+                ]+          case parseCAES input of+            Left err -> assertFailure $ "Parse error: " ++ show err+            Right (CAES (argSet, _, _)) -> do+              length (getAllArgs argSet) @?= 2++      , testCase "parses BeyondReasonableDoubt standard" $ do+          let input = unlines+                [ "argument a1 [\"w\"] [] \"intent\""+                , "weight a1 0.9"+                , "assumptions [\"w\"]"+                , "standard \"intent\" beyond_reasonable_doubt"+                ]+          case parseCAES input of+            Left err -> assertFailure $ "Parse error: " ++ show err+            Right (CAES (_, _, std)) ->+              std (mkProp "intent") @?= BeyondReasonableDoubt++      , testCase "parses constructor-style standard names" $ do+          let input = unlines+                [ "argument a1 [\"x\"] [] \"y\""+                , "weight a1 0.5"+                , "assumptions [\"x\"]"+                , "standard \"y\" Preponderance"+                ]+          case parseCAES input of+            Left err -> assertFailure $ "Parse error: " ++ show err+            Right (CAES (_, _, std)) ->+              std (mkProp "y") @?= Preponderance++      , testCase "handles Haskell-style comments" $ do+          let input = unlines+                [ "-- This is a comment"+                , "argument a1 [\"p\"] [] \"q\""+                , "{- block comment -}"+                , "weight a1 0.5"+                , "assumptions [\"p\"]"+                , "standard \"q\" scintilla"+                ]+          case parseCAES input of+            Left err -> assertFailure $ "Parse error: " ++ show err+            Right (CAES (argSet, _, _)) ->+              length (getAllArgs argSet) @?= 1++      , testCase "rejects malformed input" $ do+          let input = "this is not valid CAES input"+          case parseCAES input of+            Left _  -> return ()+            Right _ -> assertFailure "Expected parse error"+      ]+  , testGroup "round-trip with examplecaes.txt"+      [ testCase "parses example file" $ do+          input <- readFile "examplecaes.txt"+          case parseCAES input of+            Left err -> assertFailure $ "Parse error: " ++ show err+            Right (CAES (argSet, (assumps, _), std)) -> do+              length (getAllArgs argSet) @?= 3+              length assumps @?= 4+              std (mkProp "intent") @?= BeyondReasonableDoubt+              std (mkProp "kill") @?= Scintilla+      ]+  ]