{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE Rank2Types #-}
{-# OPTIONS_HADDOCK not-home #-}
--------------------------------------------------------------------
-- |
-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Ersatz.Bit
  ( Bit(..)
  , assert
  , Boolean(..)
  ) where

import Prelude hiding ((&&),(||),not,and,or,all,any)
import qualified Prelude

import Control.Applicative
import Control.Monad (MonadPlus(..), liftM2, liftM3)
import Data.Foldable (toList)
import qualified Data.Foldable as Foldable
import qualified Data.Traversable as Traversable
import Data.Sequence (Seq, (<|), (|>), (><))
import qualified Data.Sequence as Seq
import Ersatz.Codec
import Ersatz.Internal.Formula
import Ersatz.Internal.Literal
import Ersatz.Internal.StableName
import Ersatz.Problem
import Ersatz.Solution
import Ersatz.Variable
import GHC.Generics
import System.IO.Unsafe

infixr 3 &&, &&#
infixr 2 ||, ||#
infixr 0 ==>

-- Bit

-- | A 'Bit' provides a reference to a possibly indeterminate boolean
-- value that can be determined by an external SAT solver.
data Bit
  = And !(Seq Bit)
  | Xor !Bit !Bit
  | Mux !Bit !Bit !Bit
  | Not !Bit
  | Var !Literal
  | Run ( forall m s . MonadSAT s m => m Bit )

instance Show Bit where
  showsPrec :: Int -> Bit -> ShowS
showsPrec Int
d (And Seq Bit
xs)  = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"And " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Seq Bit
xs
  showsPrec Int
d (Xor Bit
x Bit
y) = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"Xor " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
y
  showsPrec Int
d (Mux Bit
x Bit
y Bit
z) = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"Mux " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
y forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
z
  showsPrec Int
d (Not Bit
x)  = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Not " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
x
  showsPrec Int
d (Var Literal
x)  = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Var " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Literal
x
  showsPrec Int
d (Run forall (m :: * -> *) s. MonadSAT s m => m Bit
_)  = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Run ..."

instance Boolean Bit where
  -- improve the stablemap this way
  bool :: Bool -> Bit
bool Bool
True  = forall b. Boolean b => b
true
  bool Bool
False = forall b. Boolean b => b
false
  true :: Bit
true  = Literal -> Bit
Var Literal
literalTrue
  false :: Bit
false = Literal -> Bit
Var Literal
literalFalse

  && :: Bit -> Bit -> Bit
(&&) = Bit -> Bit -> Bit
and2
  Bit
a || :: Bit -> Bit -> Bit
|| Bit
b = forall b. Boolean b => b -> b
not (forall b. Boolean b => b -> b
not Bit
a forall b. Boolean b => b -> b -> b
&& forall b. Boolean b => b -> b
not Bit
b)

  not :: Bit -> Bit
not (Not Bit
c) = Bit
c
  not (Var Literal
l) = Literal -> Bit
Var (Literal -> Literal
negateLiteral Literal
l)
  not Bit
c       = Bit -> Bit
Not Bit
c

  Bit
a xor :: Bit -> Bit -> Bit
`xor` Var (Literal (-1)) = Bit
a
  Var (Literal (-1)) `xor` Bit
b = Bit
b
  Bit
a `xor` Var (Literal Int
1) = forall b. Boolean b => b -> b
not Bit
a
  Var (Literal Int
1) `xor` Bit
b = forall b. Boolean b => b -> b
not Bit
b
  -- following 3 clauses might enable some AIG magic
  Not Bit
a `xor` Not Bit
b = Bit -> Bit -> Bit
Xor Bit
a Bit
b
  Bit
a `xor` Not Bit
b = Bit -> Bit
Not (Bit -> Bit -> Bit
Xor Bit
a Bit
b)
  Not Bit
a `xor` Bit
b = Bit -> Bit
Not (Bit -> Bit -> Bit
Xor Bit
a Bit
b)
  Bit
a `xor` Bit
b    = Bit -> Bit -> Bit
Xor Bit
a Bit
b

  and :: forall (t :: * -> *). Foldable t => t Bit -> Bit
and = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Foldable.foldl' forall b. Boolean b => b -> b -> b
(&&) forall b. Boolean b => b
true
  or :: forall (t :: * -> *). Foldable t => t Bit -> Bit
or  = forall b. Boolean b => b -> b
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
all forall b. Boolean b => b -> b
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

  all :: forall (t :: * -> *) a. Foldable t => (a -> Bit) -> t a -> Bit
all a -> Bit
p = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Foldable.foldl' (\Bit
res a
b -> Bit
res forall b. Boolean b => b -> b -> b
&& a -> Bit
p a
b) forall b. Boolean b => b
true
  any :: forall (t :: * -> *) a. Foldable t => (a -> Bit) -> t a -> Bit
any a -> Bit
p = forall b. Boolean b => b -> b
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
all (forall b. Boolean b => b -> b
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bit
p)

  choose :: Bit -> Bit -> Bit -> Bit
choose Bit
f Bit
_ (Var (Literal (-1))) = Bit
f
  choose Bit
_ Bit
t (Var (Literal Int
1))    = Bit
t
  choose Bit
t Bit
f (Not Bit
s) = forall b. Boolean b => b -> b -> b -> b
choose Bit
f Bit
t Bit
s
  choose Bit
f Bit
t Bit
s = Bit -> Bit -> Bit -> Bit
Mux Bit
f Bit
t Bit
s

and2 :: Bit -> Bit -> Bit
and2 :: Bit -> Bit -> Bit
and2 a :: Bit
a@(Var (Literal (-1))) Bit
_ = Bit
a
and2 Bit
_ b :: Bit
b@(Var (Literal (-1))) = Bit
b
and2 Bit
a (Var (Literal Int
1)) = Bit
a
and2 (Var (Literal Int
1)) Bit
b = Bit
b
and2 (And Seq Bit
as) (And Seq Bit
bs) = Seq Bit -> Bit
And (Seq Bit
as forall a. Seq a -> Seq a -> Seq a
>< Seq Bit
bs)
and2 (And Seq Bit
as) Bit
b      = Seq Bit -> Bit
And (Seq Bit
as forall a. Seq a -> a -> Seq a
|> Bit
b)
and2 Bit
a (And Seq Bit
bs) = Seq Bit -> Bit
And (Bit
a forall a. a -> Seq a -> Seq a
<| Seq Bit
bs)
and2 Bit
a Bit
b = Seq Bit -> Bit
And (Bit
a forall a. a -> Seq a -> Seq a
<| Bit
b forall a. a -> Seq a -> Seq a
<| forall a. Seq a
Seq.empty)

instance Variable Bit where
  literally :: forall s (m :: * -> *). MonadSAT s m => m Literal -> m Bit
literally = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Literal -> Bit
Var forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (m :: * -> *).
(Variable t, MonadSAT s m) =>
m Literal -> m t
literally

-- a Bit you don't assert is actually a boolean function that you can evaluate later after compilation
instance Codec Bit where
  type Decoded Bit = Bool
  encode :: Decoded Bit -> Bit
encode = forall b. Boolean b => Bool -> b
bool
  decode :: forall (f :: * -> *).
MonadPlus f =>
Solution -> Bit -> f (Decoded Bit)
decode Solution
sol Bit
b
      = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        Solution -> StableName () -> Maybe Bool
solutionStableName Solution
sol (forall a. IO a -> a
unsafePerformIO (forall a. a -> IO (StableName ())
makeStableName' Bit
b))
     -- The StableName didn’t have an associated literal with a solution,
     -- recurse to compute the value.
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> case Bit
b of
          And Seq Bit
cs  -> [Maybe Bool] -> Maybe Bool
andMaybeBools forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq Bit
cs
          Xor Bit
x Bit
y -> forall b. Boolean b => b -> b -> b
xor forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol Bit
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol Bit
y
          Mux Bit
cf Bit
ct Bit
cp -> do
            Bool
p <- forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol Bit
cp
            forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol forall a b. (a -> b) -> a -> b
$ if Bool
p then Bit
ct else Bit
cf
          Not Bit
c'  -> forall b. Boolean b => b -> b
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol Bit
c'
          Var Literal
l   -> forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol Literal
l
          Run forall (m :: * -> *) s. MonadSAT s m => m Bit
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
    where
      andMaybeBools :: [Maybe Bool] -> Maybe Bool
      andMaybeBools :: [Maybe Bool] -> Maybe Bool
andMaybeBools [Maybe Bool]
mbs
        | forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
any forall b. Boolean b => b -> b
not [Bool]
knowns = forall a. a -> Maybe a
Just Bool
False  -- One is known to be false.
        | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [()]
unknowns  = forall a. a -> Maybe a
Just Bool
True   -- All are known to be true.
        | Bool
otherwise      = forall a. Maybe a
Nothing     -- Unknown.
        where
          ([()]
unknowns, [Bool]
knowns) = forall a. [Maybe a] -> ([()], [a])
partitionMaybes [Maybe Bool]
mbs

      partitionMaybes :: [Maybe a] -> ([()], [a])
      partitionMaybes :: forall a. [Maybe a] -> ([()], [a])
partitionMaybes = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {a}. Maybe a -> ([()], [a]) -> ([()], [a])
go ([],[])
        where
          go :: Maybe a -> ([()], [a]) -> ([()], [a])
go Maybe a
Nothing  ~([()]
ns, [a]
js) = (()forall a. a -> [a] -> [a]
:[()]
ns, [a]
js)
          go (Just a
a) ~([()]
ns, [a]
js) = ([()]
ns,    a
aforall a. a -> [a] -> [a]
:[a]
js)

-- | Assert claims that 'Bit' must be 'true' in any satisfying interpretation
-- of the current problem.
assert :: MonadSAT s m => Bit -> m ()
assert :: forall s (m :: * -> *). MonadSAT s m => Bit -> m ()
assert (And Seq Bit
bs) = forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
Foldable.for_ Seq Bit
bs forall s (m :: * -> *). MonadSAT s m => Bit -> m ()
assert
-- the following (when switched on) produces extra clauses, why?
assert (Not (And Seq Bit
bs)) | () forall a. Eq a => a -> a -> Bool
/= () = do
  Seq Literal
ls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
Traversable.for Seq Bit
bs forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit
  forall s (m :: * -> *). MonadSAT s m => Formula -> m ()
assertFormula forall a b. (a -> b) -> a -> b
$ Clause -> Formula
fromClause forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Literal -> Clause
fromLiteral forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Literal
negateLiteral) Seq Literal
ls
assert Bit
b = do
  Literal
