{-# LANGUAGE BangPatterns, DeriveDataTypeable, DeriveGeneric, MultiParamTypeClasses, OverloadedStrings, Safe, TypeApplications #-}

{-|
Module      : Dep.Data.Sum
Description : A module that defines data structures for a sum, and a product-of-sums.
Maintainer  : hapytexeu+gh@gmail.com
Stability   : experimental
Portability : POSIX

This module provides utility functions to compress/decompress sums, and render these 'Dep.Data.Product.Product''s to
a unicode string.
-}

module Dep.Data.Sum (
    -- * Type synonyms to represent synthesis
    Sum(Sum), Sum', CompactSum(CompactSum), CompactSum', ProductOfSums(ProductOfSums), ProductOfSums'
    -- * Print sums and product of sums
  , showProductOfSums, showSum, showSum'
  ) where

import Control.DeepSeq(NFData)

import Data.Bool(bool)
import Data.Data(Data)
import Data.Hashable(Hashable)
import Data.Text(Text, cons)

import Dep.Class.Opposite(opposite)
import Dep.Class.Simplify(simplify)
import Dep.Data.LogicItem(EvaluateItem(evaluateItem, isTrivial, numberOfVariables), ToCompact(fromCompact, toCompact), getThreeList, putThreeList, subscriptVariable)
import Dep.Data.Three(ThreePath, Three(Leaf), wipeAll)
import Dep.Data.ThreeValue(ThreeValue(Zero, One, DontCare))
import Data.Binary(Binary(get, put, putList))

import GHC.Generics(Generic)

import Test.QuickCheck.Arbitrary(Arbitrary(arbitrary, shrink))

-- | A type alias for a sum that is a 'ThreePath'.
type Sum' = ThreePath

-- | A data type that can be used to specify a sum. By using a newtype,
-- we can add special instance to the 'Sum'.
newtype Sum = Sum Sum' deriving (Typeable Sum
DataType
Constr
Typeable Sum
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Sum -> c Sum)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Sum)
-> (Sum -> Constr)
-> (Sum -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Sum))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sum))
-> ((forall b. Data b => b -> b) -> Sum -> Sum)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sum -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sum -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sum -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sum -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sum -> m Sum)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sum -> m Sum)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sum -> m Sum)
-> Data Sum
Sum -> DataType
Sum -> Constr
(forall b. Data b => b -> b) -> Sum -> Sum
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sum -> c Sum
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sum
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Sum -> u
forall u. (forall d. Data d => d -> u) -> Sum -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sum -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sum -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sum -> m Sum
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sum -> m Sum
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sum
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sum -> c Sum
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sum)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sum)
$cSum :: Constr
$tSum :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sum -> m Sum
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sum -> m Sum
gmapMp :: (forall d. Data d => d -> m d) -> Sum -> m Sum
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sum -> m Sum
gmapM :: (forall d. Data d => d -> m d) -> Sum -> m Sum
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sum -> m Sum
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sum -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sum -> u
gmapQ :: (forall d. Data d => d -> u) -> Sum -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sum -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sum -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sum -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sum -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sum -> r
gmapT :: (forall b. Data b => b -> b) -> Sum -> Sum
$cgmapT :: (forall b. Data b => b -> b) -> Sum -> Sum
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sum)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sum)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sum)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sum)
dataTypeOf :: Sum -> DataType
$cdataTypeOf :: Sum -> DataType
toConstr :: Sum -> Constr
$ctoConstr :: Sum -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sum
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sum
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sum -> c Sum
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sum -> c Sum
$cp1Data :: Typeable Sum
Data, Sum -> Sum -> Bool
(Sum -> Sum -> Bool) -> (Sum -> Sum -> Bool) -> Eq Sum
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sum -> Sum -> Bool
$c/= :: Sum -> Sum -> Bool
== :: Sum -> Sum -> Bool
$c== :: Sum -> Sum -> Bool
Eq, (forall x. Sum -> Rep Sum x)
-> (forall x. Rep Sum x -> Sum) -> Generic Sum
forall x. Rep Sum x -> Sum
forall x. Sum -> Rep Sum x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Sum x -> Sum
$cfrom :: forall x. Sum -> Rep Sum x
Generic, Eq Sum
Eq Sum
-> (Sum -> Sum -> Ordering)
-> (Sum -> Sum -> Bool)
-> (Sum -> Sum -> Bool)
-> (Sum -> Sum -> Bool)
-> (Sum -> Sum -> Bool)
-> (Sum -> Sum -> Sum)
-> (Sum -> Sum -> Sum)
-> Ord Sum
Sum -> Sum -> Bool
Sum -> Sum -> Ordering
Sum -> Sum -> Sum
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Sum -> Sum -> Sum
$cmin :: Sum -> Sum -> Sum
max :: Sum -> Sum -> Sum
$cmax :: Sum -> Sum -> Sum
>= :: Sum -> Sum -> Bool
$c>= :: Sum -> Sum -> Bool
> :: Sum -> Sum -> Bool
$c> :: Sum -> Sum -> Bool
<= :: Sum -> Sum -> Bool
$c<= :: Sum -> Sum -> Bool
< :: Sum -> Sum -> Bool
$c< :: Sum -> Sum -> Bool
compare :: Sum -> Sum -> Ordering
$ccompare :: Sum -> Sum -> Ordering
$cp1Ord :: Eq Sum
Ord, ReadPrec [Sum]
ReadPrec Sum
Int -> ReadS Sum
ReadS [Sum]
(Int -> ReadS Sum)
-> ReadS [Sum] -> ReadPrec Sum -> ReadPrec [Sum] -> Read Sum
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Sum]
$creadListPrec :: ReadPrec [Sum]
readPrec :: ReadPrec Sum
$creadPrec :: ReadPrec Sum
readList :: ReadS [Sum]
$creadList :: ReadS [Sum]
readsPrec :: Int -> ReadS Sum
$creadsPrec :: Int -> ReadS Sum
Read, Int -> Sum -> ShowS
[Sum] -> ShowS
Sum -> String
(Int -> Sum -> ShowS)
-> (Sum -> String) -> ([Sum] -> ShowS) -> Show Sum
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sum] -> ShowS
$cshowList :: [Sum] -> ShowS
show :: Sum -> String
$cshow :: Sum -> String
showsPrec :: Int -> Sum -> ShowS
$cshowsPrec :: Int -> Sum -> ShowS
Show)

