Propositional.hs

{-# LANGUAGE DeriveFoldable    #-}
{-# LANGUAGE DeriveFunctor     #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase        #-}

module Propositional where

import           Prelude hiding (False, True)
import qualified Prelude

import Control.Applicative    (liftA2)
import Control.Monad          (ap)
import Control.Monad.Identity
import Data.Foldable
import Data.List              (nub)
import Data.Maybe             (fromMaybe)
import Data.String

import Text.Show.Pretty

-- Propositions

infixr 9 ∨
infixr 9 `Or`
infixr 8 ∧
infixr 8 `And`
infixr 7 :=>
infixr 6 :<=>

data Formula a
  = True
  | False
  | Atom a
  | Not (Formula a)
  | Formula a `And` Formula a
  | Formula a `Or`  Formula a
  | Formula a :=>   Formula a -- ^ Implication
  | Formula a :<=>  Formula a -- ^ If and only if
  | Forall String (Formula a)
  | Exists String (Formula a)
  deriving (Show, Eq, Read, Functor, Foldable, Traversable)

-- Foldable allows us to fold over the Atoms in a formula. For example, we can
-- collect them with `toList`:
--
-- > toList (Atom 1 `Or` Atom 2 `Or` False)
-- [1,2]

(∧) = And
(∨) = Or

-- The Monad instance for formulas gives substitution. Note that `Formula` is a
-- free monad.
instance Monad Formula where
  return = Atom
  fm >>= f =
    case fm of
      True       -> True
      False      -> False
      Atom a     -> f a
      Not p      -> Not (p >>= f)
      p `And` q  -> (p >>= f) `And` (q >>= f)
      p `Or` q   -> (p >>= f) `Or` (q >>= f)
      p :=> q    -> (p >>= f) :=> (q >>= f)
      p :<=> q   -> (p >>= f) :<=> (q >>= f)
      Forall x p -> Forall x (p >>= f)
      Exists x p -> Exists x (p >>= f)

-- > let sub "p" = ("p" `And` "q"); sub atm = atm
-- >  "p" `And` "q" `And` "p" `And` "q" >>= sub
-- (Atom "p" `And` Atom "q") `And` (Atom "q" `And` ((Atom "p" `And` Atom "q") `And` Atom "q"))

instance Applicative Formula where
  pure = return
  (<*>) = ap

instance IsString a => IsString (Formula a) where
  fromString = Atom . fromString

newtype Prop = P
  { pname :: String
  } deriving (Show, Eq)

-- Evaluation

eval :: Formula a -> (a -> Bool) -> Bool
eval fm v =
  case fm of
    False     -> Prelude.False
    True      -> Prelude.True
    Atom x    -> v x
    Not p     -> not (eval p v)
    p `And` q -> eval p v && eval q v
    p `Or` q  -> eval p v || eval q v
    p :=> q   -> not (eval p v) || (eval q v)
    p :<=> q  -> eval p v == eval q v

-- > let v atm = case atm of { "p" -> Prelude.True; "q" -> Prelude.False; "r" -> Prelude.True }
-- > eval (Atom "p" `And` Atom "q" :=> Atom "q" `And` Atom "r") v
-- True

-- Truth-tables mechanized

atoms :: Eq a => Formula a -> [a]
atoms = nub . toList

onAllValuationsA
  :: (Applicative f, Eq t)
  => ((t -> Bool) -> f Bool) -> (t -> Bool) -> [t] -> f Bool
onAllValuationsA subfn v ats =
  case ats of
    [] -> subfn v
    (p:ps) ->
      let v' t q
            | q == p = t
            | otherwise = v q
      in liftA2
           (&&)
           (onAllValuationsA subfn (v' Prelude.False) ps)
           (onAllValuationsA subfn (v' Prelude.True) ps)

printTruthtable fm = do
  let ats = atoms fm
      width = maximum (5 : fmap length ats) + 1
      fixw s = take width (s ++ repeat ' ')
      mkRow v = do
        let lis = map (show . v) ats
            ans = show (eval fm v)
        putStrLn (concatMap fixw lis ++ "| " ++ ans)
        return Prelude.True
      separator = replicate (width * length ats + 9) '-'
  putStrLn (concatMap fixw ats ++ "| formula")
  putStrLn separator
  _ <- onAllValuationsA mkRow (const Prelude.False) ats
  return ()

onAllValuations
  :: Eq t
  => ((t -> Bool) -> Bool) -> (t -> Bool) -> [t] -> Bool
onAllValuations subfn v ats =
    runIdentity $ onAllValuationsA (Identity . subfn) v ats

tautology :: Eq a => Formula a -> Bool
tautology fm = onAllValuations (eval fm) (const Prelude.False) (atoms fm)

unsatisfiable :: Eq a => Formula a -> Bool
unsatisfiable = tautology . Not

satisfiable :: Eq a => Formula a -> Bool
satisfiable = not . unsatisfiable

-- A version of substitution that works on partial functions (functions which
-- produce a Maybe).
psubst :: (a -> Maybe (Formula a)) -> Formula a -> Formula a
psubst subfn fn = fn >>= fromMaybe <$> Atom <*> subfn