l <- forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
b
  forall s (m :: * -> *). MonadSAT s m => Formula -> m ()
assertFormula (Literal -> Formula
formulaLiteral Literal
l)

-- | Convert a 'Bit' to a 'Literal'.
runBit :: MonadSAT s m => Bit -> m Literal
runBit :: forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit (Not Bit
c) = Literal -> Literal
negateLiteral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
c
runBit (Var Literal
l) = forall (m :: * -> *) a. Monad m => a -> m a
return Literal
l
runBit (Run forall (m :: * -> *) s. MonadSAT s m => m Bit
action) = forall (m :: * -> *) s. MonadSAT s m => m Bit
action forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit
runBit Bit
b = forall s (m :: * -> *) a.
MonadSAT s m =>
a -> (Literal -> m ()) -> m Literal
generateLiteral Bit
b forall a b. (a -> b) -> a -> b
$ \Literal
out ->
  forall s (m :: * -> *). MonadSAT s m => Formula -> m ()
assertFormula forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< case Bit
b of
    And Seq Bit
bs    -> Literal -> [Literal] -> Formula
formulaAnd Literal
out forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Bit
bs)
    Xor Bit
x Bit
y   -> forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Literal -> Literal -> Literal -> Formula
formulaXor Literal
out) (forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
x) (forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
y)
    Mux Bit
