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
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)
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 (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)
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