{-# LANGUAGE NoImplicitPrelude #-}

{- |
This module provides a more generic version of bool-like algebras than what the Prelude does for 'Bool'.

The class 'Boolean' therefore overloads most of the Preludes operators like '(&&)'.

However, as 'Bool' also features an instance of 'Boolean', you can simply hide the Prelude ones - not having to import either qualified.

==== __Example__

@
import Prelude hiding (not, any, all, (&&), (||), and, or)
import Language.Hasmtlib

problem :: MonadSMT s m => StateT s m (Expr BoolSort, Expr BoolSort)
problem = do
  x <- var \@BoolSort
  y <- var
  let b = False || True
  assert $ x && y \<==\> and [x, y, true] && encode b ==> x && y
  return (x,y)
@
-}
module Language.Hasmtlib.Boolean
(
  -- * Class
  Boolean(..)

  -- * Operators
, and, or
, nand, nor
, all, any
)
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, all, any)
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 implication with arrow reversed.
  --
  -- @
  -- forall x y. (x ==> y) === (y <== x)
  -- @
  (<==) :: b -> b -> b
  b
y <== b
x = b -> b
forall b. Boolean b => b -> b
not b
x b -> b -> b
forall b. Boolean b => b -> b -> b
|| b
y

  -- | Logical equivalence.
  (<==>) :: b -> b -> b
  b
x <==> b
y = (b
x b -> b -> b
forall b. Boolean b => b -> b -> b
==> b
y) b -> b -> b
forall b. Boolean b => b -> b -> b
&& (b
y b -> b -> b
forall b. Boolean b => b -> b -> b
==> b
x)

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

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

  infix 4 `xor`
  infixr 4 <==>
  infixr 3 &&
  infixr 2 ||
  infixr 0 ==>
  infixl 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
(/=)
  <==> :: Bool -> Bool -> Bool
(<==>) = 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
  Bit
x <==> :: Bit -> Bit -> Bit
<==> Bit
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Bit
x Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
y)

-- | 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
  Vector n Bit
x <==> :: Vector n Bit -> Vector n Bit -> Vector n Bit
<==> Vector n Bit
y = Bool -> Vector n Bit
forall b. Boolean b => Bool -> b
bool (Vector n Bit
x Vector n Bit -> Vector n Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Vector n Bit
y)