x Bit
y Bit
p -> forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (Literal -> Literal -> Literal -> Literal -> Formula
formulaMux Literal
out) (forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
x) (forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
y) (forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
p)

#if __GLASGOW_HASKELL__ < 900
    -- Already handled above, but pre-9.0 GHCs don't realize this.
    Not _ -> error "Unreachable"
    Var _ -> error "Unreachable"
    Run _ -> error "Unreachable"
#endif

class GBoolean f where
  gbool :: Bool -> f a
  (&&#) :: f a -> f a -> f a
  (||#) :: f a -> f a -> f a
  gnot :: f a -> f a
  gall :: Foldable t => (a -> f b) -> t a -> f b
  gany :: Foldable t => (a -> f b) -> t a -> f b
  gxor :: f a -> f a -> f a

instance GBoolean V1 where
  gbool :: forall a. Bool -> V1 a
gbool Bool
x    = Bool
x seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => String -> a
error String
"GBoolean[V1].gbool"
  V1 a
x &&# :: forall a. V1 a -> V1 a -> V1 a
&&# V1 a
y    = V1 a
x seq :: forall a b. a -> b -> b
`seq` V1 a
y seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => String -> a
error String
"GBoolean[V1].&&#"
  V1 a
x ||# :: forall a. V1 a -> V1 a -> V1 a
||# V1 a
y    = V1 a
x seq :: forall a b. a -> b -> b
`seq` V1 a
y seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => String -> a
error String
"GBoolean[V1].||#"
  gnot :: forall a. V1 a -> V1 a
gnot V1 a
x     = V1 a
x seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => String -> a
error String
"GBoolean[V1].gnot"
  gall :: forall (t :: * -> *) a b. Foldable t => (a -> V1 b) -> t a -> V1 b
gall a -> V1 b
x t a
y   = a -> V1 b
x seq :: forall a b. a -> b -> b
`seq` t a
y seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => String -> a
error String
"GBoolean[V1].gall"
  gany :: forall (t :: * -> *) a b. Foldable t => (a -> V1 b) -> t a -> V1 b
gany a -> V1 b
x t a
y   = a -> V1 b
x seq :: forall a b. a -> b -> b
`seq` t a
y seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => String -> a
error String
"GBoolean[V1].gany"
  gxor :: forall a. V1 a -> V1 a -> V1 a
gxor V1 a
x V1 a
y   = V1 a
x seq :: forall a b. a -> b -> b
`seq` V1 a
y seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => String -> a
error String
"GBoolean[V1].gxor"

instance GBoolean U1 where
  gbool :: forall a. Bool -> U1 a
gbool Bool
_    = forall k (p :: k). U1 p
U1
  U1 a
U1 &&# :: forall a. U1 a -> U1 a -> U1 a
&&# U1 a
U1  = forall k (p :: k). U1 p
U1
  U1 a
U1 ||# :: forall a. U1 a -> U1 a -> U1 a
||# U1 a
U1  = forall k (p :: k). U1 p
U1
  gnot :: forall a. U1 a -> U1 a
gnot U1 a
U1    = forall k (p :: k). U1 p
U1
  gall :: forall (t :: * -> *) a b. Foldable t => (a -> U1 b) -> t a -> U1 b
gall a -> U1 b
_ t a
_   = forall k (p :: k). U1 p
U1
  gany :: forall (t :: * -> *) a b. Foldable t => (a -> U1 b) -> t a -> U1 b
gany a -> U1 b
_ t a
_   = forall k (p :: k). U1 p
U1
  gxor :: forall a. U1 a -> U1 a -> U1 a
gxor U1 a
_ U1 a
_   = forall k (p :: k). U1 p
U1

instance (GBoolean f, GBoolean g) => GBoolean (f :*: g) where
  gbool :: forall a. Bool -> (:*:) f g a
gbool Bool
x = forall (f :: * -> *) a. GBoolean f => Bool -> f a
gbool Bool
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (f :: * -> *) a. GBoolean f => Bool -> f a
gbool Bool
x
  (f a
a :*: g a
b) &&# :: forall a. (:*:) f g a -> (:*:) f g a -> (:*:) f g a
&&#  (f a
c :*: g a
d) = (f a
a forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
&&# f a
c)  forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (g a
b forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
&&# g a
d)
  (f a
a :*: g a
b) ||# :: forall a. (:*:) f g a -> (:*:) f g a -> (:*:) f g a
||#  (f a
c :*: g a
d) = (f a
a forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
||# f a
c)  forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (g a
b forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
||# g a
d)
  gnot :: forall a. (:*:) f g a -> (:*:) f g a
