-- An implementation of a "block view" of Mary's FMCAD'04 multiplier. This
-- version improves Mary's by making sure there is at most one half adder per
-- column. The recursion in compressBlock is different in that it works from the
-- bottom. This allows the blocks to be chosen more greedily, and this will
-- supposedly be easier to extend to a description with 5:3-compressors (or
-- higher).
--
-- Another advantage is that (even though the code is bigger) it is easier to
-- understand the recursion. The following pictures explain the different steps:
--
--   Carry signals left:
--
--     x+1         x         x-1
--    ,---,      ,---,      ,---,
--  --| F |--  --| H |--  --| W |
--    '---'      '---'      '---'
--      x          x          x
--
--   No carry signals left:
--
--   x+2      x+1
--  ,---,    ,---,
--  | F |--  | H |--
--  '---'    '---'
--    x        x
--
-- compressY uses the steps in the upper picture until there are no carry
-- signals left (and this is bound to happen since each step removes one carry).
-- Then compressNoY uses the lower picture to compress all remaining x signals.



import Data.List hiding (insert)
import Control.Monad
import Test.QuickCheck
import System.Random

import Wired
import Libs.Nangate45.Wired



data Block = W | H | F
     deriving (Eq,Ord,Show)



smallNat :: (Random n, Integral n) => Gen n
smallNat = sized $ \n -> choose (0, fromIntegral n)

smallPos :: (Random n, Integral n) => Gen n
smallPos = sized $ \n -> choose (1, fromIntegral n + 1)

partProds :: Gen [Int]
partProds = sized $ \n -> do
    m  <- smallPos
    replicateM m smallPos

count :: Eq a => a -> [a] -> Int
count a = length . filter (==a)

maxSum :: Num a => [a] -> a
maxSum xs
    = sum
    $ map (uncurry (*))
    $ zip xs (map product $ inits $ repeat 2)
  -- The biggest number the part. prods. can sum up to

bits :: (Integral b, Integral a) => a -> b
bits n = ceiling (log (fromIntegral (n+1)) / log 2)
  -- Number of bits needed to represent n



compressBlock :: Int -> Int -> ([Block], Int)

