{- |
Description: Supporting definitions for logic and code problems
Copyright: Copyright (C) 2023 Yoo Chung
License: GPL-3.0-or-later
Maintainer: dev@chungyc.org

Supporting definitions for logic and code problems.
-}
module Problems.Logic (
  -- * Truth tables
  BoolFunc,
  -- ** Utility functions
  printTable,
  printTablen,
  Functions (Functions, getTable, getAnd, getOr, getNand, getNor, getXor, getImpl, getEqu),
  -- * Propositional logic
  Formula (..),
  -- ** Utility functions
  evaluateFormula
  ) where

import           Control.DeepSeq
import           Data.List       (sort)
import           Data.Map        (Map, (!))
import           GHC.Generics    (Generic)

-- | Define boolean functions 'Problems.P46.and'', 'Problems.P46.or'', 'Problems.P46.nand'',
-- 'Problems.P46.nor'', 'Problems.P46.xor'', 'Problems.P46.impl'', and 'Problems.P46.equ'',
-- which succeed or fail according to the result of their respective operations;
-- e.g., @(and' a b)@ is true if and only if both @a@ and @b@ are true.
-- Do not use the builtin boolean operators.
--
-- A logical expression in two variables can then be written as in the following example:
--
-- > \a b -> and' (or' a b) (nand' a b)
--
-- Write a function 'Problems.P46.table' which returns
-- the truth table of a given logical expression in two variables.
--
-- === __Notes__
--
-- There is no technical reason to define the type synonym 'BoolFunc'.
-- However, it is a good place to explain the entire problem
-- without talking about writing truth table functions first,
-- especially for inclusion in the documentation for "Problems".
--
-- The [original problem for Haskell](https://wiki.haskell.org/99_questions/46_to_50)
-- required that the truth table be printed:
-- /"Now, write a predicate table\/3 which prints the truth table of a given logical expression in two variables."/
-- It was changed here to return a list of boolean tuples, because the requirement
-- for I/O seemed uninteresting in the context of the rest of the problem.
--
-- Documentation for the expected semantics for each boolean function was added,
-- and the example for 'Problems.P46.table' was modified to avoid sensitivity to order.
type BoolFunc = Bool -> Bool -> Bool

-- | Print truth table as returned by 'Problems.P46.table'.
--
-- Given the same pair of truth tables except for order, the output will be the same.
printTable :: [(Bool, Bool, Bool)] -> IO ()
printTable :: [(Bool, Bool, Bool)] -> IO ()
printTable [(Bool, Bool, Bool)]
ts = ((Bool, Bool, Bool) -> IO ()) -> [(Bool, Bool, Bool)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn (String -> IO ())
-> ((Bool, Bool, Bool) -> String) -> (Bool, Bool, Bool) -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, Bool, Bool) -> String
showRow) ([(Bool, Bool, Bool)] -> IO ()) -> [(Bool, Bool, Bool)] -> IO ()
forall a b. (a -> b) -> a -> b
$ [(Bool, Bool, Bool)] -> [(Bool, Bool, Bool)]
forall a. Ord a => [a] -> [a]
sort [(Bool, Bool, Bool)]
ts
  where showRow :: (Bool, Bool, Bool) -> String
showRow (Bool
a, Bool
b, Bool
c) = Bool -> String
showBool Bool
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
showBool Bool
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
showBool Bool
c
        showBool :: Bool -> String
showBool Bool
a = if Bool
a then String
"True " else String
"False"

-- | Print truth table as returned by 'Problems.P48.tablen'.
--
-- Given the same pair of truth tables except for order, the output will be the same.
printTablen :: [[Bool]] -> IO ()
printTablen :: [[Bool]] -> IO ()
printTablen [[Bool]]
t = ([Bool] -> IO ()) -> [[Bool]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn (String -> IO ()) -> ([Bool] -> String) -> [Bool] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> String
showRow) ([[Bool]] -> IO ()) -> [[Bool]] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Bool]] -> [[Bool]]
forall a. Ord a => [a] -> [a]
sort [[Bool]]
t
  where showRow :: [Bool] -> String
showRow [Bool]
xs = [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Bool -> String) -> [Bool] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> String
showBool [Bool]
xs
        showBool :: Bool -> String
showBool Bool
a = if Bool
a then String
"True " else String
"False"

