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

module Rerefined.Predicate.Logical.Iff where

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

-- | Logical biconditional ("if and only if"). Also the XNOR logic gate, or
--   equivalence (loosely).
data Iff l r

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

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