{-# language FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
{-# language TupleSections #-}

module Satchmo.Set.Data

( Set , unknown, unknownSingleton, constant
, member, keys, keysSet, keys, assocs, elems
, all2, common2
) 

where

import Satchmo.Code
import qualified Satchmo.Boolean as B

import Satchmo.SAT

import qualified Data.Set as S
import qualified Data.Map.Strict as M

import Control.Monad ( guard, forM )
import Control.Applicative ( (<$>), (<*>) )
import Data.List ( tails )

newtype Set a = Set (M.Map a B.Boolean)

instance ( Functor m, Decode m B.Boolean Bool, Ord a )
         => Decode m (Set a) ( S.Set a) where
    decode :: Set a -> m (Set a)
decode (Set Map a Boolean
m) = 
        forall k a. Map k a -> Set k
M.keysSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter forall a. a -> a
id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) c a. Decode m c a => c -> m a
decode Map a Boolean
m

keys :: Set k -> [k]
keys (Set Map k Boolean
m) = forall k a. Map k a -> [k]
M.keys Map k Boolean
m
keysSet :: Set k -> Set k
keysSet (Set Map k Boolean
m) = forall k a. Map k a -> Set k
M.keysSet Map k Boolean
m
assocs :: Set k -> [(k, Boolean)]
assocs (Set Map k Boolean
m) = forall k a. Map k a -> [(k, a)]
M.assocs Map k Boolean
m
elems :: Set k -> [Boolean]
elems (Set Map k Boolean
m) = forall k a. Map k a -> [a]
M.elems Map k Boolean
m

member :: k -> Set k -> m Boolean
member k
x (Set Map k Boolean
m) = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
x Map k Boolean
m of
    Maybe Boolean
Nothing -> forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
    Just Boolean
y  -> forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
y


-- | allocate an unknown subset of these elements
unknown :: ( B.MonadSAT m , Ord a )
         => [a] -> m (Set a)
unknown :: forall (m :: * -> *) a. (MonadSAT m, Ord a) => [a] -> m (Set a)
unknown [a]
xs = forall a. Map a Boolean -> Set a
Set forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList 
     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [a]
xs forall a b. (a -> b) -> a -> b
$ \ a
x -> (a
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadSAT m => m Boolean
B.boolean )

unknownSingleton :: [k] -> m (Set k)
unknownSingleton [k]
xs = do
    Set k
s <- forall (m :: * -> *) a. (MonadSAT m, Ord a) => [a] -> m (Set a)
unknown [k]
xs
    forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
B.assert forall a b. (a -> b) -> a -> b
$ forall {k}. Set k -> [Boolean]
elems Set k
s
    forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ forall a b. (a -> b) -> a -> b
$ do 
       Boolean
x : [Boolean]
ys <- forall a. [a] -> [[a]]
tails forall a b. (a -> b) -> a -> b
$ forall {k}. Set k -> [Boolean]
elems Set k
s ; Boolean
y <- [Boolean]
ys
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
B.assert [ Boolean -> Boolean
B.not Boolean
x, Boolean -> Boolean
B.not Boolean
y ]
    forall (m :: * -> *) a. Monad m => a -> m a
return Set k
s

constant :: ( B.MonadSAT m , Ord a )
         => [a] -> m (Set a)
constant :: forall (m :: * -> *) a. (MonadSAT m, Ord a) => [a] -> m (Set a)
constant [a]
xs = forall a. Map a Boolean -> Set a
Set forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList 
     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [a]
xs forall a b. (a -> b) -> a -> b
$ \ a
x -> (a
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True )

all2 :: (Boolean -> Boolean -> m Boolean) -> Set k -> Set k -> m Boolean
all2 Boolean -> Boolean -> m Boolean
f Set k
s Set k
t = forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and
 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
S.union (forall {k}. Set k -> Set k
keysSet Set k
s)(forall {k}. Set k -> Set k
keysSet Set k
t))
 ( \ k
x -> do Boolean
a <- forall {k} {m :: * -> *}.
(Ord k, MonadSAT m) =>
k -> Set k -> m Boolean
member k
x Set k
s; Boolean
b <- forall {k} {m :: * -> *}.
(Ord k, MonadSAT m) =>
k -> Set k -> m Boolean
member k
x Set k
t; Boolean -> Boolean -> m Boolean
f Boolean
a Boolean
b )

common2 :: (Boolean -> Boolean -> f Boolean) -> Set a -> Set a -> f (Set a)
common2 Boolean -> Boolean -> f Boolean
f Set a
s Set a
t = forall a. Map a Boolean -> Set a
Set forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
 forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
S.union (forall {k}. Set k -> Set k
keysSet Set a
s)(forall {k}. Set k -> Set k
keysSet Set a
t))
 ( \ a
x -> do Boolean
a <- forall {k} {m :: * -> *}.
(Ord k, MonadSAT m) =>
k -> Set k -> m Boolean
member a
x Set a
s; Boolean
b <- forall {k} {m :: * -> *}.
(Ord k, MonadSAT m) =>
k -> Set k -> m Boolean
member a
x Set a
t
             Boolean
y <- Boolean -> Boolean -> f Boolean
f Boolean
a Boolean
b ; forall (m :: * -> *) a. Monad m => a -> m a
return (a
x,Boolean
y) )