-- # Software Tools for Discrete Mathematics
module Stdm13 where

-- # Chapter 13.  Discrete Mathematics in Circuit Design
inv :: Bool -> Bool
inv = not

and2 :: Bool -> Bool -> Bool
and2 = (&&)

and3 :: Bool -> Bool -> Bool -> Bool
and3 True True True = True
and3 _ _ _ = False

or2 :: Bool -> Bool -> Bool
or2 = (||)

-- xor circuit truth table
-- a b | out | long
-- 0 0   0
-- 1 1   0
-- 0 1   1     ¬a ∧ b
-- 1 0   1     a ∧ ¬b

-- Derived from table:
-- (¬a ∧ b) ∨ (a ∧ ¬b)

xor :: Bool -> Bool -> Bool
xor = (/=)

-- Table-derived construction:
xorV0 :: Bool -> Bool -> Bool
xorV0 a b = or2 (and2 (inv a) b) (and2 a (inv b))

-- The xor gate can be made from other gates as well:
-- https://en.wikipedia.org/wiki/XOR_gate#Alternatives

xorV1 :: Bool -> Bool -> Bool
xorV1 a b = and2 (inv (and2 a b)) (or2 a b)

xorV2 :: Bool -> Bool -> Bool
xorV2 a b =
  inv
    ( and2
        ( inv
            ( and2
                a
                (inv (and2 a b))
            )
        )
        ( inv
            ( and2
                (inv (and2 a b))
                b
            )
        )
    )

xorV3 :: Bool -> Bool -> Bool
xorV3 a b =
  or2
    ( inv
        ( or2
            a
            (inv (or2 a b))
        )
    )
    ( inv
        ( or2
            (inv (or2 a b))
            b
        )
    )

-- A multiplexor is the hardware equivalent of a conditional (if—then—else) expression.
-- It takes a control input a and two data inputs, x and y.
-- There is one output;
-- if a is 0 then the output is x,
-- but if a is 1 then the output is y.
-- The circuit is implemented using the standard logic gates.

-- | if not True then True else False
-- >>> mux1 True True False
-- False

-- | if not True then False else True
-- >>> mux1 True False True
-- True

-- | if not False then True else False
-- >>> mux1 False True False
-- True

-- | if not False then False else True
-- >>> mux1 False False True
-- False
mux1 :: Bool -> Bool -> Bool -> Bool
mux1 a x y = or2 (and2 (inv a) x) (and2 a y)

-- A demultiplexor is the opposite of a multiplexor.
-- It has a single data input x and a control input a.
-- The circuit produces two outputs (z0, z1).
-- The x input is sent to whichever output is selected by a,
-- and the other output is 0 regardless of the value of x.

-- |
-- >>> demux1 True True
-- (False,True)

-- |
-- >>> demux1 True False
-- (False,False)

-- |
-- >>> demux1 False True
-- (True,False)

-- |
-- >>> demux1 False False
-- (False,False)
demux1 :: Bool -> Bool -> (Bool, Bool)
demux1 a x = (and2 (inv a) x, and2 a x)

-- | Convert True to 1
-- >>> bitValue True
-- 1

-- | Convert False to 0
-- >>> bitValue False
-- 0
bitValue :: Bool -> Int
bitValue x = if x == False then 0 else 1

-- | Convert any array of [Bool] to it's base 10 integer value.
-- >>> wordValue [True,False,False,True,False]
-- 18

-- | Max value in a Byte.
-- >>> wordValue (replicate 8 True)
-- 255
wordValue :: [Bool] -> Int
wordValue [] = 0
wordValue (x : xs) =
  let k = length xs
   in 2 ^ k * bitValue x + wordValue xs

-- Half adder adds two bits.
-- https://en.wikipedia.org/wiki/Adder_(electronics)#Half_adder
-- Theorem 106 (correctness of half-adder). Let (c, s) = halfAdd a b.
-- Then 2 × bitValue c + bitValue s = bitValue a + bitValue b.
-- Proof. This theorem is easily proved by checking the equation,
-- for each of the four possible combinations of input values.

-- | 0 + 0
-- >>> halfAdd False False
-- (False,False)

-- | 0 + 1
-- >>> halfAdd False True
-- (False,True)

-- | 1 + 0
-- >>> halfAdd True False
-- (False,True)

-- | 1 + 1
-- >>> halfAdd True True
-- (True,False)
halfAdd :: Bool -> Bool -> (Bool, Bool)
halfAdd a b = (and2 a b, xor a b)

