{- |
Description: Generation of truth tables for 'Logic's.
License: GNU LGPLv3
Maintainer: paul.bittner@uni-ulm.de

Generation of truth tables for 'Logic's.
-}
module Truthtable where

import Logic

-- | For a unary operator and a set of values, produces all results when applying that operator to that set of values.
unarytable :: Logic a => (a -> a) -> [a] -> [a]
unarytable :: (a -> a) -> [a] -> [a]
unarytable op :: a -> a
op values :: [a]
values = (a -> a) -> a -> a
forall l. Logic l => (l -> l) -> l -> l
leval a -> a
forall a. a -> a
id (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
op (a -> a) -> [a] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
values

-- | Builds the cartesions product of two lists.
cartesian :: [a] -> [b] -> [(a, b)]
cartesian :: [a] -> [b] -> [(a, b)]
cartesian x :: [a]
x y :: [b]
y = (,) (a -> b -> (a, b)) -> [a] -> [b -> (a, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
x [b -> (a, b)] -> [b] -> [(a, b)]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b]
y

-- | For a binary operator and a set of values, produces all results when applying that operator to all combinations of values.
binarytable :: Logic a => (a -> a -> a) -> [a] -> [a]
binarytable :: (a -> a -> a) -> [a] -> [a]
binarytable op :: a -> a -> a
op values :: [a]
values = (a -> a) -> a -> a
forall l. Logic l => (l -> l) -> l -> l
leval a -> a
forall a. a -> a
id (a -> a) -> ((a, a) -> a) -> (a, a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> a) -> (a, a) -> a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> a
op ((a, a) -> a) -> [(a, a)] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian [a]
values [a]
values

-- | Creates a function of two arguments by reusing a function on lists.
binarify :: ([a] -> b) -> (a -> a -> b)
binarify :: ([a] -> b) -> a -> a -> b
binarify f :: [a] -> b
f = \x :: a
x -> \y :: a
y -> [a] -> b
f [a
x, a
y]

-- | Appends spaces to the given string until it has length @i@ (first argument).
hfillto :: Int -> String -> String
hfillto :: Int -> String -> String
hfillto i :: Int
i s :: String
s
    | Int
missingspace Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 = (String
sString -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
missingspace ' '
    | Bool
otherwise = String
s
    where missingspace :: Int
missingspace = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s

-- | Default value for width of lines when printing truth tables.
defaultlinewidth :: Int
defaultlinewidth :: Int
defaultlinewidth = 7

-- | 'hfillto' with 'defaultlinewidth'
defaulthfillto :: String -> String
defaulthfillto :: String -> String
defaulthfillto = Int -> String -> String
hfillto Int
defaultlinewidth

-- | For a list of values and a unary operator, generates a truth table with the given name.
prettyunarytable :: (Logic a, Show a) => [a] -> (a -> a) -> String -> String
prettyunarytable :: [a] -> (a -> a) -> String -> String
prettyunarytable values :: [a]
values op :: a -> a
op name :: String
name = ((String
nameString -> String -> String
forall a. [a] -> [a] -> [a]
++"\n"String -> String -> String
forall a. [a] -> [a] -> [a]
++(Int -> Char -> String
forall a. Int -> a -> [a]
replicate (2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
defaultlinewidthInt -> Int -> Int
forall a. Num a => a -> a -> a
+3) '_')String -> String -> String
forall a. [a] -> [a] -> [a]
++"\n")String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall a. Monoid a => [a] -> a
mconcat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (\(val :: a
val, res :: a
res) -> [String] -> String
unwords [String -> String
defaulthfillto (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
val, "|", String -> String
defaulthfillto (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
res, "\n"]) ((a, a) -> String) -> [(a, a)] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
values ((a -> a) -> [a] -> [a]
forall a. Logic a => (a -> a) -> [a] -> [a]
unarytable a -> a
op [a]
values)

-- | For a list of values and a binary operator, generates a truth table with the given name.
prettybinarytable :: (Logic a, Show a) => [a] -> (a -> a -> a) -> String -> String
prettybinarytable :: [a] -> (a -> a -> a) -> String -> String
prettybinarytable values :: [a]
values op :: a -> a -> a
op name :: String
name = ((String
nameString -> String -> String
forall a. [a] -> [a] -> [a]
++"\n"String -> String -> String
forall a. [a] -> [a] -> [a]
++(Int -> Char -> String
forall a. Int -> a -> [a]
replicate (3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
defaultlinewidthInt -> Int -> Int
forall a. Num a => a -> a -> a
+4) '_')String -> String -> String
forall a. [a] -> [a] -> [a]
++"\n")String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall a. Monoid a => [a] -> a
mconcat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (\((a :: a
a, b :: a
b), res :: a
res) -> [String] -> String
unwords [String -> String
defaulthfillto (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
a, String -> String
defaulthfillto (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
b, "|", String -> String
defaulthfillto (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
res, "\n"]) (((a, a), a) -> String) -> [((a, a), a)] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, a)] -> [a] -> [((a, a), a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(a, a)]
pairs ((a -> a -> a) -> [a] -> [a]
forall a. Logic a => (a -> a -> a) -> [a] -> [a]
binarytable a -> a -> a
op [a]
values)
    where pairs :: [(a, a)]
pairs = [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian [a]
values [a]
values

-- | Generates a truthtable for all common operators of a logic (not, and, or, implies, equals) for the given set of values.
generatetruthtablesfor :: (Logic a, Show a) => [a] -> String
generatetruthtablesfor :: [a] -> String
generatetruthtablesfor values :: [a]
values =
    let
        notname :: String
notname = "¬"
        andname :: String
andname = "∧"
        orname :: String
orname  = "∨"
        impliesname :: String
impliesname = "⇒"
        equalsname :: String
equalsname = "⇔"
        in
    [a] -> (a -> a) -> String -> String
forall a. (Logic a, Show a) => [a] -> (a -> a) -> String -> String
prettyunarytable [a]
values a -> a
forall l. Logic l => l -> l
lnot String
notname
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Monoid a => [a] -> a
mconcat (("\n\n"String -> String -> String
forall a. [a] -> [a] -> [a]
++)(String -> String)
-> ((a -> a -> a, String) -> String)
-> (a -> a -> a, String)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.((a -> a -> a) -> String -> String)
-> (a -> a -> a, String) -> String
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([a] -> (a -> a -> a) -> String -> String
forall a.
(Logic a, Show a) =>
[a] -> (a -> a -> a) -> String -> String
prettybinarytable [a]
values)
        ((a -> a -> a, String) -> String)
-> [(a -> a -> a, String)] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [
              (([a] -> a) -> a -> a -> a
forall a b. ([a] -> b) -> a -> a -> b
binarify [a] -> a
forall l. Logic l => [l] -> l
land, String
andname)
            , (([a] -> a) -> a -> a -> a
forall a b. ([a] -> b) -> a -> a -> b
binarify [a] -> a
forall l. Logic l => [l] -> l
lor, String
orname)
            , (a -> a -> a
forall l. Logic l => l -> l -> l
limplies, String
impliesname)
            , (a -> a -> a
forall l. Logic l => l -> l -> l
lequals, String
equalsname)
            ])