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

module Rerefined.Predicate.Logical.Nand where

import Rerefined.Predicate.Common.Binary
import Rerefined.Predicate.Common

-- | NAND logic gate. Also called the Sheffer stroke, or non-conjunction.
data Nand l r

-- | Precedence of 3 (matching 'Data.Bool.&&').
instance (Predicate l, Predicate r) => Predicate (Nand l r) where
    type PredicateName d (Nand l r) = PredicateNameBOp " ⊼ " 3 d l r

instance (Refine l a, Refine r a, KnownPredicateName (Nand l r))
  => Refine (Nand l r) a where
    validate :: Proxy# (Nand l r) -> a -> Maybe RefineFailure
validate Proxy# (Nand l r)
p a
a =
        case Maybe RefineFailure
l of
          Just RefineFailure
_  -> Maybe RefineFailure
forall a. Maybe a
Nothing
          Maybe RefineFailure
Nothing ->
            case Maybe RefineFailure
r of
              Just RefineFailure
_  -> Maybe RefineFailure
forall a. Maybe a
Nothing
              Maybe RefineFailure
Nothing -> Proxy# (Nand l r)
-> Builder -> [RefineFailure] -> Maybe RefineFailure
forall {k} (p :: k).
(Predicate p, KnownPredicateName p) =>
Proxy# p -> Builder -> [RefineFailure] -> Maybe RefineFailure
validateFail Proxy# (Nand l r)
p Builder
"NAND: l&r succeeded" []
      where
        l :: Maybe RefineFailure
l = Proxy# l -> 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# @l) a
a
        r :: Maybe RefineFailure
r = Proxy# r -> 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# @r) a
a