gnot (f a
a :*: g a
b) = forall (f :: * -> *) a. GBoolean f => f a -> f a
gnot f a
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (f :: * -> *) a. GBoolean f => f a -> f a
gnot g a
b
  gall :: forall (t :: * -> *) a b.
Foldable t =>
(a -> (:*:) f g b) -> t a -> (:*:) f g b
gall a -> (:*:) f g b
p t a
xs = forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gall forall a. a -> a
id [f b]
ls forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gall forall a. a -> a
id [g b]
rs
    where ([f b]
ls, [g b]
rs) = forall (f :: * -> *) (g :: * -> *) a.
[(:*:) f g a] -> ([f a], [g a])
gunzip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map a -> (:*:) f g b
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ t a
xs
  gany :: forall (t :: * -> *) a b.
Foldable t =>
(a -> (:*:) f g b) -> t a -> (:*:) f g b
gany a -> (:*:) f g b
p t a
xs = forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gany forall a. a -> a
id [f b]
ls forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gany forall a. a -> a
id [g b]
rs
    where ([f b]
ls, [g b]
rs) = forall (f :: * -> *) (g :: * -> *) a.
[(:*:) f g a] -> ([f a], [g a])
gunzip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map a -> (:*:) f g b
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ t a
xs
  gxor :: forall a. (:*:) f g a -> (:*:) f g a -> (:*:) f g a
