text:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ViewPatterns      #-}
{-# LANGUAGE RecordWildCards   #-}
{-# LANGUAGE CPP               #-}
module ArrayFire.Internal.Types where

#include "af/seq.h"
#include "af/complex.h"
#include "af/graphics.h"
#include "af/index.h"

import ArrayFire.Internal.Defines

import Data.Complex
import Data.Proxy
import Data.Word
import Foreign.C.String
import Foreign.C.Types
import Foreign.ForeignPtr
import Foreign.Storable
import GHC.Int

data AFSeq
  = AFSeq
  { afSeqBegin :: {-# UNPACK #-} !Double
  , afSeqEnd   :: {-# UNPACK #-} !Double
  , afSeqStep  :: {-# UNPACK #-} !Double
  } deriving (Show, Eq)

instance Storable AFSeq where
  sizeOf _ = #{size af_seq}
  alignment _ = #{alignment af_seq}
  peek ptr = do
    afSeqBegin <- #{peek af_seq, begin} ptr
    afSeqEnd <- #{peek af_seq, end} ptr
    afSeqStep <- #{peek af_seq, step} ptr
    pure AFSeq {..}
  poke ptr AFSeq{..} = do
    #{poke af_seq, begin} ptr afSeqBegin
    #{poke af_seq, end} ptr afSeqEnd
    #{poke af_seq, step} ptr afSeqStep

-- | Type used for indexing into 'Array'
data AFIndex
  = AFIndex
  { afIdx :: !(Either AFArray AFSeq)
  , afIsSeq :: !Bool
  , afIsBatch :: !Bool
  }
instance Storable AFIndex where
  sizeOf _ = #{size af_index_t}
  alignment _ = #{alignment af_index_t}
  peek ptr = do
    afIsSeq <- #{peek af_index_t, isSeq} ptr
    afIsBatch <- #{peek af_index_t, isBatch} ptr
    afIdx <-
      if afIsSeq
        then Left <$> #{peek af_index_t, idx.arr} ptr
        else Right <$> #{peek af_index_t, idx.seq} ptr
    pure AFIndex{..}
  poke ptr AFIndex{..} = do
    case afIdx of
      Left afarr -> #{poke af_index_t, idx.arr} ptr afarr
      Right afseq -> #{poke af_index_t, idx.seq} ptr afseq
    #{poke af_index_t, isSeq} ptr afIsSeq
    #{poke af_index_t, isBatch} ptr afIsBatch

data AFCFloat
  = AFCFloat
  { afcReal :: {-# UNPACK #-} !Float
  , afcImag :: {-# UNPACK #-} !Float
  } deriving (Eq, Show)

instance Storable AFCFloat where
  sizeOf _ = #{size af_cfloat}
  alignment _ = #{alignment af_cfloat}
  peek ptr = do
    afcReal <- #{peek af_cfloat, real} ptr
    afcImag <- #{peek af_cfloat, imag} ptr
    pure AFCFloat{..}
  poke ptr AFCFloat{..} = do
    #{poke af_cfloat, real} ptr afcReal
    #{poke af_cfloat, imag} ptr afcImag

data AFCell
  = AFCell
  { afCellRow :: {-# UNPACK #-} !Int
  , afCellCol :: {-# UNPACK #-} !Int
  , afCellTitle :: {-# UNPACK #-} !CString
  , afCellColorMap :: {-# UNPACK #-} !AFColorMap
  } deriving (Show, Eq)

instance Storable AFCell where
  sizeOf _ = #{size af_cell}
  alignment _ = #{alignment af_cell}
  peek ptr = do
    afCellRow <- #{peek af_cell, row} ptr
    afCellCol <- #{peek af_cell, col} ptr
    afCellTitle <- #{peek af_cell, title} ptr
    afCellColorMap <- #{peek af_cell, cmap} ptr
    pure AFCell{..}
  poke ptr AFCell{..} = do
    #{poke af_cell, row} ptr afCellRow
    #{poke af_cell, col} ptr afCellCol
    #{poke af_cell, title} ptr afCellTitle
    #{poke af_cell, cmap} ptr afCellColorMap

-- | ArrayFire 'Array'
newtype Array a = Array (ForeignPtr ())

-- | ArrayFire 'Features'
newtype Features = Features (ForeignPtr ())

-- | ArrayFire 'RandomEngine'
newtype RandomEngine = RandomEngine (ForeignPtr ())

-- | ArrayFire 'Window'
newtype Window = Window (ForeignPtr ())

-- | Mapping of Haskell types to ArrayFire types
class Storable a => AFType a where
  afType :: Proxy a -> AFDtype

instance AFType Double where
  afType Proxy = f64

instance AFType Float where
  afType Proxy = f32

instance AFType (Complex Double) where
  afType Proxy = c64

instance AFType (Complex Float) where
  afType Proxy = c32

instance AFType CBool where
  afType Proxy = b8

instance AFType Int32 where
  afType Proxy = s32

instance AFType Word32 where
  afType Proxy = u32

instance AFType Word8 where
  afType Proxy = u8

instance AFType Int64 where
  afType Proxy = s64

instance AFType Int where
  afType Proxy = s64

instance AFType Int16 where
  afType Proxy = s16

instance AFType Word16 where
  afType Proxy = u16

instance AFType Word64 where
  afType Proxy = u64

instance AFType Word where
  afType Proxy = u64

-- | ArrayFire backends
data Backend
  = Default
  | CPU
  | CUDA
  | OpenCL
  deriving (Show, Eq, Ord)

-- | Low-level to high-level Backend conversion
toBackend :: AFBackend -> Backend
toBackend (AFBackend 0) = Default
toBackend (AFBackend 1) = CPU
toBackend (AFBackend 2) = CUDA
toBackend (AFBackend 4) = OpenCL
toBackend (AFBackend x) = error $ "Invalid backend: " <> show x

-- | High-level to low-level Backend conversion
toAFBackend :: Backend -> AFBackend
toAFBackend Default = (AFBackend 0)
toAFBackend CPU = (AFBackend 1)
toAFBackend CUDA = (AFBackend 2)
toAFBackend OpenCL = (AFBackend 4)

-- | Read multiple backends
toBackends :: Int -> [Backend]
toBackends 1 = [CPU]
toBackends 2 = [CUDA]
toBackends 3 = [CPU,CUDA]
toBackends 4 = [OpenCL]
toBackends 5 = [CPU,OpenCL]
toBackends 6 = [CUDA,OpenCL]
toBackends 7 = [CPU,CUDA,OpenCL]
toBackends _ = []

-- | Matrix properties
data MatProp
  = None
  | Trans
  | CTrans
  | Conj
  | Upper
  | Lower
  | DiagUnit
  | Sym
  | PosDef
  | Orthog
  | TriDiag
  | BlockDiag
  deriving (Show, Eq, Ord)

-- | Low-level to High-level 'MatProp' conversion
fromMatProp
  :: AFMatProp
  -> MatProp
fromMatProp (AFMatProp 0) = None
fromMatProp (AFMatProp 1) = Trans
fromMatProp (AFMatProp 2) = CTrans
fromMatProp (AFMatProp 4) = Conj
fromMatProp (AFMatProp 32) = Upper
fromMatProp (AFMatProp 64) = Lower
fromMatProp (AFMatProp 128) = DiagUnit
fromMatProp (AFMatProp 512) = Sym
fromMatProp (AFMatProp 1024) = PosDef
fromMatProp (AFMatProp 2048) = Orthog
fromMatProp (AFMatProp 4096) = TriDiag
fromMatProp (AFMatProp 8192) = BlockDiag
fromMatProp x = error $ "Invalid AFMatProp value: " <> show x

-- | High-level to low-level 'MatProp' conversion
toMatProp
  :: MatProp
  -> AFMatProp
toMatProp None = (AFMatProp 0)
toMatProp Trans = (AFMatProp 1)
toMatProp CTrans = (AFMatProp 2)
toMatProp Conj = (AFMatProp 4)
toMatProp Upper = (AFMatProp 32)
toMatProp Lower = (AFMatProp 64)
toMatProp DiagUnit = (AFMatProp 128)
toMatProp Sym = (AFMatProp 512)
toMatProp PosDef = (AFMatProp 1024)
toMatProp Orthog = (AFMatProp 2048)
toMatProp TriDiag = (AFMatProp 4096)
toMatProp BlockDiag = (AFMatProp 8192)

-- | Binary operation support
data BinaryOp
  = Add
  | Mul
  | Min
  | Max
  deriving (Show, Eq, Ord)

-- | High-level to low-level 'MatProp' conversion
toBinaryOp :: BinaryOp -> AFBinaryOp
toBinaryOp Add = AFBinaryOp 0
toBinaryOp Mul = AFBinaryOp 1
toBinaryOp Min = AFBinaryOp 2
toBinaryOp Max = AFBinaryOp 3

-- | 'BinaryOp' conversion helper
fromBinaryOp :: AFBinaryOp -> BinaryOp
fromBinaryOp (AFBinaryOp 0) = Add
fromBinaryOp (AFBinaryOp 1) = Mul
fromBinaryOp (AFBinaryOp 2) = Min
fromBinaryOp (AFBinaryOp 3) = Max
fromBinaryOp x = error ("Invalid Binary Op: " <> show x)

-- | Storage type used for Sparse arrays
data Storage
  = Dense
  | CSR
  | CSC
  | COO
  deriving (Show, Eq, Ord, Enum)

toStorage :: Storage -> AFStorage
toStorage = AFStorage . fromIntegral . fromEnum

fromStorage :: AFStorage -> Storage
fromStorage (AFStorage (fromIntegral -> x))
  | x `elem` [0..3] = toEnum x
  | otherwise = error $ "Invalid Storage " <> (show x)

-- | Type for different RandomEngines
data RandomEngineType
  = Philox
  | ThreeFry
  | Mersenne
  deriving (Eq, Show)

toRandomEngine :: AFRandomEngineType -> RandomEngineType
toRandomEngine (AFRandomEngineType 100) = Philox
toRandomEngine (AFRandomEngineType 200) = ThreeFry
toRandomEngine (AFRandomEngineType 300) = Mersenne
toRandomEngine (AFRandomEngineType x) =
  error ("Invalid random engine: " <> show x)

fromRandomEngine :: RandomEngineType ->  AFRandomEngineType
fromRandomEngine Philox = (AFRandomEngineType 100)
fromRandomEngine ThreeFry = (AFRandomEngineType 200)
fromRandomEngine Mersenne = (AFRandomEngineType 300)

-- | Interpolation type
data InterpType
  = Nearest
  | Linear
  | Bilinear
  | Cubic
  | LowerInterp
  | LinearCosine
  | BilinearCosine
  | Bicubic
  | CubicSpline
  | BicubicSpline
  deriving (Show, Eq, Ord, Enum)

toInterpType :: AFInterpType -> InterpType
toInterpType (AFInterpType (fromIntegral -> x)) = toEnum x

fromInterpType :: InterpType -> AFInterpType
fromInterpType = AFInterpType . fromIntegral . fromEnum

-- | Border Type
data BorderType
  = PadZero
  | PadSym
  deriving (Show, Ord, Enum, Eq)

toBorderType :: AFBorderType -> BorderType
toBorderType (AFBorderType (fromIntegral -> x)) = toEnum x

fromBorderType :: BorderType -> AFBorderType
fromBorderType = AFBorderType . fromIntegral . fromEnum

-- | Connectivity Type
data Connectivity
  = Conn4
  | Conn8
  deriving (Show, Ord, Enum, Eq)

toConnectivity :: AFConnectivity -> Connectivity
toConnectivity (AFConnectivity 4) = Conn4
toConnectivity (AFConnectivity 8) = Conn4
toConnectivity (AFConnectivity x) = error ("Unknown connectivity option: " <> show x)

fromConnectivity :: Connectivity -> AFConnectivity
fromConnectivity Conn4 = AFConnectivity 4
fromConnectivity Conn8 = AFConnectivity 8

-- | Color Space type
data CSpace
  = Gray
  | RGB
  | HSV
  | YCBCR
  deriving (Show, Eq, Ord, Enum)

toCSpace :: AFCSpace -> CSpace
toCSpace (AFCSpace (fromIntegral -> x)) = toEnum x

fromCSpace :: CSpace -> AFCSpace
fromCSpace = AFCSpace . fromIntegral . fromEnum

-- | YccStd type
data YccStd
  = Ycc601
  | Ycc709
  | Ycc2020
  deriving (Show, Eq, Ord)

toAFYccStd :: AFYccStd -> YccStd
toAFYccStd (AFYccStd 601) = Ycc601
toAFYccStd (AFYccStd 709) = Ycc709
toAFYccStd (AFYccStd 2020) = Ycc2020
toAFYccStd (AFYccStd x) = error ("Unknown AFYccStd option: " <> show x)

fromAFYccStd :: YccStd -> AFYccStd
fromAFYccStd Ycc601 = afYcc601
fromAFYccStd Ycc709 = afYcc709
fromAFYccStd Ycc2020 = afYcc2020

-- | Moment types
data MomentType
  = M00
  | M01
  | M10
  | M11
  | FirstOrder
  deriving (Show, Eq, Ord)

toMomentType :: AFMomentType -> MomentType
toMomentType x
  | x == afMomentM00 = M00
  | x == afMomentM01 = M01
  | x == afMomentM10 = M10
  | x == afMomentM11 = M11
  | x == afMomentFirstOrder = FirstOrder
  | otherwise = error ("Unknown moment type: " <> show x)

fromMomentType :: MomentType -> AFMomentType
fromMomentType M00 = afMomentM00
fromMomentType M01 = afMomentM01
fromMomentType M10 = afMomentM10
fromMomentType M11 = afMomentM11
fromMomentType FirstOrder = afMomentFirstOrder

-- | Canny Theshold type
data CannyThreshold
  = Manual
  | AutoOtsu
  deriving (Show, Eq, Ord, Enum)

toCannyThreshold :: AFCannyThreshold -> CannyThreshold
toCannyThreshold (AFCannyThreshold (fromIntegral -> x)) = toEnum x

fromCannyThreshold :: CannyThreshold -> AFCannyThreshold
fromCannyThreshold = AFCannyThreshold . fromIntegral . fromEnum

-- | Flux function type
data FluxFunction
  = FluxDefault
  | FluxQuadratic
  | FluxExponential
  deriving (Show, Eq, Ord, Enum)

toFluxFunction :: AFFluxFunction -> FluxFunction
toFluxFunction (AFFluxFunction (fromIntegral -> x)) = toEnum x

fromFluxFunction :: FluxFunction -> AFFluxFunction
fromFluxFunction = AFFluxFunction . fromIntegral . fromEnum

-- | Diffusion type
data DiffusionEq
  = DiffusionDefault
  | DiffusionGrad
  | DiffusionMCDE
  deriving (Show, Eq, Ord, Enum)

toDiffusionEq :: AFDiffusionEq -> DiffusionEq
toDiffusionEq (AFDiffusionEq (fromIntegral -> x)) = toEnum x

fromDiffusionEq :: DiffusionEq -> AFDiffusionEq
fromDiffusionEq = AFDiffusionEq . fromIntegral . fromEnum

-- | Iterative deconvolution algo type
data IterativeDeconvAlgo
  = DeconvDefault
  | DeconvLandweber
  | DeconvRichardsonLucy
  deriving (Show, Eq, Ord, Enum)

toIterativeDeconvAlgo :: AFIterativeDeconvAlgo -> IterativeDeconvAlgo
toIterativeDeconvAlgo (AFIterativeDeconvAlgo (fromIntegral -> x)) = toEnum x

fromIterativeDeconvAlgo :: IterativeDeconvAlgo -> AFIterativeDeconvAlgo
fromIterativeDeconvAlgo = AFIterativeDeconvAlgo . fromIntegral . fromEnum

-- | Inverse deconvolution algo type
data InverseDeconvAlgo
  = InverseDeconvDefault
  | InverseDeconvTikhonov
  deriving (Show, Eq, Ord, Enum)

toInverseDeconvAlgo :: AFInverseDeconvAlgo -> InverseDeconvAlgo
toInverseDeconvAlgo (AFInverseDeconvAlgo (fromIntegral -> x)) = toEnum x

fromInverseDeconvAlgo :: InverseDeconvAlgo -> AFInverseDeconvAlgo
fromInverseDeconvAlgo = AFInverseDeconvAlgo . fromIntegral . fromEnum

-- | Cell type, used in Graphics module
data Cell
  = Cell
  { cellRow :: Int
  , cellCol :: Int
  , cellTitle :: String
  , cellColorMap :: ColorMap
  } deriving (Show, Eq)

cellToAFCell :: Cell -> IO AFCell
cellToAFCell Cell {..} =
  withCString cellTitle $ \cstr ->
    pure AFCell { afCellRow = cellRow
                , afCellCol = cellCol
                , afCellTitle = cstr
                , afCellColorMap = fromColorMap cellColorMap
                }

-- | ColorMap type
data ColorMap
  = ColorMapDefault
  | ColorMapSpectrum
  | ColorMapColors
  | ColorMapRed
  | ColorMapMood
  | ColorMapHeat
  | ColorMapBlue
  | ColorMapInferno
  | ColorMapMagma
  | ColorMapPlasma
  | ColorMapViridis
  deriving (Show, Eq, Ord, Enum)

fromColorMap :: ColorMap -> AFColorMap
fromColorMap = AFColorMap . fromIntegral . fromEnum

toColorMap :: AFColorMap -> ColorMap
toColorMap (AFColorMap (fromIntegral -> x)) = toEnum x

-- | Marker type
data MarkerType
  = MarkerTypeNone
  | MarkerTypePoint
  | MarkerTypeCircle
  | MarkerTypeSquare
  | MarkerTypeTriangle
  | MarkerTypeCross
  | MarkerTypePlus
  | MarkerTypeStar
  deriving (Show, Eq, Ord, Enum)

fromMarkerType :: MarkerType -> AFMarkerType
fromMarkerType = AFMarkerType . fromIntegral . fromEnum

toMarkerType :: AFMarkerType -> MarkerType
toMarkerType (AFMarkerType (fromIntegral -> x)) = toEnum x

-- | Match type
data MatchType
  = MatchTypeSAD
  | MatchTypeZSAD
  | MatchTypeLSAD
  | MatchTypeSSD
  | MatchTypeZSSD
  | MatchTypeLSSD
  | MatchTypeNCC
  | MatchTypeZNCC
  | MatchTypeSHD
  deriving (Show, Eq, Ord, Enum)

fromMatchType :: MatchType -> AFMatchType
fromMatchType = AFMatchType . fromIntegral . fromEnum

toMatchType :: AFMatchType -> MatchType
toMatchType (AFMatchType (fromIntegral -> x)) = toEnum x

-- | TopK type
data TopK
  = TopKDefault
  | TopKMin
  | TopKMax
  deriving (Show, Eq, Ord, Enum)

fromTopK :: TopK -> AFTopkFunction
fromTopK = AFTopkFunction . fromIntegral . fromEnum

toTopK :: AFTopkFunction -> TopK
toTopK (AFTopkFunction (fromIntegral -> x)) = toEnum x

-- | Homography Type
data HomographyType
  = RANSAC
  | LMEDS
  deriving (Show, Eq, Ord, Enum)

fromHomographyType :: HomographyType -> AFHomographyType
fromHomographyType = AFHomographyType . fromIntegral . fromEnum

toHomographyType :: AFHomographyType -> HomographyType
toHomographyType (AFHomographyType (fromIntegral -> x)) = toEnum x

-- | Sequence Type
data Seq
  = Seq
  { seqBegin :: !Double
  , seqEnd :: !Double
  , seqStep :: !Double
  } deriving (Show, Eq, Ord)

toAFSeq :: Seq -> AFSeq
toAFSeq (Seq x y z) = (AFSeq x y z)

-- | Index Type
data Index a
  = Index
  { idx :: Either (Array a) Seq
  , isSeq :: !Bool
  , isBatch :: !Bool
  }

seqIdx :: Seq -> Bool -> Index a
seqIdx s = Index (Right s) True

arrIdx :: Array a -> Bool -> Index a
arrIdx a = Index (Left a) False

toAFIndex :: Index a -> IO AFIndex
toAFIndex (Index a b c) = do
  case a of
    Right s -> pure $ AFIndex (Right (toAFSeq s)) b c
    Left (Array fptr) -> do
      withForeignPtr fptr $ \ptr ->
        pure $ AFIndex (Left ptr) b c

-- | Type alias for ArrayFire API version
type Version = (Int,Int,Int)

-- | Norm Type
data NormType
  = NormVectorOne
  -- ^ treats the input as a vector and returns the sum of absolute values
  | NormVectorInf
  -- ^ treats the input as a vector and returns the max of absolute values
  | NormVector2
  -- ^ treats the input as a vector and returns euclidean norm
  | NormVectorP
  -- ^ treats the input as a vector and returns the p-norm
  | NormMatrix1
  -- ^ return the max of column sums
  | NormMatrixInf
  -- ^ return the max of row sums
  | NormMatrix2
  -- ^ returns the max singular value). Currently NOT SUPPORTED
  | NormMatrixLPQ
  -- ^ returns Lpq-norm
  | NormEuclid
  -- ^ The default. Same as AF_NORM_VECTOR_2
  deriving (Show, Eq, Enum)

fromNormType :: NormType -> AFNormType
fromNormType = AFNormType . fromIntegral . fromEnum

toNormType :: AFNormType -> NormType
toNormType (AFNormType (fromIntegral -> x)) = toEnum x

-- | Convolution Domain
data ConvDomain
  = ConvDomainAuto
  -- ^ ArrayFire automatically picks the right convolution algorithm
  | ConvDomainSpatial
  -- ^ Perform convolution in spatial domain
  | ConvDomainFreq
  -- ^ Perform convolution in frequency domain
  deriving (Show, Eq, Enum)

-- | Convolution Mode
data ConvMode
  = ConvDefault
  -- ^ Output of the convolution is the same size as input
  | ConvExpand
  -- ^ Output of the convolution is signal_len + filter_len - 1
  deriving (Show, Eq, Enum)

fromConvDomain :: ConvDomain -> AFConvDomain
fromConvDomain = AFConvDomain . fromIntegral . fromEnum

toConvDomain :: AFConvDomain -> ConvDomain
toConvDomain (AFConvDomain (fromIntegral -> x)) = toEnum x

fromConvMode :: AFConvMode -> ConvMode
fromConvMode (AFConvMode (fromIntegral -> x)) = toEnum x

toConvMode :: ConvMode -> AFConvMode
toConvMode = AFConvMode . fromIntegral . fromEnum

-- | Array Fire types
data AFDType
  = F32
  | C32
  | F64
  | C64
  | B8
  | S32
  | U32
  | U8
  | S64
  | U64
  | S16
  | U16
  deriving (Show, Eq, Enum)

fromAFType :: AFDtype -> AFDType
fromAFType (AFDtype (fromIntegral -> x)) = toEnum x

toAFType :: AFDType -> AFDtype
toAFType = AFDtype . fromIntegral . fromEnum

ext: hsc

max_stars_repo_name: danielkroeni/arrayfire-haskell

max_issues_repo_name: danielkroeni/arrayfire-haskell

max_forks_repo_name: danielkroeni/arrayfire-haskell


text:
{-# OPTIONS_GHC -Wall -Wno-orphans #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module TestBDD (bddTestGroup) where

import Control.Monad
import Control.Monad.ST
import Data.IntMap.Lazy (IntMap)
import qualified Data.IntMap.Lazy as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.IORef
import Data.List
import qualified Data.Map.Lazy as Map
import Data.Proxy
import qualified Data.Set as Set
import Data.Vector (Vector)
import Data.Word
import Statistics.Distribution
import Statistics.Distribution.ChiSquared (chiSquared)
import System.IO.Unsafe
import qualified System.Random.MWC as Rand
import Test.QuickCheck.Function (apply)
import Test.QuickCheck.Instances.Vector ()
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck
import Test.Tasty.TH

import Data.DecisionDiagram.BDD (BDD (..), ItemOrder (..))
import qualified Data.DecisionDiagram.BDD as BDD

import Utils

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

instance BDD.ItemOrder a => Arbitrary (BDD a) where
  arbitrary = arbitraryBDDOver =<< arbitrary

  shrink (BDD.Leaf _) = []
  shrink (BDD.Branch x p0 p1) =
    [p0, p1]
    ++
    [ BDD.Branch x p0' p1'
    | (p0', p1') <- shrink (p0, p1), p0' /= p1'
    ]

arbitraryBDDOver :: forall a. BDD.ItemOrder a => IntSet -> Gen (BDD a)
arbitraryBDDOver xs = do
  let f vs n = oneof $
        [ return BDD.true
        , return BDD.false
        ]
        ++
        [ do v <- elements vs
             let vs' = dropWhile (\v' -> compareItem (Proxy :: Proxy a) v' v  /= GT) vs
             lo <- f vs' (n `div` 2)
             hi <- f vs' (n `div` 2) `suchThat` (/= lo)
             return (BDD.Branch v lo hi)
        | n > 0, not (null vs)
        ]
  sized $ f (sortBy (BDD.compareItem (Proxy :: Proxy a)) $ IntSet.toList xs)

arbitrarySatisfyingAssignment :: forall a. BDD.ItemOrder a => BDD a -> IntSet -> Gen (IntMap Bool)
arbitrarySatisfyingAssignment bdd xs = do
  m1 <- arbitrarySatisfyingPartialAssignment bdd
  let ys = xs `IntSet.difference` IntMap.keysSet m1
  m2 <- liftM(IntMap.fromAscList) $ forM (IntSet.toAscList ys) $ \y -> do
    v <- arbitrary
    return (y,v)
  return $ m1 `IntMap.union` m2

arbitrarySatisfyingPartialAssignment :: forall a. BDD.ItemOrder a => BDD a -> Gen (IntMap Bool)
arbitrarySatisfyingPartialAssignment = f
  where
    f (BDD.Leaf True) = return IntMap.empty
    f (BDD.Leaf False) = undefined
    f (BDD.Branch x lo hi) = oneof $
      [liftM (IntMap.insert x False) (f lo) | lo /= BDD.Leaf False]
      ++
      [liftM (IntMap.insert x True) (f hi) | hi /= BDD.Leaf False]

-- ------------------------------------------------------------------------
-- conjunction
-- ------------------------------------------------------------------------

prop_and_unitL :: Property
prop_and_unitL =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (BDD.true BDD..&&. a) === a

prop_and_unitR :: Property
prop_and_unitR =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a BDD..&&. BDD.true) === a

prop_and_falseL :: Property
prop_and_falseL =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (BDD.false BDD..&&. a) === BDD.false

prop_and_falseR :: Property
prop_and_falseR =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a BDD..&&. BDD.false) === BDD.false

prop_and_comm :: Property
prop_and_comm =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      (a BDD..&&. b) === (b BDD..&&. a)

prop_and_assoc :: Property
prop_and_assoc =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b, c) ->
      (a BDD..&&. (b BDD..&&. c)) === ((a BDD..&&. b) BDD..&&. c)

prop_and_idempotent :: Property
prop_and_idempotent =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a BDD..&&. a) === a

-- ------------------------------------------------------------------------
-- disjunction
-- ------------------------------------------------------------------------

prop_or_unitL :: Property
prop_or_unitL =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (BDD.false BDD..||. a) === a

prop_or_unitR :: Property
prop_or_unitR =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a BDD..||. BDD.false) === a

prop_or_trueL :: Property
prop_or_trueL =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (BDD.true BDD..||. a) === BDD.true

prop_or_trueR :: Property
prop_or_trueR =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a BDD..||. BDD.true) === BDD.true

prop_or_comm :: Property
prop_or_comm =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      (a BDD..||. b) === (b BDD..||. a)

prop_or_assoc :: Property
prop_or_assoc =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b, c) ->
      (a BDD..||. (b BDD..||. c)) === ((a BDD..||. b) BDD..||. c)

prop_or_idempotent :: Property
prop_or_idempotent =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a BDD..||. a) === a

-- ------------------------------------------------------------------------
-- xor
-- ------------------------------------------------------------------------

prop_xor_unitL :: Property
prop_xor_unitL =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (BDD.false `BDD.xor` a) === a

prop_xor_unitR :: Property
prop_xor_unitR =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a `BDD.xor` BDD.false) === a

prop_xor_comm :: Property
prop_xor_comm =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      (a `BDD.xor` b) === (b `BDD.xor` a)

prop_xor_assoc :: Property
prop_xor_assoc =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b, c) ->
      (a `BDD.xor` (b `BDD.xor` c)) === ((a `BDD.xor` b) `BDD.xor` c)

prop_xor_involution :: Property
prop_xor_involution =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a `BDD.xor` a) === BDD.false

