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

module Rerefined.Predicate.Logical.And where

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

-- | Logical conjunction. Also AND logic gate.
data And l r

-- | Precedence of 3 (matching 'Data.Bool.&&').
instance (Predicate l, Predicate r) => Predicate (And l r) where
    type PredicateName d (And l r) = PredicateNameBOp " ∧ " 3 d l r

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

-- | Take just the left predicate from an 'And'.
rerefineAndL :: Refined (And l r) a -> Refined l a
rerefineAndL :: forall {k} {k} (l :: k) (r :: k) a.
Refined (And l r) a -> Refined l a
rerefineAndL = Refined (And l r) a -> Refined l a
forall {k1} {k2} (pNew :: k1) (pOld :: k2) a.
Refined pOld a -> Refined pNew a
unsafeRerefine

-- | Take just the right predicate from an 'And'.
rerefineAndR :: Refined (And l r) a -> Refined r a
rerefineAndR :: forall {k} {k} (l :: k) (r :: k) a.
Refined (And l r) a -> Refined r a
rerefineAndR = Refined (And l r) a -> Refined r a
forall {k1} {k2} (pNew :: k1) (pOld :: k2) a.
Refined pOld a -> Refined pNew a
unsafeRerefine

-- | Eliminate an 'And' by applying the left predicate, then the right.
eliminateAndLR :: Refined (And l r) a -> Refined r (Refined l a)
eliminateAndLR :: forall {k} {k} (l :: k) (r :: k) a.
Refined (And l r) a -> Refined r (Refined l a)
eliminateAndLR = Refined l a -> Refined r (Refined l a)
forall {k} a (p :: k). a -> Refined p a
unsafeRefine (Refined l a -> Refined r (Refined l a))
-> (Refined (And l r) a -> Refined l a)
-> Refined (And l r) a
-> Refined r (Refined l a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Refined l a
forall {k} a (p :: k). a -> Refined p a
unsafeRefine (a -> Refined l a)
-> (Refined (And l r) a -> a) -> Refined (And l r) a -> Refined l a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined (And l r) a -> a
forall {k} (p :: k) a. Refined p a -> a
unrefine

-- | Eliminate an 'And' by applying the right predicate, then the left.
eliminateAndRL :: Refined (And l r) a -> Refined l (Refined r a)
eliminateAndRL :: forall {k} {k} (l :: k) (r :: k) a.
Refined (And l r) a -> Refined l (Refined r a)
eliminateAndRL = Refined r a -> Refined l (Refined r a)
forall {k} a (p :: k). a -> Refined p a
unsafeRefine (Refined r a -> Refined l (Refined r a))
-> (Refined (And l r) a -> Refined r a)
-> Refined (And l r) a
-> Refined l (Refined r a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Refined r a
forall {k} a (p :: k). a -> Refined p a
unsafeRefine (a -> Refined r a)
-> (Refined (And l r) a -> a) -> Refined (And l r) a -> Refined r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined (And l r) a -> a
forall {k} (p :: k) a. Refined p a -> a
unrefine

-- | Introduce an 'And' given a double-'Refined'. Inner is left.
introduceAndLR :: Refined r (Refined l a) -> Refined (And l r) a
introduceAndLR :: forall {k} {k} (r :: k) (l :: k) a.
Refined r (Refined l a) -> Refined (And l r) a
introduceAndLR = a -> Refined (And l r) a
forall {k} a (p :: k). a -> Refined p a
unsafeRefine (a -> Refined (And l r) a)
-> (Refined r (Refined l a) -> a)
-> Refined r (Refined l a)
-> Refined (And l r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined l a -> a
forall {k} (p :: k) a. Refined p a -> a
unrefine (Refined l a -> a)
-> (Refined r (Refined l a) -> Refined l a)
-> Refined r (Refined l a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined r (Refined l a) -> Refined l a
forall {k} (p :: k) a. Refined p a -> a
unrefine

-- | Introduce an 'And' given a double-'Refined'. Inner is right.
introduceAndRL :: Refined l (Refined r a) -> Refined (And l r) a
introduceAndRL :: forall {k} {k} (l :: k) (r :: k) a.
Refined l (Refined r a) -> Refined (And l r) a
introduceAndRL = a -> Refined (And l r) a
forall {k} a (p :: k). a -> Refined p a
unsafeRefine (a -> Refined (And l r) a)
-> (Refined l (Refined r a) -> a)
-> Refined l (Refined r a)
-> Refined (And l r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined r a -> a
forall {k} (p :: k) a. Refined p a -> a
unrefine (Refined r a -> a)
-> (Refined l (Refined r a) -> Refined r a)
-> Refined l (Refined r a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined l (Refined r a) -> Refined r a
forall {k} (p :: k) a. Refined p a -> a
unrefine