> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE UndecidableInstances #-}

| Core data type for the game.

> module Core.BitField
>      where


Import List
-----------

> import Data.PContainer

> import Test.LazySmallCheck hiding (empty)
> import Number.Peano
> import Control.Monad
> import Data.Binary
> import Data.DeriveTH
> import Data.Derive.Binary
> import Data.Derive.Functor

> import qualified Data.Set as S

> import Data.Monoid
> import Data.Function
> import Data.Maybe
> import Data.List



> type Set a = S.Set a


Subset of Subsets
-----------------


| @Subsets c@: @c@ is a data structure which represents a subset of all subsets of a given set.

> class Ord (Elem c) => Subsets c where

>     type Elem c

>     domain        :: c -> Set (Elem c)
#ifdef TEST
>     subsets       :: c -> [Set (Elem c)]
#endif
>     subsetsNum    :: c -> Integer

>     empty         :: Set (Elem c) -> c

| @isTriviallyEmpty@ should be fast but may give @False@ also for empty subsets.

>     isTriviallyEmpty :: c -> Bool

| All subsets of the empty set.

>     emptySubsets  :: Set (Elem c) -> c



#ifdef TEST
Properties
----------

all subsets ⊂ domain

> prop_subsetsNum :: Subsets c => c -> Bool
> prop_subsetsNum e
>     = subsetsNum e == genericLength (subsets e)

> prop_empty :: Subsets a => a -> Set (Elem a) -> Bool
> prop_empty a d
>     = subsetsNum (empty d `asTypeOf` a) == 0

isTriviallyEmpty ==> isEmpty

> prop_emptySubsets :: Subsets a => a -> Set (Elem a) -> Bool
> prop_emptySubsets a d
>     = domain e == d  && subsets e == [S.empty]  where e = emptySubsets d `asTypeOf` a

| Test helper function.

> isEmpty :: Subsets c => c -> Bool
> isEmpty 
>     = null . subsets
#endif


#ifdef TEST
Simple Implementation
---------------------

| Subset of all subsets of a given set.

> data SimpleSubsets a 
>     = SimpleSubsets (Set a) [Set a]
>         deriving (Show)

> instance Ord a => Eq (SimpleSubsets a) where
> 
>     SimpleSubsets da sa == SimpleSubsets db sb
>         = da == db && sort sa == sort sb

> instance Ord a => Subsets (SimpleSubsets a) where
> 
>     type Elem (SimpleSubsets a) = a
> 
>     domain  (SimpleSubsets d _) = d
>     subsets (SimpleSubsets _ s) = s
>     subsetsNum                  = genericLength . subsets
>     empty d                     = SimpleSubsets d []
>     isTriviallyEmpty            = null . subsets
>     emptySubsets d              = SimpleSubsets d [S.empty]

> toSimple :: (Subsets c) => c -> SimpleSubsets (Elem c)
> toSimple x 
>     = SimpleSubsets (domain x) (subsets x)

| This property states that @Simple@ is universal.

> prop_Simple :: Subsets c => (forall d. Subsets d => d -> Bool) -> c -> Bool
> prop_Simple p a
>   = p a  <==>  p (toSimple a)
#endif

Cached Size Implementation
--------------------------

> data CachedSize a
>     = CachedSize a Integer
>         deriving (Read, Show)

| smart constructor

> cachedSize :: Subsets c => c -> CachedSize c
> cachedSize c 
>     | s == 0    = CachedSize (empty $ domain c) s
>     | otherwise = CachedSize c s
>  where
>     s = subsetsNum c

> instance Subsets c => Subsets (CachedSize c)  where

>     type Elem (CachedSize c)    = Elem c

#ifdef TEST
>     subsets (CachedSize x _)    = subsets x
#endif
>     domain (CachedSize x _)     = domain x
>     subsetsNum (CachedSize _ i) = i
>     emptySubsets                = cachedSize . emptySubsets
>     empty                       = cachedSize . empty
>     isTriviallyEmpty c          = subsetsNum c == 0

> instance SetSum a c => SetSum a (CachedSize c) where
>     setSum' e (CachedSize c _)  = cachedSize $ setSum' e c



