{-# LANGUAGE AllowAmbiguousTypes #-}

module Rerefined.Predicate.Logical where

import Rerefined.Predicate.Common
import Rerefined.Refined
import Rerefined.Refine.Unsafe

-- | Logical binary operator.
--
-- No need to disambiguate that these are binary operators, because there's only
-- one logical unary operator 'Not'.
data LogicOp = And | Or | Nand | Nor | Xor | Xnor

-- | A logical binary operation on two predicates.
data Logical (op :: LogicOp) l r

-- TODO could do whatever we want here e.g. infix. (but idk what e.g. XNOR uses)
instance (Predicate l, Predicate r, ReifyLogicOp op)
  => Predicate (Logical op l r) where
    predicateName :: Proxy# (Logical op l r) -> Int -> ShowS
predicateName Proxy# (Logical op l r)
_ Int
d = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
          String -> ShowS
showString String
"Logical "
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString (forall (op :: LogicOp). ReifyLogicOp op => String
reifyLogicOpPretty @op) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy# l -> Int -> ShowS
forall {k} (p :: k). Predicate p => Proxy# p -> Int -> ShowS
predicateName (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @l) Int
11 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy# r -> Int -> ShowS
forall {k} (p :: k). Predicate p => Proxy# p -> Int -> ShowS
predicateName (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @r) Int
11

instance (Refine l a, Refine r a, ReifyLogicOp op)
  => Refine (Logical op l r) a where
    validate :: Proxy# (Logical op l r) -> a -> Maybe (RefineFailure String)
validate Proxy# (Logical op l r)
p a
a =
        forall (op :: LogicOp) a.
ReifyLogicOp op =>
(String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
reifyLogicOp @op (Proxy# (Logical op l r)
-> String -> [RefineFailure String] -> Maybe (RefineFailure String)
forall {k} (p :: k).
Predicate p =>
Proxy# p
-> String -> [RefineFailure String] -> Maybe (RefineFailure String)
validateFail Proxy# (Logical op l r)
p)
            (Proxy# l -> a -> Maybe (RefineFailure String)
forall {k} (p :: k) a.
Refine p a =>
Proxy# p -> a -> Maybe (RefineFailure String)
validate (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @l) a
a)
            (Proxy# r -> a -> Maybe (RefineFailure String)
forall {k} (p :: k) a.
Refine p a =>
Proxy# p -> a -> Maybe (RefineFailure String)
validate (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @r) a
a)

-- | Reify a logical binary operator type tag.
class ReifyLogicOp (op :: LogicOp) where
    reifyLogicOpPretty :: String
    reifyLogicOp
        :: (String -> [a] -> Maybe a)
        -> Maybe a
        -> Maybe a
        -> Maybe a

instance ReifyLogicOp And where
    reifyLogicOpPretty :: String
reifyLogicOpPretty = String
"And"
    reifyLogicOp :: forall a.
(String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
reifyLogicOp String -> [a] -> Maybe a
fFail Maybe a
l Maybe a
r =
        case Maybe a
l of
          Maybe a
Nothing ->
            case Maybe a
r of
              Maybe a
Nothing -> Maybe a
forall a. Maybe a
Nothing
              Just a
er -> String -> [a] -> Maybe a
fFail String
"AND:  right failed"    [    a
er]
          Just a
el ->
            case Maybe a
r of
              Maybe a
Nothing -> String -> [a] -> Maybe a
fFail String
"AND:   left failed"    [a
el    ]
              Just a
er -> String -> [a] -> Maybe a
fFail String
"AND:    l&r failed"    [a
el, a
er]

instance ReifyLogicOp Or where
    reifyLogicOpPretty :: String
reifyLogicOpPretty = String
"Or"
    reifyLogicOp :: forall a.
(String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
reifyLogicOp String -> [a] -> Maybe a
fFail Maybe a
l Maybe a
r =
        case Maybe a
l of
          Maybe a
Nothing -> Maybe a
forall a. Maybe a
Nothing
          Just a
el ->
            case Maybe a
r of
              Maybe a
Nothing -> Maybe a
forall a. Maybe a
Nothing
              Just a
er -> String -> [a] -> Maybe a
fFail String
"OR:     l&r failed"    [a
el, a
er]

instance ReifyLogicOp Nand where
    reifyLogicOpPretty :: String
reifyLogicOpPretty = String
"Nand"
    reifyLogicOp :: forall a.
(String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
reifyLogicOp String -> [a] -> Maybe a
fFail Maybe a
l Maybe a
r =
        case Maybe a
l of
          Just a
_  -> Maybe a
forall a. Maybe a
Nothing
          Maybe a
Nothing ->
            case Maybe a
r of
              Just a
_  -> Maybe a
forall a. Maybe a
Nothing
              Maybe a
Nothing -> String -> [a] -> Maybe a
fFail String
"NAND:   l&r succeeded" [      ]

instance ReifyLogicOp Nor where
    reifyLogicOpPretty :: String
reifyLogicOpPretty = String
"Nor"
    reifyLogicOp :: forall a.
(String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
reifyLogicOp String -> [a] -> Maybe a
fFail Maybe a
l Maybe a
r =
        case Maybe a
l of
          Just a
el ->
            case Maybe a
r of
              Just a
_  -> Maybe a
forall a. Maybe a
Nothing
              Maybe a
Nothing -> String -> [a] -> Maybe a
fFail String
"NOR:  right succeeded" [a
el    ]
          Maybe a
Nothing ->
            case Maybe a
r of
              Just a
er -> String -> [a] -> Maybe a
fFail String
"NOR:   left succeeded" [    a
er]
              Maybe a
Nothing -> String -> [a] -> Maybe a
fFail String
"NOR:    l&r succeeded" [      ]

instance ReifyLogicOp Xor where
    reifyLogicOpPretty :: String
reifyLogicOpPretty = String
"Xor"
    reifyLogicOp :: forall a.
(String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
reifyLogicOp String -> [a] -> Maybe a
fFail Maybe a
l Maybe a
r =
        case Maybe a
l of
          Maybe a
Nothing ->
            case Maybe a
r of
              Just a
_  -> Maybe a
forall a. Maybe a
Nothing
              Maybe a
Nothing -> String -> [a] -> Maybe a
fFail String
"XOR:    l&r succeeded" [      ]
          Just a
el ->
            case Maybe a
r of
              Maybe a
Nothing -> Maybe a
forall a. Maybe a
Nothing
              Just a
er -> String -> [a] -> Maybe a
fFail String
"XOR:    l&r failed"    [a
el, a
er]

instance ReifyLogicOp Xnor where
    reifyLogicOpPretty :: String
reifyLogicOpPretty = String
"Xnor"
    reifyLogicOp :: forall a.
(String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
reifyLogicOp String -> [a] -> Maybe a
fFail Maybe a
l Maybe a
r =
        case Maybe a
l of
          Maybe a
Nothing ->
            case Maybe a
r of
              Maybe a
Nothing -> Maybe a
forall a. Maybe a
Nothing
              Just a
er -> String -> [a] -> Maybe a
fFail String
"XNOR: right failed"    [    a
er]
          Just a
el ->
            case Maybe a
r of
              Just a
_  -> Maybe a
forall a. Maybe a
Nothing
              Maybe a
Nothing -> String -> [a] -> Maybe a
fFail String
"XNOR:  left failed"    [a
el    ]

data Not p

instance Predicate p => Predicate (Not p) where
    predicateName :: Proxy# (Not p) -> Int -> ShowS
predicateName Proxy# (Not p)
_ = forall (p :: k). Predicate p => String -> Int -> ShowS
forall {k} (p :: k). Predicate p => String -> Int -> ShowS
predicateName1 @p String
"Not"

instance Refine p a => Refine (Not p) a where
    validate :: Proxy# (Not p) -> a -> Maybe (RefineFailure String)
validate Proxy# (Not p)
p a
a =
        case Proxy# p -> a -> Maybe (RefineFailure String)
forall {k} (p :: k) a.
Refine p a =>
Proxy# p -> a -> Maybe (RefineFailure String)
validate (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @p) a
a of
          Just RefineFailure String
_  -> Maybe (RefineFailure String)
forall a. Maybe a
Nothing
          Maybe (RefineFailure String)
Nothing -> Proxy# (Not p)
-> String -> [RefineFailure String] -> Maybe (RefineFailure String)
forall {k} (p :: k).
Predicate p =>
Proxy# p
-> String -> [RefineFailure String] -> Maybe (RefineFailure String)
validateFail Proxy# (Not p)
p String
"NOT: predicate succeeded" []

-- TODO principle of explosion? (p and not p -> anything)

-- TODO
rerefineDeMorgans1
    :: Refined (Not (Logical Or  l r))       a
    -> Refined (Logical And (Not l) (Not r)) a
rerefineDeMorgans1 :: forall {k} {k} (l :: k) (r :: k) a.
Refined (Not (Logical 'Or l r)) a
-> Refined (Logical 'And (Not l) (Not r)) a
rerefineDeMorgans1 = Refined (Not (Logical 'Or l r)) a
-> Refined (Logical 'And (Not l) (Not r)) a
forall {k1} {k2} (pNew :: k1) (pOld :: k2) a.
Refined pOld a -> Refined pNew a
unsafeRerefine

-- TODO
rerefineDeMorgans2
    :: Refined (Not (Logical And l r))       a
    -> Refined (Logical Or  (Not l) (Not r)) a
rerefineDeMorgans2 :: forall {k} {k} (l :: k) (r :: k) a.
Refined (Not (Logical 'And l r)) a
-> Refined (Logical 'Or (Not l) (Not r)) a
rerefineDeMorgans2 = Refined (Not (Logical 'And l r)) a
-> Refined (Logical 'Or (Not l) (Not r)) a
forall {k1} {k2} (pNew :: k1) (pOld :: k2) a.
Refined pOld a -> Refined pNew a
unsafeRerefine