gxor (f a
a :*: g a
b) (f a
c :*: g a
d) = forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
gxor f a
a f a
c forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
gxor g a
b g a
d

instance Boolean a => GBoolean (K1 i a) where
  gbool :: forall a. Bool -> K1 i a a
gbool = forall k i c (p :: k). c -> K1 i c p
K1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. Boolean b => Bool -> b
bool
  K1 a
a &&# :: forall a. K1 i a a -> K1 i a a -> K1 i a a
&&# K1 a
b = forall k i c (p :: k). c -> K1 i c p
K1 (a
a forall b. Boolean b => b -> b -> b
&& a
b)
  K1 a
a ||# :: forall a. K1 i a a -> K1 i a a -> K1 i a a
||# K1 a
b = forall k i c (p :: k). c -> K1 i c p
K1 (a
a forall b. Boolean b => b -> b -> b
|| a
b)
  gnot :: forall a. K1 i a a -> K1 i a a
gnot (K1 a
a) = forall k i c (p :: k). c -> K1 i c p
K1 (forall b. Boolean b => b -> b
not a
a)
  gall :: forall (t :: * -> *) a b.
Foldable t =>
(a -> K1 i a b) -> t a -> K1 i a b
gall a -> K1 i a b
p t a
as = forall k i c (p :: k). c -> K1 i c p
K1 (forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
all (forall k i c (p :: k). K1 i c p -> c
unK1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> K1 i a b
p) t a
as)
  gany :: forall (t :: * -> *) a b.
