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