-- vim: expandtab: ts=2: sw=2: autoindent:
module TestType where

import Data.SparseBIT
import Type
import Monad
import Test.QuickCheck

bit :: Type -> Gen (BIT Type)
bit t = sized (bit' t)

bit' t 0        = oneof $ map return [I t, O t]
bit' t n | n>0  =
  case expand t of
    []  ->  bit' t 0
    ts  ->  liftM Bs  (sequence [bit' t k | t<-ts]) `ap`
                      return t
            where k = (n-1) `div` length ts


bits = sequence . map bit

forAllb t = forAll (bit t)
forAllbs ts = forAll (bits ts)


prop_or_O_lhs t  = forAllb t $ \x-> O t .| x =:= x
prop_or_O_rhs t  = forAllb t $ \x-> x .| O t =:= x

prop_or_I_lhs t  = forAllb t $ \x-> I t .| x =:= I t
prop_or_I_rhs t  = forAllb t $ \x-> x .| I t =:= I t

prop_or_xx t     = forAllb t $ \x-> x .| x =:= x

prop_or_commute t   = forAllbs[t,t] $ \[x,y]->
    x .| y =:= y .| x
prop_or_assoc t     = forAllbs[t,t,t] $ \[x,y,z]->
    (x.|y) .| z =:= x .| (y.|z)

prop_or_reduce_l t  = forAllbs[t,t] $ \[x,y]->
    x .| y =:= reduce x .| y
prop_or_reduce_r t  = forAllbs[t,t] $ \[x,y]->
    x .| y =:= x .| reduce y
prop_or_reduce t    = forAllbs[t,t] $ \[x,y]->
    x .| y =:= reduce x .| reduce y


prop_and_O_lhs t  = forAllb t $ \x-> O t .& x =:= O t
prop_and_O_rhs t  = forAllb t $ \x-> x .& O t =:= O t

prop_and_I_lhs t  = forAllb t $ \x-> I t .& x =:= x
prop_and_I_rhs t  = forAllb t $ \x-> x .& I t =:= x

prop_and_xx t     = forAllb t $ \x-> x .& x =:= x

prop_and_commute t   = forAllbs[t,t] $ \[x,y]->
    x .& y =:= y .& x
prop_and_assoc t     = forAllbs[t,t,t] $ \[x,y,z]->
    (x.&y) .& z =:= x .& (y.&z)

prop_and_reduce_l t  = forAllbs[t,t] $ \[x,y]->
    x .& y =:= reduce x .& y
prop_and_reduce_r t  = forAllbs[t,t] $ \[x,y]->
    x .& y =:= x .& reduce y
prop_and_reduce t    = forAllbs[t,t] $ \[x,y]->
    x .& y =:= reduce x .& reduce y

prop_tprod_O_lhs t u  = forAllb u $ \y->
    O t .** y =:= O (t*.u)
prop_tprod_O_rhs t u  = forAllb t $ \x->
    x .** O u =:= O (t*.u)

prop_tprod_II t u     = I t .** I u =:= I (t*.u) where types = (t::Type,u::Type)

prop_tprod_reduce_l t u  = forAllbs[t,u] $ \[x,y]->
    x.**y =:= reduce x .** y
prop_tprod_reduce_r t u  = forAllbs[t,u] $ \[x,y]->
    x.**y =:= x .** reduce y
prop_tprod_reduce t u    = forAllbs[t,u] $ \[x,y]->
    x.**y =:= reduce x .** reduce y


prop_dist_or_and t      = forAllbs[t,t,t] $ \[x,y,z]->
    x .| (y.&z) =:= (x.|y) .& (x.|z)

prop_dist_and_or t      = forAllbs[t,t,t] $ \[x,y,z]->
    x .& (y.|z) =:= (x.&y) .| (x.&z)

prop_dist_tprod_or t u  = forAllbs[t,u,u] $ \[x,y,z]->
    x .** (y.|z) =:= (x.**y) .| (x.**z)

prop_dist_tprod_and t u = forAllbs[t,u,u] $ \[x,y,z]->
    x .** (y.&z) =:= (x.**y) .& (x.**z)