instance Arbitrary Sum where
  arbitrary :: Gen Sum
arbitrary = Sum' -> Sum
Sum (Sum' -> Sum) -> Gen Sum' -> Gen Sum
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Sum'
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: Sum -> [Sum]
shrink (Sum Sum'
s) = Sum' -> Sum
Sum (Sum' -> Sum) -> [Sum'] -> [Sum]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sum' -> [Sum']
forall a. Arbitrary a => a -> [a]
shrink Sum'
s

instance Binary Sum where
  get :: Get Sum
get  = Sum' -> Sum
Sum (Sum' -> Sum) -> Get Sum' -> Get Sum
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Sum'
getThreeList
  put :: Sum -> Put
put (Sum Sum'
s) = Sum' -> Put
putThreeList Sum'
s

instance EvaluateItem Sum where
  evaluateItem :: (Int -> Bool) -> Sum -> Bool
evaluateItem Int -> Bool
f ~(Sum Sum'
s) = Int -> Sum' -> Bool
go Int
1 Sum'
s
    where go :: Int -> Sum' -> Bool
go Int
_ [] = Bool
False
          go !Int
n (ThreeValue
Zero:Sum'
xs) = Bool -> Bool
not (Int -> Bool
f Int
n) Bool -> Bool -> Bool
|| Int -> Sum' -> Bool
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Sum'
xs
          go !Int
n (ThreeValue
One:Sum'
xs) = Int -> Bool
f Int
n Bool -> Bool -> Bool
|| Int -> Sum' -> Bool
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Sum'
xs
          go !Int
n (~ThreeValue
DontCare:Sum'
xs) = Int -> Sum' -> Bool
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Sum'
xs
  isTrivial :: Sum -> ThreeValue
isTrivial ~(Sum Sum'
s) = ThreeValue -> ThreeValue -> Bool -> ThreeValue
forall a. a -> a -> Bool -> a
bool ThreeValue
DontCare ThreeValue
Zero ((ThreeValue -> Bool) -> Sum' -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ThreeValue
DontCare ThreeValue -> ThreeValue -> Bool
forall a. Eq a => a -> a -> Bool
==) Sum'
s)
  numberOfVariables :: Sum -> Int