prop_xor_dist :: Property
prop_xor_dist =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b, c) ->
      (a BDD..&&. (b `BDD.xor` c)) === ((a BDD..&&. b) `BDD.xor` (a BDD..&&. c))

-- ------------------------------------------------------------------------
-- distributivity
-- ------------------------------------------------------------------------

prop_dist_1 :: Property
prop_dist_1 =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b, c) ->
      (a BDD..&&. (b BDD..||. c)) === ((a BDD..&&. b) BDD..||. (a BDD..&&. c))

prop_dist_2 :: Property
prop_dist_2 =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b, c) ->
      (a BDD..||. (b BDD..&&. c)) === ((a BDD..||. b) BDD..&&. (a BDD..||. c))

prop_absorption_1 :: Property
prop_absorption_1 =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      (a BDD..&&. (a BDD..||. b)) === a

prop_absorption_2 :: Property
prop_absorption_2 =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      (a BDD..||. (a BDD..&&. b)) === a

-- ------------------------------------------------------------------------
-- negation
-- ------------------------------------------------------------------------

prop_double_negation :: Property
prop_double_negation =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      BDD.notB (BDD.notB a) === a

prop_and_complement :: Property
prop_and_complement =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a BDD..&&. BDD.notB a) === BDD.false

prop_or_complement :: Property
prop_or_complement =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a BDD..||. BDD.notB a) === BDD.true

