Boolean.hs

{-# 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 True

  -- | The false constant.
  -- @'false' = 'bool' 'False'@
  false :: b
  false = bool False

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

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

  -- | Logical implication.
  (==>) :: b -> b -> b
  x ==> y = not x || y

  -- | Logical implication with arrow reversed.
  --
  -- @
  -- forall x y. (x ==> y) === (y <== x)
  -- @
  (<==) :: b -> b -> b
  y <== x = not x || y

  -- | Logical equivalence.
  (<==>) :: b -> b -> b
  x <==> y = (x ==> y) && (y ==> 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 = foldl (&&) true

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

-- | The negated logical conjunction of several values.
--
-- @'nand' = 'not' . 'and'@
nand :: (Foldable t, Boolean b) => t b -> b
nand = not . and

-- | The negated logical disjunction of several values.
--
-- @'nor' = 'not' . 'or'@
nor :: (Foldable t, Boolean b) => t b -> b
nor = not . or

-- | The logical conjunction of the mapping of a function over several values.
all :: (Foldable t, Boolean b) => (a -> b) -> t a -> b
all p = foldl (\acc b -> acc && p 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 p = foldl (\acc b -> acc || p b) false

instance Boolean Bool where
  bool   = id
  true   = True
  false  = False
  (&&)   = (P.&&)
  (||)   = (P.||)
  not    = P.not
  xor    = (/=)
  (<==>) = (==)

instance Boolean Bit where
  bool     = Bit
  (&&)     = (.&.)
  (||)     = (.|.)
  not      = complement
  xor      = Bits.xor
  x <==> y = bool (x == y)

-- | Defined bitwise
instance KnownNat n => Boolean (V.Vector n Bit) where
  bool = V.replicate . coerce
  (&&) = V.zipWith (&&)
  (||) = V.zipWith (||)
  not  = V.map not
  xor  = V.zipWith Bits.xor
  x <==> y = bool (x == y)