numberOfVariables (Sum Sum'
s) = (Sum' -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Sum' -> Int) -> (Sum' -> Sum') -> Sum' -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ThreeValue -> Bool) -> Sum' -> Sum'
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (ThreeValue
DontCare ThreeValue -> ThreeValue -> Bool
forall a. Eq a => a -> a -> Bool
==) (Sum' -> Sum') -> (Sum' -> Sum') -> Sum' -> Sum'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sum' -> Sum'
forall a. [a] -> [a]
reverse) Sum'
s

instance Hashable Sum

instance NFData Sum

-- | A more compact representation of a sum where the indexes that have 'Zero'
-- or 'One' are listed by the /positive/ or /negative/ index respectively.
type CompactSum' = [Int]

-- | A data type that can be used to specify a 'CompactSum'. By using a new
-- type, this means that we can define other instances than these for a list of 'Int'.
newtype CompactSum = CompactSum CompactSum' deriving (Typeable CompactSum
DataType
Constr
Typeable CompactSum
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CompactSum -> c CompactSum)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CompactSum)
-> (CompactSum -> Constr)
-> (CompactSum -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CompactSum))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c CompactSum))
-> ((forall b. Data b => b -> b) -> CompactSum -> CompactSum)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CompactSum -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CompactSum -> r)
-> (forall u. (forall d. Data d => d -> u) -> CompactSum -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> CompactSum -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CompactSum -> m CompactSum)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CompactSum -> m CompactSum)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CompactSum -> m CompactSum)
-> Data CompactSum
CompactSum -> DataType
CompactSum -> Constr
(forall b. Data b => b -> b) -> CompactSum -> CompactSum
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CompactSum -> c CompactSum
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CompactSum
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CompactSum -> u
forall u. (forall d. Data d => d -> u) -> CompactSum -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CompactSum -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CompactSum -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CompactSum -> m CompactSum
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CompactSum -> m CompactSum
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CompactSum
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CompactSum -> c CompactSum
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CompactSum)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompactSum)
$cCompactSum :: Constr
$tCompactSum :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CompactSum -> m CompactSum
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CompactSum -> m CompactSum
gmapMp :: (forall d. Data d => d -> m d) -> CompactSum -> m CompactSum
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CompactSum -> m CompactSum
gmapM :: (forall d. Data d => d -> m d) -> CompactSum -> m CompactSum
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CompactSum -> m CompactSum
gmapQi :: Int -> (forall d. Data d => d -> u) -> CompactSum -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CompactSum -> u
gmapQ :: (forall d. Data d => d -> u) -> CompactSum -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CompactSum -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CompactSum -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CompactSum -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CompactSum -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CompactSum -> r
gmapT :: (forall b. Data b => b -> b) -> CompactSum -> CompactSum
$cgmapT :: (forall b. Data b => b -> b) -> CompactSum -> CompactSum
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompactSum)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompactSum)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CompactSum)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CompactSum)
dataTypeOf :: CompactSum -> DataType
$cdataTypeOf :: CompactSum -> DataType
toConstr :: CompactSum -> Constr
$ctoConstr :: CompactSum -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CompactSum
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CompactSum
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CompactSum -> c CompactSum
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CompactSum -> c CompactSum
$cp1Data :: Typeable CompactSum
Data, CompactSum -> CompactSum -> Bool
(CompactSum -> CompactSum -> Bool)
-> (CompactSum -> CompactSum -> Bool) -> Eq CompactSum
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CompactSum -> CompactSum -> Bool
$c/= :: CompactSum -> CompactSum -> Bool
== :: CompactSum -> CompactSum -> Bool
$c== :: CompactSum -> CompactSum -> Bool
Eq, (forall x. CompactSum -> Rep CompactSum x)
-> (forall x. Rep CompactSum x -> CompactSum) -> Generic CompactSum
forall x. Rep CompactSum x -> CompactSum
forall x. CompactSum -> Rep CompactSum x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CompactSum x -> CompactSum
$cfrom :: forall x. CompactSum -> Rep CompactSum x
Generic, Eq CompactSum
Eq CompactSum
-> (CompactSum -> CompactSum -> Ordering)
-> (CompactSum -> CompactSum -> Bool)
-> (CompactSum -> CompactSum -> Bool)
-> (CompactSum -> CompactSum -> Bool)
-> (CompactSum -> CompactSum -> Bool)
-> (CompactSum -> CompactSum -> CompactSum)
-> (CompactSum -> CompactSum -> CompactSum)
-> Ord CompactSum
CompactSum -> CompactSum -> Bool
CompactSum -> CompactSum -> Ordering
CompactSum -> CompactSum -> CompactSum
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CompactSum -> CompactSum -> CompactSum
$cmin :: CompactSum -> CompactSum -> CompactSum
max :: CompactSum -> CompactSum -> CompactSum
$cmax :: CompactSum -> CompactSum -> CompactSum
>= :: CompactSum -> CompactSum -> Bool
$c>= :: CompactSum -> CompactSum -> Bool
> :: CompactSum -> CompactSum -> Bool
$c> :: CompactSum -> CompactSum -> Bool
<= :: CompactSum -> CompactSum -> Bool
$c<= :: CompactSum -> CompactSum -> Bool
< :: CompactSum -> CompactSum -> Bool
$c< :: CompactSum -> CompactSum -> Bool
compare :: CompactSum -> CompactSum -> Ordering
$ccompare :: CompactSum -> CompactSum -> Ordering
$cp1Ord :: Eq CompactSum
Ord, ReadPrec [CompactSum]
ReadPrec CompactSum
Int -> ReadS CompactSum
ReadS [CompactSum]
(Int -> ReadS CompactSum)
-> ReadS [CompactSum]
-> ReadPrec CompactSum
-> ReadPrec [CompactSum]
-> Read CompactSum
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [CompactSum]
$creadListPrec :: ReadPrec [CompactSum]
readPrec :: ReadPrec CompactSum
$creadPrec :: ReadPrec CompactSum
readList :: ReadS [CompactSum]
$creadList :: ReadS [CompactSum]
readsPrec :: Int -> ReadS CompactSum
$creadsPrec :: Int -> ReadS CompactSum
Read, Int -> CompactSum -> ShowS
[CompactSum] -> ShowS
CompactSum -> String
(Int -> CompactSum -> ShowS)
-> (CompactSum -> String)
-> ([CompactSum] -> ShowS)
-> Show CompactSum
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CompactSum] -> ShowS
$cshowList :: [CompactSum] -> ShowS
show :: CompactSum -> String
$cshow :: CompactSum -> String
showsPrec :: Int -> CompactSum -> ShowS
$cshowsPrec :: Int -> CompactSum -> ShowS
Show)

