content: {-# language TypeFamilies #-}
  
  module Ersatz.Relation.Data (
  -- * The @Relation@ type
    Relation
  -- * Construction
  , relation, symmetric_relation
  , build
  , buildFrom, buildFromM
  , identity
  -- * Components
  , bounds, (!), indices, assocs, elems
  , domain, codomain, universe
  , universeSize
  , is_homogeneous
  , card
  -- * Pretty printing
  , table
  )  where
  
  import Prelude hiding ( and, (&&), any )
  
  import Ersatz.Bit
  import Ersatz.Bits ( Bits, sumBit )
  import Ersatz.Codec
  import Ersatz.Variable (exists)
  import Ersatz.Problem (MonadSAT)
  
  import Control.Monad (guard)
  import qualified Data.Array as A
  import Data.Array ( Array, Ix )
  
  
  -- | @Relation a b@ represents a binary relation \(R \subseteq A \times B \),
  -- where the domain \(A\) is a finite subset of the type @a@,
  -- and the codomain \(B\) is a finite subset of the type @b@.
  --
  -- A relation is stored internally as @Array (a,b) Bit@,
  -- so @a@ and @b@ have to be instances of 'Ix',
  -- and both \(A\) and \(B\) are intervals.
  
  newtype Relation a b = Relation (Array (a, b) Bit)
  
  instance (Ix a, Ix b) => Codec (Relation a b) where
    type Decoded (Relation a b) = Array (a, b) Bool
    decode s (Relation a) = decode s a
    encode a = Relation $ encode a
  
  
  -- | @relation ((amin,bmin),(amax,mbax))@ constructs an indeterminate relation \( R \subseteq A \times B \)
  -- where \(A\) is @{amin .. amax}@ and \(B\) is @{bmin .. bmax}@.
  relation :: ( Ix a, Ix b, MonadSAT s m ) =>
    ((a,b),(a,b))
    -> m ( Relation a b )
  relation bnd = do
      pairs <- sequence $ do
          p <- A.range bnd
          return $ do
              x <- exists
              return ( p, x )
      return $ build bnd pairs
  
  -- | Constructs an indeterminate relation \( R \subseteq B \times B \)
  -- that is symmetric, i.e., \( \forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) \).
  symmetric_relation ::
    (MonadSAT s m, Ix b) =>
    ((b, b), (b, b)) -- ^ Since a symmetric relation must be homogeneous, the domain must equal the codomain.
                     -- Therefore, given bounds @((p,q),(r,s))@, it must hold that @p=q@ and @r=s@.
    -> m (Relation b b)
  symmetric_relation bnd = do
      pairs <- sequence $ do
          (p,q) <- A.range bnd
          guard $ p <= q
          return $ do
              x <- exists
              return $   ((p,q), x)
                     : [ ((q,p), x) | p /= q ]
      return $ build bnd $ concat pairs
  
  -- | Constructs a relation \(R \subseteq A \times B \) from a list.
  --
  -- ==== __Example__
  --
  -- @
  -- r = build ((0,'a'),(1,'b')) [ ((0,'a'), true), ((0,'b'), false)
  --                         , ((1,'a'), false), ((1,'b'), true) ]
  -- @
  build :: ( Ix a, Ix b )
        => ((a,b),(a,b))
        -> [ ((a,b), Bit ) ] -- ^ A list of tuples, where the first element represents an element
                             -- \( (x,y) \in A \times B \) and the second element is a positive 'Bit'
                             -- if \( (x,y) \in R \), or a negative 'Bit' if \( (x,y) \notin R \).
        -> Relation a b
  build bnd pairs = Relation $ A.array bnd pairs
  
  -- | Constructs a relation \(R \subseteq A \times B \) from a function.
  buildFrom :: (Ix a, Ix b)
            => ((a,b),(a,b))
            -> ((a,b) -> Bit) -- ^ A function that assigns a 'Bit'-value
                              -- to each element \( (x,y) \in A \times B \).
            -> Relation a b
  buildFrom bnd p = build bnd $ flip map (A.range bnd) $ \ i -> (i, p i)
  
  -- | Constructs an indeterminate relation \(R \subseteq A \times B\) from a function.
  buildFromM :: (Ix a, Ix b, MonadSAT s m)
            => ((a,b),(a,b))
            -> ((a,b) -> m Bit)
            -> m (Relation a b)
  buildFromM bnd p = do
      pairs <- sequence $ do
          i <- A.range bnd
          return $ do
              x <- p i
              return (i, x)
      return $ build bnd pairs
  
  -- | Constructs the identity relation \(I = \{ (x,x) ~|~ x \in A \} \subseteq A \times A\).
  identity :: (Ix a)
           => ((a,a),(a,a)) -- ^ Since the identity relation is homogeneous, the domain must equal the codomain.
                            -- Therefore, given bounds @((p,q),(r,s))@, it must hold that @p=q@ and @r=s@.
           -> Relation a a
  identity ((a,b),(c,d))
      | (a,c) == (b,d) = buildFrom ((a,b),(c,d)) (\ (i,j) -> bool $ i == j)
      | otherwise      = error "The domain must equal the codomain!"
  
  
  -- | The bounds of the array that correspond to the matrix representation of the given relation.
  --
  -- ==== __Example__
  --
  -- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false)]
  -- >>> bounds r
  -- ((0,0),(1,1))
  bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b))
  bounds ( Relation r ) = A.bounds r
  
  -- | The list of indices, where each index represents an element \( (x,y) \in A \times B \)
  -- that may be contained in the given relation \(R \subseteq A \times B \).
  --
  -- ==== __Example__
  --
  -- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false)]
  -- >>> indices r
  -- [(0,0),(0,1),(1,0),(1,1)]
  indices :: (Ix a, Ix b) => Relation a b -> [(a, b)]
  indices ( Relation r ) = A.indices r
  
  -- | The list of tuples for the given relation \(R \subseteq A \times B \),
  -- where the first element represents an element \( (x,y) \in A \times B \)
  -- and the second element indicates via a 'Bit' , if \( (x,y) \in R \) or not.
  --
  -- ==== __Example__
  --
  -- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false)]
  -- >>> assocs r
  -- [((0,0),Var (-1)),((0,1),Var 1),((1,0),Var 1),((1,1),Var (-1))]
  assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Bit)]
  assocs ( Relation r ) = A.assocs r
  
  -- | The list of elements of the array
  -- that correspond to the matrix representation of the given relation.
  --
  -- ==== __Example__
  --
  -- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]
  -- >>> elems r
  -- [Var (-1),Var 1,Var 1,Var (-1)]
  elems :: (Ix a, Ix b) => Relation a b -> [Bit]
  elems ( Relation r ) = A.elems r
  
  -- | The 'Bit'-value for a given element \( (x,y) \in A \times B \)
  -- and a given relation \(R \subseteq A \times B \) that indicates
  -- if \( (x,y) \in R \) or not.
  --
  -- ==== __Example__
  --
  -- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]
  -- >>> r ! (0,0)
  -- Var (-1)
  -- >>> r ! (0,1)
  -- Var 1
  (!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
  Relation r ! p = r A.! p
  
  -- | The domain \(A\) of a relation \(R \subseteq A \times B\).
  domain :: (Ix a, Ix b) => Relation a b -> [a]
  domain r =
    let ((x,_),(x',_)) = bounds r
    in A.range (x,x')
  
  -- | The codomain \(B\) of a relation \(R \subseteq A \times B\).
  codomain :: (Ix a, Ix b) => Relation a b -> [b]
  codomain r =
    let ((_,y),(_,y')) = bounds r
    in A.range (y,y')
  
  -- | The universe \(A\) of a relation \(R \subseteq A \times A\).
  universe :: Ix a => Relation a a -> [a]
  universe r
    | is_homogeneous r = domain r
    | otherwise = error "Relation is not homogeneous!"
  
  -- | The size of the universe \(A\) of a relation \(R \subseteq A \times A\).
  universeSize :: Ix a => Relation a a -> Int
  universeSize r
    | is_homogeneous r =
        let ((a,_),(c,_)) = bounds r
        in A.rangeSize (a,c)
    | otherwise = error "Relation is not homogeneous!"
  
  -- | Tests if a relation is homogeneous, i.e., if the domain is equal to the codomain.
  is_homogeneous :: Ix a => Relation a a -> Bool
  is_homogeneous r =
    let ((a,b),(c,d)) = bounds r
    in (a == b) && (c == d)
  
  -- | The number of pairs \( (x,y) \in R \) for the given relation
  -- \( R \subseteq A \times B \).
  card :: (Ix a, Ix b) => Relation a b -> Bits
  card = sumBit . elems
  
  -- | Print a satisfying assignment from a SAT solver, where the assignment is interpreted as a relation.
  -- @putStrLn $ table \</assignment/\>@ corresponds to the matrix representation of this relation.
  table :: (Ix a, Ix b)
        => Array (a,b) Bool -> String
  table r = unlines $ do
      let ((a,b),(c,d)) = A.bounds r
      x <- A.range (a,c)
      return $ unwords $ do
          y <- A.range (b,d)
          return $ if r A.! (x,y) then "*" else "."
  