module Data.Logic.Classes.Negate
     ( Negatable(..)
     , negated
     , (.~.)
     , (¬)
     , negative
     , positive
     ) where

-- |The class of formulas that can be negated.  There are some types
-- that can be negated but do not support the other Boolean Logic
-- operators, such as the 'Literal' class.
class Negatable formula where
    -- | Negate a formula in a naive fashion, the operators below
    -- prevent double negation.
    negatePrivate :: formula -> formula
    -- | Test whether a formula is negated or normal
    foldNegation :: (formula -> r) -- ^ called for normal formulas
                 -> (formula -> r) -- ^ called for negated formulas
                 -> formula -> r
-- | Is this formula negated at the top level?
negated :: Negatable formula => formula -> Bool
negated = foldNegation (const False) (not . negated)

-- | Negate the formula, avoiding double negation
(.~.) :: Negatable formula => formula -> formula
(.~.) = foldNegation negatePrivate id

(¬) :: Negatable formula => formula -> formula
(¬) = (.~.)

infix 5 .~., ¬

-- ------------------------------------------------------------------------- 
-- Some operations on literals.  (These names are used in Harrison's code.)
-- ------------------------------------------------------------------------- 

negative :: Negatable formula => formula -> Bool
negative = negated

positive :: Negatable formula => formula -> Bool
positive = not . negative