{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName
{-# LANGUAGE OverloadedStrings #-} -- for builder

module Rerefined.Predicate.Logical.Not where

import Rerefined.Predicate.Common
import TypeLevelShow.Utils

-- | Logical negation. Also NOT logic gate, or logical complement.
data Not p

-- | Precedence of 9 (one below function application).
instance Predicate p => Predicate (Not p) where
    type PredicateName d (Not p) = ShowParen (d > 9)
        ("¬ " ++ PredicateName 10 p)

instance (Refine p a, KnownPredicateName (Not p))
  => Refine (Not p) a where
    validate :: Proxy# (Not p) -> a -> Maybe RefineFailure
validate Proxy# (Not p)
p a
a =
        case Proxy# p -> a -> Maybe RefineFailure
forall {k} (p :: k) a.
Refine p a =>
Proxy# p -> a -> Maybe RefineFailure
validate (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @p) a
a of
          Just RefineFailure
_  -> Maybe RefineFailure
forall a. Maybe a
Nothing
          Maybe RefineFailure
Nothing -> Proxy# (Not p) -> Builder -> [RefineFailure] -> Maybe RefineFailure
forall {k} (p :: k).
(Predicate p, KnownPredicateName p) =>
Proxy# p -> Builder -> [RefineFailure] -> Maybe RefineFailure
validateFail Proxy# (Not p)
p Builder
"NOT: predicate succeeded" []