{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveDataTypeable #-}
--------------------------------------------------------------------
-- |
-- Copyright :  © Oleg Grenrus 2014
-- License   :  MIT
-- Maintainer:  Oleg Grenrus <oleg.grenrus@iki.fi>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Data.Algebra.Boolean.Negable (
  Neg(..),
  Negable(..)
)
  where

import Data.Algebra.Boolean.CoBoolean

import Data.Monoid
import Data.Typeable
import Control.DeepSeq (NFData(rnf))

import Prelude hiding (not)
import qualified Prelude as P

import qualified Data.Algebra.Boolean as B

-- | Free 'Negable'.
data Neg a = Pos a -- ^ Positive value
           | Neg a -- ^ Negative value
  deriving (Eq, Ord, Show, Read, Functor, Typeable)

instance CoBoolean (Neg a) where
  toBoolean (Pos _) = B.true
  toBoolean (Neg _) = B.false

instance CoBoolean1 Neg where
  toBooleanWith f (Pos x) = f x
  toBooleanWith f (Neg x) = B.not $ f x

instance NFData a => NFData (Neg a) where
  rnf (Pos a) = rnf a
  rnf (Neg a) = rnf a

-- | Class to represent invertible values.
--
-- Must obey the double negation law: @not (not x) = x@
--
-- The negation appears only in leafs of normal forms, and the underlying proposition class
-- might have built-in negation, thus we use 'Negable'.
class Negable x where
  -- | Invert the value.
  not :: x -> x

instance Negable (Neg a) where
  not (Pos x)  = Neg x
  not (Neg x)  = Pos x

instance Negable Bool where
  not = P.not

instance Monoid m => Negable (Maybe m) where
  not (Just _)  = Nothing
  not Nothing   = Just mempty

instance (Negable a, Negable b) => Negable (a, b) where
  not (x, y) = (not x, not y)

instance (Negable a, Negable b) => Negable (Either a b) where
  not (Left x)  = Left $ not x
  not (Right y) = Right $ not y