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

module Rerefined.Predicate.Logical.Xor where

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

-- | Logical exclusive disjunction. Also XOR logic gate.
data Xor l r

-- | Precedence of 4 (matching '==').
instance (Predicate l, Predicate r) => Predicate (Xor l r) where
    type PredicateName d (Xor l r) = PredicateNameBOp " ⊕ " 4 d l r

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