instance Arbitrary CompactSum where
  arbitrary :: Gen CompactSum
arbitrary = forall b. ToCompact Sum b => Sum -> b
forall a b. ToCompact a b => a -> b
toCompact @Sum (Sum -> CompactSum) -> Gen Sum -> Gen CompactSum
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Sum
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: CompactSum -> [CompactSum]
shrink CompactSum
cs = forall b. ToCompact Sum b => Sum -> b
forall a b. ToCompact a b => a -> b
toCompact @Sum (Sum -> CompactSum) -> [Sum] -> [CompactSum]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sum -> [Sum]
forall a. Arbitrary a => a -> [a]
shrink (CompactSum -> Sum
forall a b. ToCompact a b => b -> a
fromCompact CompactSum
cs)

instance Binary CompactSum where
  put :: CompactSum -> Put
put (CompactSum CompactSum'
cs) = CompactSum' -> Put
forall t. Binary t => t -> Put
put CompactSum'
cs
  get :: Get CompactSum
get = CompactSum' -> CompactSum
CompactSum (CompactSum' -> CompactSum) -> Get CompactSum' -> Get CompactSum
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get CompactSum'
forall t. Binary t => Get t
get

instance Hashable CompactSum

instance EvaluateItem CompactSum where
  evaluateItem :: (Int -> Bool) -> CompactSum -> Bool
evaluateItem Int -> Bool
f ~(CompactSum CompactSum'
s) = (Int -> Bool) -> CompactSum' -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Int -> Bool
go CompactSum'
s
    where go :: Int -> Bool
go Int
n
            | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = Bool -> Bool
not (Int -> Bool
f (-Int
n))
            | Bool
otherwise = Int -> Bool
f Int
n
  isTrivial :: CompactSum -> ThreeValue
isTrivial ~(CompactSum CompactSum'
cs) = ThreeValue -> ThreeValue -> Bool -> ThreeValue
forall a. a -> a -> Bool -> a
bool ThreeValue
DontCare ThreeValue
Zero ((Int -> Bool) -> CompactSum' -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int
0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) CompactSum'
cs)
  numberOfVariables :: CompactSum -> Int
