rerefined-0.3.0: src/Rerefined/Predicate/Logical/Nor.hs

{-# 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

-- | Precendence 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 p a =
        case l of
          Just _ ->
            case r of
              Just _  -> Nothing
              Nothing -> validateFail p "NOR: left succeeded"  []
          Nothing ->
            case r of
              Just _  -> validateFail p "NOR: right succeeded" []
              Nothing -> validateFail p "NOR: l&r succeeded"   []
      where
        l = validate (proxy# @l) a
        r = validate (proxy# @r) a