{-# language TypeFamilies #-}

module Ersatz.Relation.Data ( Relation
, relation, symmetric_relation
, build
, buildFrom
, identity
, bounds, (!), indices, assocs, elems
, table
)  where

import Ersatz.Bit
import Ersatz.Codec
import Ersatz.Variable (exists)
import Ersatz.Problem (MonadSAT)

import qualified Data.Array as A
import Data.Array ( Array, Ix )
import Control.Monad.State

newtype Relation a b = Relation (A.Array (a, b) Bit)

instance (Ix a, Ix b) => Codec (Relation a b) where
  type Decoded (Relation a b) = A.Array (a, b) Bool
  decode :: Solution -> Relation a b -> f (Decoded (Relation a b))
decode Solution
s (Relation Array (a, b) Bit
a) = Solution -> Array (a, b) Bit -> f (Decoded (Array (a, b) Bit))
forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
s Array (a, b) Bit
a
  encode :: Decoded (Relation a b) -> Relation a b
encode Decoded (Relation a b)
a = Array (a, b) Bit -> Relation a b
forall a b. Array (a, b) Bit -> Relation a b
Relation (Array (a, b) Bit -> Relation a b)
-> Array (a, b) Bit -> Relation a b
forall a b. (a -> b) -> a -> b
$ Decoded (Array (a, b) Bit) -> Array (a, b) Bit
forall a. Codec a => Decoded a -> a
encode Decoded (Array (a, b) Bit)
Decoded (Relation a b)
a

relation :: ( Ix a, Ix b, MonadSAT s m )
         => ((a,b),(a,b)) -> m ( Relation a b )
relation :: ((a, b), (a, b)) -> m (Relation a b)
relation ((a, b), (a, b))
bnd = do
    [((a, b), Bit)]
pairs <- [m ((a, b), Bit)] -> m [((a, b), Bit)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([m ((a, b), Bit)] -> m [((a, b), Bit)])
-> [m ((a, b), Bit)] -> m [((a, b), Bit)]
forall a b. (a -> b) -> a -> b
$ do
        (a, b)
p <- ((a, b), (a, b)) -> [(a, b)]
forall a. Ix a => (a, a) -> [a]
A.range ((a, b), (a, b))
bnd
        m ((a, b), Bit) -> [m ((a, b), Bit)]
forall (m :: * -> *) a. Monad m => a -> m a
return (m ((a, b), Bit) -> [m ((a, b), Bit)])
-> m ((a, b), Bit) -> [m ((a, b), Bit)]
forall a b. (a -> b) -> a -> b
$ do
            Bit
x <- m Bit
forall a s (m :: * -> *). (Variable a, MonadSAT s m) => m a
exists
            ((a, b), Bit) -> m ((a, b), Bit)
forall (m :: * -> *) a. Monad m => a -> m a
return ( (a, b)
p, Bit
x )
    Relation a b -> m (Relation a b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Relation a b -> m (Relation a b))
-> Relation a b -> m (Relation a b)
forall a b. (a -> b) -> a -> b
$ ((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ((a, b), (a, b))
bnd [((a, b), Bit)]
pairs

symmetric_relation ::
  (MonadSAT s m, Ix b) =>
  ((b, b), (b, b)) -> m (Relation b b)
symmetric_relation :: ((b, b), (b, b)) -> m (Relation b b)
symmetric_relation ((b, b), (b, b))
bnd = do
    [[((b, b), Bit)]]
pairs <- [m [((b, b), Bit)]] -> m [[((b, b), Bit)]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([m [((b, b), Bit)]] -> m [[((b, b), Bit)]])
-> [m [((b, b), Bit)]] -> m [[((b, b), Bit)]]
forall a b. (a -> b) -> a -> b
$ do
        (b
p,b
q) <- ((b, b), (b, b)) -> [(b, b)]
forall a. Ix a => (a, a) -> [a]
A.range ((b, b), (b, b))
bnd
        Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ b
p b -> b -> Bool
forall a. Ord a => a -> a -> Bool
<= b
q
        m [((b, b), Bit)] -> [m [((b, b), Bit)]]
forall (m :: * -> *) a. Monad m => a -> m a
return (m [((b, b), Bit)] -> [m [((b, b), Bit)]])
-> m [((b, b), Bit)] -> [m [((b, b), Bit)]]
forall a b. (a -> b) -> a -> b
$ do
            Bit
x <- m Bit
forall a s (m :: * -> *). (Variable a, MonadSAT s m) => m a
exists
            [((b, b), Bit)] -> m [((b, b), Bit)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([((b, b), Bit)] -> m [((b, b), Bit)])
-> [((b, b), Bit)] -> m [((b, b), Bit)]
forall a b. (a -> b) -> a -> b
$   ((b
p,b
q), Bit
x)
                   ((b, b), Bit) -> [((b, b), Bit)] -> [((b, b), Bit)]
forall a. a -> [a] -> [a]
: [ ((b
q,b
p), Bit
x) | b
p b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/= b
q ]
    Relation b b -> m (Relation b b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Relation b b -> m (Relation b b))
-> Relation b b -> m (Relation b b)
forall a b. (a -> b) -> a -> b
$ ((b, b), (b, b)) -> [((b, b), Bit)] -> Relation b b
forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ((b, b), (b, b))
bnd ([((b, b), Bit)] -> Relation b b)
-> [((b, b), Bit)] -> Relation b b
forall a b. (a -> b) -> a -> b
$ [[((b, b), Bit)]] -> [((b, b), Bit)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[((b, b), Bit)]]
pairs

build :: ( Ix a, Ix b )
      => ((a,b),(a,b))
      -> [ ((a,b), Bit ) ]
      -> Relation a b
build :: ((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ((a, b), (a, b))
bnd [((a, b), Bit)]
pairs = Array (a, b) Bit -> Relation a b
forall a b. Array (a, b) Bit -> Relation a b
Relation (Array (a, b) Bit -> Relation a b)
-> Array (a, b) Bit -> Relation a b
forall a b. (a -> b) -> a -> b
$ ((a, b), (a, b)) -> [((a, b), Bit)] -> Array (a, b) Bit
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
A.array ((a, b), (a, b))
bnd [((a, b), Bit)]
pairs

buildFrom :: (Ix a, Ix b)
          => (a -> b -> Bit) -> ((a,b),(a,b)) -> Relation a b
buildFrom :: (a -> b -> Bit) -> ((a, b), (a, b)) -> Relation a b
buildFrom a -> b -> Bit
p ((a, b), (a, b))
bnd = ((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ((a, b), (a, b))
bnd ([((a, b), Bit)] -> Relation a b)
-> [((a, b), Bit)] -> Relation a b
forall a b. (a -> b) -> a -> b
$ (((a, b) -> ((a, b), Bit)) -> [(a, b)] -> [((a, b), Bit)])
-> [(a, b)] -> ((a, b) -> ((a, b), Bit)) -> [((a, b), Bit)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a, b) -> ((a, b), Bit)) -> [(a, b)] -> [((a, b), Bit)]
forall a b. (a -> b) -> [a] -> [b]
map (((a, b), (a, b)) -> [(a, b)]
forall a. Ix a => (a, a) -> [a]
A.range ((a, b), (a, b))
bnd) (((a, b) -> ((a, b), Bit)) -> [((a, b), Bit)])
-> ((a, b) -> ((a, b), Bit)) -> [((a, b), Bit)]
forall a b. (a -> b) -> a -> b
$ \ (a
i,b
j) ->
    ((a
i,b
j), a -> b -> Bit
p a
i b
j)

identity :: (Ix a)
         => ((a,a),(a,a)) -> Relation a a
identity :: ((a, a), (a, a)) -> Relation a a
identity = (a -> a -> Bit) -> ((a, a), (a, a)) -> Relation a a
forall a b.
(Ix a, Ix b) =>
(a -> b -> Bit) -> ((a, b), (a, b)) -> Relation a b
buildFrom (\ a
i a
j -> Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Bool -> Bit) -> Bool -> Bit
forall a b. (a -> b) -> a -> b
$ a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j)


bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b))
bounds :: Relation a b -> ((a, b), (a, b))
bounds ( Relation Array (a, b) Bit
r ) = Array (a, b) Bit -> ((a, b), (a, b))
forall i e. Array i e -> (i, i)
A.bounds Array (a, b) Bit
r

indices :: (Ix a, Ix b) => Relation a b -> [(a, b)]
indices :: Relation a b -> [(a, b)]
indices ( Relation Array (a, b) Bit
r ) = Array (a, b) Bit -> [(a, b)]
forall i e. Ix i => Array i e -> [i]
A.indices Array (a, b) Bit
r

assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Bit)]
assocs :: Relation a b -> [((a, b), Bit)]
assocs ( Relation Array (a, b) Bit
r ) = Array (a, b) Bit -> [((a, b), Bit)]
forall i e. Ix i => Array i e -> [(i, e)]
A.assocs Array (a, b) Bit
r

elems :: (Ix a, Ix b) => Relation a b -> [Bit]
elems :: Relation a b -> [Bit]
elems ( Relation Array (a, b) Bit
r ) = Array (a, b) Bit -> [Bit]
forall i e. Array i e -> [e]
A.elems Array (a, b) Bit
r

(!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
Relation Array (a, b) Bit
r ! :: Relation a b -> (a, b) -> Bit
! (a, b)
p = Array (a, b) Bit
r Array (a, b) Bit -> (a, b) -> Bit
forall i e. Ix i => Array i e -> i -> e
A.! (a, b)
p


table :: (Enum a, Ix a, Enum b, Ix b)
      => Array (a,b) Bool -> String
table :: Array (a, b) Bool -> String
table Array (a, b) Bool
r = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ do
    let ((a
a,b
b),(a
c,b
d)) = Array (a, b) Bool -> ((a, b), (a, b))
forall i e. Array i e -> (i, i)
A.bounds Array (a, b) Bool
r
    a
x <- [ a
a .. a
c ]
    String -> [String]
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ do
        b
y <- [ b
b .. b
d ]
        String -> [String]
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ if Array (a, b) Bool
r Array (a, b) Bool -> (a, b) -> Bool
forall i e. Ix i => Array i e -> i -> e
A.! (a
x,b
y) then String
"*" else String
"."