-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A truth table generator for classical propositional logic.
--   
--   Hatt is a command-line program which prints truth tables for
--   expressions in classical propositional logic, and a library allowing
--   its parser, evaluator and truth table generator to be used in other
--   programs.
@package hatt
@version 1.0


-- | The <a>Data.Logic.Propositional</a> module provides a set of functions
--   for parsing, manipulating and generating truth tables for expressions
--   in classical propositional logic.
--   
--   The core of the API is the <a>Expr</a> data type, which has
--   constructors for all the usual expression forms: variables, standing
--   for atomic propositions; negation, the only unary connective; and the
--   binary connectives of conjunction, disjunction, material implication
--   and logical equivalence.
module Data.Logic.Propositional
data Expr
Variable :: String -> Expr
Negation :: Expr -> Expr
Conjunction :: Expr -> Expr -> Expr
Disjunction :: Expr -> Expr -> Expr
Conditional :: Expr -> Expr -> Expr
Biconditional :: Expr -> Expr -> Expr
type Mapping = Map String Bool

-- | Determines whether two expressions are extensionally equivalent (that
--   is, have the same values under all interpretations).
equivalent :: Expr -> Expr -> Bool

-- | In order to interpret an expression, a mapping from variables to truth
--   values needs to be provided. Truth values are compositional; that's to
--   say, the value of a composite expression (any expression which is not
--   atomic) depends on the truth values of its component parts. For
--   example, the Haskell expression below would evaluate to
--   <tt>False</tt>.
--   
--   <pre>
--   interpret
--       (Conjunction (Variable "A") (Variable "B"))
--       (fromList [("A", True), ("B", False)])
--   </pre>
interpret :: Expr -> Mapping -> Bool

-- | Generates the possible assignments of variables in an expression.
assignments :: Expr -> [Mapping]

-- | Determines whether an expression is contingent (that is, true in at
--   least one interpretation and false in at least one interpretation).
isContingent :: Expr -> Bool

-- | Determines whether an expression is contradictory.
isContradiction :: Expr -> Bool

-- | Determines whether an expression is tautological.
isTautology :: Expr -> Bool

-- | The <a>parseExpr</a> function accepts the name of a source, and a
--   string to be parsed, and attempts to parse the string as a logical
--   expression of the following forms, where <tt>φ</tt> and <tt>ψ</tt> are
--   metalinguistic variables standing for any valid expression.
--   
--   <ul>
--   <li>Variables: <tt>"P"</tt>, <tt>"Q"</tt>, <tt>"R"</tt> etc.;
--   basically anything in the character class <tt>[A-Z]</tt></li>
--   <li>Negation: <tt>"~φ"</tt></li>
--   <li>Conjunction: <tt>"(φ &amp; ψ)"</tt></li>
--   <li>Disjunction: <tt>"(φ | ψ)"</tt></li>
--   <li>Conditional: <tt>"(φ -&gt; ψ)"</tt></li>
--   <li>Biconditional: <tt>"(φ &lt;-&gt; ψ)"</tt></li>
--   </ul>
parseExpr :: SourceName -> String -> Either ParseError Expr

-- | A specialised variant of <a>showsPrec</a>, using precedence context
--   zero, and returning an ordinary <a>String</a>.
show :: Show a => a -> String

-- | Represents expressions using only ASCII characters (the <a>show</a>
--   function pretty-prints expressions using logical symbols only present
--   in extended character sets).
showAscii :: Expr -> String

-- | The <a>truthTable</a> function produces a truth table for the given
--   expression.
truthTable :: Expr -> String

-- | The <a>truthTableP</a> is a configurable version of <a>truthTable</a>
--   which allows a printer function to be selected, so for example one can
--   print ASCII truth tables by passing <a>showAscii</a> to
--   <a>truthTableP</a> instead of <a>show</a>.
truthTableP :: (Expr -> String) -> Expr -> String

-- | Lists the names of variables present in an expression.
variables :: Expr -> [String]