{- |
Description: Universal logic gates
Copyright: Copyright (C) 2021 Yoo Chung
License: GPL-3.0-or-later
Maintainer: dev@chungyc.org

Some solutions to "Problems.P47" of Ninety-Nine Haskell "Problems".
-}
module Solutions.P47 (evaluateCircuit, buildCircuit) where

import           Data.List     (nub)
import           Data.Map.Lazy (Map, (!))
import qualified Data.Map.Lazy as Map
import           Data.Maybe    (fromJust)
import           Data.Set      (Set)
import qualified Data.Set      as Set

-- | Evaluates a logic circuit.
evaluateCircuit :: [(Int,Int)] -> Bool -> Bool -> Bool
evaluateCircuit :: [(Int, Int)] -> Bool -> Bool -> Bool
evaluateCircuit [(Int, Int)]
circuit Bool
x Bool
y = Int -> [(Int, Int)] -> [(Int, Bool)] -> Bool
eval Int
1 [(Int, Int)]
circuit [(-Int
2,Bool
y), (-Int
1,Bool
x)]

eval :: Int -> [(Int,Int)] -> [(Int,Bool)] -> Bool
eval :: Int -> [(Int, Int)] -> [(Int, Bool)] -> Bool
eval Int
_ [] []                   = Bool
forall a. HasCallStack => a
undefined
eval Int
_ [] ((Int, Bool)
r:[(Int, Bool)]
_)                = (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd (Int, Bool)
r
eval Int
i ((Int
k,Int
l):[(Int, Int)]
circuit) [(Int, Bool)]
outputs = Int -> [(Int, Int)] -> [(Int, Bool)] -> Bool
eval (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [(Int, Int)]
circuit ([(Int, Bool)] -> Bool) -> [(Int, Bool)] -> Bool
forall a b. (a -> b) -> a -> b
$ (Int
i, Bool -> Bool -> Bool
nand Bool
x Bool
y) (Int, Bool) -> [(Int, Bool)] -> [(Int, Bool)]
forall a. a -> [a] -> [a]
: [(Int, Bool)]
outputs
  where x :: Bool
x = Maybe Bool -> Bool
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> [(Int, Bool)] -> Maybe Bool
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
k [(Int, Bool)]
outputs
        y :: Bool
y = Maybe Bool -> Bool
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> [(Int, Bool)] -> Maybe Bool
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
l [(Int, Bool)]
outputs

nand :: Bool -> Bool -> Bool
nand :: Bool -> Bool -> Bool
nand Bool
x Bool
y = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool
x Bool -> Bool -> Bool
&& Bool
y

{- |
Returns a logic circuit composed of NAND gates
which computes a given a binary boolean function.
The logic circuit should be in a form which 'evaluateCircuit' can evaluate.
-}
buildCircuit :: (Bool -> Bool -> Bool) -> [(Int,Int)]
buildCircuit :: (Bool -> Bool -> Bool) -> [(Int, Int)]
buildCircuit Bool -> Bool -> Bool
f = [(Table, Table)] -> [(Int, Int)]
indexCircuit [(Table, Table)]
c
  where c :: [(Table, Table)]
c = Map Table [(Table, Table)]
circuits Map Table [(Table, Table)] -> Table -> [(Table, Table)]
forall k a. Ord k => Map k a -> k -> a
! (Bool -> Bool -> Bool
f Bool
False Bool
False, Bool -> Bool -> Bool
f Bool
False Bool
True, Bool -> Bool -> Bool
f Bool
True Bool
False, Bool -> Bool -> Bool
f Bool
True Bool
True)

-- | Turns gates identified by the truth tables they produce into numerical indexes in the list.
indexCircuit :: [(Table,Table)] -> [(Int,Int)]
indexCircuit :: [(Table, Table)] -> [(Int, Int)]
indexCircuit [(Table, Table)]
c = [(Int, Int)] -> [(Int, Int)]
forall a. [a] -> [a]
reverse ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ [(Table, Table)]
-> Map Table Int -> Int -> [(Int, Int)] -> [(Int, Int)]
indexCircuit' [(Table, Table)]
c Map Table Int
rawinputs Int
1 []
  where rawinputs :: Map Table Int
rawinputs = [(Table, Int)] -> Map Table Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Table
inputLeft, -Int
1), (Table
inputRight, -Int
2)]

indexCircuit' :: [(Table,Table)] -> Map Table Int -> Int -> [(Int,Int)] -> [(Int,Int)]
indexCircuit' :: [(Table, Table)]
-> Map Table Int -> Int -> [(Int, Int)] -> [(Int, Int)]
indexCircuit' [] Map Table Int
_ Int
_ [(Int, Int)]
c         = [(Int, Int)]
c
indexCircuit' ((Table
l,Table
r):[(Table, Table)]
gs) Map Table Int
m Int
i [(Int, Int)]
c = [(Table, Table)]
-> Map Table Int -> Int -> [(Int, Int)] -> [(Int, Int)]
indexCircuit' [(Table, Table)]
gs Map Table Int
m' Int
i' [(Int, Int)]
c'
  where m' :: Map Table Int