Foldable t =>
(a -> K1 i a b) -> t a -> K1 i a b
gany a -> K1 i a b
p t a
as = forall k i c (p :: k). c -> K1 i c p
K1 (forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
any (forall k i c (p :: k). K1 i c p -> c
unK1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> K1 i a b
p) t a
as)
  gxor :: forall a. K1 i a a -> K1 i a a -> K1 i a a
gxor (K1 a
a) (K1 a
b) = forall k i c (p :: k). c -> K1 i c p
K1 (forall b. Boolean b => b -> b -> b
xor a
a a
b)

instance GBoolean a => GBoolean (M1 i c a) where
  gbool :: forall a. Bool -> M1 i c a a
gbool = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. GBoolean f => Bool -> f a
gbool
  M1 a a
a &&# :: forall a. M1 i c a a -> M1 i c a a -> M1 i c a a
&&# M1 a a
b = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a
a forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
&&# a a
b)
  M1 a a
a ||# :: forall a. M1 i c a a -> M1 i c a a -> M1 i c a a
||# M1 a a
b = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a
a forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
||# a a
b)
  gnot :: forall a. M1 i c a a -> M1 i c a a
gnot (M1 a a
a) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (f :: * -> *) a. GBoolean f => f a -> f a
gnot a a
a)
  gall :: forall (t :: * -> *) a b.
Foldable t =>
(a -> M1 i c a b) -> t a -> M1 i c a b
gall a -> M1 i c a b
p t a
as = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gall (forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> M1 i c a b
p) t a
as)
  gany :: forall (t :: * -> *) a b.
Foldable t =>
(a -> M1 i c a b) -> t a -> M1 i c a b
gany a -> M1 i c a b
p t a
as = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gany (forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> M1 i c a b
p) t a
as)
  gxor :: forall a. M1 i c a a -> M1 i c a a -> M1 i c a a
gxor (M1 a a
a) (M1 a a
b) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
gxor a a
a a a
b)

-- | The normal 'Bool' operators in Haskell are not overloaded. This
-- provides a richer set that are.
--
-- Instances for this class for product-like types can be automatically derived
-- for any type that is an instance of 'Generic'
class Boolean b where
  -- | Lift a 'Bool'
  bool :: Bool -> b
  -- |
  -- @'true' = 'bool' 'True'@
  true :: b
  true = forall b. Boolean b => Bool -> b
bool Bool
True
  -- |
  -- @'false' = 'bool' 'False'@
  false :: b
  false = forall b. Boolean b => Bool -> b
bool Bool
False

  -- | Logical conjunction.
  (&&) :: b -> b -> b

  -- | Logical disjunction (inclusive or).
  (||) :: b -> b -> b

  -- | Logical implication.
  (==>) :: b -> b -> b
  b
x ==> b
y = forall b. Boolean b => b -> b
not b
x forall b. Boolean b => b -> b -> b
|| b
y

  -- | Logical negation
  not :: b -> b

  -- | The logical conjunction of several values.
  and :: Foldable t => t b -> b
  and = forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
Ersatz.Bit.all forall a. a -> a
id  -- qualified for HLint

  -- | The logical disjunction of several values.
  or :: Foldable t => t b -> b
  or = forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
Ersatz.Bit.any forall a. a -> a
id  -- qualified for HLint

  -- | The negated logical conjunction of several values.
  --
  -- @'nand' = 'not' . 'and'@
  nand :: Foldable t => t b -> b
  nand = forall b. Boolean b => b -> b
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and

  -- | The negated logical disjunction of several values.
  --
  -- @'nor' = 'not' . 'or'@
  nor :: Foldable t => t b -> b
  nor = forall b. Boolean b => b -> b
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
or

  -- | The logical conjunction of the mapping of a function over several values.
  all :: Foldable t => (a -> b) -> t a -> b

  -- | The logical disjunction of the mapping of a function over several values.
  any :: Foldable t => (a -> b) -> t a -> b

  -- | Exclusive-or
  xor :: b -> b -> b

  -- | Choose between two alternatives based on a selector bit.
  choose :: b  -- ^ False branch
         -> b  -- ^ True branch
         -> b  -- ^ Predicate/selector branch
         -> b
  choose b
