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

module Rerefined.Predicate.Logical.If where

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

-- | Logical implication. "If l then r".
data If l r

-- | Precedence of 4 (matching '==').
instance (Predicate l, Predicate r) => Predicate (If l r) where
    -- TODO double arrow? idk
    type PredicateName d (If l r) = PredicateNameBOp " → " 4 d l r

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