{-# OPTIONS_GHC -Wunused-imports #-}

-- | Boolean algebras and types isomorphic to 'Bool'.
--
-- There are already solutions for 'Boolean' algebras in the Haskell ecosystem,
-- but they do not offer easy instantiations for types isomorphic to 'Bool'.
-- In particular, if type @a@ is isomorphic to 'Bool', so it satisfies `IsBool a`,
-- we would like to instantiate 'Boolean a' by just giving 'true' and 'false'.
-- To facilitate this within the limits of the Haskell class system,
-- we define the class 'Boolean' mutually with class 'IsBool',
-- so that operations 'not', '(&&)', and '(||)' can get default implementations.
--
-- Usage:
-- @
--    import Prelude hiding ( not, (&&), (||) )
--    import Agda.Utils.Boolean
-- @

module Agda.Utils.Boolean where

import Prelude ( Bool(True,False), Eq, ($), (.), const, id )
import qualified Prelude as P

infixr 3 &&
infixr 2 ||

-- | Boolean algebras.
--
class Boolean a where
  fromBool :: Bool -> a

  true :: a
  true = Bool -> a
forall a. Boolean a => Bool -> a
fromBool Bool
True

  false :: a
  false = Bool -> a
forall a. Boolean a => Bool -> a
fromBool Bool
False

  not :: a -> a

  (&&) :: a -> a -> a

  (||) :: a -> a -> a

  implies :: a -> a -> a
  implies a
a a
b = a
b a -> a -> a
forall a. Boolean a => a -> a -> a
|| a -> a
forall a. Boolean a => a -> a
not a
a

  -- | Set difference, dual to 'implies'.
  butNot :: a -> a -> a
  butNot a
a a
b = a
a a -> a -> a
forall a. Boolean a => a -> a -> a
&& a -> a
forall a. Boolean a => a -> a
not a
b

  default not :: IsBool a => a -> a
  not = (Bool -> Bool) -> a -> a
forall a. IsBool a => (Bool -> Bool) -> a -> a
fromBool1 Bool -> Bool
P.not

  default (&&) :: IsBool a => a -> a -> a
  (&&) = (Bool -> Bool -> Bool) -> a -> a -> a
forall a. IsBool a => (Bool -> Bool -> Bool) -> a -> a -> a
fromBool2 Bool -> Bool -> Bool
(P.&&)

  default (||) :: IsBool a => a -> a -> a
  (||) = (Bool -> Bool -> Bool) -> a -> a -> a
forall a. IsBool a => (Bool -> Bool -> Bool) -> a -> a -> a
fromBool2 Bool -> Bool -> Bool
(P.||)

-- | Types isomorphic to 'Bool'.
--
class (Boolean a, Eq a) => IsBool a where
  toBool :: a -> Bool

  ifThenElse :: a -> b -> b -> b
  ifThenElse a
c b
t b
e = if a -> Bool
forall a. IsBool a => a -> Bool
toBool a
c then b
t else b
e

  fromBool1 :: (Bool -> Bool) -> (a -> a)
  fromBool1 Bool -> Bool
f = Bool -> a
forall a. Boolean a => Bool -> a
fromBool (Bool -> a) -> (a -> Bool) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
f (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
forall a. IsBool a => a -> Bool
toBool

  fromBool2 :: (Bool -> Bool -> Bool) -> (a -> a -> a)
  fromBool2 Bool -> Bool -> Bool
f a
a a
b = Bool -> a
forall a. Boolean a => Bool -> a
fromBool (Bool -> a) -> Bool -> a
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
f (a -> Bool
forall a. IsBool a => a -> Bool
toBool a
a) (a -> Bool
forall a. IsBool a => a -> Bool
toBool a
b)

  {-# MINIMAL toBool #-}

instance Boolean Bool where
  fromBool :: Bool -> Bool
fromBool = Bool -> Bool
forall a. a -> a
id

instance IsBool Bool where
  toBool :: Bool -> Bool
toBool = Bool -> Bool
forall a. a -> a
id
  -- optional
  fromBool1 :: (Bool -> Bool) -> Bool -> Bool
fromBool1 = (Bool -> Bool) -> Bool -> Bool
forall a. a -> a
id
  fromBool2 :: (Bool -> Bool -> Bool) -> Bool -> Bool -> Bool
fromBool2 = (Bool -> Bool -> Bool) -> Bool -> Bool -> Bool
forall a. a -> a
id

instance Boolean b => Boolean (a -> b) where
  fromBool :: Bool -> a -> b
fromBool   = b -> a -> b
forall a b. a -> b -> a
const (b -> a -> b) -> (Bool -> b) -> Bool -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> b
forall a. Boolean a => Bool -> a
fromBool
  not :: (a -> b) -> a -> b
not a -> b
f      = b -> b
forall a. Boolean a => a -> a
not (b -> b) -> (a -> b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f
  (a -> b
f && :: (a -> b) -> (a -> b) -> a -> b
&& a -> b
g) a
a = a -> b
f a
a b -> b -> b
forall a. Boolean a => a -> a -> a
&& a -> b
g a
a
  (a -> b
f || :: (a -> b) -> (a -> b) -> a -> b
|| a -> b
g) a
a = a -> b
f a
a b -> b -> b
forall a. Boolean a => a -> a -> a
|| a -> b
g a
a