numberOfVariables (CompactSum CompactSum'
cs) = CompactSum' -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> CompactSum' -> CompactSum'
forall a. a -> [a] -> [a]
: (Int -> Int) -> CompactSum' -> CompactSum'
forall a b. (a -> b) -> [a] -> [b]
map Int -> Int
forall a. Num a => a -> a
abs CompactSum'
cs)

instance NFData CompactSum

-- | A type synonym to present a product of sums where each item of the list is a 'Sum''.
type ProductOfSums' = [Sum']

-- | A data type that is used to specify a product of sums. This type can be used
-- to specify new instance other than these of a list of lists of 'Int's.
newtype ProductOfSums = ProductOfSums [Sum] deriving (Typeable ProductOfSums
DataType
Constr
Typeable ProductOfSums
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ProductOfSums -> c ProductOfSums)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ProductOfSums)
-> (ProductOfSums -> Constr)
-> (ProductOfSums -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ProductOfSums))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ProductOfSums))
-> ((forall b. Data b => b -> b) -> ProductOfSums -> ProductOfSums)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ProductOfSums -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ProductOfSums -> r)
-> (forall u. (forall d. Data d => d -> u) -> ProductOfSums -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ProductOfSums -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums)
-> Data ProductOfSums
ProductOfSums -> DataType
ProductOfSums -> Constr
(forall b. Data b => b -> b) -> ProductOfSums -> ProductOfSums
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProductOfSums -> c ProductOfSums
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProductOfSums
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ProductOfSums -> u
forall u. (forall d. Data d => d -> u) -> ProductOfSums -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProductOfSums -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProductOfSums -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProductOfSums
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProductOfSums -> c ProductOfSums
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProductOfSums)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProductOfSums)
$cProductOfSums :: Constr
$tProductOfSums :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums
gmapMp :: (forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums
gmapM :: (forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProductOfSums -> m ProductOfSums
gmapQi :: Int -> (forall d. Data d => d -> u) -> ProductOfSums -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ProductOfSums -> u
gmapQ :: (forall d. Data d => d -> u) -> ProductOfSums -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ProductOfSums -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProductOfSums -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProductOfSums -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProductOfSums -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProductOfSums -> r
gmapT :: (forall b. Data b => b -> b) -> ProductOfSums -> ProductOfSums
$cgmapT :: (forall b. Data b => b -> b) -> ProductOfSums -> ProductOfSums
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProductOfSums)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProductOfSums)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ProductOfSums)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProductOfSums)
dataTypeOf :: ProductOfSums -> DataType
$cdataTypeOf :: ProductOfSums -> DataType
toConstr :: ProductOfSums -> Constr
$ctoConstr :: ProductOfSums -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProductOfSums
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProductOfSums
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProductOfSums -> c ProductOfSums
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProductOfSums -> c ProductOfSums
$cp1Data :: Typeable ProductOfSums
Data, ProductOfSums -> ProductOfSums -> Bool
(ProductOfSums -> ProductOfSums -> Bool)
-> (ProductOfSums -> ProductOfSums -> Bool) -> Eq ProductOfSums
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProductOfSums -> ProductOfSums -> Bool
$c/= :: ProductOfSums -> ProductOfSums -> Bool
== :: ProductOfSums -> ProductOfSums -> Bool
$c== :: ProductOfSums -> ProductOfSums -> Bool
Eq, (forall x. ProductOfSums -> Rep ProductOfSums x)
-> (forall x. Rep ProductOfSums x -> ProductOfSums)
-> Generic ProductOfSums
forall x. Rep ProductOfSums x -> ProductOfSums
forall x. ProductOfSums -> Rep ProductOfSums x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ProductOfSums x -> ProductOfSums
$cfrom :: forall x. ProductOfSums -> Rep ProductOfSums x
Generic, Eq ProductOfSums
Eq ProductOfSums
-> (ProductOfSums -> ProductOfSums -> Ordering)
-> (ProductOfSums -> ProductOfSums -> Bool)
-> (ProductOfSums -> ProductOfSums -> Bool)
-> (ProductOfSums -> ProductOfSums -> Bool)
-> (ProductOfSums -> ProductOfSums -> Bool)
-> (ProductOfSums -> ProductOfSums -> ProductOfSums)
-> (ProductOfSums -> ProductOfSums -> ProductOfSums)
-> Ord ProductOfSums
ProductOfSums -> ProductOfSums -> Bool
ProductOfSums -> ProductOfSums -> Ordering
ProductOfSums -> ProductOfSums -> ProductOfSums
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ProductOfSums -> ProductOfSums -> ProductOfSums
$cmin :: ProductOfSums -> ProductOfSums -> ProductOfSums
max :: ProductOfSums -> ProductOfSums -> ProductOfSums
$cmax :: ProductOfSums -> ProductOfSums -> ProductOfSums
>= :: ProductOfSums -> ProductOfSums -> Bool
$c>= :: ProductOfSums -> ProductOfSums -> Bool
> :: ProductOfSums -> ProductOfSums -> Bool
$c> :: ProductOfSums -> ProductOfSums -> Bool
<= :: ProductOfSums -> ProductOfSums -> Bool
$c<= :: ProductOfSums -> ProductOfSums -> Bool
< :: ProductOfSums -> ProductOfSums -> Bool
$c< :: ProductOfSums -> ProductOfSums -> Bool
compare :: ProductOfSums -> ProductOfSums -> Ordering
$ccompare :: ProductOfSums -> ProductOfSums -> Ordering
$cp1Ord :: Eq ProductOfSums
Ord, ReadPrec [ProductOfSums]
ReadPrec ProductOfSums
Int -> ReadS ProductOfSums
ReadS [ProductOfSums]
(Int -> ReadS ProductOfSums)
-> ReadS [ProductOfSums]
-> ReadPrec ProductOfSums
-> ReadPrec [ProductOfSums]
-> Read ProductOfSums
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [ProductOfSums]
$creadListPrec :: ReadPrec [ProductOfSums]
readPrec :: ReadPrec ProductOfSums
$creadPrec :: ReadPrec ProductOfSums
readList :: ReadS [ProductOfSums]
$creadList :: ReadS [ProductOfSums]
readsPrec :: Int -> ReadS ProductOfSums
$creadsPrec :: Int -> ReadS ProductOfSums
Read, Int -> ProductOfSums -> ShowS
[ProductOfSums] -> ShowS
ProductOfSums -> String
(Int -> ProductOfSums -> ShowS)
-> (ProductOfSums -> String)
-> ([ProductOfSums] -> ShowS)
-> Show ProductOfSums
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProductOfSums] -> ShowS
$cshowList :: [ProductOfSums] -> ShowS
show :: ProductOfSums -> String
$cshow :: ProductOfSums -> String
showsPrec :: Int -> ProductOfSums -> ShowS
$cshowsPrec :: Int -> ProductOfSums -> ShowS
Show)