#ifdef TEST
Combining Sets of Subsets
-------------------------

Definition:

> prop_mappend :: (Monoid c, Subsets c) => c -> c -> Bool
> prop_mappend a b
>   =   domain (a `mappend` b) == domain a `S.union` domain b
>   &&  all (\s -> 
>                   s `elem` subsets (a `mappend` b)  
>           <==>   (s `S.intersection` domain a) `elem` subsets a  
>               && (s `S.intersection` domain b) `elem` subsets b 
>           ) (allSubsets $ domain $ a `mappend` b)

> allSubsets 
>     = map (S.fromList . concat) . sequence . map (\x -> [[],[x]]) . S.toList   

Properties:

> prop_monoid :: (Eq c, Monoid c) => c -> c -> c -> Bool
> prop_monoid a b c
>   =   a `mappend` b == b `mappend` a
>   &&  a `mappend` (b `mappend` c) == (a `mappend` b) `mappend` c
>   &&  mempty `mappend` a == a

     isEmpty a ==> isEmpty (a `mappend` b)


Implementation for @SimpleSubsets@:

> instance (Ord a) => Monoid (SimpleSubsets a) where

>     mempty 
>         = emptySubsets S.empty

>     SimpleSubsets da sa `mappend` SimpleSubsets db sb 
>         = SimpleSubsets (da `S.union` db) 
>             [a `S.union` b | a <- sa, b <- sb, a `S.intersection` c == b `S.intersection` c, c S.\\ a == c S.\\ b]
>      where
>         c = da `S.intersection` db


> tests = do
>     smallCheck 20 (prop_subsetsNum :: Equal Char -> Bool)
> --    smallCheck 5 (prop_mappend :: SimpleSubsets Char -> SimpleSubsets Char -> Bool)
#endif


> class Subsets c => Inters c where
>     intersection :: c -> c -> [[c]]

#ifdef TEST
> prop_intersection a b 
>   = unions [mconcat $ map toSimple x | x <- a `intersection` b] == toSimple a `mappend` toSimple b

> unions l = SimpleSubsets (S.unions $ map domain l) (concat $ map subsets l)
#endif

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


| @Equal a@ represents some subsets of a given set.

> data Equal a
>     = Equal (Set a) Int
>         deriving (Eq, Read, Show)

> instance (Ord a, Binary a) => Binary (Equal a) where
> 
>     put (Equal a b) = put (a, b)
>     get = do (a,b) <- get
>              return (Equal a b)

> instance Ord a => Particles (Equal a) where
>     type P (Equal a) = a
>     particles = domain



| Semantics

> instance Ord a => Subsets (Equal a) where

>     type Elem (Equal a) 
>         = a

>     domain (Equal d _) 
>         = d

#ifdef TEST
>     subsets (Equal d n) 
>         = map S.fromDistinctAscList (f (S.toList d) n)  where

>         f as 0 = [[]]
>         f as n = [x:bl | (x: xs) <- tails as, bl <- f xs (n-1)]
#endif

>     subsetsNum (Equal d n) 
>         = binomial (S.size d) n

>     emptySubsets d
>         = Equal d 0

>     empty d
>         = Equal d (-1)

>     isTriviallyEmpty (Equal d n)
>         = n<0 || n> S.size d


#ifdef TEST
| For testing

> instance Serial (Equal Char) where
>     series = cons1 f where

>         f :: Nat -> Equal Char
>         f i = Equal (S.fromList $ take n ['a'..]) m   where

>             (n, m) = [(n, m) | n <- [0..], m <- [0..n]] !! fromIntegral i
#endif



> instance Ord a => Inters (Equal a)  where

>     Equal a av `intersection` Equal b bv
>         = [ [ Equal (a S.\\ c) (av - cv)
>             , Equal  c          cv
>             , Equal (b S.\\ c) (bv - cv) 
>             ] 
>           | cv <- [min' .. max'] ]     where 
> 
>         c = S.intersection a b      -- a
> 
>         min' = 0 `max` (av - (S.size a - S.size c)) `max` (bv - (S.size b - S.size c))      -- av `max` (bv - (size b - size a))
>         max' = S.size c `min` av `min` bv       -- av `min` bv