-- | Set of functions grouped together.
--
-- Useful for passing in a particular set of functions.
-- E.g., testing and benchmarking particular implementations.
data Functions = Functions { Functions -> (Bool -> Bool -> Bool) -> [(Bool, Bool, Bool)]
getTable :: (Bool -> Bool -> Bool) -> [(Bool, Bool, Bool)]
                           , Functions -> Bool -> Bool -> Bool
getAnd   :: Bool -> Bool -> Bool
                           , Functions -> Bool -> Bool -> Bool
getOr    :: Bool -> Bool -> Bool
                           , Functions -> Bool -> Bool -> Bool
getNand  :: Bool -> Bool -> Bool
                           , Functions -> Bool -> Bool -> Bool
getNor   :: Bool -> Bool -> Bool
                           , Functions -> Bool -> Bool -> Bool
getXor   :: Bool -> Bool -> Bool
                           , Functions -> Bool -> Bool -> Bool
getImpl  :: Bool -> Bool -> Bool
                           , Functions -> Bool -> Bool -> Bool
getEqu   :: Bool -> Bool -> Bool
                           }

-- | Represents a boolean formula.
data Formula
  -- | A constant value.
  = Value Bool
  -- | A variable with given name.
  | Variable String
  -- | Logical complement.  I.e., it is true only if its clause is false.
  | Complement Formula
  -- | Disjunction.  I.e., it is true if any of its clauses are true.
  | Disjoin [Formula]
  -- | Conjunction.   I.e., it is true only if all of its clauses are true.
  | Conjoin [Formula]
  deriving (Formula -> Formula -> Bool
(Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool) -> Eq Formula
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Formula -> Formula -> Bool
== :: Formula -> Formula -> Bool
$c/= :: Formula -> Formula -> Bool
/= :: Formula -> Formula -> Bool
Eq, Eq Formula
Eq Formula =>
(Formula -> Formula -> Ordering)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Formula)
-> (Formula -> Formula -> Formula)
-> Ord Formula
Formula -> Formula -> Bool
Formula -> Formula -> Ordering
Formula -> Formula -> Formula
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Formula -> Formula -> Ordering
compare :: Formula -> Formula -> Ordering
$c< :: Formula -> Formula -> Bool
< :: Formula -> Formula -> Bool
$c<= :: Formula -> Formula -> Bool
<= :: Formula -> Formula -> Bool
$c> :: Formula -> Formula -> Bool
> :: Formula -> Formula -> Bool
$c>= :: Formula -> Formula -> Bool
>= :: Formula -> Formula -> Bool
$cmax :: Formula -> Formula -> Formula
max :: Formula -> Formula -> Formula
$cmin :: Formula -> Formula -> Formula
min :: Formula -> Formula -> Formula
Ord, Int -> Formula -> String -> String
[Formula] -> String -> String
Formula -> String
(Int -> Formula -> String -> String)
-> (Formula -> String)
-> ([Formula] -> String -> String)
-> Show Formula
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Formula -> String -> String
showsPrec :: Int -> Formula -> String -> String
$cshow :: Formula -> String
show :: Formula -> String
$cshowList :: [Formula] -> String -> String
showList :: [Formula] -> String -> String
Show, (forall x. Formula -> Rep Formula x)
-> (forall x. Rep Formula x -> Formula) -> Generic Formula
forall x. Rep Formula x -> Formula
forall x. Formula -> Rep Formula x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Formula -> Rep Formula x
from :: forall x. Formula -> Rep Formula x
$cto :: forall x. Rep Formula x -> Formula
to :: forall x. Rep Formula x -> Formula
Generic, Formula -> ()
(Formula -> ()) -> NFData Formula
forall a. (a -> ()) -> NFData a
$crnf :: Formula -> ()
rnf :: Formula -> ()
NFData)

-- | Evaluate a boolean formula with the given mapping of variable names to values.
evaluateFormula :: Map String Bool -> Formula -> Bool
evaluateFormula :: Map String Bool -> Formula -> Bool
evaluateFormula Map String Bool
_ (Value Bool
x)      = Bool
x
evaluateFormula Map String Bool
m (Variable String
s)   = Map String Bool
m Map String Bool -> String -> Bool
forall k a. Ord k => Map k a -> k -> a
! String
s
evaluateFormula Map String Bool
m (Complement Formula
f) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map String Bool -> Formula -> Bool
evaluateFormula Map String Bool
m Formula
f
evaluateFormula Map String Bool
m (Disjoin [Formula]
fs)   = (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Map String Bool -> Formula -> Bool
evaluateFormula Map String Bool
m) [Formula]
fs
evaluateFormula Map String Bool
m (Conjoin [Formula]
fs)   = (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Map String Bool -> Formula -> Bool
evaluateFormula Map String Bool
m) [Formula]
fs