-- Full adder adds 3 bits.
-- https://en.wikipedia.org/wiki/Adder_(electronics)#Full_adder
-- Theorem 107 (Correctness of full adder).
-- Let (c' , s) = fullAdd (a, b) c,
-- so that c' is the carry output,
-- and s is the sum output.
-- Then bitValue c' × 2 + bitValue s = bitValue a + bitValue b + bitValue c.

-- | 0 + 0 + 0
-- >>> fullAdd (False, False) False
-- (False,False)

-- | 0 + 0 + 1
-- >>> fullAdd (False, False) True
-- (False,True)

-- | 0 + 1 + 0
-- >>> fullAdd (False, True) False
-- (False,True)

-- | 0 + 1 + 1
-- >>> fullAdd (False, True) True
-- (True,False)

-- | 1 + 0 + 0
-- >>> fullAdd (True, False) False
-- (False,True)

-- | 1 + 0 + 1
-- >>> fullAdd (True, False) True
-- (True,False)

-- | 1 + 1 + 0
-- >>> fullAdd (True, True) False
-- (True,False)

-- | 1 + 1 + 1
-- >>> fullAdd (True,  True)  True
-- (True,True)
fullAdd :: (Bool, Bool) -> Bool -> (Bool, Bool)
fullAdd (a, b) c =
  let (w, x) = halfAdd a b
      (y, z) = halfAdd x c
   in (or2 w y, z)

-- Ripple carry adders
-- https://en.wikipedia.org/wiki/Adder_(electronics)#Ripple-carry_adder
-- Example: addition of 3 + 8
--    3 + 8
--    =   0011   (  2+1 =  3)
--      + 1000   (    8 =  8)
--    =   1011   (8+2+1 = 11)

-- | 3 + 8
-- >>> add4 False [(False,True),(False,False),(True,False),(True,False)]
-- (False,[True,False,True,True])
add4 :: Bool -> [(Bool, Bool)] -> (Bool, [Bool])
add4 c [(x0, y0), (x1, y1), (x2, y2), (x3, y3)] =
  let (c3, s3) = fullAdd (x3, y3) c
      (c2, s2) = fullAdd (x2, y2) c3
      (c1, s1) = fullAdd (x1, y1) c2
      (c0, s0) = fullAdd (x0, y0) c1
   in (c0, [s0, s1, s2, s3])

-- Theorem 108 (The n-Bit Ripple Carry Adder).
-- Let xs and ys be k-bit words, so xs, ys :: Signal a ⇒ [a].
-- Define (c, sum) = rippleAdd zero (zip xs ys);
-- thus c :: a is the carry output and ss :: [a] is the sum word. Then:
-- bitValue c * (2 ^ k) + wordValue ss = wordValue xs + wordValue ys.

-- |
-- >>> mscanr fullAdd True [(True,True)]
-- (True,[True])

-- |
-- >>> mscanr fullAdd True [(True,True),(True,True)]
-- (True,[True,True])
mscanr :: ((Bool, Bool) -> Bool -> (Bool, Bool)) -> Bool -> [(Bool, Bool)] -> (Bool, [Bool])
mscanr f a [] = (a, [])
mscanr f a (x : xs) =
  let (a', ys) = mscanr f a xs
      (a'', y) = f x a'
   in (a'', y : ys)

-- Example: addition of 23+11
--    23 + 11
--    =   010111   (16+4+2+1 = 23)
--      + 001011   (   8+2+1 = 11) with carry input = 0
--    =   100010   (    32+2 = 34) with carry output = 0

-- | 23 + 11
-- >>> rippleAdd False [(False,False),(True,False),(False,True),(True,False),(True,True),(True,True)]
-- (False,[True,False,False,False,True,False])
rippleAdd :: Bool -> [(Bool, Bool)] -> (Bool, [Bool])
rippleAdd c zs = mscanr fullAdd c zs

-- Comparison of binary numbers is nearly as fundamental as adding them.
-- It is particularly interesting to consider how to implement a comparison circuit,
-- since this problem has some strong similarities and also some strong differences,
-- to the ripple carry adder.
-- halfCmp that compares two one-bit numbers x and y,
-- with the result of a Boolean in one position, either: (lt, eq, gt).

-- | Compare 0 to 1
-- >>> halfCmp (False, True)
-- (True,False,False)

-- | Compare 0 to 0
-- >>> halfCmp (False, False)
-- (False,True,False)

-- | Compare 1 to 1
-- >>> halfCmp (False, False)
-- (False,True,False)

-- | Compare 1 to 0
-- >>> halfCmp (True, False)
-- (False,False,True)
halfCmp :: (Bool, Bool) -> (Bool, Bool, Bool)
halfCmp (x, y) =
  ( and2 (inv x) y, -- x<y when x=0,y=1
    inv (xor x y), -- x=y when x=0,y=0 or x=1,y=1
    and2 x (inv y) -- x>y when x=1,y=0
  )

-- Next, we'll build a ripple comparator that takes two words representing binary numbers
-- (the words must have the same size),
-- and returns a triple of three bits (lt, eq, gt)
-- that indicate the result of comparing x and y.
-- Just as you compare two numbers by looking first at the most significant digits,
-- a binary comparison is performed by moving from left to right through the word.
-- Initially we assume the two words are equal;
-- represent this by (lt, eq, gt) = (0, 1, 0).
-- If the next bit position has x = 1 and y = 0,
-- then we know that the final result must be (0, 0, 1),
-- regardless of any bits to the right;
-- conversely if x = 0 and y = 1,
-- then the final result must be (1, 0, 0),
-- regardless of the bit values to the right.
-- However, if x and y have the same value in this bit position,
-- then as far as we know the result is still (0, 1, 0),
-- but that result might be changed later.

-- |
-- >>> foldl fullCmp (False, True, False) [(False,False),(True,False),(False,True),(True,False),(True,True),(True,True)]
-- (False,False,True)
fullCmp :: (Bool, Bool, Bool) -> (Bool, Bool) -> (Bool, Bool, Bool)
fullCmp (lt, eq, gt) (x, y) =
  ( or2 lt (and3 eq (inv x) y), -- <
    and2 eq (inv (xor x y)), -- =
    or2 gt (and3 eq x (inv y)) -- >
  )

-- | Compare 23 to 11:
-- >>> rippleCmp [(False,False),(True,False),(False,True),(True,False),(True,True),(True,True)]
rippleCmp :: [(Bool, Bool)] -> (Bool, Bool, Bool)
rippleCmp z = foldl fullCmp (False, True, False) z