module Data.Logic.Propositional.Core where
import Prelude hiding (lookup)
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)
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
| Conditional Expr Expr
| Biconditional Expr Expr
deriving Eq
instance Show Expr where
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
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
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
assignments :: Expr -> [Mapping]
assignments expr = let vs = variables expr
ps = replicateM (length vs) [True, False]
in map (fromList . zip vs) ps
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 map head . group . sort $ vars_ expr []
equivalent :: Expr -> Expr -> Bool
equivalent exp1 exp2 = values exp1 == values exp2
isTautology :: Expr -> Bool
isTautology = and . values
isContradiction :: Expr -> Bool
isContradiction = not . or . values
isContingent :: Expr -> Bool
isContingent expr = not (isTautology expr || isContradiction expr)
values :: Expr -> [Bool]
values expr = map (interpret expr) (assignments expr)
showAscii :: Expr -> String
showAscii (Variable name) = show 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