{- |
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 = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, Bool, Bool) -> String
showRow) forall a b. (a -> b) -> a -> b
$ 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 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Bool -> String
showBool Bool
b forall a. [a] -> [a] -> [a]
++ 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> String
showRow) forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
sort [[Bool]]
t
  where showRow :: [Bool] -> String
showRow [Bool]
xs = [String] -> String
unwords forall a b. (a -> b) -> a -> b
$ 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Formula -> Formula -> Bool
$c/= :: Formula -> Formula -> Bool
== :: Formula -> Formula -> Bool
$c== :: Formula -> Formula -> Bool
Eq, Eq 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
min :: Formula -> Formula -> Formula
$cmin :: Formula -> Formula -> Formula
max :: Formula -> Formula -> Formula
$cmax :: Formula -> Formula -> Formula
>= :: Formula -> Formula -> Bool
$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
compare :: Formula -> Formula -> Ordering
$ccompare :: Formula -> Formula -> Ordering
Ord, Int -> Formula -> ShowS
[Formula] -> ShowS
Formula -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Formula] -> ShowS
$cshowList :: [Formula] -> ShowS
show :: Formula -> String
$cshow :: Formula -> String
showsPrec :: Int -> Formula -> ShowS
$cshowsPrec :: Int -> Formula -> ShowS
Show, 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
$cto :: forall x. Rep Formula x -> Formula
$cfrom :: forall x. Formula -> Rep Formula x
Generic, Formula -> ()
forall a. (a -> ()) -> NFData a
rnf :: Formula -> ()
$crnf :: 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 forall k a. Ord k => Map k a -> k -> a
! String
s
evaluateFormula Map String Bool
m (Complement Formula
f) = Bool -> Bool
not 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)   = 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)   = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Map String Bool -> Formula -> Bool
evaluateFormula Map String Bool
m) [Formula]
fs