import SparseCheck
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)        =  fromEnum a + 2 * num as

-- Property

gen_binMux :: Term [a] -> Term [[b]] -> Pred
gen_binMux sel xs = exists $ \(n, m, o) ->
                        len xs n
                      & len sel m
                      & pow (i 2) m n
                      & forall xs (\x -> len x o)

prop_binMux sel xs = binaryMux sel xs == xs !! num sel

check_binMux n = check2 n gen_binMux prop_binMux