{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# 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.State
#if __GLASGOW_HASKELL__ < 710
import Data.Foldable (Foldable, toList)
#else
import Data.Foldable (toList)
#endif
import qualified Data.Foldable as Foldable
import qualified Data.Traversable as Traversable
import Data.Sequence (Seq, (<|), (|>), (><))
import qualified Data.Sequence as Seq
import Data.Typeable
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 )
deriving (Typeable)
instance Show Bit where
showsPrec :: Int -> Bit -> ShowS
showsPrec Int
d (And Seq Bit
xs) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"And " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Seq Bit -> ShowS
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"Xor " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bit -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bit -> ShowS
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"Mux " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bit -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bit -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
y ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bit -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
z
showsPrec Int
d (Not Bit
x) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Not " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bit -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Bit
x
showsPrec Int
d (Var Literal
x) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Var " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Literal -> ShowS
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Run ..."
instance Boolean Bit where
bool :: Bool -> Bit
bool Bool
True = Bit
forall b. Boolean b => b
true
bool Bool
False = Bit
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 = Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit
forall b. Boolean b => b -> b
not Bit
a Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
&& Bit -> Bit
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) = Bit -> Bit
forall b. Boolean b => b -> b
not Bit
a
Var (Literal Int
1) `xor` Bit
b = Bit -> Bit
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 :: t Bit -> Bit
and = (Bit -> Bit -> Bit) -> Bit -> t Bit -> Bit
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Foldable.foldl' Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
(&&) Bit
forall b. Boolean b => b
true
or :: t Bit -> Bit
or = Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit) -> (t Bit -> Bit) -> t Bit -> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bit -> Bit) -> [Bit] -> Bit
forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
all Bit -> Bit
forall b. Boolean b => b -> b
not ([Bit] -> Bit) -> (t Bit -> [Bit]) -> t Bit -> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t Bit -> [Bit]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
all :: (a -> Bit) -> t a -> Bit
all a -> Bit
p = (Bit -> a -> Bit) -> Bit -> t a -> Bit
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Foldable.foldl' (\Bit
res a
b -> Bit
res Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
&& a -> Bit
p a
b) Bit
forall b. Boolean b => b
true
any :: (a -> Bit) -> t a -> Bit
any a -> Bit
p = Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit) -> (t a -> Bit) -> t a -> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Bit) -> t a -> Bit
forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
all (Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit) -> (a -> Bit) -> a -> Bit
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) = Bit -> Bit -> Bit -> Bit
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 Seq Bit -> Seq Bit -> Seq Bit
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 Seq Bit -> Bit -> Seq Bit
forall a. Seq a -> a -> Seq a
|> Bit
b)
and2 Bit
a (And Seq Bit
bs) = Seq Bit -> Bit
And (Bit
a Bit -> Seq Bit -> Seq Bit
forall a. a -> Seq a -> Seq a
<| Seq Bit
bs)
and2 Bit
a Bit
b = Seq Bit -> Bit
And (Bit
a Bit -> Seq Bit -> Seq Bit
forall a. a -> Seq a -> Seq a
<| Bit
b Bit -> Seq Bit -> Seq Bit
forall a. a -> Seq a -> Seq a
<| Seq Bit
forall a. Seq a
Seq.empty)
instance Variable Bit where
literally :: m Literal -> m Bit
literally = (Literal -> Bit) -> m Literal -> m Bit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Literal -> Bit
Var (m Literal -> m Bit)
-> (m Literal -> m Literal) -> m Literal -> m Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Literal -> m Literal
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 = Decoded Bit -> Bit
forall b. Boolean b => Bool -> b
bool
decode :: Solution -> Bit -> f (Decoded Bit)
decode Solution
sol Bit
b
= f Bool -> (Bool -> f Bool) -> Maybe Bool -> f Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> f Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False f Bool -> f Bool -> f Bool
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> f Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) Bool -> f Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Bool -> f Bool) -> Maybe Bool -> f Bool
forall a b. (a -> b) -> a -> b
$
Solution -> StableName () -> Maybe Bool
solutionStableName Solution
sol (IO (StableName ()) -> StableName ()
forall a. IO a -> a
unsafePerformIO (Bit -> IO (StableName ())
forall a. a -> IO (StableName ())
makeStableName' Bit
b))
Maybe Bool -> Maybe Bool -> Maybe Bool
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> case Bit
b of
And Seq Bit
cs -> [Maybe Bool] -> Maybe Bool
andMaybeBools ([Maybe Bool] -> Maybe Bool)
-> (Seq (Maybe Bool) -> [Maybe Bool])
-> Seq (Maybe Bool)
-> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (Maybe Bool) -> [Maybe Bool]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Seq (Maybe Bool) -> Maybe Bool) -> Seq (Maybe Bool) -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Solution -> Bit -> Maybe (Decoded Bit)
forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol (Bit -> Maybe Bool) -> Seq Bit -> Seq (Maybe Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq Bit
cs
Xor Bit
x Bit
y -> Bool -> Bool -> Bool
forall b. Boolean b => b -> b -> b
xor (Bool -> Bool -> Bool) -> Maybe Bool -> Maybe (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Bit -> Maybe (Decoded Bit)
forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol Bit
x Maybe (Bool -> Bool) -> Maybe Bool -> Maybe Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Bit -> Maybe (Decoded Bit)
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 <- Solution -> Bit -> Maybe (Decoded Bit)
forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol Bit
cp
Solution -> Bit -> Maybe (Decoded Bit)
forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol (Bit -> Maybe (Decoded Bit)) -> Bit -> Maybe (Decoded Bit)
forall a b. (a -> b) -> a -> b
$ if Bool
p then Bit
ct else Bit
cf
Not Bit
c' -> Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> Maybe Bool -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Bit -> Maybe (Decoded Bit)
forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode Solution
sol Bit
c'
Var Literal
l -> Solution -> Literal -> Maybe (Decoded Literal)
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
_ -> Maybe Bool
forall (m :: * -> *) a. MonadPlus m => m a
mzero
where
andMaybeBools :: [Maybe Bool] -> Maybe Bool
andMaybeBools :: [Maybe Bool] -> Maybe Bool
andMaybeBools [Maybe Bool]
mbs
| (Bool -> Bool) -> [Bool] -> Bool
forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
any Bool -> Bool
forall b. Boolean b => b -> b
not [Bool]
knowns = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
| [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [()]
unknowns = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
| Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing
where
([()]
unknowns, [Bool]
knowns) = [Maybe Bool] -> ([()], [Bool])
forall a. [Maybe a] -> ([()], [a])
partitionMaybes [Maybe Bool]
mbs
partitionMaybes :: [Maybe a] -> ([()], [a])
partitionMaybes :: [Maybe a] -> ([()], [a])
partitionMaybes = (Maybe a -> ([()], [a]) -> ([()], [a]))
-> ([()], [a]) -> [Maybe a] -> ([()], [a])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Maybe a -> ([()], [a]) -> ([()], [a])
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
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
js)
assert :: MonadSAT s m => Bit -> m ()
assert :: Bit -> m ()
assert (And Seq Bit
bs) = Seq Bit -> (Bit -> m ()) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
Foldable.for_ Seq Bit
bs Bit -> m ()
forall s (m :: * -> *). MonadSAT s m => Bit -> m ()
assert
assert (Not (And Seq Bit
bs)) | () () -> () -> Bool
forall a. Eq a => a -> a -> Bool
/= () = do
Seq Literal
ls <- Seq Bit -> (Bit -> m Literal) -> m (Seq Literal)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
Traversable.for Seq Bit
bs Bit -> m Literal
forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit
Formula -> m ()
forall s (m :: * -> *). MonadSAT s m => Formula -> m ()
assertFormula (Formula -> m ()) -> Formula -> m ()
forall a b. (a -> b) -> a -> b
$ Clause -> Formula
fromClause (Clause -> Formula) -> Clause -> Formula
forall a b. (a -> b) -> a -> b
$ (Literal -> Clause) -> Seq Literal -> Clause
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Literal -> Clause
fromLiteral (Literal -> Clause) -> (Literal -> Literal) -> Literal -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Literal
negateLiteral) Seq Literal
ls
assert Bit
b = do
Literal
l <- Bit -> m Literal
forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
b
Formula -> m ()
forall s (m :: * -> *). MonadSAT s m => Formula -> m ()
assertFormula (Literal -> Formula
formulaLiteral Literal
l)
runBit :: MonadSAT s m => Bit -> m Literal
runBit :: Bit -> m Literal
runBit (Not Bit
c) = Literal -> Literal
negateLiteral (Literal -> Literal) -> m Literal -> m Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Bit -> m Literal
forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
c
runBit (Var Literal
l) = Literal -> m Literal
forall (m :: * -> *) a. Monad m => a -> m a
return Literal
l
runBit (Run forall (m :: * -> *) s. MonadSAT s m => m Bit
action) = m Bit
forall (m :: * -> *) s. MonadSAT s m => m Bit
action m Bit -> (Bit -> m Literal) -> m Literal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bit -> m Literal
forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit
runBit Bit
b = Bit -> (Literal -> m ()) -> m Literal
forall s (m :: * -> *) a.
MonadSAT s m =>
a -> (Literal -> m ()) -> m Literal
generateLiteral Bit
b ((Literal -> m ()) -> m Literal) -> (Literal -> m ()) -> m Literal
forall a b. (a -> b) -> a -> b
$ \Literal
out ->
Formula -> m ()
forall s (m :: * -> *). MonadSAT s m => Formula -> m ()
assertFormula (Formula -> m ()) -> m Formula -> m ()
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 ([Literal] -> Formula) -> m [Literal] -> m Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Bit -> m Literal) -> [Bit] -> m [Literal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Bit -> m Literal
forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit (Seq Bit -> [Bit]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Bit
bs)
Xor Bit
x Bit
y -> (Literal -> Literal -> Formula)
-> m Literal -> m Literal -> m Formula
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Literal -> Literal -> Literal -> Formula
formulaXor Literal
out) (Bit -> m Literal
forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
x) (Bit -> m Literal
forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
y)
Mux Bit
x Bit
y Bit
p -> (Literal -> Literal -> Literal -> Formula)
-> m Literal -> m Literal -> m Literal -> m Formula
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) (Bit -> m Literal
forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
x) (Bit -> m Literal
forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
y) (Bit -> m Literal
forall s (m :: * -> *). MonadSAT s m => Bit -> m Literal
runBit Bit
p)
#if __GLASGOW_HASKELL__ < 900
Not Bit
_ -> String -> m Formula
forall a. HasCallStack => String -> a
error String
"Unreachable"
Var Literal
_ -> String -> m Formula
forall a. HasCallStack => String -> a
error String
"Unreachable"
Run forall (m :: * -> *) s. MonadSAT s m => m Bit
_ -> String -> m Formula
forall a. HasCallStack => String -> a
error String
"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 :: Bool -> V1 a
gbool Bool
x = Bool
x Bool -> V1 a -> V1 a
`seq` String -> V1 a
forall a. HasCallStack => String -> a
error String
"GBoolean[V1].gbool"
V1 a
x &&# :: V1 a -> V1 a -> V1 a
&&# V1 a
y = V1 a
x V1 a -> V1 a -> V1 a
`seq` V1 a
y V1 a -> V1 a -> V1 a
`seq` String -> V1 a
forall a. HasCallStack => String -> a
error String
"GBoolean[V1].&&#"
V1 a
x ||# :: V1 a -> V1 a -> V1 a
||# V1 a
y = V1 a
x V1 a -> V1 a -> V1 a
`seq` V1 a
y V1 a -> V1 a -> V1 a
`seq` String -> V1 a
forall a. HasCallStack => String -> a
error String
"GBoolean[V1].||#"
gnot :: V1 a -> V1 a
gnot V1 a
x = V1 a
x V1 a -> V1 a -> V1 a
`seq` String -> V1 a
forall a. HasCallStack => String -> a
error String
"GBoolean[V1].gnot"
gall :: (a -> V1 b) -> t a -> V1 b
gall a -> V1 b
x t a
y = a -> V1 b
x (a -> V1 b) -> V1 b -> V1 b
`seq` t a
y t a -> V1 b -> V1 b
`seq` String -> V1 b
forall a. HasCallStack => String -> a
error String
"GBoolean[V1].gall"
gany :: (a -> V1 b) -> t a -> V1 b
gany a -> V1 b
x t a
y = a -> V1 b
x (a -> V1 b) -> V1 b -> V1 b
`seq` t a
y t a -> V1 b -> V1 b
`seq` String -> V1 b
forall a. HasCallStack => String -> a
error String
"GBoolean[V1].gany"
gxor :: V1 a -> V1 a -> V1 a
gxor V1 a
x V1 a
y = V1 a
x V1 a -> V1 a -> V1 a
`seq` V1 a
y V1 a -> V1 a -> V1 a
`seq` String -> V1 a
forall a. HasCallStack => String -> a
error String
"GBoolean[V1].gxor"
instance GBoolean U1 where
gbool :: Bool -> U1 a
gbool Bool
_ = U1 a
forall k (p :: k). U1 p
U1
U1 a
U1 &&# :: U1 a -> U1 a -> U1 a
&&# U1 a
U1 = U1 a
forall k (p :: k). U1 p
U1
U1 a
U1 ||# :: U1 a -> U1 a -> U1 a
||# U1 a
U1 = U1 a
forall k (p :: k). U1 p
U1
gnot :: U1 a -> U1 a
gnot U1 a
U1 = U1 a
forall k (p :: k). U1 p
U1
gall :: (a -> U1 b) -> t a -> U1 b
gall a -> U1 b
_ t a
_ = U1 b
forall k (p :: k). U1 p
U1
gany :: (a -> U1 b) -> t a -> U1 b
gany a -> U1 b
_ t a
_ = U1 b
forall k (p :: k). U1 p
U1
gxor :: U1 a -> U1 a -> U1 a
gxor U1 a
_ U1 a
_ = U1 a
forall k (p :: k). U1 p
U1
instance (GBoolean f, GBoolean g) => GBoolean (f :*: g) where
gbool :: Bool -> (:*:) f g a
gbool Bool
x = Bool -> f a
forall (f :: * -> *) a. GBoolean f => Bool -> f a
gbool Bool
x f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Bool -> g a
forall (f :: * -> *) a. GBoolean f => Bool -> f a
gbool Bool
x
(f a
a :*: g a
b) &&# :: (:*:) f g a -> (:*:) f g a -> (:*:) f g a
&&# (f a
c :*: g a
d) = (f a
a f a -> f a -> f a
forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
&&# f a
c) f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (g a
b g a -> g a -> g a
forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
&&# g a
d)
(f a
a :*: g a
b) ||# :: (:*:) f g a -> (:*:) f g a -> (:*:) f g a
||# (f a
c :*: g a
d) = (f a
a f a -> f a -> f a
forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
||# f a
c) f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (g a
b g a -> g a -> g a
forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
||# g a
d)
gnot :: (:*:) f g a -> (:*:) f g a
gnot (f a
a :*: g a
b) = f a -> f a
forall (f :: * -> *) a. GBoolean f => f a -> f a
gnot f a
a f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a -> g a
forall (f :: * -> *) a. GBoolean f => f a -> f a
gnot g a
b
gall :: (a -> (:*:) f g b) -> t a -> (:*:) f g b
gall a -> (:*:) f g b
p t a
xs = (f b -> f b) -> [f b] -> f b
forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gall f b -> f b
forall a. a -> a
id [f b]
ls f b -> g b -> (:*:) f g b
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (g b -> g b) -> [g b] -> g b
forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gall g b -> g b
forall a. a -> a
id [g b]
rs
where ([f b]
ls, [g b]
rs) = [(:*:) f g b] -> ([f b], [g b])
forall (f :: * -> *) (g :: * -> *) a.
[(:*:) f g a] -> ([f a], [g a])
gunzip ([(:*:) f g b] -> ([f b], [g b]))
-> (t a -> [(:*:) f g b]) -> t a -> ([f b], [g b])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> (:*:) f g b) -> [a] -> [(:*:) f g b]
forall a b. (a -> b) -> [a] -> [b]
map a -> (:*:) f g b
p ([a] -> [(:*:) f g b]) -> (t a -> [a]) -> t a -> [(:*:) f g b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (t a -> ([f b], [g b])) -> t a -> ([f b], [g b])
forall a b. (a -> b) -> a -> b
$ t a
xs
gany :: (a -> (:*:) f g b) -> t a -> (:*:) f g b
gany a -> (:*:) f g b
p t a
xs = (f b -> f b) -> [f b] -> f b
forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gany f b -> f b
forall a. a -> a
id [f b]
ls f b -> g b -> (:*:) f g b
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (g b -> g b) -> [g b] -> g b
forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gany g b -> g b
forall a. a -> a
id [g b]
rs
where ([f b]
ls, [g b]
rs) = [(:*:) f g b] -> ([f b], [g b])
forall (f :: * -> *) (g :: * -> *) a.
[(:*:) f g a] -> ([f a], [g a])
gunzip ([(:*:) f g b] -> ([f b], [g b]))
-> (t a -> [(:*:) f g b]) -> t a -> ([f b], [g b])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> (:*:) f g b) -> [a] -> [(:*:) f g b]
forall a b. (a -> b) -> [a] -> [b]
map a -> (:*:) f g b
p ([a] -> [(:*:) f g b]) -> (t a -> [a]) -> t a -> [(:*:) f g b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (t a -> ([f b], [g b])) -> t a -> ([f b], [g b])
forall a b. (a -> b) -> a -> b
$ t a
xs
gxor :: (:*:) f g a -> (:*:) f g a -> (:*:) f g a
gxor (f a
a :*: g a
b) (f a
c :*: g a
d) = f a -> f a -> f a
forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
gxor f a
a f a
c f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a -> g a -> g a
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 :: Bool -> K1 i a a
gbool = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> (Bool -> a) -> Bool -> K1 i a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> a
forall b. Boolean b => Bool -> b
bool
K1 a
a &&# :: K1 i a a -> K1 i a a -> K1 i a a
&&# K1 a
b = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a
a a -> a -> a
forall b. Boolean b => b -> b -> b
&& a
b)
K1 a
a ||# :: K1 i a a -> K1 i a a -> K1 i a a
||# K1 a
b = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a
a a -> a -> a
forall b. Boolean b => b -> b -> b
|| a
b)
gnot :: K1 i a a -> K1 i a a
gnot (K1 a
a) = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> a
forall b. Boolean b => b -> b
not a
a)
gall :: (a -> K1 i a b) -> t a -> K1 i a b
gall a -> K1 i a b
p t a
as = a -> K1 i a b
forall k i c (p :: k). c -> K1 i c p
K1 ((a -> a) -> t a -> a
forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
all (K1 i a b -> a
forall i c k (p :: k). K1 i c p -> c
unK1 (K1 i a b -> a) -> (a -> K1 i a b) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> K1 i a b
p) t a
as)
gany :: (a -> K1 i a b) -> t a -> K1 i a b
gany a -> K1 i a b
p t a
as = a -> K1 i a b
forall k i c (p :: k). c -> K1 i c p
K1 ((a -> a) -> t a -> a
forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
any (K1 i a b -> a
forall i c k (p :: k). K1 i c p -> c
unK1 (K1 i a b -> a) -> (a -> K1 i a b) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> K1 i a b
p) t a
as)
gxor :: K1 i a a -> K1 i a a -> K1 i a a
gxor (K1 a
a) (K1 a
b) = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> a -> a
forall b. Boolean b => b -> b -> b
xor a
a a
b)
instance GBoolean a => GBoolean (M1 i c a) where
gbool :: Bool -> M1 i c a a
gbool = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i c a a) -> (Bool -> a a) -> Bool -> M1 i c a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> a a
forall (f :: * -> *) a. GBoolean f => Bool -> f a
gbool
M1 a a
a &&# :: M1 i c a a -> M1 i c a a -> M1 i c a a
&&# M1 a a
b = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a
a a a -> a a -> a a
forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
&&# a a
b)
M1 a a
a ||# :: M1 i c a a -> M1 i c a a -> M1 i c a a
||# M1 a a
b = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a
a a a -> a a -> a a
forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
||# a a
b)
gnot :: M1 i c a a -> M1 i c a a
gnot (M1 a a
a) = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a -> a a
forall (f :: * -> *) a. GBoolean f => f a -> f a
gnot a a
a)
gall :: (a -> M1 i c a b) -> t a -> M1 i c a b
gall a -> M1 i c a b
p t a
as = a b -> M1 i c a b
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 ((a -> a b) -> t a -> a b
forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gall (M1 i c a b -> a b
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 (M1 i c a b -> a b) -> (a -> M1 i c a b) -> a -> a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> M1 i c a b
p) t a
as)
gany :: (a -> M1 i c a b) -> t a -> M1 i c a b
gany a -> M1 i c a b
p t a
as = a b -> M1 i c a b
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 ((a -> a b) -> t a -> a b
forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gany (M1 i c a b -> a b
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 (M1 i c a b -> a b) -> (a -> M1 i c a b) -> a -> a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> M1 i c a b
p) t a
as)
gxor :: M1 i c a a -> M1 i c a a -> M1 i c a a
gxor (M1 a a
a) (M1 a a
b) = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a -> a a -> a a
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 = Bool -> b
forall b. Boolean b => Bool -> b
bool Bool
True
false :: b
false = Bool -> b
forall b. Boolean b => Bool -> b
bool Bool
False
(&&) :: b -> b -> b
(||) :: b -> b -> b
(==>) :: b -> b -> b
b
x ==> b
y = b -> b
forall b. Boolean b => b -> b
not b
x b -> b -> b
forall b. Boolean b => b -> b -> b
|| b
y
not :: b -> b
and :: Foldable t => t b -> b
and = (b -> b) -> t b -> b
forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
Ersatz.Bit.all b -> b
forall a. a -> a
id
or :: Foldable t => t b -> b
or = (b -> b) -> t b -> b
forall b (t :: * -> *) a.
(Boolean b, Foldable t) =>
(a -> b) -> t a -> b
Ersatz.Bit.any b -> b
forall a. a -> a
id
nand :: Foldable t => t b -> b
nand = b -> b
forall b. Boolean b => b -> b
not (b -> b) -> (t b -> b) -> t b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t b -> b
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and
nor :: Foldable t => t b -> b
nor = b -> b
forall b. Boolean b => b -> b
not (b -> b) -> (t b -> b) -> t b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t b -> b
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 b -> b -> b
forall b. Boolean b => b -> b -> b
&& b -> b
forall b. Boolean b => b -> b
not b
s) b -> b -> b
forall b. Boolean b => b -> b -> b
|| (b
t b -> b -> b
forall b. Boolean b => b -> b -> b
&& b
s)
default bool :: (Generic b, GBoolean (Rep b)) => Bool -> b
bool = Rep b Any -> b
forall a x. Generic a => Rep a x -> a
to (Rep b Any -> b) -> (Bool -> Rep b Any) -> Bool -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Rep b Any
forall (f :: * -> *) a. GBoolean f => Bool -> f a
gbool
default (&&) :: (Generic b, GBoolean (Rep b)) => b -> b -> b
b
x && b
y = Rep b Any -> b
forall a x. Generic a => Rep a x -> a
to (b -> Rep b Any
forall a x. Generic a => a -> Rep a x
from b
x Rep b Any -> Rep b Any -> Rep b Any
forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
&&# b -> Rep b Any
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 = Rep b Any -> b
forall a x. Generic a => Rep a x -> a
to (b -> Rep b Any
forall a x. Generic a => a -> Rep a x
from b
x Rep b Any -> Rep b Any -> Rep b Any
forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
||# b -> Rep b Any
forall a x. Generic a => a -> Rep a x
from b
y)
default not :: (Generic b, GBoolean (Rep b)) => b -> b
not = Rep b Any -> b
forall a x. Generic a => Rep a x -> a
to (Rep b Any -> b) -> (b -> Rep b Any) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep b Any -> Rep b Any
forall (f :: * -> *) a. GBoolean f => f a -> f a
gnot (Rep b Any -> Rep b Any) -> (b -> Rep b Any) -> b -> Rep b Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Rep b Any
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 = Rep b Any -> b
forall a x. Generic a => Rep a x -> a
to (Rep b Any -> b) -> (t a -> Rep b Any) -> t a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Rep b Any) -> t a -> Rep b Any
forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gall (b -> Rep b Any
forall a x. Generic a => a -> Rep a x
from (b -> Rep b Any) -> (a -> b) -> a -> Rep b Any
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 = Rep b Any -> b
forall a x. Generic a => Rep a x -> a
to (Rep b Any -> b) -> (t a -> Rep b Any) -> t a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Rep b Any) -> t a -> Rep b Any
forall (f :: * -> *) (t :: * -> *) a b.
(GBoolean f, Foldable t) =>
(a -> f b) -> t a -> f b
gany (b -> Rep b Any
forall a x. Generic a => a -> Rep a x
from (b -> Rep b Any) -> (a -> b) -> a -> Rep b Any
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 = Rep b Any -> b
forall a x. Generic a => Rep a x -> a
to (b -> Rep b Any
forall a x. Generic a => a -> Rep a x
from b
x Rep b Any -> Rep b Any -> Rep b Any
forall (f :: * -> *) a. GBoolean f => f a -> f a -> f a
`gxor` b -> Rep b Any
forall a x. Generic a => a -> Rep a x
from b
y)
instance Boolean Bool where
bool :: Bool -> 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 :: t Bool -> Bool
and = t Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Foldable.and
or :: t Bool -> Bool
or = t Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Foldable.or
all :: (a -> Bool) -> t a -> Bool
all = (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Foldable.all
any :: (a -> Bool) -> t a -> Bool
any = (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Foldable.any
xor :: Bool -> Bool -> Bool
xor = Bool -> Bool -> Bool
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 :: [(:*:) f g a] -> ([f a], [g a])
gunzip = ((:*:) f g a -> ([f a], [g a]) -> ([f a], [g a]))
-> ([f a], [g a]) -> [(:*:) f g a] -> ([f a], [g a])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (:*:) f g a -> ([f a], [g a]) -> ([f a], [g a])
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
af p -> [f p] -> [f p]
forall a. a -> [a] -> [a]
:[f p]
as, g p
bg p -> [g p] -> [g p]
forall a. a -> [a] -> [a]
:[g p]
bs)