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

-- TODO (Issue #18): hide this constructor
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