m' = Table -> Int -> Map Table Int -> Map Table Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Table -> Table -> Table
nandTable Table
l Table
r) Int
i Map Table Int
m
        i' :: Int
i' = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
        c' :: [(Int, Int)]
c' = (Map Table Int
m Map Table Int -> Table -> Int
forall k a. Ord k => Map k a -> k -> a
! Table
l, Map Table Int
m Map Table Int -> Table -> Int
forall k a. Ord k => Map k a -> k -> a
! Table
r) (Int, Int) -> [(Int, Int)] -> [(Int, Int)]
forall a. a -> [a] -> [a]
: [(Int, Int)]
c

-- | Representation of a binary boolean function with a truth table.
--
-- The values are indexed by the input values in
-- the order of  @[(False, False), (False, True), (True, False), (True, True)]@.
type Table = (Bool, Bool, Bool, Bool)

-- | All possible truth tables.
tables :: [Table]
tables :: [Table]
tables = [(Bool
x,Bool
y,Bool
z,Bool
w) | Bool
x <- [Bool]
bools, Bool
y <- [Bool]
bools, Bool
z <- [Bool]
bools, Bool
w <- [Bool]
bools]
  where bools :: [Bool]
bools = [Bool
False, Bool
True]

-- | The truth table for the output of a NAND gate,
-- given that the outputs of the NAND gates serving as inputs
-- have the given truth tables.
--
-- The truth tables are indexed by the inputs to the entire logic circuit,
-- not the direct inputs into a gate.
-- Truth tables based on the latter would all be identical.
nandTable :: Table -> Table -> Table
nandTable :: Table -> Table -> Table
nandTable (Bool
x,Bool
y,Bool
z,Bool
w) (Bool
x',Bool
y',Bool
z',Bool
w') = (Bool
x Bool -> Bool -> Bool
`nand` Bool
x', Bool
y Bool -> Bool -> Bool
`nand` Bool
y', Bool
z Bool -> Bool -> Bool
`nand` Bool
z', Bool
w Bool -> Bool -> Bool
`nand` Bool
w')

-- | Truth table which behaves identically to the first input boolean variable.
-- I.e., the truth table for @\x -> \_ -> x@.
inputLeft :: Table
inputLeft :: Table
inputLeft = (Bool
False, Bool
False, Bool
True, Bool
True)

-- | Truth table which behaves identically to the second input boolean variable.
-- I.e., the truth table for @\_ -> \x -> x@.
inputRight :: Table
inputRight :: Table
inputRight = (Bool
False, Bool
True, Bool
False, Bool
True)

-- | Maps a truth table to a circuit producing the truth table.
--
-- Due to the way they are constructed, while the circuits may not have the minimum
-- number of gates possible, by induction they will be as shallow as possible.
circuits :: Map Table [(Table,Table)]
circuits :: Map Table [(Table, Table)]
circuits = ([(Table, Table)] -> [(Table, Table)])
-> Map Table [(Table, Table)] -> Map Table [(Table, Table)]
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map [(Table, Table)] -> [(Table, Table)]
forall a. Eq a => [a] -> [a]
nub (Map Table [(Table, Table)] -> Map Table [(Table, Table)])
-> Map Table [(Table, Table)] -> Map Table [(Table, Table)]
forall a b. (a -> b) -> a -> b
$ Map Table [(Table, Table)]
-> Set (Table, Table) -> Map Table [(Table, Table)]
build Map Table [(Table, Table)]
directCircuits Set (Table, Table)
remaining
  where gates :: Set (Table, Table)
gates = [(Table, Table)] -> Set (Table, Table)
forall a. Ord a => [a] -> Set a
Set.fromList [(Table
x,Table
y) | Table
x <- [Table]
tables, Table
y <- [Table]
tables]
        directGates :: [(Table, Table)]
directGates = [(Table
x,Table
y) | Table
x <- [Table
inputLeft, Table
inputRight], Table
y <- [Table
inputLeft, Table
inputRight]]
        directCircuits :: Map Table [(Table, Table)]
directCircuits = [(Table, [(Table, Table)])] -> Map Table [(Table, Table)]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Table, [(Table, Table)])] -> Map Table [(Table, Table)])
-> [(Table, [(Table, Table)])] -> Map Table [(Table, Table)]
forall a b. (a -> b) -> a -> b
$ ((Table, Table) -> (Table, [(Table, Table)]))
-> [(Table, Table)] -> [(Table, [(Table, Table)])]
forall a b. (a -> b) -> [a] -> [b]
map (\g :: (Table, Table)
g@(Table
l,Table
r) -> (Table
l Table -> Table -> Table
`nandTable` Table
r, [(Table, Table)
g])) [(Table, Table)]
directGates
        remaining :: Set (Table, Table)