prop_de_morgan_1 :: Property
prop_de_morgan_1 =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      BDD.notB (a BDD..||. b) === (BDD.notB a BDD..&&. BDD.notB b)

prop_de_morgan_2 :: Property
prop_de_morgan_2 =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      BDD.notB (a BDD..&&. b) === (BDD.notB a BDD..||. BDD.notB b)

-- ------------------------------------------------------------------------
-- Implication
-- ------------------------------------------------------------------------

prop_imply :: Property
prop_imply =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      (a BDD..=>. b) === (BDD.notB a BDD..||. b)

prop_imply_currying :: Property
prop_imply_currying =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b, c) ->
      ((a BDD..&&. b) BDD..=>. c) === (a BDD..=>. (b BDD..=>. c))

-- ------------------------------------------------------------------------
-- Equivalence
-- ------------------------------------------------------------------------

prop_equiv :: Property
prop_equiv =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      (a BDD..<=>. b) === ((a BDD..=>. b) BDD..&&. (b BDD..=>. a))

-- ------------------------------------------------------------------------
-- If-then-else
-- ------------------------------------------------------------------------

prop_ite :: Property
prop_ite =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(c :: BDD o, t, e) ->
      BDD.ite c t e === ((c BDD..&&. t) BDD..||. (BDD.notB c BDD..&&. e))

prop_ite_swap_branch :: Property
prop_ite_swap_branch =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(c :: BDD o, t, e) ->
      BDD.ite c t e === BDD.ite (BDD.notB c) e t

prop_ite_dist_not :: Property
prop_ite_dist_not =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(c :: BDD o, t, e) ->
      BDD.notB (BDD.ite c t e) === BDD.ite c (BDD.notB t) (BDD.notB e)

prop_ite_dist_and :: Property
prop_ite_dist_and =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(c :: BDD o, t, e, d) ->
      (d BDD..&&. BDD.ite c t e) === BDD.ite c (d BDD..&&. t) (d BDD..&&. e)

prop_ite_dist_or :: Property
prop_ite_dist_or =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(c :: BDD o, t, e, d) ->
      (d BDD..||. BDD.ite c t e) === BDD.ite c (d BDD..||. t) (d BDD..||. e)

-- ------------------------------------------------------------------------
-- Pseudo-Boolean
-- ------------------------------------------------------------------------

prop_pbAtLeast :: Property
prop_pbAtLeast =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrarySmallIntMap $ \(xs :: IntMap Integer) ->
      forAll arbitrary $ \k ->
        let a :: BDD o
            a = BDD.pbAtLeast xs k
         in counterexample (show a) $
              if a == BDD.Leaf False then
                property (k > sum [max 0 w | (_,w) <- IntMap.toList xs])
              else
                forAll (arbitrarySatisfyingAssignment a (IntMap.keysSet xs)) $ \ys ->
                  (IntMap.keysSet ys `IntSet.isSubsetOf` IntMap.keysSet xs)
                  .&&.
                  sum [xs IntMap.! y | (y,b) <- IntMap.toList ys, b] >= k

prop_pbAtMost :: Property
prop_pbAtMost =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrarySmallIntMap $ \(xs :: IntMap Integer) ->
      forAll arbitrary $ \k ->
        let a :: BDD o
            a = BDD.pbAtMost xs k
         in counterexample (show a) $
              if a == BDD.Leaf False then
                property (k < sum [min 0 w | (_,w) <- IntMap.toList xs])
              else
                forAll (arbitrarySatisfyingAssignment a (IntMap.keysSet xs)) $ \ys ->
                  (IntMap.keysSet ys `IntSet.isSubsetOf` IntMap.keysSet xs)
                  .&&.
                  sum [xs IntMap.! y | (y,b) <- IntMap.toList ys, b] <= k

prop_pbExactly :: Property
prop_pbExactly =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrarySmallIntMap $ \(xs :: IntMap Integer) ->
      forAll arbitrary $ \k ->
        let a :: BDD o
            a = BDD.pbExactly xs k
         in counterexample (show a) $
              if a == BDD.Leaf False then
                property True
              else
                forAll (arbitrarySatisfyingAssignment a (IntMap.keysSet xs)) $ \ys ->
                  (IntMap.keysSet ys `IntSet.isSubsetOf` IntMap.keysSet xs)
                  .&&.
                  sum [xs IntMap.! y | (y,b) <- IntMap.toList ys, b] === k

prop_pbExactly_2 :: Property
prop_pbExactly_2 =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrarySmallIntMap $ \(xs :: IntMap Integer) ->
      forAll (gen xs) $ \(m, k) ->
        let a :: BDD o
            a = BDD.pbExactly xs k
         in counterexample (show a) $ BDD.evaluate (m IntMap.!) a
  where
    gen :: IntMap Integer -> Gen (IntMap Bool, Integer)
    gen xs = do
      ys <- sublistOf (IntMap.toList xs)
      let ys' = IntSet.fromList [y | (y,_) <- ys]
      return
        ( IntMap.mapWithKey (\x _ -> x `IntSet.member` ys') xs
        , sum [w | (_,w) <- ys]
        )

prop_pbExactlyIntegral :: Property
prop_pbExactlyIntegral =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrarySmallIntMap $ \(xs :: IntMap Integer) ->
      forAll arbitrary $ \k ->
        (BDD.pbExactlyIntegral xs k :: BDD o) === BDD.pbExactly xs k

-- ------------------------------------------------------------------------
-- Quantification
-- ------------------------------------------------------------------------

prop_forAll :: Property
prop_forAll =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(x, a :: BDD o) ->
      BDD.forAll x a === (BDD.restrict x True a BDD..&&. BDD.restrict x False a)

prop_exists :: Property
prop_exists =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(x, a :: BDD o) ->
      BDD.exists x a === (BDD.restrict x True a BDD..||. BDD.restrict x False a)

prop_existsUnique :: Property
prop_existsUnique =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(x, a :: BDD o) ->
      BDD.existsUnique x a === (BDD.restrict x True a `BDD.xor` BDD.restrict x False a)

prop_forAll_support :: Property
prop_forAll_support =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(x, a :: BDD o) ->
      let b = BDD.forAll x a
          xs = BDD.support b
       in counterexample (show (b, xs)) $
            x `IntSet.notMember` xs

prop_exists_support :: Property
prop_exists_support =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(x, a :: BDD o) ->
      let b = BDD.exists x a
          xs = BDD.support b
       in counterexample (show (b, xs)) $
            x `IntSet.notMember` xs

prop_existsUnique_support :: Property
prop_existsUnique_support =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(x, a :: BDD o) ->
      let b = BDD.existsUnique x a
          xs = BDD.support b
       in counterexample (show (b, xs)) $
            x `IntSet.notMember` xs

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

prop_forAllSet_empty :: Property
prop_forAllSet_empty =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      BDD.forAllSet IntSet.empty a === a

prop_existsSet_empty :: Property
prop_existsSet_empty =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      BDD.existsSet IntSet.empty a === a

prop_existsUniqueSet_empty :: Property
prop_existsUniqueSet_empty =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      BDD.existsUniqueSet IntSet.empty a === a

prop_forAllSet_singleton :: Property
prop_forAllSet_singleton =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(x, a :: BDD o) ->
      BDD.forAllSet (IntSet.singleton x) a === BDD.forAll x a

prop_existsSet_singleton :: Property
prop_existsSet_singleton =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(x, a :: BDD o) ->
      BDD.existsSet (IntSet.singleton x) a === BDD.exists x a

prop_existsUniqueSet_singleton :: Property
prop_existsUniqueSet_singleton =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(x, a :: BDD o) ->
      BDD.existsUniqueSet (IntSet.singleton x) a === BDD.existsUnique x a

prop_forAllSet_union :: Property
prop_forAllSet_union =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(xs1, xs2, a :: BDD o) ->
      BDD.forAllSet (xs1 `IntSet.union` xs2) a === BDD.forAllSet xs2 (BDD.forAllSet xs1 a)

prop_existsSet_union :: Property
prop_existsSet_union =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(xs1, xs2, a :: BDD o) ->
      BDD.existsSet (xs1 `IntSet.union` xs2) a === BDD.existsSet xs2 (BDD.existsSet xs1 a)

prop_existsUniqueSet_union :: Property
prop_existsUniqueSet_union =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitraryDisjointSets $ \(xs1, xs2) ->
    forAll arbitrary $ \(a :: BDD o) ->
      BDD.existsUniqueSet (xs1 `IntSet.union` xs2) a === BDD.existsUniqueSet xs2 (BDD.existsUniqueSet xs1 a)
  where
    arbitraryDisjointSets = do
      (u, v) <- arbitrary
      return (u `IntSet.intersection` v, u IntSet.\\ v)

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

case_fold_laziness :: Assertion
case_fold_laziness = do
  let bdd :: BDD BDD.AscOrder
      bdd = BDD.Branch 0 (BDD.Branch 1 (BDD.Leaf False) (BDD.Leaf True)) (BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True))
      f x lo _hi =
        if x == 2 then
          error "unused value should not be evaluated"
        else
          lo
  seq (BDD.fold f id bdd) $ return ()

