content: {-# 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 = fromBool True
  
    false :: a
    false = fromBool False
  
    not :: a -> a
  
    (&&) :: a -> a -> a
  
    (||) :: a -> a -> a
  
    implies :: a -> a -> a
    implies a b = b || not a
  
    -- | Set difference, dual to 'implies'.
    butNot :: a -> a -> a
    butNot a b = a && not b
  
    default not :: IsBool a => a -> a
    not = fromBool1 P.not
  
    default (&&) :: IsBool a => a -> a -> a
    (&&) = fromBool2 (P.&&)
  
    default (||) :: IsBool a => a -> a -> a
    (||) = fromBool2 (P.||)
  
  -- | Types isomorphic to 'Bool'.
  --
  class (Boolean a, Eq a) => IsBool a where
    toBool :: a -> Bool
  
    ifThenElse :: a -> b -> b -> b
    ifThenElse c t e = if toBool c then t else e
  
    fromBool1 :: (Bool -> Bool) -> (a -> a)
    fromBool1 f = fromBool . f . toBool
  
    fromBool2 :: (Bool -> Bool -> Bool) -> (a -> a -> a)
    fromBool2 f a b = fromBool $ f (toBool a) (toBool b)
  
    {-# MINIMAL toBool #-}
  
  instance Boolean Bool where
    fromBool = id
  
  instance IsBool Bool where
    toBool = id
    -- optional
    fromBool1 = id
    fromBool2 = id
  
  instance Boolean b => Boolean (a -> b) where
    fromBool   = const . fromBool
    not f      = not . f
    (f && g) a = f a && g a
    (f || g) a = f a || g a
  