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

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

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

module Dep.Data.Product (
    -- * Type synonyms to represent synthesis
    Product(Product), Product', CompactProduct(CompactProduct), CompactProduct', SumOfProducts(SumOfProducts), SumOfProducts'
    -- * Print products and sums-of-products
  , showSumOfProducts, showProduct, showProduct', subscriptVariable
  ) where

import Control.DeepSeq(NFData)

import Data.Binary(Binary(get, put), putList)
import Data.Bool(bool)
import Data.Data(Data)
import Data.Hashable(Hashable)
import Data.Text(Text, cons)

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 GHC.Generics(Generic)

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

-- | A type alias for a product that is a 'ThreePath'.
type Product' = ThreePath

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

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

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

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

instance Hashable Product

instance NFData Product

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

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

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

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

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

instance EvaluateItem CompactProduct where
  evaluateItem :: (Int -> Bool) -> CompactProduct -> Bool
evaluateItem Int -> Bool
f ~(CompactProduct CompactProduct'
p) = (Int -> Bool) -> CompactProduct' -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Int -> Bool
go CompactProduct'
p
    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 :: CompactProduct -> ThreeValue
isTrivial (CompactProduct CompactProduct'
cp) = ThreeValue -> ThreeValue -> Bool -> ThreeValue
forall a. a -> a -> Bool -> a
bool ThreeValue
DontCare ThreeValue
One ((Int -> Bool) -> CompactProduct' -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int
0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) CompactProduct'
cp)
  numberOfVariables :: CompactProduct -> Int
numberOfVariables (CompactProduct CompactProduct'
cp) = CompactProduct' -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> CompactProduct' -> CompactProduct'
forall a. a -> [a] -> [a]
: (Int -> Int) -> CompactProduct' -> CompactProduct'
forall a b. (a -> b) -> [a] -> [b]
map Int -> Int
forall a. Num a => a -> a
abs CompactProduct'
cp)

instance Hashable CompactProduct

instance NFData CompactProduct

-- | A type synonym to present a sum of products where each item of the list is a 'Product''.
type SumOfProducts' = [Product']

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

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

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

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

instance Hashable SumOfProducts

instance NFData SumOfProducts

instance Semigroup SumOfProducts where
  SumOfProducts [Product]
sopa <> :: SumOfProducts -> SumOfProducts -> SumOfProducts
<> SumOfProducts [Product]
sopb = [Product] -> SumOfProducts
SumOfProducts ([Product]
sopa [Product] -> [Product] -> [Product]
forall a. Semigroup a => a -> a -> a
<> [Product]
sopb)

instance Monoid SumOfProducts where
  mempty :: SumOfProducts
mempty = [Product] -> SumOfProducts
SumOfProducts []

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

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

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

-- | Print a given product as a sequence of variables that can be negated.
-- for example:
--
-- >>> showProduct' 'x' mempty [One, DontCare, Zero, One]
-- "x₀x₂'x₃"
showProduct'
  :: 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 products.
  -> Product' -- ^ The given product to convert to a 'Text'.
  -> Text -- ^ The corresponding 'Text' object that presents the given 'Product''.
showProduct' :: Char -> Text -> Product' -> Text
showProduct' = (Int -> Text) -> Text -> Product' -> Text
showProduct'' ((Int -> Text) -> Text -> Product' -> Text)
-> (Char -> Int -> Text) -> Char -> Text -> Product' -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int -> Text
subscriptVariable

-- | Print a given product as a sequence of variables that can be negated.
-- for example:
--
-- >>> showProduct' (subscriptVariable 'y') mempty [One, DontCare, Zero, One]
-- "y₀y₂'y₃"
showProduct''
  :: (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 products.
  -> Product' -- ^ The given product to convert to a 'Text'.
  -> Text -- ^ The corresponding 'Text' object that presents the given 'Product''.
showProduct'' :: (Int -> Text) -> Text -> Product' -> Text
showProduct'' Int -> Text
ci Text
tl = Int -> Product' -> Text
go (Int
0 :: Int)
    where go :: Int -> Product' -> Text
go Int
_ [] = Text
tl
          go Int
n (ThreeValue
DontCare:Product'
xs) = Int -> Product' -> Text
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Product'
xs
          go Int
n (ThreeValue
One:Product'
xs) = (Text -> Text) -> Int -> Product' -> Text
_printvar Text -> Text
forall a. a -> a
id Int
n Product'
xs
          go Int
n ~(ThreeValue
Zero:Product'
xs) = (Text -> Text) -> Int -> Product' -> Text
_printvar (Char -> Text -> Text
cons Char
'\'') Int
n Product'
xs
          _printvar :: (Text -> Text) -> Int -> Product' -> Text
_printvar Text -> Text
f Int
n Product'
xs = Int -> Text
ci Int
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
f (Int -> Product' -> Text
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Product'
xs)