packages feed

hatt (empty) → 0.1

raw patch · 9 files changed

+415/−0 lines, 9 filesdep +basedep +cmdargsdep +containerssetup-changed

Dependencies added: base, cmdargs, containers, parsec

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c)2011, Benedict Eastaugh++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Benedict Eastaugh nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,72 @@+Hatt+====++[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.+++Installation+------------++Hatt is available from [Hackage]. To install it with `cabal-install`, update+your list of known packages and then install Hatt.++    $ cabal update+    $ cabal install hatt++To build it from source, `cd` into the directory containing the Hatt source+files, including `hatt.cabal`, and run `cabal install`.+++Valid Hatt expressions+----------------------++The following are all valid expression forms which can be parsed by Hatt, where+ϕ and ψ are metalinguistic variables standing in for any valid expression. The+parser isn't as smart about parentheses as it could be, so you have to follow+these rules quite literally. This shouldn't be a great hardship, but it does+mean that, for example, while `(A -> B)` is a valid expression, `A -> B` isn't.++* Variables: `P`, `Q`, `R` etc.---basically anything in the character class+  `[A-Z]`+* Negation: `~ϕ`+* Conjunction: `(ϕ & ψ)`+* Disjunction: `(ϕ | ψ)`+* Conditional: `(ϕ -> ψ)`+* Biconditional: `(ϕ <-> ψ)`+++Using the `hatt` command-line program+-------------------------------------++The `--evaluate` flag lets you pass an expression to be evaluated directly.+Here's an example session doing just that.++    $ hatt --evaluate="(P -> (Q | ~R))"+    P Q R | (P → (Q ∨ ¬R))+    ----------------------+    T T T | F+    T T F | F+    T F T | F+    T F F | F+    F T T | F+    F T F | F+    F F T | T+    F F F | F++Note that while you need to use ASCII symbols to interact with `hatt`, it+pretty-prints expressions using the more common logical symbols. The Hatt+library exposes the `showAscii` function which will print expressions in the+format in which they're entered.+++Using Hatt in other programs+----------------------------++Hatt exposes the `Data.Logic.Propositional` module, which provides a simple API+for parsing, evaluating, and printing truth tables.+++[Hatt]:    http://extralogical.net/projects/hatt+[Hackage]: http://hackage.haskell.org/
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ hatt.cabal view
@@ -0,0 +1,44 @@+Name:               hatt+Version:            0.1+Stability:          experimental++Synopsis:           A truth table generator for classical propositional logic.+Description:        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.+License:            BSD3+License-file:       LICENSE+Author:             Benedict Eastaugh+Maintainer:         benedict@eastaugh.net+Copyright:          (c) 2011 Benedict Eastaugh+Homepage:           https://github.com/beastaugh/hatt+Category:           Logic+Cabal-version:      >= 1.6++Build-type:         Simple+Extra-source-files: README.md++Source-repository head+  Type:             git+  Location:         git://github.com/beastaugh/hatt.git++Library+  Hs-Source-Dirs:   src+  GHC-options:      -Wall+  Build-depends:    base       >= 4.2 && < 4.3,+                    containers >= 0.3 && < 0.4,+                    parsec     >= 2.1 && < 2.2+  Exposed-modules:  Data.Logic.Propositional,+                    Data.Logic.Propositional.Core,+                    Data.Logic.Propositional.Parser,+                    Data.Logic.Propositional.Tables++Executable hatt+  Hs-Source-Dirs:   src+  Main-Is:          hatt.hs+  GHC-options:      -Wall+  Build-depends:    base       >= 4.2 && < 4.3,+                    cmdargs    >= 0.6 && < 0.7,+                    containers >= 0.3 && < 0.4,+                    parsec     >= 2.1 && < 2.2
+ src/Data/Logic/Propositional.hs view
@@ -0,0 +1,28 @@+-- | The "Data.Logic.Propositional" 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 'Expr' 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+    ( Expr (..)+    , Mapping+    +    , equivalent+    , interpret+    , assignments+    , isContingent+    , isContradiction+    , isTautology+    , parseExpr+    , show+    , showAscii+    , truthTable+    , variables+    ) where++import Data.Logic.Propositional.Core+import Data.Logic.Propositional.Parser+import Data.Logic.Propositional.Tables
+ src/Data/Logic/Propositional/Core.hs view
@@ -0,0 +1,104 @@+{-# OPTIONS_HADDOCK hide #-}++module Data.Logic.Propositional.Core where++import Prelude hiding (lookup)++import Control.Monad (replicateM)+import Data.Map (Map, fromList, lookup)+import Data.Maybe (fromMaybe)++data Expr = Variable      String+          | Negation      Expr+          | Conjunction   Expr Expr+          | Disjunction   Expr Expr+          | Conditional   Expr Expr+          | Biconditional Expr Expr+          deriving Eq++instance Show Expr where+  show (Variable      name)      = name+  show (Negation      expr)      = '¬' : show expr+  show (Conjunction   exp1 exp2) = showBC "∧" exp1 exp2+  show (Disjunction   exp1 exp2) = showBC "∨" exp1 exp2+  show (Conditional   exp1 exp2) = showBC "→" exp1 exp2+  show (Biconditional exp1 exp2) = showBC "↔" exp1 exp2++type Mapping = Map String 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 @False@.+--+-- > interpret+-- >     (Conjunction (Variable "A") (Variable "B"))+-- >     (fromList [("A", True), ("B", False)])+interpret :: Expr -> Mapping -> Bool+interpret (Variable      v)         vs = fromMaybe False (lookup v vs)+interpret (Negation      expr)      vs = not $ interpret expr vs+interpret (Conjunction   exp1 exp2) vs = interpret exp1 vs && interpret exp2 vs+interpret (Disjunction   exp1 exp2) vs = interpret exp1 vs || interpret exp2 vs+interpret (Conditional   exp1 exp2) vs = not $ interpret exp1 vs || interpret exp2 vs+interpret (Biconditional exp1 exp2) vs = interpret exp1 vs == interpret exp2 vs++-- | Generates the possible assignments of variables in an expression.+assignments :: Expr -> [Mapping]+assignments expr = let vs = variables expr+                       ps = replicateM (length vs) [True, False]+                   in  map (fromList . zip vs) ps++-- | Lists the names of variables present in an expression.+variables :: Expr -> [String]+variables expr = let vars_ (Variable      v)     vs = v : vs+                     vars_ (Negation      e)     vs = vars_ e vs+                     vars_ (Conjunction   e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs+                     vars_ (Disjunction   e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs+                     vars_ (Conditional   e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs+                     vars_ (Biconditional e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs+                 in  vars_ expr []++-- | Determines whether two expressions are extensionally equivalent (that is,+-- have the same values under all interpretations).+equivalent :: Expr -> Expr -> Bool+equivalent exp1 exp2 = values exp1 == values exp2++-- | Determines whether an expression is tautological.+isTautology :: Expr -> Bool+isTautology = and . values++-- | Determines whether an expression is contradictory.+isContradiction :: Expr -> Bool+isContradiction = not . or . values++-- | Determines whether an expression is contingent (that is, true in at least+-- one interpretation and false in at least one interpretation).+isContingent :: Expr -> Bool+isContingent expr = not (isTautology expr || isContradiction expr)++-- | Lists the values of an expression under all interpretations (that is, all+-- assignments of values to variables).+values :: Expr -> [Bool]+values expr = map (interpret expr) (assignments expr)++-- | Represents expressions using only ASCII characters (the 'show' function+-- pretty-prints expressions using logical symbols only present in extended+-- character sets).+showAscii :: Expr -> String+showAscii (Variable      name)      = name+showAscii (Negation      expr)      = '~' : showAscii expr+showAscii (Conjunction   exp1 exp2) = showBCA "&"   exp1 exp2+showAscii (Disjunction   exp1 exp2) = showBCA "|"   exp1 exp2+showAscii (Conditional   exp1 exp2) = showBCA "->"  exp1 exp2+showAscii (Biconditional exp1 exp2) = showBCA "<->" exp1 exp2++showBinaryConnective :: (Expr -> String) -> String -> Expr -> Expr -> String+showBinaryConnective show_ symbol exp1 exp2 =+  '(' : show_ exp1 ++ " " ++ symbol ++ " " ++ show_ exp2 ++ ")"++showBC :: String -> Expr -> Expr -> String+showBC = showBinaryConnective show++showBCA :: String -> Expr -> Expr -> String+showBCA = showBinaryConnective showAscii
+ src/Data/Logic/Propositional/Parser.hs view
@@ -0,0 +1,74 @@+{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}+{-# OPTIONS_HADDOCK hide #-}++module Data.Logic.Propositional.Parser+    ( parseExpr+    ) where++import Data.Logic.Propositional.Core (Expr (..))++import Text.ParserCombinators.Parsec+    (char, choice, eof, oneOf, parse, spaces, string)++import Text.ParserCombinators.Parsec.Error (ParseError)+import Text.ParserCombinators.Parsec.Pos (SourceName)+import Text.ParserCombinators.Parsec.Prim (GenParser)++-- | The 'parseExpr' 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 @&#966;@ and @&#968;@ are metalinguistic variables+-- standing for any valid expression.+--+-- * Variables: @\"P\"@, @\"Q\"@, @\"R\"@ etc.; basically anything in the+--   character class @[A-Z]@+--+-- * Negation: @\"~&#966;\"@+--+-- * Conjunction: @\"(&#966; & &#968;)\"@+--+-- * Disjunction: @\"(&#966; | &#968;)\"@+--+-- * Conditional: @\"(&#966; -> &#968;)\"@+--+-- * Biconditional: @\"(&#966; \<-> &#968;)\"@+parseExpr :: SourceName -> String -> Either ParseError Expr+parseExpr = parse statement++statement :: GenParser Char st Expr+statement = do spaces+               x <- expr+               spaces+               eof+               return x++expr :: GenParser Char st Expr+expr = choice [binaryP, negation, variable]++variable :: GenParser Char st Expr+variable = do c <- oneOf ['A'..'Z']+              return $ Variable [c]++negation :: GenParser Char st Expr+negation = do char '~'+              x <- expr+              return $ Negation x++binaryP :: GenParser Char st Expr+binaryP = do char '('+             x <- binary+             char ')'+             return x++binary :: GenParser Char st Expr+binary = do x1 <- expr+            spaces+            s  <- choice [string "&", string "|", string "->", string "<->"]+            spaces+            x2 <- expr+            return $ connective s x1 x2+  where+    connective "&"   = Conjunction+    connective "|"   = Disjunction+    connective "->"  = Conditional+    connective "<->" = Biconditional+    connective _     = error "Impossible case"
+ src/Data/Logic/Propositional/Tables.hs view
@@ -0,0 +1,30 @@+{-# OPTIONS_HADDOCK hide #-}++module Data.Logic.Propositional.Tables+    ( truthTable+    ) where++import Data.Logic.Propositional.Core++import Data.Map (fold)++-- | The 'truthTable' function produces a truth table for the given expression.+truthTable :: Expr -> String+truthTable expr = unlines [header, separator, body]+  where+    header    = unwords vs ++ " | " ++ show expr+    body      = unlines $ map (showAssignment expr) as+    separator = concat $ replicate sepLength "-"+    sepLength = length vs * 2 + length (show expr) + 2+    as        = assignments expr+    vs        = variables   expr++showAssignment :: Expr -> Mapping -> String+showAssignment expr a = showVarValues ++ " | " ++ showExprValue+  where+    showVarValues = unwords $ fold ((:) . showBool) [] a+    showExprValue = showBool $ interpret expr a++showBool :: Bool -> String+showBool True  = "T"+showBool False = "F"
+ src/hatt.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE DeriveDataTypeable #-}++module Main+    ( main+    ) where++import Data.Logic.Propositional++import System.Console.CmdArgs++data HattOpts = HattOpts+    { evaluate :: String+    } deriving (Show, Data, Typeable)++hattOpts :: HattOpts+hattOpts = HattOpts+  { evaluate = def &= opt "" &= typ "EXPRESSION"+                   &= help "Print the truth table for the given expression"+  } &= summary "Hatt 0.1, (c) Benedict Eastaugh 2011"+    &= program "hatt"++main :: IO ()+main = do opts <- cmdArgs hattOpts+          case evaluate opts of+               ""   -> putStrLn "Try using the --evaluate[=EXPRESSION] flag"+               expr -> putStr (eval expr)++eval :: String -> String+eval str = case parseExpr "" str of+                Left  err  -> "parse error at " ++ show err ++ "\n"+                Right expr -> truthTable expr