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

module Rerefined.Predicate.Logical.Nor where

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

-- | NOR logic gate. Also called non-disjunction, or joint denial.
data Nor l r

-- | Precedence of 2 (matching 'Data.Bool.||').
instance (Predicate l, Predicate r) => Predicate (Nor l r) where
    type PredicateName d (Nor l r) = PredicateNameBOp " ⊽ " 2 d l r

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