instance Arbitrary ProductOfSums where
  arbitrary :: Gen ProductOfSums
arbitrary = [Sum] -> ProductOfSums
ProductOfSums ([Sum] -> ProductOfSums) -> Gen [Sum] -> Gen ProductOfSums
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen [Sum]
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: ProductOfSums -> [ProductOfSums]
shrink (ProductOfSums [Sum]
sop) = [Sum] -> ProductOfSums
ProductOfSums ([Sum] -> ProductOfSums) -> [[Sum]] -> [ProductOfSums]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sum] -> [[Sum]]
forall a. Arbitrary a => a -> [a]
shrink [Sum]
sop

instance Binary ProductOfSums where
  get :: Get ProductOfSums
get = [Sum] -> ProductOfSums
ProductOfSums ([Sum] -> ProductOfSums) -> Get [Sum] -> Get ProductOfSums
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get [Sum]
forall t. Binary t => Get t
get
  put :: ProductOfSums -> Put
put (ProductOfSums [Sum]
ps) = [Sum] -> Put
forall t. Binary t => [t] -> Put
putList [Sum]
ps

instance EvaluateItem ProductOfSums where
  evaluateItem :: (Int -> Bool) -> ProductOfSums -> Bool
evaluateItem Int -> Bool
f ~(ProductOfSums [Sum]
p) = (Sum -> Bool) -> [Sum] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Int -> Bool) -> Sum -> Bool
forall a. EvaluateItem a => (Int -> Bool) -> a -> Bool
evaluateItem Int -> Bool
f) [Sum]
p
  isTrivial :: ProductOfSums -> ThreeValue
