{-# LANGUAGE DerivingStrategies #-}
module ZkFold.Symbolic.Data.Bool (
BoolType(..),
Bool(..),
all,
all1,
any
) where
import Prelude hiding (Bool, Num (..), all, any, not, (&&), (/), (||))
import qualified Prelude as Haskell
import ZkFold.Base.Algebra.Basic.Class
import ZkFold.Base.Data.Vector (Vector)
import ZkFold.Symbolic.Compiler.Arithmetizable
class BoolType b where
true :: b
false :: b
not :: b -> b
infixr 3 &&
(&&) :: b -> b -> b
infixr 2 ||
(||) :: b -> b -> b
xor :: b -> b -> b
instance BoolType Haskell.Bool where
true :: Bool
true = Bool
True
false :: Bool
false = Bool
False
not :: Bool -> Bool
not = Bool -> Bool
Haskell.not
&& :: Bool -> Bool -> Bool
(&&) = Bool -> Bool -> Bool
(Haskell.&&)
|| :: Bool -> Bool -> Bool
(||) = Bool -> Bool -> Bool
(Haskell.||)
xor :: Bool -> Bool -> Bool
xor = Bool -> Bool -> Bool
forall b. BoolType b => b -> b -> b
xor
newtype Bool x = Bool x
deriving (Bool x -> Bool x -> Bool
(Bool x -> Bool x -> Bool)
-> (Bool x -> Bool x -> Bool) -> Eq (Bool x)
forall x. Eq x => Bool x -> Bool x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall x. Eq x => Bool x -> Bool x -> Bool
== :: Bool x -> Bool x -> Bool
$c/= :: forall x. Eq x => Bool x -> Bool x -> Bool
/= :: Bool x -> Bool x -> Bool
Eq)
deriving newtype instance Arithmetizable a x => Arithmetizable a (Bool x)
instance (Field x, Eq x) => Show (Bool x) where
show :: Bool x -> String
show (Bool x
x) = if x
x x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
forall a. MultiplicativeMonoid a => a
one then String
"True" else String
"False"
instance {-# OVERLAPPABLE #-} (Ring x) => BoolType (Bool x) where
true :: Bool x
true = x -> Bool x
forall x. x -> Bool x
Bool x
forall a. MultiplicativeMonoid a => a
one
false :: Bool x
false = x -> Bool x
forall x. x -> Bool x
Bool x
forall a. AdditiveMonoid a => a
zero
not :: Bool x -> Bool x
not (Bool x
b) = x -> Bool x
forall x. x -> Bool x
Bool (x -> Bool x) -> x -> Bool x
forall a b. (a -> b) -> a -> b
$ x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
b
&& :: Bool x -> Bool x -> Bool x
(&&) (Bool x
b1) (Bool x
b2) = x -> Bool x
forall x. x -> Bool x
Bool (x -> Bool x) -> x -> Bool x
forall a b. (a -> b) -> a -> b
$ x
b1 x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* x
b2
|| :: Bool x -> Bool x -> Bool x
(||) (Bool x
b1) (Bool x
b2) = x -> Bool x
forall x. x -> Bool x
Bool (x -> Bool x) -> x -> Bool x
forall a b. (a -> b) -> a -> b
$ x
b1 x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
b2 x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
b1 x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* x
b2
xor :: Bool x -> Bool x -> Bool x
xor (Bool x
b1) (Bool x
b2) = x -> Bool x
forall x. x -> Bool x
Bool (x -> Bool x) -> x -> Bool x
forall a b. (a -> b) -> a -> b
$ x
b1 x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
b2 x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- (x
b1 x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* x
b2 x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
b1 x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* x
b2)
instance (Ring x) => BoolType (Bool (Vector 1 x)) where
true :: Bool (Vector 1 x)
true = Vector 1 x -> Bool (Vector 1 x)
forall x. x -> Bool x
Bool (Vector 1 x -> Bool (Vector 1 x))
-> Vector 1 x -> Bool (Vector 1 x)
forall a b. (a -> b) -> a -> b
$ x -> Vector 1 x
forall a. a -> Vector 1 a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure x
forall a. MultiplicativeMonoid a => a
one
false :: Bool (Vector 1 x)
false = Vector 1 x -> Bool (Vector 1 x)
forall x. x -> Bool x
Bool (Vector 1 x -> Bool (Vector 1 x))
-> Vector 1 x -> Bool (Vector 1 x)
forall a b. (a -> b) -> a -> b
$ x -> Vector 1 x
forall a. a -> Vector 1 a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure x
forall a. AdditiveMonoid a => a
zero
not :: Bool (Vector 1 x) -> Bool (Vector 1 x)
not (Bool Vector 1 x
b) = Vector 1 x -> Bool (Vector 1 x)
forall x. x -> Bool x
Bool (Vector 1 x -> Bool (Vector 1 x))
-> Vector 1 x -> Bool (Vector 1 x)
forall a b. (a -> b) -> a -> b
$ (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
-) (x -> x) -> Vector 1 x -> Vector 1 x
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector 1 x
b
&& :: Bool (Vector 1 x) -> Bool (Vector 1 x) -> Bool (Vector 1 x)
(&&) (Bool Vector 1 x
b1) (Bool Vector 1 x
b2) = Vector 1 x -> Bool (Vector 1 x)
forall x. x -> Bool x
Bool (Vector 1 x -> Bool (Vector 1 x))
-> Vector 1 x -> Bool (Vector 1 x)
forall a b. (a -> b) -> a -> b
$ x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) (x -> x -> x) -> Vector 1 x -> Vector 1 (x -> x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector 1 x
b1 Vector 1 (x -> x) -> Vector 1 x -> Vector 1 x
forall a b. Vector 1 (a -> b) -> Vector 1 a -> Vector 1 b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Vector 1 x
b2
|| :: Bool (Vector 1 x) -> Bool (Vector 1 x) -> Bool (Vector 1 x)
(||) (Bool Vector 1 x
b1) (Bool Vector 1 x
b2) = Vector 1 x -> Bool (Vector 1 x)
forall x. x -> Bool x
Bool (Vector 1 x -> Bool (Vector 1 x))
-> Vector 1 x -> Bool (Vector 1 x)
forall a b. (a -> b) -> a -> b
$ (\x
x x
y -> x
x x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
y x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
x x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* x
y) (x -> x -> x) -> Vector 1 x -> Vector 1 (x -> x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector 1 x
b1 Vector 1 (x -> x) -> Vector 1 x -> Vector 1 x
forall a b. Vector 1 (a -> b) -> Vector 1 a -> Vector 1 b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Vector 1 x
b2
xor :: Bool (Vector 1 x) -> Bool (Vector 1 x) -> Bool (Vector 1 x)
xor (Bool Vector 1 x
b1) (Bool Vector 1 x
b2) = Vector 1 x -> Bool (Vector 1 x)
forall x. x -> Bool x
Bool (Vector 1 x -> Bool (Vector 1 x))
-> Vector 1 x -> Bool (Vector 1 x)
forall a b. (a -> b) -> a -> b
$ (\x
x x
y -> x
x x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
y x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- (x
x x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* x
y x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
x x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* x
y)) (x -> x -> x) -> Vector 1 x -> Vector 1 (x -> x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector 1 x
b1 Vector 1 (x -> x) -> Vector 1 x -> Vector 1 x
forall a b. Vector 1 (a -> b) -> Vector 1 a -> Vector 1 b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Vector 1 x
b2
all :: (BoolType b, Foldable t) => (x -> b) -> t x -> b
all :: forall b (t :: Type -> Type) x.
(BoolType b, Foldable t) =>
(x -> b) -> t x -> b
all x -> b
f = (x -> b -> b) -> b -> t x -> b
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (b -> b -> b
forall b. BoolType b => b -> b -> b
(&&) (b -> b -> b) -> (x -> b) -> x -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> b
f) b
forall b. BoolType b => b
true
all1 :: (BoolType b, Functor t, Foldable t) => (x -> b) -> t x -> b
all1 :: forall b (t :: Type -> Type) x.
(BoolType b, Functor t, Foldable t) =>
(x -> b) -> t x -> b
all1 x -> b
f = (b -> b -> b) -> t b -> b
forall a. (a -> a -> a) -> t a -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldr1 b -> b -> b
forall b. BoolType b => b -> b -> b
(&&) (t b -> b) -> (t x -> t b) -> t x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> b) -> t x -> t b
forall a b. (a -> b) -> t a -> t b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> b
f
any :: (BoolType b, Foldable t) => (x -> b) -> t x -> b
any :: forall b (t :: Type -> Type) x.
(BoolType b, Foldable t) =>
(x -> b) -> t x -> b
any x -> b
f = (x -> b -> b) -> b -> t x -> b
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (b -> b -> b
forall b. BoolType b => b -> b -> b
(||) (b -> b -> b) -> (x -> b) -> x -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> b
f) b
forall b. BoolType b => b
false