{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE Rank2Types #-}
{-# OPTIONS_HADDOCK not-home #-}
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 ==>
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
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
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
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))
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
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [()]
unknowns = forall a. a -> Maybe a
Just Bool
True
| Bool
otherwise = forall a. Maybe a
Nothing
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 :: 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
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)
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
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)
class Boolean b where
bool :: Bool -> b
true :: b
true = forall b. Boolean b => Bool -> b
bool Bool
True
false :: b
false = forall b. Boolean b => Bool -> b
bool Bool
False
(&&) :: b -> b -> b
(||) :: b -> b -> b
(==>) :: 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
not :: b -> b
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
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
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
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
all :: Foldable t => (a -> b) -> t a -> b
any :: Foldable t => (a -> b) -> t a -> b
xor :: b -> b -> b
choose :: b
-> b
-> b
-> 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)