case_fold'_strictness :: Assertion
case_fold'_strictness = do
  ref <- newIORef False
  let bdd :: BDD BDD.AscOrder
      bdd = BDD.Branch 0 (BDD.Branch 1 (BDD.Leaf False) (BDD.Leaf True)) (BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True))
      f x lo _hi = unsafePerformIO $ do
        when (x==2) $ writeIORef ref True
        return lo
  seq (BDD.fold' f id bdd) $ do
    flag <- readIORef ref
    assertBool "unused value should be evaluated" flag

prop_fold_inSig :: Property
prop_fold_inSig =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(bdd :: BDD o) ->
      BDD.fold (\x lo hi -> BDD.inSig (BDD.SBranch x lo hi)) (BDD.inSig . BDD.SLeaf) bdd
      ===
      bdd

prop_fold'_inSig :: Property
prop_fold'_inSig =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(bdd :: BDD o) ->
      BDD.fold' (\x lo hi -> BDD.inSig (BDD.SBranch x lo hi)) (BDD.inSig . BDD.SLeaf) bdd
      ===
      bdd

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

prop_unfoldHashable_outSig :: Property
prop_unfoldHashable_outSig =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(bdd :: BDD o) ->
      BDD.unfoldHashable BDD.outSig bdd === bdd

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

case_support_false :: Assertion
case_support_false = BDD.support BDD.false @?= IntSet.empty

case_support_true :: Assertion
case_support_true = BDD.support BDD.true @?= IntSet.empty

prop_support_var :: Property
prop_support_var =
  forAll arbitrary $ \x ->
    BDD.support (BDD.var x) === IntSet.singleton x

prop_support_not :: Property
prop_support_not =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      let lhs = BDD.support a
          rhs = BDD.support (BDD.notB a)
       in lhs === rhs

prop_support_and :: Property
prop_support_and =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      let lhs = BDD.support (a BDD..&&. b)
          rhs = BDD.support a `IntSet.union` BDD.support b
       in counterexample (show (lhs, rhs)) $ lhs `IntSet.isSubsetOf` rhs

prop_support_or :: Property
prop_support_or =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      let lhs = BDD.support (a BDD..||. b)
          rhs = BDD.support a `IntSet.union` BDD.support b
       in counterexample (show (lhs, rhs)) $ lhs `IntSet.isSubsetOf` rhs

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

prop_evaluate_var :: Property
prop_evaluate_var =
 forAll arbitrary $ \(f' :: Fun Int Bool) ->
   let f = apply f'
    in forAllItemOrder $ \(_ :: Proxy o) ->
         forAll arbitrary $ \x ->
           BDD.evaluate f (BDD.var x :: BDD o) === f x

prop_evaluate_not :: Property
prop_evaluate_not =
 forAll arbitrary $ \(f' :: Fun Int Bool) ->
   let f = apply f'
    in forAllItemOrder $ \(_ :: Proxy o) ->
         forAll arbitrary $ \(a :: BDD o) ->
           BDD.evaluate f (BDD.notB a) === not (BDD.evaluate f a)

prop_evaluate_and :: Property
prop_evaluate_and =
 forAll arbitrary $ \(f' :: Fun Int Bool) ->
   let f = apply f'
    in forAllItemOrder $ \(_ :: Proxy o) ->
         forAll arbitrary $ \(a :: BDD o, b) ->
           BDD.evaluate f (a BDD..&&. b) === (BDD.evaluate f a && BDD.evaluate f b)

prop_evaluate_or :: Property
prop_evaluate_or =
 forAll arbitrary $ \(f' :: Fun Int Bool) ->
   let f = apply f'
    in forAllItemOrder $ \(_ :: Proxy o) ->
         forAll arbitrary $ \(a :: BDD o, b) ->
           BDD.evaluate f (a BDD..||. b) === (BDD.evaluate f a || BDD.evaluate f b)

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

case_numNodes :: Assertion
case_numNodes = do
  let bdd, bdd1 :: BDD BDD.AscOrder
      bdd = BDD.Branch 0 (BDD.Branch 1 BDD.false bdd1) (BDD.Branch 2 BDD.false bdd1)
      bdd1 = BDD.Branch 3 BDD.true BDD.false
  BDD.numNodes bdd @?= 6

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

prop_restrict :: Property
prop_restrict =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \x ->
        let b = (BDD.var x BDD..&&. BDD.restrict x True a) BDD..||.
                (BDD.notB (BDD.var x) BDD..&&. BDD.restrict x False a)
         in a === b

prop_restrict_idempotent :: Property
prop_restrict_idempotent =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \(x, val) ->
        let b = BDD.restrict x val a
            c = BDD.restrict x val b
         in counterexample (show (b, c)) $ b === c

prop_restrict_not :: Property
prop_restrict_not =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \(x, val) ->
        BDD.restrict x val (BDD.notB a) === BDD.notB (BDD.restrict x val a)

prop_restrict_and :: Property
prop_restrict_and =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      forAll arbitrary $ \(x, val) ->
        BDD.restrict x val (a BDD..&&. b) === (BDD.restrict x val a BDD..&&. BDD.restrict x val b)

prop_restrict_or :: Property
prop_restrict_or =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      forAll arbitrary $ \(x, val) ->
        BDD.restrict x val (a BDD..||. b) === (BDD.restrict x val a BDD..||. BDD.restrict x val b)

prop_restrict_var :: Property
prop_restrict_var =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \x ->
      let a :: BDD o
          a = BDD.var x
       in (BDD.restrict x True a === BDD.true) .&&.
          (BDD.restrict x False a === BDD.false)

prop_restrict_support :: Property
prop_restrict_support =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \(x, val) ->
        let b = BDD.restrict x val a
            xs = BDD.support b
         in counterexample (show b) $
            counterexample (show xs) $
              x `IntSet.notMember` xs

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

prop_restrictSet_empty :: Property
prop_restrictSet_empty =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      BDD.restrictSet IntMap.empty a === a

prop_restrictSet_singleton :: Property
prop_restrictSet_singleton =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \(x, val) ->
        BDD.restrict x val a === BDD.restrictSet (IntMap.singleton x val) a

prop_restrictSet_union :: Property
prop_restrictSet_union =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \(val1, val2) ->
        and (IntMap.intersectionWith (==) val1 val2)
        ==>
        (BDD.restrictSet val2 (BDD.restrictSet val1 a) === BDD.restrictSet (val1 `IntMap.union` val2) a)

prop_restrictSet_idempotent :: Property
prop_restrictSet_idempotent =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \val ->
        let b = BDD.restrictSet val a
            c = BDD.restrictSet val b
         in counterexample (show (b, c)) $ b === c

prop_restrictSet_not :: Property
prop_restrictSet_not =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \val ->
        BDD.restrictSet val (BDD.notB a) === BDD.notB (BDD.restrictSet val a)

prop_restrictSet_and :: Property
prop_restrictSet_and =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      forAll arbitrary $ \val ->
        BDD.restrictSet val (a BDD..&&. b) === (BDD.restrictSet val a BDD..&&. BDD.restrictSet val b)

prop_restrictSet_or :: Property
prop_restrictSet_or =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      forAll arbitrary $ \val ->
        BDD.restrictSet val (a BDD..||. b) === (BDD.restrictSet val a BDD..||. BDD.restrictSet val b)

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

prop_restrictLaw :: Property
prop_restrictLaw =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \law ->
        (law BDD..&&. BDD.restrictLaw law a) === (law BDD..&&. a)

case_restrictLaw_case_0 :: Assertion
case_restrictLaw_case_0 = (law BDD..&&. BDD.restrictLaw law a) @?= (law BDD..&&. a)
  where
    a, law :: BDD BDD.AscOrder
    a = BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True)
    law = BDD.Branch 1 (BDD.Branch 2 (BDD.Leaf True) (BDD.Leaf False)) (BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True))

prop_restrictLaw_true :: Property
prop_restrictLaw_true =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      BDD.restrictLaw BDD.true a === a

prop_restrictLaw_self :: Property
prop_restrictLaw_self =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a /= BDD.false) ==> BDD.restrictLaw a a === BDD.true

prop_restrictLaw_not_self :: Property
prop_restrictLaw_not_self =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      (a /= BDD.true) ==> BDD.restrictLaw (BDD.notB a) a === BDD.false

prop_restrictLaw_restrictSet :: Property
prop_restrictLaw_restrictSet =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \val ->
        let b = BDD.andB [if v then BDD.var x else BDD.notB (BDD.var x) | (x,v) <- IntMap.toList val]
         in BDD.restrictLaw b a === BDD.restrictSet val a

-- prop_restrictLaw_and_condition :: Property
-- prop_restrictLaw_and_condition =
--   forAllItemOrder $ \(_ :: Proxy o) ->
--     forAll arbitrary $ \(a :: BDD o) ->
--       forAll arbitrary $ \(val1, val2) ->
--         let val = val1 BDD..&&. val2
--          in counterexample (show val) $
--               (val /= BDD.false)
--               ==>
--               (BDD.restrictLaw val a === BDD.restrictLaw val2 (BDD.restrictLaw val1 a))

-- counterexample to the above prop_restrictLaw_and_condition
case_restrictLaw_case_1 :: Assertion
case_restrictLaw_case_1 = do
  -- BDD.restrictLaw val a @?= BDD.restrictLaw val2 (BDD.restrictLaw val1 a)
  BDD.restrictLaw val a @?= BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True)
  BDD.restrictLaw val2 (BDD.restrictLaw val1 a) @?= BDD.Branch 1 (BDD.Leaf True) (Branch 2 (BDD.Leaf False) (BDD.Leaf True))
  where
    a :: BDD BDD.AscOrder
    a = Branch 2 (BDD.Leaf False) (BDD.Leaf True) -- x2
    val1 = BDD.Branch 1 (BDD.Leaf False) (BDD.Leaf True) -- x1
    val2 = BDD.Branch 1 (BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True)) (BDD.Leaf True) -- x1 ∨ x2
    val = val1 BDD..&&. val2 -- x1

prop_restrictLaw_or_condition :: Property
prop_restrictLaw_or_condition =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \(val1, val2) ->
        let val = val1 BDD..||. val2
         in counterexample (show val) $
              (val BDD..&&. BDD.restrictLaw val a) === (val1 BDD..&&. BDD.restrictLaw val1 a BDD..||. val2 BDD..&&. BDD.restrictLaw val2 a)

prop_restrictLaw_idempotent :: Property
prop_restrictLaw_idempotent =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll arbitrary $ \val ->
        let b = BDD.restrictLaw val a
            c = BDD.restrictLaw val b
         in counterexample (show (b, c)) $ b === c

prop_restrictLaw_not :: Property
prop_restrictLaw_not =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      forAll (arbitrary `suchThat` (/= BDD.false)) $ \val ->
        BDD.restrictLaw val (BDD.notB a) === BDD.notB (BDD.restrictLaw val a)

prop_restrictLaw_and :: Property
prop_restrictLaw_and =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      forAll (arbitrary `suchThat` (/= BDD.false)) $ \val ->
        BDD.restrictLaw val (a BDD..&&. b) === (BDD.restrictLaw val a BDD..&&. BDD.restrictLaw val b)

prop_restrictLaw_or :: Property
prop_restrictLaw_or =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o, b) ->
      forAll (arbitrary `suchThat` (/= BDD.false)) $ \val ->
        BDD.restrictLaw val (a BDD..||. b) === (BDD.restrictLaw val a BDD..||. BDD.restrictLaw val b)