> {-
> prop_factor a b
>     = b `subDomain` a  
>     ==>  toSimple a `mappend` toSimple b  ==  toSimple (a `factor` b) `mappend` toSimple b
> -}

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

> class (Subsets a, Subsets c {-, Elem a ~ Elem c -}) => SetSum a c  where
> 
>     setSum'  :: a -> c -> c



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

> a_limit = 3
> b_limit = 3


> subsetsNumStep 
>     :: (Container c, Subsets c, Inters (CElem c))
>      => c -> Integer
> subsetsNumStep x | isTriviallyEmpty x = 0
> subsetsNumStep x = case fromC x of
>     [] -> 1
>     l  -> snd $ minimumBy (compare `on` fst) $ take a_limit $ map cont l
>  where
>     cont c = case relatedElems c x' of
>         [] -> (0, subsetsNum c * subsetsNum x' )
>         b ->
>             let ll = [ subsetsNum $ foldr addToContainer x'' y
>                      | let (d, ys) = minimumBy (compare `on` (length . snd)) $ take b_limit $ map (\d -> (d, intersection c d)) b
>                      , let x'' = deleteL d x'
>                      , y <- ys]
>             in (length ll, sum ll)  
> 
>         where  x' = deleteL c x


> addToContainer 
>     :: (Container c, Subsets c, Inters (CElem c))
>     => CElem c -> c -> c
> addToContainer n c
>     |  isTriviallyEmpty n
>     || isTriviallyEmpty c
>     || any (null . snd) strength 
>         = empty $ domain c
>     | (x, y): _ <- [(x, y) | (x, [y]) <- strength]
>         = foldr addToContainer (deleteL x c) y
>     | otherwise 
>         = insertL n c 
>  where
>     strength = [(x, intersection n x) | x <- relatedElems n c]


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


> instance (Container c, Inters (CElem c)) => Subsets (Maybe c) where
>     type Elem (Maybe c) = Elem (CElem c)

>     domain      = maybe (error "domain vanished") (S.unions . map domain . fromC)
#ifdef TEST
>     subsets     = maybe [] (subsets . mconcat . map toSimple . fromC)
#endif
>     empty _     = Nothing

>     emptySubsets d 
>           | S.null d  = Just emptyC
>           | otherwise = Just $ insertL (emptySubsets d) emptyC

>     subsetsNum  = subsetsNumStep

>     isTriviallyEmpty Nothing = True
>     isTriviallyEmpty _  = False


> instance (Inters a, Container c, a ~ CElem c) => SetSum a (Maybe c) where
>     setSum'     = addToContainer




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

> data EmptyEqual a

> instance Decision (EmptyEqual a) where
>     type DecisionDomain (EmptyEqual a) = Equal a
>     holds _ (Equal _ n) = n == 0

> data SetAsEmptyEqual a

> instance Ord a => Bijection (SetAsEmptyEqual a) where
> 
>   type From (SetAsEmptyEqual a) = S.Set a
>   type To (SetAsEmptyEqual a) = Equal a
> 
>   fw _ d = Equal d 0
>   bw _ (Equal d 0) = d
>   bw _ _ = S.empty        


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


Auxiliary Definitions
---------------------


#ifdef TEST
| Natural number type with @Serial@ instance for testing.

> type Nat = Number.Peano.T

> instance Serial Number.Peano.T where
>     series = cons0 Zero \/ cons1 Succ

> infix 1 <==>
> (<==>) :: Bool -> Bool -> Bool
> (<==>) = (==)
#endif



| Cached binomial numbers. The first arguent should be non-negative.

> binomial :: Int -> Int -> Integer
> binomial m n 
>     | n' < 0    = 0
>     | otherwise = pascalsTriangle !! m !! n'
>  where
>     n' = min n (m-n)

| Pascal's triangle. It has to be a global constant to be cached.

> pascalsTriangle :: [[Integer]]
> pascalsTriangle 
>     = iterate nextRow [1]  where nextRow r = zipWith (+) (0:r) (r++[0])


Derived Instances
-----------------

> $( derive makeBinary ''CachedSize )
> $( derive makeBinary ''Tr )