packages feed

lazysmallcheck-0.1: benchmarks/Mux.hs

import Data.List

-- Binary multiplexor

tree              :: (a -> a -> a) -> [a] -> a
tree f [x]        =  x
tree f (x:y:ys)   =  tree f (ys ++ [f x y])

unaryMux          :: [Bool] -> [[Bool]] -> [Bool]
unaryMux sel xs   =  map (tree (||))
                  $  transpose
                  $  zipWith (\s x -> map (s &&) x) sel xs

decode []         =  [True]
decode [x]        =  [not x,x]
decode (x:xs)     =  concatMap (\y -> [not x && y,x && y]) rest
  where
    rest          =  decode xs

binaryMux         :: [Bool] -> [[Bool]] -> [Bool]
binaryMux sel xs  =  unaryMux (decode sel) xs

num               :: [Bool] -> Int
num []            =  0
num (a:as)        =  (if a then 1 else 0) + 2 * num as

-- Property

prop_binMux :: ([Bool], [[Bool]]) -> Bool
prop_binMux (sel, xs) =
     ((length xs == 2 ^ length sel)
  && all ((== length (head xs)) . length) xs)
  ==> (binaryMux sel xs == xs !! num sel)