hatt 1.4.0.2 → 1.5.0.0
raw patch · 10 files changed
+277/−52 lines, 10 filesdep +QuickCheckdep +hattdep +test-framework
Dependencies added: QuickCheck, hatt, test-framework, test-framework-quickcheck2
Files
- LICENSE +1/−1
- README.md +15/−1
- hatt.cabal +21/−11
- src/Data/Logic/Propositional.hs +7/−2
- src/Data/Logic/Propositional/Core.hs +45/−8
- src/Data/Logic/Propositional/NormalForms.hs +94/−0
- src/Data/Logic/Propositional/Parser.hs +2/−2
- src/Data/Logic/Propositional/Tables.hs +1/−1
- src/hatt.hs +59/−26
- test/main.hs +32/−0
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2011, Benedict Eastaugh+Copyright (c) 2012, Benedict Eastaugh All rights reserved.
README.md view
@@ -116,13 +116,27 @@ tables which it prints: green for true, red for false. You can enable colouring during interactive mode by using the `colour` command. +You can print out the normal forms of expressions too, by prefixing an+expression with `nnf`, `dnf` or `cnf`. + $ hatt --pretty+ > nnf ~(P -> (Q & R))+ (P ∧ (¬Q ∨ ¬R))++The three supported normal forms are [negation normal form], [conjunctive normal+form] and [disjunctive normal form].++ Using Hatt in other programs ---------------------------- Hatt exposes the `Data.Logic.Propositional` module, which provides a simple API-for parsing, evaluating, and printing truth tables.+for parsing, evaluating, and printing truth tables, and for converting logical+expressions into normal forms. [Hatt]: http://extralogical.net/projects/hatt [Hackage]: http://hackage.haskell.org/+[negation normal form]: http://en.wikipedia.org/wiki/Negation_normal_form+[conjunctive normal form]: http://en.wikipedia.org/wiki/Conjunctive_normal_form+[disjunctive normal form]: http://en.wikipedia.org/wiki/Disjunctive_normal_form
hatt.cabal view
@@ -1,11 +1,13 @@ Name: hatt-Version: 1.4.0.2+Version: 1.5.0.0 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.+ generator to be used in other programs. It includes support+ for converting logical expressions into several normal+ forms. License: BSD3 License-file: LICENSE Author: Benedict Eastaugh@@ -13,7 +15,7 @@ Copyright: (c) 2012 Benedict Eastaugh Homepage: http://extralogical.net/projects/hatt Category: Logic-Cabal-version: >= 1.6+Cabal-version: >= 1.8 Build-type: Simple Extra-source-files: README.md@@ -28,19 +30,27 @@ Build-depends: base >= 4 && < 5, containers >= 0.3 && < 0.5, parsec >= 2.1 && < 3.2,+ QuickCheck >= 2.4, ansi-wl-pprint >= 0.6 && < 0.7- Exposed-modules: Data.Logic.Propositional+ Exposed-modules: Data.Logic.Propositional,+ Data.Logic.Propositional.Tables,+ Data.Logic.Propositional.NormalForms Other-modules: Data.Logic.Propositional.Core,- Data.Logic.Propositional.Parser,- Data.Logic.Propositional.Tables+ Data.Logic.Propositional.Parser Executable hatt- Hs-Source-Dirs: src- Main-Is: hatt.hs+ Main-Is: src/hatt.hs GHC-options: -Wall Build-depends: base >= 4 && < 5,+ hatt, cmdargs >= 0.7,- containers >= 0.3 && < 0.5,- parsec >= 2.1 && < 3.2,- ansi-wl-pprint >= 0.6 && < 0.7, haskeline >= 0.6 && < 0.7++Test-Suite test-hatt+ Type: exitcode-stdio-1.0+ Main-is: test/main.hs+ GHC-options: -Wall+ Build-depends: base >= 4 && < 5,+ hatt,+ test-framework >= 0.4.1,+ test-framework-quickcheck2
src/Data/Logic/Propositional.hs view
@@ -8,22 +8,27 @@ -- conjunction, disjunction, material implication and logical equivalence. module Data.Logic.Propositional ( Expr (..)+ , Var (..) , Mapping , equivalent , interpret , assignments+ , values+ , variables , isContingent , isContradiction , isTautology+ , parseExpr+ , show , showAscii+ , truthTable , truthTableP- , variables ) where import Data.Logic.Propositional.Core import Data.Logic.Propositional.Parser-import Data.Logic.Propositional.Tables+import Data.Logic.Propositional.Tables (truthTable, truthTableP)
src/Data/Logic/Propositional/Core.hs view
@@ -4,12 +4,21 @@ import Prelude hiding (lookup) -import Control.Monad (replicateM)-import Data.List (nub)+import Control.Monad (liftM, liftM2, replicateM)+import Data.Char (chr)+import Data.Functor ((<$>))+import Data.List (group, sort) import Data.Map (Map, fromList, lookup) import Data.Maybe (fromMaybe)+import Test.QuickCheck (Arbitrary, Gen, arbitrary, elements, oneof, sized) -data Expr = Variable String+newtype Var = Var Char+ deriving (Eq, Ord)++instance Show Var where+ show (Var v) = [v]++data Expr = Variable Var | Negation Expr | Conjunction Expr Expr | Disjunction Expr Expr@@ -18,15 +27,43 @@ deriving Eq instance Show Expr where- show (Variable name) = name+ show (Variable name) = show 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+instance Arbitrary Var where+ arbitrary = liftM Var . elements . map chr $ [65..90] ++ [97..122] +instance Arbitrary Expr where+ arbitrary = randomExpr++randomExpr :: Gen Expr+randomExpr = sized randomExpr'++randomExpr' :: Int -> Gen Expr+randomExpr' n | n > 0 = oneof [ randomVar+ , randomNeg boundedExpr+ , randomBin boundedExpr+ ]+ | otherwise = randomVar+ where+ boundedExpr = randomExpr' (n `div` 2)++randomBin :: Gen Expr -> Gen Expr+randomBin rExp = oneof . map (\c -> liftM2 c rExp rExp)+ $ [Conjunction, Disjunction, Conditional, Biconditional]++randomNeg :: Gen Expr -> Gen Expr+randomNeg rExp = Negation <$> rExp++randomVar :: Gen Expr+randomVar = Variable <$> arbitrary++type Mapping = Map Var 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)@@ -51,14 +88,14 @@ in map (fromList . zip vs) ps -- | Lists the names of variables present in an expression.-variables :: Expr -> [String]+variables :: Expr -> [Var] 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 nub $ vars_ expr []+ in map head . group . sort $ vars_ expr [] -- | Determines whether two expressions are extensionally equivalent (that is, -- have the same values under all interpretations).@@ -87,7 +124,7 @@ -- pretty-prints expressions using logical symbols only present in extended -- character sets). showAscii :: Expr -> String-showAscii (Variable name) = name+showAscii (Variable name) = show name showAscii (Negation expr) = '~' : showAscii expr showAscii (Conjunction exp1 exp2) = showBCA "&" exp1 exp2 showAscii (Disjunction exp1 exp2) = showBCA "|" exp1 exp2
+ src/Data/Logic/Propositional/NormalForms.hs view
@@ -0,0 +1,94 @@+{-# OPTIONS_HADDOCK hide #-}++module Data.Logic.Propositional.NormalForms+ ( toNNF+ , toCNF+ , toDNF+ ) where++import Data.Logic.Propositional.Core++-- | The 'toNNF' function converts expressions to negation normal form. This+-- function is total: it's defined for all expressions, not just those which+-- only use negation, conjunction and disjunction, although all expressions in+-- negation normal form do in fact only use those connectives.+--+-- The conversion is carried out by replacing any condtitionals or+-- biconditionals with equivalent expressions using only negation, conjunction+-- and disjunction. Then de Morgan's laws are applied to convert negated+-- conjunctions and disjunctions into the conjunction or disjunction of the+-- negation of their conjuncts: @¬(φ ∧ ψ)@ is converted to @(¬φ ∨ ¬ψ)@+-- while @¬(φ ∨ ψ)@ becomes @(¬φ ∧ ¬ψ)@.+toNNF :: Expr -> Expr+toNNF expr@(Variable _) = expr+toNNF expr@(Negation (Variable _)) = expr+toNNF (Negation (Negation expr)) = expr++toNNF (Conjunction exp1 exp2) = toNNF exp1 `conj` toNNF exp2+toNNF (Negation (Conjunction exp1 exp2)) = toNNF $ neg exp1 `disj` neg exp2++toNNF (Disjunction exp1 exp2) = toNNF exp1 `disj` toNNF exp2+toNNF (Negation (Disjunction exp1 exp2)) = toNNF $ neg exp1 `conj` neg exp2++toNNF (Conditional exp1 exp2) = toNNF $ neg exp1 `disj` exp2+toNNF (Negation (Conditional exp1 exp2)) = toNNF $ exp1 `conj` neg exp2++toNNF (Biconditional exp1 exp2) = let a = exp1 `conj` exp2+ b = neg exp1 `conj` neg exp2+ in toNNF $ a `disj` b+toNNF (Negation (Biconditional exp1 exp2)) = let a = exp1 `disj` exp2+ b = neg exp1 `disj` neg exp2+ in toNNF $ a `conj` b++-- | The 'toCNF' function converts expressions to conjunctive normal form: a+-- conjunction of clauses, where a clause is a disjunction of literals+-- (variables and negated variables).+--+-- The conversion is carried out by first converting the expression into+-- negation normal form, and then applying the distributive law.+--+-- Because it first applies 'toNNF', it is a total function and can handle+-- expressions which include conditionals and biconditionals.+toCNF :: Expr -> Expr+toCNF = toCNF' . toNNF+ where+ toCNF' :: Expr -> Expr+ toCNF' (Conjunction exp1 exp2) = toCNF' exp1 `conj` toCNF' exp2+ toCNF' (Disjunction exp1 exp2) = toCNF' exp1 `dist` toCNF' exp2+ toCNF' expr = expr+ + dist :: Expr -> Expr -> Expr+ dist (Conjunction e11 e12) e2 = (e11 `dist` e2) `conj` (e12 `dist` e2)+ dist e1 (Conjunction e21 e22) = (e1 `dist` e21) `conj` (e1 `dist` e22)+ dist e1 e2 = e1 `disj` e2++-- | The 'toDNF' function converts expressions to disjunctive normal form: a+-- disjunction of clauses, where a clause is a conjunction of literals+-- (variables and negated variables).+--+-- The conversion is carried out by first converting the expression into+-- negation normal form, and then applying the distributive law.+--+-- Because it first applies 'toNNF', it is a total function and can handle+-- expressions which include conditionals and biconditionals.+toDNF :: Expr -> Expr+toDNF = toDNF' . toNNF+ where+ toDNF' :: Expr -> Expr+ toDNF' (Conjunction exp1 exp2) = toDNF' exp1 `dist` toDNF' exp2+ toDNF' (Disjunction exp1 exp2) = toDNF' exp1 `disj` toDNF' exp2+ toDNF' expr = expr+ + dist :: Expr -> Expr -> Expr+ dist (Disjunction e11 e12) e2 = (e11 `dist` e2) `disj` (e12 `dist` e2)+ dist e1 (Disjunction e21 e22) = (e1 `dist` e21) `disj` (e1 `dist` e22)+ dist e1 e2 = e1 `conj` e2++neg :: Expr -> Expr+neg = Negation++disj :: Expr -> Expr -> Expr+disj = Disjunction++conj :: Expr -> Expr -> Expr+conj = Conjunction
src/Data/Logic/Propositional/Parser.hs view
@@ -5,7 +5,7 @@ ( parseExpr ) where -import Data.Logic.Propositional.Core (Expr (..))+import Data.Logic.Propositional.Core (Expr (..), Var (..)) import Text.ParserCombinators.Parsec ((<|>), char, choice, eof, letter, parse, spaces, string, try)@@ -50,7 +50,7 @@ variable :: GenParser Char st Expr variable = do c <- letter- return $ Variable [c]+ return $ Variable (Var c) negation :: GenParser Char st Expr negation = do char '~'
src/Data/Logic/Propositional/Tables.hs view
@@ -25,7 +25,7 @@ truthTableP :: Printer -> Expr -> String truthTableP (expPrinter, boolPrinter) expr = unlines [header, separator, body] where- header = unwords vs ++ " | " ++ expPrinter expr+ header = (unwords . map show) vs ++ " | " ++ expPrinter expr body = init . unlines $ map (showAssignment boolPrinter expr) as separator = concat $ replicate sepLength "-" sepLength = length vs * 2 + length (expPrinter expr) + 2
src/hatt.hs view
@@ -4,17 +4,26 @@ import Data.Logic.Propositional import Data.Logic.Propositional.Tables+import Data.Logic.Propositional.NormalForms import Control.Monad (when, unless)-import Data.Char (isSpace, toLower)+import Data.Char (toLower) import System.Console.CmdArgs-import System.Console.Haskeline (InputT, runInputT, defaultSettings, getInputLine, outputStr, outputStrLn)+import System.Console.Haskeline+ ( InputT+ , runInputT+ , defaultSettings+ , getInputLine+ , outputStr+ , outputStrLn+ ) data Command = Exit | Help | Pretty | Coloured | Eval Expr+ | Convert NormalForm Expr | Error String data ProgramMode = ProgramMode@@ -24,6 +33,8 @@ , coloured :: Bool } deriving (Show, Data, Typeable) +data NormalForm = NNF | CNF | DNF+ programMode :: ProgramMode programMode = ProgramMode { evaluate = "" &= typ "EXPRESSION"@@ -58,17 +69,19 @@ case minput of Nothing -> return () Just cmd -> case parseCommand cmd of- Exit -> return ()- Help -> outputStr (replHelpText printer)- >> repl mode- Pretty -> outputStrLn ppMessage- >> repl (mode {pretty = not isPretty})- Coloured -> outputStrLn cpMessage- >> repl (mode {coloured = not isColoured})- (Eval expr) -> outputStr (truthTableP printer expr)- >> repl mode- (Error err) -> outputStrLn ("Error: " ++ err)- >> repl mode+ Exit -> return ()+ Help -> outputStr (replHelpText printer)+ >> repl mode+ Pretty -> outputStrLn ppMessage+ >> repl (mode {pretty = not isPretty})+ Coloured -> outputStrLn cpMessage+ >> repl (mode {coloured = not isColoured})+ (Eval expr) -> outputStr (truthTableP printer expr)+ >> repl mode+ (Convert nf expr) -> outputStrLn (toNFStr nf (fst printer) expr)+ >> repl mode+ (Error err) -> outputStrLn ("Error: " ++ err)+ >> repl mode where printer = selectPrinter mode isPretty = pretty mode@@ -82,20 +95,29 @@ Right expr -> truthTableP p expr parseCommand :: String -> Command-parseCommand input = case cmd . words . dropWhile isSpace $ input of+parseCommand input = case cmd . words $ input of "" -> Error "you must enter an expression or a command." "exit" -> Exit "help" -> Help "pretty" -> Pretty "colour" -> Coloured- _ -> eval_ input+ "nnf" -> eval_ (Convert NNF) (getExpr input)+ "cnf" -> eval_ (Convert CNF) (getExpr input)+ "dnf" -> eval_ (Convert DNF) (getExpr input)+ _ -> eval_ Eval input where- cmd [] = ""- cmd ws = map toLower . head $ ws- eval_ str = case parseExpr "" str of- Left err -> Error $ "parse error at " ++ show err- Right expr -> Eval expr+ cmd [] = ""+ cmd ws = map toLower . head $ ws+ eval_ dt str = case parseExpr "hatt" str of+ Left err -> Error $ "parse error at " ++ show err+ Right expr -> dt expr+ getExpr = unwords . tail . words +toNFStr :: NormalForm -> (Expr -> String) -> Expr -> String+toNFStr NNF p = p . toNNF+toNFStr CNF p = p . toCNF+toNFStr DNF p = p . toDNF+ replIntroText :: String replIntroText = unwords [ "Entering interactive mode."@@ -128,14 +150,25 @@ , "For example, if you enter \"(A -> B)\" at the prompt, Hatt will print the" , "truth table for that expression. Here's an example console session." , ""- , " > A | B"- , indentBy 4 $ truthTableP printer (Disjunction (Variable "A") (Variable "B"))- ++ "> P -> (Q & R)\n"- ++ truthTableP printer (Conditional- (Variable "P")- (Conjunction (Variable "Q") (Variable "R")))+ , " > " ++ showAscii exp1+ , indentBy 4 $ truthTableP printer exp1+ ++ "> " ++ showAscii exp2 ++ "\n"+ ++ truthTableP printer exp2+ , "You can also convert expressions to different normal forms: negation"+ , "normal form, conjunctive normal form and disjunctive normal form. To do"+ , "this just prepend the expression you want to convert with \"nnf\", \"cnf\""+ , "or \"dnf\". For example,"+ , ""+ , " > nnf " ++ showAscii exp3+ , " " ++ (fst printer . toNNF) exp3+ , "" , "If none of this makes any sense, try reading the README file." ]+ where+ exp1 = Disjunction (Variable $ Var 'A') (Variable $ Var 'B')+ exp2 = Conditional (Variable $ Var 'P') exp4+ exp3 = Negation exp2+ exp4 = Conjunction (Variable $ Var 'Q') (Variable $ Var 'R') selectPrinter :: ProgramMode -> Printer selectPrinter m = let expPrinter = if pretty m then show else showAscii
+ test/main.hs view
@@ -0,0 +1,32 @@+module Main (main) where++import Data.Logic.Propositional+import Data.Logic.Propositional.NormalForms++import Test.Framework as TF (defaultMain, testGroup, Test)+import Test.Framework.Providers.QuickCheck2 (testProperty)++main :: IO ()+main = defaultMain tests++tests :: [TF.Test]+tests =+ [ testGroup "QuickCheck Data.Logic.Propositional.NormalForms"+ [ testProperty "SelfEquiv" propSelfEquiv+ , testProperty "NNFEquiv" propNNFEquiv+ , testProperty "CNFEquiv" propCNFEquiv+ , testProperty "DNFEquiv" propDNFEquiv+ ]+ ]++propSelfEquiv :: Expr -> Bool+propSelfEquiv expr = expr `equivalent` expr++propNNFEquiv :: Expr -> Bool+propNNFEquiv expr = expr `equivalent` toNNF expr++propCNFEquiv :: Expr -> Bool+propCNFEquiv expr = expr `equivalent` toCNF expr++propDNFEquiv :: Expr -> Bool+propDNFEquiv expr = expr `equivalent` toDNF expr