-- prop_restrictLaw_minimality :: Property
-- prop_restrictLaw_minimality =
--   forAllItemOrder $ \(_ :: Proxy o) ->
--     forAll arbitrary $ \(a :: BDD o) ->
--       forAll arbitrary $ \law ->
--         let b = BDD.restrictLaw law a
--          in counterexample (show b) $
--               ((law BDD..&&. b) === (law BDD..&&. a))
--               .&&.
--               conjoin [counterexample (show b') $ (law BDD..&&. b') =/= (law BDD..&&. a) | b' <- shrink b]

case_restrictLaw_non_minimal_1 :: Assertion
case_restrictLaw_non_minimal_1 = do
  (law BDD..&&. BDD.restrictLaw law a) @?= (law BDD..&&. a)
  BDD.restrictLaw law a @?= b -- should be 'a'?
  where
    law, a :: BDD BDD.AscOrder
    law = BDD.Branch 1 (BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True)) (BDD.Leaf True) -- x1 ∨ x2
    a = BDD.Branch 2 (BDD.Leaf True) (BDD.Leaf False) -- ¬x2
    b = BDD.Branch 1 (BDD.Leaf False) (BDD.Branch 2 (BDD.Leaf True) (BDD.Leaf False)) -- x1 ∧ ¬x2

case_restrictLaw_non_minimal_2 :: Assertion
case_restrictLaw_non_minimal_2 = do
  (law BDD..&&. BDD.restrictLaw law a) @?= (law BDD..&&. a)
  BDD.restrictLaw law a @?= b -- should be 'a'?
  where
    law, a, b :: BDD BDD.AscOrder
    law = BDD.Branch 1 (BDD.Leaf True) (BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True)) -- ¬x1 ∨ x2
    a = BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True) -- x2
    b = BDD.Branch 1 (BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True)) (BDD.Leaf True) -- x1 ∨ x2

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

prop_subst_restrict_constant :: Property
prop_subst_restrict_constant =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(m :: BDD o) ->
    forAll arbitrary $ \x ->
    forAll arbitrary $ \val ->
      BDD.subst x (if val then BDD.true else BDD.false) m === BDD.restrict x val m

prop_subst_restrict :: Property
prop_subst_restrict =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(m :: BDD o) ->
    forAll arbitrary $ \x ->
    forAll arbitrary $ \(n :: BDD o) ->
      BDD.subst x n m === ((n BDD..&&. BDD.restrict x True m) BDD..||. (BDD.notB n BDD..&&. BDD.restrict x False m))

prop_subst_same_var :: Property
prop_subst_same_var =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(m :: BDD o) ->
    forAll arbitrary $ \x ->
      BDD.subst x (BDD.var x) m === m

prop_subst_not_occured :: Property
prop_subst_not_occured =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(m :: BDD o) ->
    forAll (arbitrary `suchThat` (\x -> x `IntSet.notMember` (BDD.support m))) $ \x ->
    forAll arbitrary $ \(n :: BDD o) ->
      BDD.subst x n m === m

-- If x1≠x2 and x1∉FV(M2) then M[x1 ↦ M1][x2 ↦ M2] = M[x2 ↦ M2][x1 ↦ M1[x2 ↦ M2]].
prop_subst_dist :: Property
prop_subst_dist =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(x1, m1) ->
    forAll ((,) <$> (arbitrary `suchThat` (/= x1)) <*> (arbitrary `suchThat` (\m2 -> x1 `IntSet.notMember` BDD.support m2))) $ \(x2, m2) ->
    forAll arbitrary $ \(m :: BDD o) ->
      BDD.subst x2 m2 (BDD.subst x1 m1 m) === BDD.subst x1 (BDD.subst x2 m2 m1) (BDD.subst x2 m2 m)

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

prop_substSet_empty :: Property
prop_substSet_empty =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(m :: BDD o) ->
      BDD.substSet IntMap.empty m === m

prop_substSet_singleton :: Property
prop_substSet_singleton =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(m :: BDD o) ->
    forAll arbitrary $ \x ->
    forAll arbitrary $ \m1 ->
      BDD.substSet (IntMap.singleton x m1) m === BDD.subst x m1 m

case_substSet_case_1 :: Assertion
case_substSet_case_1 = do
  BDD.substSet (IntMap.singleton x m1) m @?= BDD.subst x m1 m
  where
    m :: BDD BDD.AscOrder
    m = BDD.Branch 1 (BDD.Branch 2 (BDD.Leaf True) (BDD.Leaf False)) (BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True))
    x = 1
    m1 = BDD.Branch 1 (BDD.Leaf True) (BDD.Leaf False)

prop_substSet_same_vars :: Property
prop_substSet_same_vars =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(m :: BDD o) ->
    forAll arbitrary $ \xs ->
      BDD.substSet (IntMap.fromAscList [(x, BDD.var x) | x <- IntSet.toAscList xs]) m === m

prop_substSet_not_occured :: Property
prop_substSet_not_occured =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(m :: BDD o) ->
    forAll (f (BDD.support m)) $ \s ->
      BDD.substSet s m === m
  where
    f xs = liftM IntMap.fromList $ listOf $ do
      y <- arbitrary `suchThat` (`IntSet.notMember` xs)
      m <- arbitrary
      return (y, m)

prop_substSet_compose :: Property
prop_substSet_compose =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \xs ->
    forAll arbitrary $ \ys ->
    forAll (liftM IntMap.fromList $ mapM (\x -> (,) <$> pure x <*> arbitraryBDDOver ys) (IntSet.toList xs)) $ \s1 ->
    forAll (liftM IntMap.fromList $ mapM (\y -> (,) <$> pure y <*> arbitrary) (IntSet.toList ys)) $ \s2 ->
    forAll (arbitraryBDDOver xs) $ \(m :: BDD o) ->
      BDD.substSet s2 (BDD.substSet s1 m) === BDD.substSet (IntMap.map (BDD.substSet s2) s1) m

case_substSet_case_2 :: Assertion
case_substSet_case_2 = do
  let m :: BDD BDD.AscOrder
      m = BDD.var 1 BDD..&&. BDD.var 2
  BDD.substSet (IntMap.fromList [(1, BDD.var 2), (2, BDD.var 3)]) m @?= BDD.var 2 BDD..&&. BDD.var 3
  BDD.substSet (IntMap.fromList [(1, BDD.var 3), (2, BDD.var 1)]) m @?= BDD.var 3 BDD..&&. BDD.var 1

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

data MonotoneExpr a
  = MVar a
  | MAnd (MonotoneExpr a) (MonotoneExpr a)
  | MOr (MonotoneExpr a) (MonotoneExpr a)
  | MConst Bool
  deriving (Show)

arbitraryMonotoneExpr :: forall a. Gen a -> Gen (MonotoneExpr a)
arbitraryMonotoneExpr gen = sized f
  where
    f :: Int -> Gen (MonotoneExpr a)
    f n = oneof $
      [ liftM MConst arbitrary
      , liftM MVar gen
      ]
      ++
      concat
      [ [liftM2 MAnd sub sub, liftM2 MOr sub sub]
      | n > 0, let sub = f (n `div` 2)
      ]

evalMonotoneExpr :: ItemOrder a => (b -> BDD a) -> MonotoneExpr b -> BDD a
evalMonotoneExpr f = g
  where
    g (MVar a) = f a
    g (MConst v) = BDD.Leaf v
    g (MOr a b) = g a BDD..||. g b
    g (MAnd a b) = g a BDD..&&. g b

forAllMonotonicFunction :: forall o prop. (ItemOrder o, Testable prop) => IntSet -> ((BDD o -> BDD o) -> prop) -> Property
forAllMonotonicFunction xs k =
  forAll (arbitraryMonotoneExpr (elements (Nothing : map Just (IntSet.toList xs)))) $ \e -> do
    let f :: BDD o -> BDD o
        f x = evalMonotoneExpr g e
          where
            g Nothing = x
            g (Just v) = BDD.var v
     in k f

prop_lfp_is_fixed_point :: Property
prop_lfp_is_fixed_point =
 forAll arbitrary $ \(xs :: IntSet) ->
   forAllItemOrder $ \(_ :: Proxy o) ->
     forAllMonotonicFunction xs $ \(f :: BDD o -> BDD o) -> do
       let a = BDD.lfp f
        in counterexample (show a) $ f a === a

prop_gfp_is_fixed_point :: Property
prop_gfp_is_fixed_point =
 forAll arbitrary $ \(xs :: IntSet) ->
   forAllItemOrder $ \(_ :: Proxy o) ->
     forAllMonotonicFunction xs $ \(f :: BDD o -> BDD o) -> do
       let a = BDD.gfp f
        in counterexample (show a) $ f a === a

prop_lfp_imply_gfp :: Property
prop_lfp_imply_gfp =
 forAll arbitrary $ \(xs :: IntSet) ->
   forAllItemOrder $ \(_ :: Proxy o) ->
     forAllMonotonicFunction xs $ \(f :: BDD o -> BDD o) -> do
       let a = BDD.lfp f
           b = BDD.gfp f
        in counterexample (show (a, b)) $ (a BDD..=>. b) === BDD.true

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

prop_anySat :: Property
prop_anySat =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(bdd :: BDD o) ->
      case BDD.anySat bdd of
        Just p -> counterexample (show p) $ BDD.evaluate (p IntMap.!) bdd
        Nothing -> bdd === BDD.Leaf False

prop_allSat :: Property
prop_allSat =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrarySmallIntSet $ \xs ->
      forAll (arbitraryBDDOver xs) $ \(bdd :: BDD o) ->
         let ps = BDD.allSat bdd
         in null ps === (bdd == BDD.Leaf False)
            .&&.
            conjoin [counterexample (show p) $ BDD.evaluate (p IntMap.!) bdd |  p <- ps]

prop_anySatComplete :: Property
prop_anySatComplete =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \xs ->
      forAll (arbitraryBDDOver xs) $ \(bdd :: BDD o) ->
        case BDD.anySatComplete xs bdd of
          Just p -> counterexample (show p) $
            IntMap.keysSet p === xs
            .&&.
            BDD.evaluate (p IntMap.!) bdd
          Nothing -> bdd === BDD.Leaf False

prop_allSatComplete :: Property
prop_allSatComplete =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrarySmallIntSet $ \xs ->
      forAll (arbitraryBDDOver xs) $ \(bdd :: BDD o) ->
        let ps = BDD.allSatComplete xs bdd
            qs = [q | q <- foldM (\m x -> [IntMap.insert x v m | v <- [False, True]]) IntMap.empty (IntSet.toList xs)
                    , BDD.evaluate (q IntMap.!) bdd]
         in conjoin [counterexample (show p) (IntMap.keysSet p === xs) | p <- ps]
            .&&.
            Set.fromList ps === Set.fromList qs

prop_countSat_allSatComplete :: Property
prop_countSat_allSatComplete =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrarySmallIntSet $ \xs ->
      forAll (arbitraryBDDOver xs) $ \(bdd :: BDD o) ->
        let ps = BDD.allSatComplete xs bdd
            n = BDD.countSat xs bdd
         in counterexample (show n) $
              if bdd == BDD.Leaf False then
                n === 0
              else
                -- Note that the number of partial assignments is smaller than the number of total assignments
                (n > 0) .&&. n === length ps

prop_uniformSatM :: Property
prop_uniformSatM =
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll (arbitrarySmallIntSet `suchThat` ((>= 2) . IntSet.size)) $ \xs ->
      forAll (arbitraryBDDOver xs `suchThat` ((>= (2::Integer)) . BDD.countSat xs)) $ \(bdd :: BDD o) ->
        forAll arbitrary $ \(seed :: Vector Word32) ->
          let m :: Integer
              m = BDD.countSat xs bdd
              n = 1000
              samples = runST $ do
                gen <- Rand.initialize seed
                replicateM n $ BDD.uniformSatM xs bdd gen
              hist_actual = Map.fromListWith (+) [(s, 1 :: Double) | s <- samples]
              hist_expected = [(s, fromIntegral n / fromIntegral m :: Double) | s <- BDD.allSatComplete xs bdd]
              chi_sq = sum [(Map.findWithDefault 0 s hist_actual - cnt) ** 2 / cnt | (s, cnt) <- hist_expected]
              threshold = complQuantile (chiSquared (fromIntegral m - 1)) 0.0001
           in counterexample (show hist_actual ++ " /= " ++ show (Map.fromList hist_expected)) $
                and [BDD.evaluate (a IntMap.!) bdd | a <- Map.keys hist_actual]
                .&&.
                counterexample ("χ² = " ++ show chi_sq ++ " >= " ++ show threshold) (chi_sq < threshold)

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

prop_toGraph_fromGraph :: Property
prop_toGraph_fromGraph = do
  forAllItemOrder $ \(_ :: Proxy o) ->
    forAll arbitrary $ \(a :: BDD o) ->
      BDD.fromGraph (BDD.toGraph a) === a

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

arbitrarySmallIntSet :: Gen IntSet
arbitrarySmallIntSet = do
  n <- choose (0, 12)
  liftM IntSet.fromList $ replicateM n arbitrary

arbitrarySmallIntMap :: Arbitrary a => Gen (IntMap a)
arbitrarySmallIntMap = do
  n <- choose (0, 12)
  liftM IntMap.fromList $ replicateM n $ do
    k <- arbitrary
    v <- arbitrary
    return (k, v)

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