isTrivial (ProductOfSums []) = ThreeValue
One
  isTrivial (ProductOfSums [Sum]
pos)
    | Leaf Bool
False <- Three Bool -> Three Bool
forall a. Simplify a => a -> a
simplify (Bool -> Three Bool -> [Sum'] -> Three Bool
forall a. a -> Three a -> [Sum'] -> Three a
wipeAll Bool
False (Bool -> Three Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) ((Sum -> Sum') -> [Sum] -> [Sum']
forall a b. (a -> b) -> [a] -> [b]
map Sum -> Sum'
go [Sum]
pos)) = ThreeValue
Zero
    | Bool
otherwise = ThreeValue
DontCare
    where go :: Sum -> Sum'
go ~(Sum Sum'
s) = Sum' -> Sum'
forall a. Opposite a => a -> a
opposite Sum'
s
  numberOfVariables :: ProductOfSums -> Int
numberOfVariables (ProductOfSums [Sum]
pos) = CompactSum' -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> CompactSum' -> CompactSum'
forall a. a -> [a] -> [a]
: (Sum -> Int) -> [Sum] -> CompactSum'
forall a b. (a -> b) -> [a] -> [b]
map Sum -> Int
forall a. EvaluateItem a => a -> Int
numberOfVariables [Sum]
pos)

instance Hashable ProductOfSums

instance NFData ProductOfSums

instance Semigroup ProductOfSums where
  ProductOfSums [Sum]
posa <> :: ProductOfSums -> ProductOfSums -> ProductOfSums
<> ProductOfSums [Sum]
posb = [Sum] -> ProductOfSums
ProductOfSums ([Sum]
posa [Sum] -> [Sum] -> [Sum]
forall a. Semigroup a => a -> a -> a
<> [Sum]
posb)

instance Monoid ProductOfSums where
  mempty :: ProductOfSums
mempty = [Sum] -> ProductOfSums
ProductOfSums []

instance ToCompact Sum CompactSum where
  toCompact :: Sum -> CompactSum
toCompact (Sum Sum'
s) = CompactSum' -> CompactSum
CompactSum (Sum' -> CompactSum'
forall a b. ToCompact a b => a -> b
toCompact Sum'
s)
  fromCompact :: CompactSum -> Sum
fromCompact (CompactSum CompactSum'
s) = Sum' -> Sum
Sum (CompactSum' -> Sum'
forall a b. ToCompact a b => b -> a
fromCompact CompactSum'
s)

-- | Convert the given product of sums to a 'Text' object that presents
-- the 'ProductOfSums'' as a 'Text' object with variables as subscript.
--
-- >>> showProductOfSums 'x' [[One, One], [DontCare, Zero, One]]
-- "(x₀x₁)(x₁'x₂)"
showProductOfSums
  :: Char  -- ^ The name of the root variable that will be used with subscripts.
  -> ProductOfSums' -- ^ The given sum of products to convert to a 'Text'.
  -> Text -- ^ The corresponding 'Text' object that presents the given 'ProductOfSums''.
showProductOfSums :: Char -> [Sum'] -> Text
showProductOfSums = (Int -> Text) -> [Sum'] -> Text
showProductOfSums' ((Int -> Text) -> [Sum'] -> Text)
-> (Char -> Int -> Text) -> Char -> [Sum'] -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int -> Text
subscriptVariable

-- | Convert the given product of sums to a 'Text' object that presents
-- the 'ProductOfSums'' as a 'Text' object with variables as subscript.
--
-- >>> showProductOfSums' (subscriptVariable 'y') [[One, One], [DontCare, Zero, One]]
-- "(y₀ + y₁)(y₁ + 'y₂)"
showProductOfSums'
  :: (Int -> Text) -- ^ A function that maps the given index to the variable name.
  -> ProductOfSums' -- ^ The given sum of products to convert to a 'Text'.
  -> Text -- ^ The corresponding 'Text' object that presents the given 'Dep.ProductOfSums''.
showProductOfSums' :: (Int -> Text) -> [Sum'] -> Text
showProductOfSums' Int -> Text
_ [] = Text
forall a. Monoid a => a
mempty
showProductOfSums' Int -> Text
f (Sum'
x:[Sum']
xs) = Sum' -> [Sum'] -> Text
go Sum'
x [Sum']
xs
  where go :: Sum' -> [Sum'] -> Text
go Sum'
z [] = Text -> Sum' -> Text
go' Text
forall a. Monoid a => a
mempty Sum'
z
        go Sum'
z ~(Sum'
y:[Sum']
ys) = Text -> Sum' -> Text
go' (Text
" + " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Sum' -> [Sum'] -> Text
go Sum'
y [Sum']
ys) Sum'
z
        go' :: Text -> Sum' -> Text
go' = (Int -> Text) -> Text -> Sum' -> Text
showSum'' Int -> Text
f

-- | Print a given sum as a sequence of variables that can be negated.
-- for example:
--
-- >>> showSum 'x' [One, DontCare, Zero, One]
-- "x₀ + x₂' + x₃"
showSum
  :: Char  -- ^ The name of the root variable that will be used with subscripts.
  -> Sum' -- ^ The given sum to convert to a 'Text'.
  -> Text -- ^ The corresponding 'Text' object that presents the given 'Dep.Data.Product.Product''.
showSum :: Char -> Sum' -> Text
showSum = (Char -> Text -> Sum' -> Text
`showSum'` Text
forall a. Monoid a => a
mempty)

-- | Print a given sum as a sequence of variables that can be negated.
-- for example:
--
-- >>> showSum' 'x' mempty [One, DontCare, Zero, One]
-- "x₀ + x₂' + x₃"
showSum'
  :: Char  -- ^ The name of the root variable that will be used with subscripts.
  -> Text  -- ^ The text that will be added as tail, this is useful if we combine Sums.
  -> Sum' -- ^ The given sum to convert to a 'Text'.
  -> Text -- ^ The corresponding 'Text' object that presents the given 'Sum''.
showSum' :: Char -> Text -> Sum' -> Text
showSum' = (Int -> Text) -> Text -> Sum' -> Text
showSum'' ((Int -> Text) -> Text -> Sum' -> Text)
-> (Char -> Int -> Text) -> Char -> Text -> Sum' -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int -> Text
subscriptVariable

-- | Print a given sum as a sequence of variables that can be negated.
-- for example:
--
-- >>> showSum' (subscriptVariable 'y') mempty [One, DontCare, Zero, One]
-- "y₀ + y₂' + y₃"
showSum''
  :: (Int -> Text) -- ^ A function that maps the given index to the variable name.
  -> Text  -- ^ The text that will be added as tail, this is useful if we combine sums.
  -> Sum' -- ^ The given sum to convert to a 'Text'.
  -> Text -- ^ The corresponding 'Text' object that presents the given 'Sum''.
showSum'' :: (Int -> Text) -> Text -> Sum' -> Text
showSum'' Int -> Text
ci Text
tl = Int -> Sum' -> Text
go (Int
0 :: Int)
    where go :: Int -> Sum' -> Text
go Int
_ [] = Text
tl
          go Int
n (ThreeValue
DontCare:Sum'
xs) = Int -> Sum' -> Text
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Sum'
xs
          go Int
n (ThreeValue
One:Sum'
xs) = (Text -> Text) -> Int -> Sum' -> Text
_printvar Text -> Text
forall a. a -> a
id Int
n Sum'
xs
          go Int
n ~(ThreeValue
Zero:Sum'
xs) = (Text -> Text) -> Int -> Sum' -> Text
_printvar (Char -> Text -> Text
cons Char
'\'') Int
n Sum'
xs
          _printvar :: (Text -> Text) -> Int -> Sum' -> Text
_printvar Text -> Text
f Int
n Sum'
xs = Int -> Text
ci Int
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
f (Int -> Sum' -> Text
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Sum'
xs)