f b
t b
s = (b
f forall b. Boolean b => b -> b -> b
&& forall b. Boolean b => b -> b
not b
s) forall b. Boolean b => b -> b -> b
|| (b
t forall b. Boolean b => b -> b -> b
&& b
s)

  default bool :: (Generic b, GBoolean (Rep b)) => Bool -> b
  bool = forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. GBoolean f => Bool -> f a
gbool

  default (&&) :: (Generic b, GBoolean (Rep b)) => b -> b -> b
  b
x && b
y = forall a x. Generic a => Rep a x -> a
to (forall a x. Generic a => a -> Rep a x
from b
x forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
&&# forall a x. Generic a => a -> Rep a x
from b
y)

  default (||) :: (Generic b, GBoolean (Rep b)) => b -> b -> b
  b
x || b
y = forall a x. Generic a => Rep a x -> a
to (forall a x. Generic a => a -> Rep a x
from b
x forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
||# forall a x. Generic a => a -> Rep a x
from b
y)

  default not :: (Generic b, GBoolean (Rep b)) => b -> b
  not = forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. GBoolean f => f a -> f a
gnot forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. Generic a => a -> Rep a x
from

  default all :: (Foldable t, Generic b, GBoolean (Rep b)) => (a -> b) -> t a -> b
  all a -> b
p = forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gall (forall a x. Generic a => a -> Rep a x
from forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
p)

  default any :: (Foldable t, Generic b, GBoolean (Rep b)) => (a -> b) -> t a -> b
  any a -> b
p = forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gany (forall a x. Generic a => a -> Rep a x
from forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
p)

  default xor :: (Generic b, GBoolean (Rep b)) => b -> b -> b
  xor b
x b
y = forall a x. Generic a => Rep a x -> a
to (forall a x. Generic a => a -> Rep a x
from b
x forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
`gxor` forall a x. Generic a => a -> Rep a x
from b
y)

instance Boolean Bool where
  bool :: Bool -> Bool
bool = forall a. a -> a
id
  true :: Bool
true = Bool
True
  false :: Bool
false = Bool
False

  && :: Bool -> Bool -> Bool
(&&) = Bool -> Bool -> Bool
(Prelude.&&)
  || :: Bool -> Bool -> Bool
(||) = Bool -> Bool -> Bool
(Prelude.||)

  not :: Bool -> Bool
not = Bool -> Bool
Prelude.not

  and :: forall (t :: * -> *). Foldable t => t Bool -> Bool
and = forall (t :: * -> *). Foldable t => t Bool -> Bool
Foldable.and
  or :: forall (t :: * -> *). Foldable t => t Bool -> Bool
or  = forall (t :: * -> *). Foldable t => t Bool -> Bool
Foldable.or

  all :: forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Foldable.all
  any :: forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Foldable.any

  xor :: Bool -> Bool -> Bool
xor = forall a. Eq a => a -> a -> Bool
(/=)

  choose :: Bool -> Bool -> Bool -> Bool
choose Bool
f Bool
_ Bool
False = Bool
f
  choose Bool
_ Bool
t Bool
True  = Bool
t

gunzip :: [(f :*: g) a] -> ([f a], [g a])
gunzip :: forall (f :: * -> *) (g :: * -> *) a.
[(:*:) f g a] -> ([f a], [g a])
gunzip = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {f :: * -> *} {g :: * -> *} {p}.
(:*:) f g p -> ([f p], [g p]) -> ([f p], [g p])
go ([],[])
  where go :: (:*:) f g p -> ([f p], [g p]) -> ([f p], [g p])
go (f p
a :*: g p
b) ~([f p]
as, [g p]
bs) = (f p
aforall a. a -> [a] -> [a]
:[f p]
as, g p
bforall a. a -> [a] -> [a]
:[g p]
bs)