bddTestGroup :: TestTree
bddTestGroup = $(testGroupGenerator)

ext: hs

max_stars_repo_name: msakai/haskell-decision-diagrams

max_issues_repo_name: msakai/haskell-decision-diagrams

max_forks_repo_name: msakai/haskell-decision-diagrams


text:
{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE ViewPatterns          #-}

module Main where

import Control.Parallel.Strategies
import Data.Char
import Data.Foldable
import Data.List.Split (splitOn)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Maybe
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as S
import qualified Data.Vector as B
import GHC.Conc (numCapabilities)
import GHC.Generics (Generic)
import Numeric.GSL.SimulatedAnnealing
import qualified Numeric.LinearAlgebra as H

main :: IO ()
main = do
  !input <- parse <$> readFile "inputs/day-8.txt"

  -- The fun part is that doing this in parallel on a 12 core 24 thread CPU is
  -- only twice as fast as when not using any parallelization, and with 24
  -- threads it's 2.5 times slower. FFI calls require global locking, which is
  -- probably what's slowing this down.
  let chunkSize      = ceiling $ fromIntegral (length input) / (fromIntegral numCapabilities :: Float)
      mappings       = map (fromJust . solveMapping) input
      !mappedOutputs = map mapDisplayOutputs mappings `using` parListChunk chunkSize rdeepseq

  putStrLn "Part 1:"
  print . length . filter (`elem` [1, 4, 7, 8]) $ concat mappedOutputs

  putStrLn "\nPart 2:"
  print . sum $ map digitsToInt mappedOutputs

-- * Segments
--
-- These represent each value of the seven segment display in different ways.

-- | The expected lit segments for each of the ten digits that can be
-- represented by the four segment display. The segment indices for each number
-- are in sorted.
expectedSegments :: B.Vector (Set Char)
expectedSegments = B.fromList . map S.fromList $
  [ "abcefg"  -- 0
  , "cf"      -- 1
  , "acdeg"   -- 2
  , "acdfg"   -- 3
  , "bcdf"    -- 4
  , "abdfg"   -- 5
  , "abdefg"  -- 6
  , "acf"     -- 7
  , "abcdefg" -- 8
  , "abcdfg"  -- 9
  ]

-- * Solution

data Display = Display
  { -- | The ten digits from 'expectedSegments', but with the character ->
    -- segment assignments scrambled.
    patterns :: B.Vector (Set Char)
    -- | A four digit output value, with the same scrambled assignments as those
    -- in 'patterns'.
  , outputs  :: B.Vector (Set Char)
  }
  deriving (Show, Generic, NFData)

-- | The solver state for solving the mappings within a display.
data SolverState = SolverState
  { display        :: Display
    -- | The mapping from a pattern from 'patterns' to the character in
    -- 'expectedSegments'.
  , patternMapping :: !(Map Int Int)
    -- | The mapping from a character on the seven segment display as used in a
    -- 'Display' to the actual letter of the segment.
  , charMapping    :: !(Map Char Char)
  }
  deriving (Show, Generic, NFData)

-- | The actions we can take in our solver. Swapping a mapping means swapping
-- two values in either of the maps in 'SolverState'.
data SolverAction = SwapPatternMapping | SwapCharMapping
  deriving (Show, Enum, Bounded)

applyMapping :: Ord a => Map a a -> Set a -> Set a
applyMapping mapping = S.map (mapping M.!)

-- | The penalty/loss for a solver state. We want to minimize this.
solverPenalty :: SolverState -> Int
solverPenalty SolverState{..} = lengthPenalty + mappingPenalty
  where
    -- We need the pattern state from the solver permuted to match the expected
    -- segments, alongside the expected segments
    permutedPatterns = B.backpermute (patterns display) (B.fromList $ map (patternMapping M.!) [0..9])
    zippedPatterns   = B.zip expectedSegments permutedPatterns

    -- Because the set difference only tells you which elements from set A are not in set B
    symmetricDifference :: Ord a => Set a -> Set a -> Set a
    symmetricDifference a b = S.difference a b `S.union` S.difference b a

    -- | The sum of length errors when using the pattern mapping.
    lengthPenalty = getSum $
      foldMap (\(expected, actual) -> Sum . abs $ S.size expected - S.size actual)
              zippedPatterns

    -- | The number of difference characters in each segment set after applying
    -- the pattern mapping.
    mappingPenalty = getSum $
      foldMap (\(expected, actual) -> Sum . abs . S.size $ symmetricDifference expected (applyMapping charMapping actual))
              zippedPatterns

-- | Find the matching mapping from the scrambled pattern space to the expected
-- segments. There's a clever way to do this. This is not it.
solveMapping :: Display -> Maybe SolverState
solveMapping display'
  -- There should only be an exact solution
  | solverPenalty optimalSolution == 0 = Just optimalSolution
  | otherwise                          = Nothing
  where
    optimalSolution = simanSolve 420 3 solverParams initialState
      (fromIntegral . solverPenalty)
      -- This distance metric is not entirely correct
      (\x y -> fromIntegral . abs $ solverPenalty x - solverPenalty y)
      step
      Nothing -- (Just $ show . solverPenalty)

    -- This solver is WAY overkill, so the cooling rate and final temperature
    -- are relatively high to not waste too much time on the simpler to solve
    -- cases
    solverParams = SimulatedAnnealingParams
      100   -- Tries per step
      1000  -- Tries per temperature
      1     -- Maximum step size in random walk
      1.0   -- Boltzman constant for random walks
      1.0   -- Initial temperature
      2.0   -- Cooling rate
      0.069 -- Final temperature

    initialState = SolverState
      { display        = display'
      , patternMapping = M.fromList $ map (\idx -> (idx, idx)) [0..9]
      , charMapping    = M.fromList $ map (\c -> (c, c)) "abcdefg"
      }

    solverActionRange = fromIntegral (fromEnum (maxBound :: SolverAction))

    swapRange SwapPatternMapping = 9.0
    swapRange SwapCharMapping    = fromIntegral $ ord 'g' - ord 'a'

    swap :: Ord k => k -> k -> Map k v -> Map k v
    swap from to m = M.insert to (m M.! from) $ M.insert from (m M.! to) m

    -- Where n starts at 0, as generated by the RNG.
    char :: Int -> Char
    char n = chr (n + ord 'a')

    step :: H.Vector Double -> Double -> SolverState -> SolverState
    step rands _ state@SolverState{..} =
      let action   = toEnum (round $ (rands H.! 0) * solverActionRange) :: SolverAction
          -- These two can be the same
          swapFrom = round $ (rands H.! 1) * swapRange action
          swapTo   = round $ (rands H.! 2) * swapRange action
       in case action of
            SwapPatternMapping -> state { patternMapping = swap swapFrom swapTo patternMapping }
            SwapCharMapping    -> state { charMapping    = swap (char swapFrom) (char swapTo) charMapping }

-- | Grab the translated display numbers from a solver result.
mapDisplayOutputs :: SolverState -> [Int]
mapDisplayOutputs SolverState{display = Display{..}, ..}
  = map ((segmentsMapping M.!) . applyMapping charMapping)
  $ B.toList outputs
  where
    segmentsMapping :: Map (Set Char) Int
    segmentsMapping = M.fromList $ B.toList $ B.imap (\idx segment -> (segment, idx)) expectedSegments

-- | convert a list of digits to an integer.
digitsToInt :: [Int] -> Int
digitsToInt = foldl' (\acc n -> (acc * 10) + n) 0

parse :: String -> [Display]
parse = map parseLine . lines
  where
    parseLine :: String -> Display
    parseLine l = case splitOn " | " l of
      [words -> ps, words -> os] -> Display (parseSegments ps) (parseSegments os)
      _                          -> error "What is this even!?"

    parseSegments :: [[Char]] -> B.Vector (Set Char)
    parseSegments = B.fromList . map S.fromList


text:
{-# OPTIONS_GHC  -fno-warn-unused-binds -fno-warn-unused-matches -fno-warn-name-shadowing -fno-warn-missing-signatures #-}
{-# LANGUAGE FlexibleInstances, ConstraintKinds, ExistentialQuantification, GADTs, RankNTypes, MultiParamTypeClasses, RankNTypes, UndecidableInstances, FlexibleContexts, TypeSynonymInstances #-}

---------------------------------------------------------------------------------------------------
---------------------------------------------------------------------------------------------------
-- |
-- | Module : Approximate median
-- | Creator: Xiao Ling
-- | Created: 12/08/2015
-- | TODO   : test standard deviation of alpha, beta, and final version
-- |
---------------------------------------------------------------------------------------------------
---------------------------------------------------------------------------------------------------

module ApproxMedian (

      MaxSize
    , Store

    , median
    , median'

  ) where

import Control.Monad.State
import Control.Monad.Random
import Control.Monad.Random.Class

import Data.Conduit
import Data.Foldable (toList)
import qualified Data.Sequence as S
import qualified Data.Conduit.List as Cl
import Data.Sequence (Seq,(|>),update,empty,index)

import Test.QuickCheck
import Test.QuickCheck.Random

import Core
import Utils
import qualified Statistics as St

{-----------------------------------------------------------------------------
  Types
------------------------------------------------------------------------------}

type MaxSize = Float
type Store a = (Seq a, MaxSize)

-- * the algorithm uses `some m` equipped with state and randomness
-- * also consider `some'` `a`
type Some  m = (MonadState Counter m, MonadRandom m)
type Some' a = (Floating a          , Ord a        )

{-----------------------------------------------------------------------------
  Approximate Median
------------------------------------------------------------------------------}

-- * @Use: test (tMedian (E 0.05, D 0.05)) xs
-- * compute `tMedian` within accuracy `Eps` and confidence `Delta`
median' :: Some' a => EpsDelta -> Batch a IO a
median' t = median t `using` eval

-- * `tick` up a counter for each item `a` seen and with probability
-- * min(1, s/i) put item `a` into store `t` of maxSize `s`
median :: (Some m, Some' a) => EpsDelta -> Streaming a m (Store a)
median (ED e d) = Cl.foldM step $ store s
  where s = 7/(e^2) * log (2/d)

-- * a concrete `eval`uation of `m`
eval :: Some' a => StateT Counter (Rand StdGen) (Store a) -> IO a
eval m = fmap (St.median . toList) . fmap fst . evalRandIO $ evalStateT m 0

{-----------------------------------------------------------------------------
  Subroutines. Read $|> to understand the actual algorithm
------------------------------------------------------------------------------}

-- * One step of the algorithm
step :: (Some m, Some' a) => Store a -> a -> m (Store a)
step t a = tick >> t $|> a

-- * with probability `s/i` uniformly select an item from the store `t` and
-- * replace it with `a`.
-- * mnemonic: `|>` is insertion, `$f` means do f probabilistically
infixl 7 $|>
($|>) :: Some m => Store a -> a -> m (Store a)
($|>) t@(_,s) a = do
  i <- get
  if s > i then t $> a else do
    h <- toss . coin $ s/i
    if isHead h then t $> a else return t

{-----------------------------------------------------------------------------
  Utils
------------------------------------------------------------------------------}

-- * Construct an empty store given max size `s`
store :: MaxSize -> Store a
store = (,) empty

-- * Probabilistic insertion. If the store is not full, insert item `a` deterministically
-- * else with uniform probability replace some existing item in store with `a`
-- * mnemonic: `|>` is insertion, `$f` means do f probabilistically
($>) :: Some m => Store a -> a -> m (Store a)
(as,s) $> a | length as < round s = return (as |> a, s)
            | otherwise           = (\x -> (update (round x) a as, s))
                                  <$> getRandomR (0,s :: MaxSize)


text:
{-# LANGUAGE Rank2Types #-}
import Control.Monad.ST (RealWorld)
import Data.Complex (Complex)
import Data.Vector.Storable (MVector(MVector))
import Foreign (Ptr, Storable, withForeignPtr)
import Text.Printf (printf)
import Blas.Generic.Unsafe (Numeric)
import qualified Data.Vector.Storable as Vector
import qualified Blas.Primitive.Types as Blas
import qualified Blas.Generic.Unsafe as Blas
import qualified TestUtils as T

main :: IO ()
main = T.runTest $ do
  sequence_ (mapNumericTypes testGemm)

mapNumericTypes :: (forall a. (Eq a, Numeric a, Show a) => a -> b) -> [b]
mapNumericTypes f =
  [ f (dummy :: Float)
  , f (dummy :: Double)
  , f (dummy :: Complex Float)
  , f (dummy :: Complex Double)
  ]

dummy :: a
dummy = error "dummy value that shouldn't be used"

withMVector :: MVector s a -> (Ptr a -> IO b) -> IO b
withMVector (MVector _ foreignPtr) = withForeignPtr foreignPtr

mVectorFromList :: Storable a => [a] -> IO (MVector RealWorld a)
mVectorFromList = Vector.thaw . Vector.fromList

testGemm :: (Eq a, Numeric a, Show a) => a -> T.Test ()
testGemm numType = do
  let order    = Blas.RowMajor
      transa   = Blas.NoTrans
      transb   = Blas.Trans
      n        = 2
      size     = n * n
      alpha    = 1.0 `asTypeOf` numType
      beta     = 0.0
      a        = Vector.fromList [1, 2, 3, 4]
      b        = Vector.fromList [1, 2, 3, 5]
      expected = Vector.fromList [5, 13, 11, 29]

  c' <- T.liftIO $ do
    c <- mVectorFromList $ take size (repeat 0)
    Vector.unsafeWith a $ \ pa ->
      Vector.unsafeWith b $ \ pb ->
        withMVector c $ \ pc ->
          Blas.gemm order transa transb n n n alpha pa n pb n beta pc n
    Vector.freeze c

  if c' == expected
    then T.passTest "testGemm"
    else T.failTest $ printf "testGemm: c' does not match: %s != %s"
                      (show c') (show expected)

max_stars_repo_name: Rufflewind/blas-hs

max_issues_repo_name: Rufflewind/blas-hs

max_forks_repo_name: Rufflewind/blas-hs


text:
module Deanie.Density (
    logDensityBernoulli
  , logDensityBeta
  , logDensityGamma
  , logDensityGaussian
  ) where

import Numeric.SpecFunctions (logGamma)

logDensityBernoulli :: Double -> Bool -> Double
logDensityBernoulli p x
    | p < 0 || p > 1 = log 0
    | x              = log p
    | otherwise      = log (1 - p)
{-# INLINE logDensityBernoulli #-}

logDensityBeta :: Double -> Double -> Double -> Double
logDensityBeta a b x
  | x <= 0 || x >= 1 = log 0
  | a < 0 || b < 0   = log 0
  | otherwise        = (a - 1) * log x + (b - 1) * log (1 - x)
{-# INLINE logDensityBeta #-}

-- | The log-density for the gamma distribution with rate parameter b.
--
--     f(x) = b ^ a * x ^ (a - 1) * x ^ (-b * x) / Gamma(a)
logDensityGamma :: Double -> Double -> Double -> Double
logDensityGamma a b x
  | a < 0 || b < 0 = log 0
  | otherwise      = a * log b + (a - 1) * log x - b * x - logGamma a
{-# INLINE logDensityGamma #-}

-- | The density for the normal distribution with specified mean and standard
--   deviation.
logDensityGaussian :: Double -> Double -> Double -> Double
logDensityGaussian m sd x
  | sd <= 0   = log 0
  | otherwise = negate (log sd) - (x - m) * (x - m) / (2 * sd * sd)
{-# INLINE logDensityGaussian #-}

max_issues_repo_name: silky/deanie

max_forks_repo_name: silky/deanie


text:
import Data.Complex

rootsOfUnity n = [cis (2*pi*k/n) | k <- [0..n-1]]

max_stars_repo_name: djgoku/RosettaCodeData

max_issues_repo_name: djgoku/RosettaCodeData

max_forks_repo_name: djgoku/RosettaCodeData


text:
{-# LANGUAGE DataKinds #-}
module Data.Array.RankedS.MatMul(matMul) where
import Prelude hiding ((<>))
import GHC.Stack
import Data.Array.RankedS
import Numeric.LinearAlgebra as N

matMul :: (HasCallStack, N.Numeric a) => Array 2 a -> Array 2 a -> Array 2 a
matMul x y =
  case (shapeL x, shapeL y) of
    ([m, n], [n', o]) | n == n' ->
      let x' = N.reshape n $ toVector x
          y' = N.reshape o $ toVector y
          xy' = x' N.<> y'
          xy = fromVector [m, o] $ N.flatten xy'
      in  xy
    sz -> error $ "matMul: expected two conforming two-dimensional arrays, got shape " ++ show sz

max_stars_repo_name: augustss/orthotope-hmatrix

max_issues_repo_name: augustss/orthotope-hmatrix

max_forks_repo_name: augustss/orthotope-hmatrix


text:
{-# LANGUAGE BangPatterns, CPP, FlexibleContexts, GADTs, OverloadedStrings,
             RankNTypes #-}

{- |
   Module      : TestBench.Evaluate
   Description : Tree-based representation for Criterion and Weigh
   Copyright   : (c) Ivan Lazar Miljenovic
   License     : MIT
   Maintainer  : Ivan.Miljenovic@gmail.com

An extremely simple rose tree-based representation of criterion
benchmarks and weigh measurements.

 -}
module TestBench.Evaluate
  ( -- * Types
    EvalTree
  , EvalForest
  , Eval(..)
    -- ** Weights
  , GetWeight
  , getWeight
  , getWeightIO
    -- * Conversion
  , flattenBenchTree
  , flattenBenchForest
    -- * Running benchmarks
  , evalForest
    -- ** Weighing individual functions
  , weighIndex
  ) where

import TestBench.Commands  (resetUnusedConfig, weighFileArg, weighIndexArg)
import TestBench.LabelTree

import Criterion.Analysis          (OutlierVariance(ovFraction),
                                    SampleAnalysis(..))
import Criterion.Internal          (runAndAnalyseOne)
import Criterion.Measurement       (initializeTime, secs)
import Criterion.Measurement.Types (Benchmark, Benchmarkable, bench, bgroup)
import Criterion.Monad             (withConfig)
import Criterion.Types             (Config(..), DataRecord(..), Report(..))
import Statistics.Types            (ConfInt(..), Estimate(..))
import Weigh                       (weighAction, weighFunc)

import Data.Csv (DefaultOrdered(..), Field, Name, ToField, ToNamedRecord(..),
                 ToRecord(..), header, namedRecord, record, toField)

import qualified Data.DList        as DL
import           Streaming         (Of, Stream)
import           Streaming.Cassava (encodeByNameDefault)
import qualified Streaming.Prelude as S
import           Streaming.With    (writeBinaryFile)

import Control.Applicative              (liftA2)
import Control.DeepSeq                  (NFData)
import Control.Monad                    (join, when, zipWithM_)
import Control.Monad.IO.Class           (liftIO)
import Control.Monad.Trans.Class        (lift)
import Control.Monad.Trans.State.Strict (StateT, evalStateT, get, put)
import Data.Int                         (Int64)
import Data.List                        (intercalate)
import Data.Maybe                       (isJust, listToMaybe, mapMaybe)
import Data.String                      (IsString)
import System.Environment               (getExecutablePath)
import System.Exit                      (ExitCode(..))
import System.IO                        (hClose)
import System.IO.Temp                   (withSystemTempFile)
import System.Process                   (rawSystem)
import Text.Printf                      (printf)

#if MIN_VERSION_base (4,9,0)
import Data.Semigroup (Semigroup(..))
#endif

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

-- | A more explicit tree-like structure for benchmarks than using
--   Criterion's 'Benchmark' type.
type EvalTree = LabelTree Eval

type EvalForest = [EvalTree]

data Eval = Eval { eName  :: !String
                 , eBench :: !(Maybe Benchmarkable)
                 , eWeigh :: !(Maybe GetWeight)
                 }

-- | The results from measuring memory usage.
--
--   @since 0.2.0.0
data GetWeight where
  GetWeight   :: forall a b. (NFData b) => (a -> b)    -> a -> GetWeight
  GetWeightIO :: forall a b. (NFData b) => (a -> IO b) -> a -> GetWeight

runGetWeight :: GetWeight -> IO Weight
runGetWeight gw = mkWeight <$> case gw of
                                 GetWeight   f a -> weighFunc   f a
                                 GetWeightIO f a -> weighAction f a
  where
    mkWeight (b,gc,_,_) = Weight b gc

data Weight = Weight { bytesAlloc :: !Int64
                     , numGC      :: !Int64
                     }
            deriving (Eq, Ord, Show, Read)

-- | How to weigh a function.
--
--   @since 0.2.0.0
getWeight :: (NFData b) => (a -> b) -> a -> GetWeight
getWeight = GetWeight

-- | An IO-based variant of 'getWeight'.
--
--   @since 0.2.0.0
getWeightIO :: (NFData b) => (a -> IO b) -> a -> GetWeight
getWeightIO = GetWeightIO

flattenBenchTree :: EvalTree -> Maybe Benchmark
flattenBenchTree = fmap (foldLTree (const bgroup) (flip const))
                   . mapMaybeTree (liftA2 fmap (bench . eName) eBench)

-- | Remove the explicit tree-like structure into the implicit one
--   used by Criterion.
--
--   Useful for embedding the results into an existing benchmark
--   suite.
flattenBenchForest :: EvalForest -> [Benchmark]
flattenBenchForest = mapMaybe flattenBenchTree

-- | Run the specified benchmarks, printing the results (once they're
--   all complete) to stdout in a tabular format for easier
--   comparisons.
evalForest :: Config -> EvalForest -> IO ()
evalForest cfg ef = do when (hasBench ep) initializeTime
                       let ec = EC cfg ep
                       printHeaders ep
                       (`evalStateT` zeroIndex)
                         . maybeCSV
                         . S.mapM_ (liftIO . printRow ep)
                         . S.copy
                         $ toRows ec ef
  where
    ep = checkForest ef

    -- Ideally we would do the S.copy here only if we're writing to
    -- CSV; unfortunately, as we're not longer using ResourceT we
    -- don't have a MonadMask instance and thus can't use another
    -- Stream as the inner Monad; this /must/ be run after processing
    -- the stdout version.
    maybeCSV = maybe S.effects streamCSV (csvFile cfg)

    -- In reality, this type signature contains StateT, but that
    -- over-complicates understanding what it does, and to specify it
    -- generically requires bringing in MonadBaseControl and
    -- MonadThrow.

    -- streamCSV :: FilePath -> Stream (Of Row) IO () -> IO ()
    streamCSV fp = writeBinaryFile fp
                  . encodeByNameDefault
                  . S.filter isLeaf

data EvalParams = EP { hasBench  :: !Bool
                     , hasWeigh  :: !Bool
                     , nameWidth :: !Width
                     }
                deriving (Eq, Ord, Show, Read)

#if MIN_VERSION_base (4,9,0)
instance Semigroup EvalParams where
  (<>) = appendEP
#endif

instance Monoid EvalParams where
  mempty = EP { hasBench  = False
              , hasWeigh  = False
              , nameWidth = 0
              }
  mappend = appendEP

appendEP :: EvalParams -> EvalParams -> EvalParams
appendEP ec1 ec2 = EP { hasBench  = appendBy hasBench
                      , hasWeigh  = appendBy hasWeigh
                      , nameWidth = nameWidth ec1 `max` nameWidth ec2
                      }
  where
    appendBy f = f ec1 || f ec2

checkForest :: EvalForest -> EvalParams
checkForest = mconcat . map (foldLTree mergeNode calcConfig)
  where
    mergeNode d lbl ls = mempty { nameWidth = width d lbl }
                         `mappend` mconcat ls

    calcConfig d e = EP { hasBench  = isJust (eBench e)
                        , hasWeigh  = isJust (eWeigh e)
                        , nameWidth = width d (eName e)
                        }

    width d nm = indentPerLevel * d + length nm

data EvalConfig = EC { benchConfig :: {-# UNPACK #-}!Config
                     , evalParam   :: {-# UNPACK #-}!EvalParams
                     }
                deriving (Eq, Show, Read)

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

type PathList = DL.DList String

data Row = Row { rowLabel  :: !String
               , rowPath   :: !PathList -- ^ Invariant: length == rowDepth
               , rowDepth  :: {-# UNPACK #-} !Depth
               , isLeaf    :: !Bool
               , rowBench  :: !(Maybe BenchResults)
               , rowWeight :: !(Maybe Weight)
               }
  deriving (Eq, Show, Read)

pathLabel :: Row -> String
pathLabel row = intercalate "/" (DL.toList (DL.snoc (rowPath row) (rowLabel row)))

-- | Unlike terminal output, this instance creates columns for benchmarks, weighing, etc. even if they're not used.
instance ToRecord Row where
  toRecord row =
    record (toField fmtLabel : benchRecord ++ weightRecord)
    where
      fmtLabel = pathLabel row

      benchRecord = timed resMean ++ timed resStdDev ++ [bField (ovFraction . resOutVar)]
        where
          bField = mField . (. rowBench) . fmap
          timed f = map (bField . (. f)) [estPoint, estLowerBound, estUpperBound]

      weightRecord = [wField bytesAlloc, wField numGC]
        where
          wField = mField . (. rowWeight) . fmap

      mField :: (ToField a) => (Row -> Maybe a) -> Field
      mField f = maybe mempty toField (f row)

-- | Unlike terminal output, this instance creates columns for benchmarks, weighing, etc. even if they're not used.
instance ToNamedRecord Row where
  toNamedRecord row =
    namedRecord (fmtLabel : benchRecord ++ weightRecord)
    where
      fmtLabel = (labelName, toField (pathLabel row))

      benchRecord = zip benchNames
                        (timed resMean ++ timed resStdDev ++ [bField (ovFraction . resOutVar)])
        where
          bField = mField . (. rowBench) . fmap
          timed f = map (bField . (. f)) [estPoint, estLowerBound, estUpperBound]

      weightRecord = zip weighNames
                         [wField bytesAlloc, wField numGC]
        where
          wField = mField . (. rowWeight) . fmap

      mField :: (ToField a) => (Row -> Maybe a) -> Field
      mField f = maybe mempty toField (f row)

instance DefaultOrdered Row where
  headerOrder _ = header (labelName : benchNames ++ weighNames)

toRows :: EvalConfig -> EvalForest -> Stream (Of Row) (StateT Index IO) ()
toRows cfg = f2r DL.empty
  where
    f2r :: PathList -> EvalForest -> Stream (Of Row) (StateT Index IO) ()
    f2r pl = mapM_ (t2r pl)

    t2r :: PathList -> EvalTree -> Stream (Of Row) (StateT Index IO) ()
    t2r pl bt = case bt of
                  Leaf   d e      -> do i <- lift get
                                        lift (put (i+1))
                                        r <- liftIO (makeRow cfg pl i d e)
                                        S.yield r
                  Branch d lbl ts -> S.cons (Row lbl pl d False Nothing Nothing)
                                            (f2r (pl `DL.snoc` lbl) ts)

makeRow :: EvalConfig -> PathList -> Index -> Depth -> Eval -> IO Row
makeRow cfg pl idx d e = Row lbl pl d True
                         <$> tryRun hasBench eBench (getBenchResults (benchConfig cfg) lbl)
                         <*> tryRun hasWeigh eWeigh (const (tryGetWeight idx))
  where
    lbl = eName e
    ep = evalParam cfg

    tryRun :: (EvalParams -> Bool) -> (Eval -> Maybe a) -> (a -> IO (Maybe b)) -> IO (Maybe b)
    tryRun p f r =
      if p ep
         then maybe (return Nothing) r (f e)
         else return Nothing

data BenchResults = BenchResults { resMean   :: !(Estimate ConfInt Double)
                                 , resStdDev :: !(Estimate ConfInt Double)
                                 , resOutVar :: !OutlierVariance
                                 }
  deriving (Eq, Show, Read)

getBenchResults :: Config -> String -> Benchmarkable -> IO (Maybe BenchResults)
getBenchResults cfg lbl b = do dr <- withConfig cfg' (runAndAnalyseOne i lbl b)
                               return $ case dr of
                                          Measurement{} -> Nothing
                                          Analysed rpt  -> Just $
                                            let sa = reportAnalysis rpt
                                            in BenchResults { resMean   = anMean sa
                                                            , resStdDev = anStdDev sa
                                                            , resOutVar = anOutlierVar sa
                                                            }

  where
    -- Set this here just in case someone didn't use the top-level
    -- 'testBench' function.
    --
    -- Also, just in case a CSV file is being outputted, don't try and
    -- write to it.
    cfg' = resetUnusedConfig cfg { csvFile = Nothing }

    i = 0 -- We're ignoring this value anyway, so it should be OK to
          -- just set it.

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

type Index = Int

zeroIndex :: Index
zeroIndex = 0

tryGetWeight :: Index -> IO (Maybe Weight)
tryGetWeight idx = withSystemTempFile "testBench.weigh" $ \fp h -> do
  -- We use a temporary file in case the program prints something else
  -- out to stdout.
  hClose h -- We're not writing to it, just need the file
  exe <- getExecutablePath
  ec <- rawSystem exe ["--" ++ weighIndexArg, show idx, "--" ++ weighFileArg, fp, "+RTS", "-T", "-RTS"]
  case ec of
    ExitFailure{} -> return Nothing
    ExitSuccess   -> do
      out <- readFile fp
      case reads out of
        [(!mw,_)] -> return mw
        _         -> return Nothing

weighIndex :: EvalForest -> Index -> IO (Maybe Weight)
weighIndex ef = fmap join . mapM (mapM runGetWeight . eWeigh) . index es
  where
    es = concatMap leaves ef

index :: [a] -> Index -> Maybe a
index as n = listToMaybe . drop (n-1) $ as

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

printHeaders :: EvalParams -> IO ()
printHeaders ep = do putStr (replicate (nameWidth ep) ' ')
                     when (hasBench ep) (mapM_ toPrintf benchHeaders)
                     when (hasWeigh ep) (mapM_ toPrintf weighHeaders)
                     putStr "\n"
  where
    toPrintf (w,hdr) = printf "%s%*s" columnSpace w hdr

printRow :: EvalParams -> Row -> IO ()
printRow ep r = do printf "%-*s" (nameWidth ep) label
                   when (hasBench ep) (printBench (rowBench r))
                   when (hasWeigh ep) (printWeigh (rowWeight r))
                   putStr "\n"
  where
    label :: String
    label = printf "%s%s" (replicate (rowDepth r * indentPerLevel) ' ') (rowLabel r)

type Width = Int

indentPerLevel :: Width
indentPerLevel = 2

columnGap :: Width
columnGap = 2

columnSpace :: String
columnSpace = replicate columnGap ' '

labelName :: Name
labelName = "Label"

benchNames :: (IsString str) => [str]
benchNames = ["Mean", "MeanLB", "MeanUB", "Stddev", "StddevLB", "StddevUB", "OutlierVariance"]

benchHeaders :: [(Width, String)]
benchHeaders = map addWidth benchNames

weighNames :: (IsString str) => [str]
weighNames = ["AllocBytes", "NumGC"]

weighHeaders :: [(Width, String)]
weighHeaders = map addWidth weighNames

-- Maximum width a numeric field can take.  Might as well make them
-- all the same width.  All other formatters have been manually
-- adjusted to produce nothing longer than this.
secsWidth :: Width
secsWidth = length (secs ((-pi) / 000))

addWidth :: String -> (Width, String)
addWidth nm = (max (length nm) secsWidth, nm)

printBench :: Maybe BenchResults -> IO ()
printBench mr = zipWithM_ (printf "%s%*s" columnSpace) wdths cols
  where
    cols = maybe (repeat "")
                 (\r -> timed (resMean r) ++ timed (resStdDev r) ++ [ov r])
                 mr

    timed bs = [secIt estPoint, secIt estLowerBound, secIt estUpperBound]
      where
        secIt f = secs (f bs)

    ov r = percent (ovFraction (resOutVar r))

    wdths = map fst benchHeaders

estLowerBound :: (Num a) => Estimate ConfInt a -> a
estLowerBound e = estPoint e - confIntLDX (estError e)

estUpperBound :: (Num a) => Estimate ConfInt a -> a
estUpperBound e = estPoint e + confIntUDX (estError e)

printWeigh :: Maybe Weight -> IO ()
printWeigh mr = zipWithM_ (printf "%s%*s" columnSpace) wdths cols
  where
    cols = maybe (repeat "")
                 (\r -> [bytes (bytesAlloc r), count (numGC r)])
                 mr

    wdths = map fst weighHeaders

percent :: Double -> String
percent p = printf "%.3f%%" (p * 100)

-- | Human-readable description of the number of bytes used.  Assumed
--   non-negative.
bytes :: Int64 -> String
bytes b  = printf "%.3f %sB" val p
  where
    prefixes = [" ", "K", "M", "G", "T", "P", "E"] :: [String]

    base = 1024 :: Num a => a

    mult
      | b == 0    = 0
      | otherwise = floor (logBase (base :: Double) (fromIntegral b))

    val = fromIntegral b / (base ^ mult)

    p = prefixes !! mult

count :: Int64 -> String
count = printf "%.3e" . (`asTypeOf` (0::Double)) . fromIntegral

max_stars_repo_name: ivan-m/testbench

max_issues_repo_name: ivan-m/testbench

max_forks_repo_name: ivan-m/testbench


text:
----------------------------------------------------------------------------
-- |
-- Module      :  ListBasedVectorProperties
-- Copyright   :  (c) Thomas Peiselt 2018
-- License     :  Public Domain (see COPYRIGHT)
--
-- property-based tests for the list-based implementation of the linear algebra
-- packages.
module Chapter04.LinearAlgebra.ListBasedVectorProperties (
        linearAlgebraTests )

  where

import           Chapter04.LinearAlgebra.ListBased
import           Data.Complex                      (Complex)
import           Test.Invariant
import           Test.QuickCheck
import           Test.Tasty
import           Test.Tasty.QuickCheck

linearAlgebraTests :: TestTree
linearAlgebraTests = testProperties "Linear Algebra"
  [ ("addition of zero", property (plusZero :: [Double] -> Bool))
  , ("commutative add", property (commutativeAdd :: [Double] -> [Double] -> Bool))
  -- associativity doesn't hold for double due to lack of numeric precision
  , ("associative add", property (associativeAdd :: [Int] -> [Int] -> [Int] -> Bool))
  , ("subtraction of zero", property (minusZero :: [Double] -> Bool))
  , ("subtraction from itself", property (minusItself :: [Integer] -> Bool))
  , ("subtraction inverts addition", property (subtractionInvertsAddition :: [Rational] -> [Rational] -> Property))
  , ("vector sum two", property (sum2 :: [Double] -> [Double] -> Bool))
  , ("vector sum three", property (sum3 :: [Double] -> [Double] -> [Double] -> Bool))
  , ("times zero", property (timesZero :: [Double] -> Bool))
  , ("times one", property (timesOne :: [Double] -> Bool))
  , ("times two", property (timesTwo :: [Complex Double]  -> Bool))
  , ("mean singleton", property (singletonMean :: Complex Double -> Bool))
  , ("magnitude is not negative", property (magnitudeNonNegative :: [Double] -> Bool))
  , ("negate . negate does nothing", property (involutoryNegate :: [Double] -> Bool))
  , ("mean of negated", property meanOfNegated)
  , ("distance to self", property (distanceToSelf :: [Double] -> Property))
  , ("distance to zero", property (distanceToZero :: [Double] -> Property))
  ]

plusZero :: (Num a, Eq a) => Vector a -> Bool
plusZero xs = vectorAdd xs (repeat 0) == xs

commutativeAdd :: (Num a, Eq a) => Vector a -> Vector a -> Bool
commutativeAdd = commutative vectorAdd

associativeAdd :: (Num a, Eq a) => Vector a -> Vector a -> Vector a -> Bool
associativeAdd = associative vectorAdd

minusZero :: (Num a, Eq a) => Vector a -> Bool
minusZero xs =  vectorSubtract xs (repeat 0) == xs

minusItself :: (Num a, Eq a) => Vector a -> Bool
minusItself xs = vectorSubtract xs xs == (replicate (length xs) 0)

subtractionInvertsAddition :: (Num a, Eq a) => Vector a -> Vector a -> Property
subtractionInvertsAddition xs ys = length xs <= length ys ==>
  inverts (`vectorAdd` ys) (`vectorSubtract` ys) xs

sum2 :: (Num a, Eq a) => Vector a -> Vector a -> Bool
sum2 xs ys = vectorSum [xs, ys] == vectorAdd xs ys

sum3 :: (Num a, Eq a) => Vector a -> Vector a -> Vector a -> Bool
sum3 xs ys zs = vectorSum [xs, ys, zs] == vectorAdd xs ( vectorAdd ys zs )

timesZero :: (Num a, Eq a) => Vector a -> Bool
timesZero xs = scalarMultiply 0 xs == replicate (length xs) 0

timesOne :: (Num a, Eq a) => Vector a -> Bool
timesOne xs = scalarMultiply 1 xs == xs

timesTwo :: (Num a, Eq a) => Vector a -> Bool
timesTwo xs = scalarMultiply 2 xs == vectorAdd xs xs

singletonMean :: (Fractional a, Eq a) => a -> Bool
singletonMean x = vectorMean [x] == x

involutoryNegate :: (Eq a, Num a) => Vector a -> Bool
involutoryNegate = involutory negateVector

meanOfNegated :: [Double] -> Property
meanOfNegated xs =  not (null xs) ==> vectorMean xs == -(vectorMean $ negateVector xs)

magnitudeNonNegative :: (Floating a, Eq a, Ord a) => Vector a -> Bool
magnitudeNonNegative xs = magnitude xs >= 0.0

distanceToSelf :: (Floating a, Eq a) => Vector a -> Property
distanceToSelf xs = not (null xs) ==> distance xs xs == 0

distanceToZero :: (Floating a, Eq a, Enum a) => Vector a -> Property
distanceToZero xs = not (null xs) ==>
  distance xs (replicate (length xs) 0) == magnitude xs