{-# LANGUAGE NoImplicitPrelude #-}

module Language.Hasmtlib.Boolean where

import Prelude (Bool(..), (.), id, Eq(..))
import qualified Prelude as P
import Data.Bit
import Data.Coerce
import Data.Bits as Bits
import Data.Foldable hiding (and, or)
import qualified Data.Vector.Unboxed.Sized as V
import GHC.TypeNats

class Boolean b where
  -- | Lift a 'Bool'
  bool :: Bool -> b

  -- | The true constant
  -- @'true' = 'bool' 'True'@
  true :: b
  true = Bool -> b
forall b. Boolean b => Bool -> b
bool Bool
True

  -- | The false constant
  -- @'false' = 'bool' 'False'@
  false :: b
  false = Bool -> b
forall b. Boolean b => Bool -> b
bool Bool
False

  -- | Logical conjunction.
  (&&) :: b -> b -> b

  -- | Logical disjunction (inclusive or).
  (||) :: b -> b -> b

  -- | Logical implication.
  (==>) :: 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

  -- | Logical negation
  not :: b -> b

  -- | Exclusive-or
  xor :: b -> b -> b

  infixr 3 &&
  infixr 2 ||
  infixr 0 ==>

-- | The logical conjunction of several values.
and :: (Foldable t, Boolean b) => t b -> b
and :: forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
and = (b -> b -> b) -> b -> t b -> b
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> b -> b
forall b. Boolean b => b -> b -> b
(&&) b
forall b. Boolean b => b
true

-- | The logical disjunction of several values.
or :: (Foldable t, Boolean b) => t b -> b
or :: forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
or = (b -> b -> b) -> b -> t b -> b
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> b -> b
forall b. Boolean b => b -> b -> b
(||) b
forall b. Boolean b => b
false

-- | The negated logical conjunction of several values.
--
-- @'nand' = 'not' . 'and'@
nand :: (Foldable t, Boolean b) => t b -> b
nand :: forall (t :: * -> *) b. (Foldable t, Boolean b) => 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 (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
and

-- | The negated logical disjunction of several values.
--
-- @'nor' = 'not' . 'or'@
nor :: (Foldable t, Boolean b) => t b -> b
nor :: forall (t :: * -> *) b. (Foldable t, Boolean b) => 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 (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
or

-- | The logical conjunction of the mapping of a function over several values.
all :: (Foldable t, Boolean b) => (a -> b) -> t a -> b
all :: forall (t :: * -> *) b a.
(Foldable t, Boolean b) =>
(a -> b) -> t a -> b
all a -> b
p = (b -> a -> b) -> b -> t a -> b
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\b
acc a
b -> b
acc b -> b -> b
forall b. Boolean b => b -> b -> b
&& a -> b
p a
b) b
forall b. Boolean b => b
true

-- | The logical disjunction of the mapping of a function over several values.
any :: (Foldable t, Boolean b) => (a -> b) -> t a -> b
any :: forall (t :: * -> *) b a.
(Foldable t, Boolean b) =>
(a -> b) -> t a -> b
any a -> b
p = (b -> a -> b) -> b -> t a -> b
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\b
acc a
b -> b
acc b -> b -> b
forall b. Boolean b => b -> b -> b
|| a -> b
p a
b) b
forall b. Boolean b => b
false

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
(P.&&)
  || :: Bool -> Bool -> Bool
(||)  = Bool -> Bool -> Bool
(P.||)
  not :: Bool -> Bool
not   = Bool -> Bool
P.not
  xor :: Bool -> Bool -> Bool
xor   = Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)

instance Boolean Bit where
  bool :: Bool -> Bit
bool = Bool -> Bit
Bit
  && :: Bit -> Bit -> Bit
(&&) = Bit -> Bit -> Bit
forall a. Bits a => a -> a -> a
(.&.)
  || :: Bit -> Bit -> Bit
(||) = Bit -> Bit -> Bit
forall a. Bits a => a -> a -> a
(.|.)
  not :: Bit -> Bit
not  = Bit -> Bit
forall a. Bits a => a -> a
complement
  xor :: Bit -> Bit -> Bit
xor  = Bit -> Bit -> Bit
forall a. Bits a => a -> a -> a
Bits.xor

-- | Defined bitwise
instance KnownNat n => Boolean (V.Vector n Bit) where
  bool :: Bool -> Vector n Bit
bool = Bit -> Vector n Bit
forall (n :: Nat) a. (KnownNat n, Unbox a) => a -> Vector n a
V.replicate (Bit -> Vector n Bit) -> (Bool -> Bit) -> Bool -> Vector n Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bit
forall a b. Coercible a b => a -> b
coerce
  && :: Vector n Bit -> Vector n Bit -> Vector n Bit
(&&) = (Bit -> Bit -> Bit) -> Vector n Bit -> Vector n Bit -> Vector n Bit
forall a b c (n :: Nat).
(Unbox a, Unbox b, Unbox c) =>
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
V.zipWith Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
(&&)
  || :: Vector n Bit -> Vector n Bit -> Vector n Bit
(||) = (Bit -> Bit -> Bit) -> Vector n Bit -> Vector n Bit -> Vector n Bit
forall a b c (n :: Nat).
(Unbox a, Unbox b, Unbox c) =>
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
V.zipWith Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
(||)
  not :: Vector n Bit -> Vector n Bit
not  = (Bit -> Bit) -> Vector n Bit -> Vector n Bit
forall a b (n :: Nat).
(Unbox a, Unbox b) =>
(a -> b) -> Vector n a -> Vector n b
V.map Bit -> Bit
forall b. Boolean b => b -> b
not
  xor :: Vector n Bit -> Vector n Bit -> Vector n Bit
xor  = (Bit -> Bit -> Bit) -> Vector n Bit -> Vector n Bit -> Vector n Bit
forall a b c (n :: Nat).
(Unbox a, Unbox b, Unbox c) =>
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
V.zipWith Bit -> Bit -> Bit
forall a. Bits a => a -> a -> a
Bits.xor