compressBlock xTot yTot

    | xTot<=1 && yTot==0 = ([],0)
    | xTot==0 && yTot==1 = ([W],0)
      -- Cases with <= 1 signal out

    | otherwise = (reverse col, y')

  where
    (col,y') = compressY 2 yTot

    compressY x 0 = compressNoY x
    compressY x y
        | diff == 0 = (W:col1, y1)
        | diff == 1 = (H:col2, y2+1)
        | diff >= 2 = (F:col3, y3+1)
      where
        diff = y+xTot-x

        (col1,y1) = compressY (x-1) (y-1)
        (col2,y2) = compressY x     (y-1)
        (col3,y3) = compressY (x+1) (y-1)

    compressNoY x
        | diff == 0 = ([],0)
        | diff == 1 = (H:col1, y1+1)
        | diff >= 2 = (F:col2, y2+1)
      where
        diff = xTot-x

        (col1,y1) = compressNoY (x+1)
        (col2,y2) = compressNoY (x+2)



prop_compressBlock1 = forAll smallNat $ \x -> forAll smallNat $ \y ->
    let blocks = fst $ compressBlock x y
     in blocks == sort blocks
  -- Blocks are ordered.

prop_compressBlock2 = forAll smallNat $ \x -> forAll smallNat $ \y ->
    let blocks = fst $ compressBlock x y
     in count H blocks <= 1
  -- There is at most one H in a column.

prop_compressBlock3 = forAll smallNat $ \x -> forAll smallNat $ \y ->
    let (blocks,y') = compressBlock x y
     in length blocks == max y y'
  -- The number of blocks in the column is equal to the maximum number of carry
  -- signals going in or out.

prop_compressBlock4 = forAll smallNat $ \x -> forAll smallNat $ \y ->
    let (blocks,yOut) = compressBlock x y
        removed       = count F blocks
     in x+y>=2 ==> removed == (x+y) - (2+yOut)
  -- The number of removed (compressed) bits is equal to the difference between
  -- #signals in and #signals out.



redArrayBlock :: [Int] -> [[Block]]
redArrayBlock xs = red xs 0
  where
    red [] 0 = []

    red [] y = blocks : red [] yOut
      where
        (blocks,yOut) = compressBlock 0 y

    red (x:xs) y = blocks : red xs yOut
      where
        (blocks,yOut) = compressBlock x y



prop_redArrayBlock1 = forAll partProds $ \xs ->
    let w    = length xs
        h    = maximum xs
        wOut = length $ redArrayBlock xs
     in wOut <= w+h-1

prop_redArrayBlock2 = forAll partProds $ \xs ->
    let w    = length xs
        wOut = length $ redArrayBlock xs
     in wOut >= w

prop_redArrayBlock3 = forAll partProds $ \xs ->
    let bss     = redArrayBlock xs
        removed = sum $ map (count F) bss
        remains = sum xs - removed
     in remains >= length bss && remains <= 2 * length bss
  -- The number of removed (compressed) bits is equal to the difference between
  -- #signals in and #signals out. It's hard to determine the #signals out,
  -- because some columns may only have one bit out. Therefore we just check the
  -- interval.

prop_redArrayBlock4 = forAll partProds $ \xs ->
    let wOut = length $ redArrayBlock xs
        s    = maxSum $ map fromIntegral xs
     in bits s `elem` [wOut, wOut+1]
  -- The number of bits needed to count all inputs (times signigicance) is equal
  -- to, or one more than the number of columns (final adder might add one bit).



checkAll = do
    quickCheck prop_compressBlock1
    quickCheck prop_compressBlock2
    quickCheck prop_compressBlock3
    quickCheck prop_compressBlock4
    quickCheck prop_redArrayBlock1
    quickCheck prop_redArrayBlock2
    quickCheck prop_redArrayBlock3
    quickCheck prop_redArrayBlock4



--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------



type CircBlock =
       (Maybe Signal, [Signal]) -> Wired Nangate45 ([Signal], Maybe Signal)

insert a bs = bs ++ [a]

bus ps = rotate 1 $ space 200e-9 () >> guide 1 200e-9 ps



c22 :: CircBlock

c22 (Nothing, ps@(_:_:_)) = do
    p1:p2:ps' <- bus ps
    (s,c) <- ha_x1 (p1,p2)
    return (insert s ps', Just c)

c22 (Just c, ps@(_:_)) = do
    ps' <- bus ps
    let p1:p2:ps'' = insert c ps'
    (s,c') <- ha_x1 (p1,p2)
    return (insert s ps'', Just c')



c32 :: CircBlock

c32 (Nothing, ps@(_:_:_:_)) = do
    p1:p2:p3:ps' <- bus ps
    (s,c) <- flipX $ fa_x1 (p1,(p2,p3))
    return (insert s ps', Just c)

c32 (Just c, ps@(_:_:_)) = do
    ps' <- bus ps
    let p1:p2:p3:ps'' = insert c ps'
    (s,c') <- flipX $ fa_x1 (p1,(p2,p3))
    return (insert s ps'', Just c')



wir :: CircBlock
wir (Just c, ps) = do
    ps' <- bus $ insert c ps
    return (ps', Nothing)

circBlock :: Block -> CircBlock
circBlock W = wir
circBlock H = c22
circBlock F = c32



buildColumn
    :: [Block]
    -> ([Maybe Signal], [Signal])
    -> Wired Nangate45 ([Signal], [Maybe Signal])

buildColumn [] (_,ps) = return (ps,[])

buildColumn (b:bs) (c:cs, ps) = do
    (ps',cs') <- buildColumn bs (cs,ps)
    -- unless (b==W) $ space 500e-9 ()
    (ss,c')   <- circBlock b (c,ps')
    return (ss, c':cs')



buildArray :: Int -> [[Block]] -> [[Signal]] -> Wired Nangate45 [[Signal]]
buildArray h bss pss = build bss [] pss
  where
    build [] _ _ = return []

    build (bs:bss) cs (ps:pss) = do
        (ss,cs') <- downwards $ do
            ps' <- space h' =<< bus ps
            (ss,cs') <- space 1000e-9 =<< buildColumn
                (reverse bs) (cs ++ repeat Nothing, ps')
            ss' <- bus ss
            return (ss',cs')
        sss <- build bss cs' pss
        return (ss:sss)
      where
        r  = result (rowHeight :: Res Nangate45 Length)
        h' = r `mulLen` (h - length (filter (/=W) bs))



redArray :: [[Signal]] -> Wired Nangate45 [[Signal]]
redArray pss = rightwards $ buildArray h bss (pss ++ repeat [])
  where
    bss = redArrayBlock $ map length pss
    h   = maximum $ map genericLength bss



inp n = sequence
     $ [inputList m | m <- [1..n]]
    ++ [inputList m | m <- reverse [1..n-1]]

redArrayIO = inp 12 >>= redArray



test1 = renderWiredWithNets "circ" redArrayIO