remaining = Set (Table, Table) -> Set (Table, Table) -> Set (Table, Table)
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set (Table, Table)
gates (Set (Table, Table) -> Set (Table, Table))
-> Set (Table, Table) -> Set (Table, Table)
forall a b. (a -> b) -> a -> b
$ [(Table, Table)] -> Set (Table, Table)
forall a. Ord a => [a] -> Set a
Set.fromList [(Table, Table)]
directGates

-- | Build logic circuits for all possible binary boolean functions.
--
-- From a minimal set of gates directly connected to the input boolean variables,
-- it will compute what truth tables can be produced by feeding their outputs
-- to a NAND gate, which also provides the circuits which can compute the new truth tables.
-- This will be repeated until all possible outputs have been combined with a NAND gate,
-- during which logic circuits for all truth tables would be derived.
--
-- This takes adavantage of the fact that NAND is a universal logic gate.
-- For a logic gate that is not universal, it would reach a point where
-- it cannot produce a circuit for a set of remaining truth tables.
--
-- The same gate may appear multiple times in a circuit;
-- keeping the first one ensures that the circuit is still valid.
build :: Map Table [(Table,Table)]  -- ^ Circuits built so far.
      -> Set (Table,Table)          -- ^ Pair of inputs that have not been tried yet.
      -> Map Table [(Table,Table)]  -- ^ Circuits for all truth tables.
build :: Map Table [(Table, Table)]
-> Set (Table, Table) -> Map Table [(Table, Table)]
build Map Table [(Table, Table)]
built Set (Table, Table)
remaining
  | Set (Table, Table) -> Bool
forall a. Set a -> Bool
Set.null Set (Table, Table)
remaining = Map Table [(Table, Table)]
built
  | Bool
otherwise = Map Table [(Table, Table)]
-> Set (Table, Table) -> Map Table [(Table, Table)]
build Map Table [(Table, Table)]
built' Set (Table, Table)
remaining'
  where (Set (Table, Table)
inputs, Set (Table, Table)
remaining') = ((Table, Table) -> Bool)
-> Set (Table, Table) -> (Set (Table, Table), Set (Table, Table))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Table, Table) -> Bool
ready Set (Table, Table)
remaining
        ready :: (Table, Table) -> Bool
ready (Table
l,Table
r) = Table -> Map Table [(Table, Table)] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Table
l Map Table [(Table, Table)]
built Bool -> Bool -> Bool
&& Table -> Map Table [(Table, Table)] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Table
r Map Table [(Table, Table)]
built
        built' :: Map Table [(Table, Table)]
built' = Map Table [(Table, Table)]
-> Map Table [(Table, Table)] -> Map Table [(Table, Table)]
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Table [(Table, Table)]
built (Map Table [(Table, Table)] -> Map Table [(Table, Table)])
-> Map Table [(Table, Table)] -> Map Table [(Table, Table)]
forall a b. (a -> b) -> a -> b
$ [(Table, [(Table, Table)])] -> Map Table [(Table, Table)]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Table, [(Table, Table)])] -> Map Table [(Table, Table)])
-> [(Table, [(Table, Table)])] -> Map Table [(Table, Table)]
forall a b. (a -> b) -> a -> b
$ ((Table, Table) -> (Table, [(Table, Table)]))
-> [(Table, Table)] -> [(Table, [(Table, Table)])]
forall a b. (a -> b) -> [a] -> [b]
map (Table, Table) -> (Table, [(Table, Table)])
extend ([(Table, Table)] -> [(Table, [(Table, Table)])])
-> [(Table, Table)] -> [(Table, [(Table, Table)])]
forall a b. (a -> b) -> a -> b
$ Set (Table, Table) -> [(Table, Table)]
forall a. Set a -> [a]
Set.toList Set (Table, Table)
inputs
        extend :: (Table, Table) -> (Table, [(Table, Table)])
extend g :: (Table, Table)
g@(Table
l,Table
r) = (Table
l Table -> Table -> Table
`nandTable` Table
r, (Map Table [(Table, Table)]
built Map Table [(Table, Table)] -> Table -> [(Table, Table)]
forall k a. Ord k => Map k a -> k -> a
! Table
l) [(Table, Table)] -> [(Table, Table)] -> [(Table, Table)]
forall a. [a] -> [a] -> [a]
++ (Map Table [(Table, Table)]
built Map Table [(Table, Table)] -> Table -> [(Table, Table)]
forall k a. Ord k => Map k a -> k -> a
! Table
r) [(Table, Table)] -> [(Table, Table)] -> [(Table, Table)]
forall a. [a] -> [a] -> [a]
++ [(Table, Table)
g])