-- | This module provides an implementation of the
-- 'Refined.Extras.Polymorphism.ImpliesBool' type family at the term
-- level, to facilitate testing the algorithm.
--
-- @since 0.1.0.0
module Refined.Extras.Polymorphism.Internal.Terms
  ( Calculus (..),
    impliesBool,
    toCNF,
    isCNF,
  )
where

-- | @since 0.1.0.0
data Calculus a
  = CAtom a
  | CNot !(Calculus a)
  | CAnd !(Calculus a) !(Calculus a)
  | COr !(Calculus a) !(Calculus a)
  | CXor !(Calculus a) !(Calculus a)
  deriving stock (Int -> Calculus a -> ShowS
[Calculus a] -> ShowS
Calculus a -> String
(Int -> Calculus a -> ShowS)
-> (Calculus a -> String)
-> ([Calculus a] -> ShowS)
-> Show (Calculus a)
forall a. Show a => Int -> Calculus a -> ShowS
forall a. Show a => [Calculus a] -> ShowS
forall a. Show a => Calculus a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Calculus a -> ShowS
showsPrec :: Int -> Calculus a -> ShowS
$cshow :: forall a. Show a => Calculus a -> String
show :: Calculus a -> String
$cshowList :: forall a. Show a => [Calculus a] -> ShowS
showList :: [Calculus a] -> ShowS
Show)

-- | @since 0.1.0.0
instance (Eq a) => Eq (Calculus a) where
  CAtom a
x == :: Calculus a -> Calculus a -> Bool
== CAtom a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
  CNot Calculus a
x == CNot Calculus a
y = Calculus a
x Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y
  CAnd Calculus a
x1 Calculus a
x2 == CAnd Calculus a
y1 Calculus a
y2 = (Calculus a
x1 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y1) Bool -> Bool -> Bool
&& (Calculus a
x2 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y2) Bool -> Bool -> Bool
|| (Calculus a
x1 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y2) Bool -> Bool -> Bool
&& (Calculus a
x2 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y1)
  COr Calculus a
x1 Calculus a
x2 == COr Calculus a
y1 Calculus a
y2 = (Calculus a
x1 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y1) Bool -> Bool -> Bool
&& (Calculus a
x2 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y2) Bool -> Bool -> Bool
|| (Calculus a
x1 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y2) Bool -> Bool -> Bool
&& (Calculus a
x2 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y1)
  CXor Calculus a
x1 Calculus a
x2 == CXor Calculus a
y1 Calculus a
y2 = (Calculus a
x1 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y1) Bool -> Bool -> Bool
&& (Calculus a
x2 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y2) Bool -> Bool -> Bool
|| (Calculus a
x1 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y2) Bool -> Bool -> Bool
&& (Calculus a
x2 Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
y1)
  Calculus a
_ == Calculus a
_ = Bool
False

infixr 3 `CAnd`

infixr 2 `COr`

infixr 2 `CXor`

-- | @since 0.1.0.0
impliesBool :: (Eq a) => Calculus a -> Calculus a -> Bool
impliesBool :: forall a. Eq a => Calculus a -> Calculus a -> Bool
impliesBool Calculus a
q Calculus a
p
  | Calculus a
q Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
p = Bool
True
  | Bool
otherwise = Calculus a -> Calculus a -> Bool
forall a. Eq a => Calculus a -> Calculus a -> Bool
impliesCNF (Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
toCNF Calculus a
q) (Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
toCNF Calculus a
p)

-- | @since 0.1.0.0
impliesCNF :: (Eq a) => Calculus a -> Calculus a -> Bool
impliesCNF :: forall a. Eq a => Calculus a -> Calculus a -> Bool
impliesCNF Calculus a
q Calculus a
p = Bool -> Calculus a -> Calculus a -> Bool
forall a. Eq a => Bool -> Calculus a -> Calculus a -> Bool
impliesCNFHelper (Calculus a
q Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
p) Calculus a
q Calculus a
p

-- | @since 0.1.0.0
impliesCNFHelper :: (Eq a) => Bool -> Calculus a -> Calculus a -> Bool
impliesCNFHelper :: forall a. Eq a => Bool -> Calculus a -> Calculus a -> Bool
impliesCNFHelper Bool
True Calculus a
_ Calculus a
_ = Bool
True
impliesCNFHelper Bool
_ Calculus a
q Calculus a
p | Calculus a
q Calculus a -> Calculus a -> Bool
forall a. Eq a => a -> a -> Bool
== Calculus a
p = Bool
True
impliesCNFHelper Bool
_ (Calculus a
q `CAnd` Calculus a
r) Calculus a
p = Calculus a -> Calculus a -> Bool
forall a. Eq a => Calculus a -> Calculus a -> Bool
impliesCNF Calculus a
q Calculus a
p Bool -> Bool -> Bool
|| Calculus a -> Calculus a -> Bool
forall a. Eq a => Calculus a -> Calculus a -> Bool
impliesCNF Calculus a
r Calculus a
p
impliesCNFHelper Bool
_ (Calculus a
q `COr` Calculus a
r) Calculus a
p = Calculus a -> Calculus a -> Bool
forall a. Eq a => Calculus a -> Calculus a -> Bool
impliesCNF Calculus a
q Calculus a
p Bool -> Bool -> Bool
&& Calculus a -> Calculus a -> Bool
forall a. Eq a => Calculus a -> Calculus a -> Bool
impliesCNF Calculus a
r Calculus a
p
impliesCNFHelper Bool
_ Calculus a
_ Calculus a
_ = Bool
False

-- | @since 0.1.0.0
toCNF :: Calculus a -> Calculus a
toCNF :: forall a. Calculus a -> Calculus a
toCNF Calculus a
p = Bool -> Calculus a -> Calculus a
forall a. Bool -> Calculus a -> Calculus a
toCNFHelper (Calculus a -> Bool
forall a. Calculus a -> Bool
isCNF Calculus a
p) Calculus a
p

-- | @since 0.1.0.0
toCNFHelper :: Bool -> Calculus a -> Calculus a
toCNFHelper :: forall a. Bool -> Calculus a -> Calculus a
toCNFHelper Bool
True Calculus a
p = Calculus a
p
toCNFHelper Bool
False Calculus a
p = Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
toCNF (Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
reduce Calculus a
p)

-- | @since 0.1.0.0
isCNF :: Calculus a -> Bool
isCNF :: forall a. Calculus a -> Bool
isCNF (CNot (CAnd Calculus a
_ Calculus a
_)) = Bool
False
isCNF (CNot (COr Calculus a
_ Calculus a
_)) = Bool
False
isCNF (CNot (CXor Calculus a
_ Calculus a
_)) = Bool
False
isCNF (CNot (CNot Calculus a
_)) = Bool
False
isCNF (CNot Calculus a
_) = Bool
True
isCNF (COr (CAnd Calculus a
_ Calculus a
_) Calculus a
_) = Bool
False
isCNF (COr Calculus a
_ (CAnd Calculus a
_ Calculus a
_)) = Bool
False
isCNF (COr Calculus a
p Calculus a
q) = Calculus a -> Bool
forall a. Calculus a -> Bool
isCNF Calculus a
p Bool -> Bool -> Bool
&& Calculus a -> Bool
forall a. Calculus a -> Bool
isCNF Calculus a
q
isCNF (CXor Calculus a
_ Calculus a
_) = Bool
False
isCNF (CAnd Calculus a
p Calculus a
q) = Calculus a -> Bool
forall a. Calculus a -> Bool
isCNF Calculus a
p Bool -> Bool -> Bool
&& Calculus a -> Bool
forall a. Calculus a -> Bool
isCNF Calculus a
q
isCNF Calculus a
_ = Bool
True

-- | @since 0.1.0.0
reduce :: Calculus a -> Calculus a
-- Eliminate CXor
reduce :: forall a. Calculus a -> Calculus a
reduce (CXor Calculus a
p Calculus a
q) = (Calculus a
p Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`COr` Calculus a
q) Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`CAnd` (Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
CNot Calculus a
p Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`COr` Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
CNot Calculus a
q)
-- Double negation
reduce (CNot (CNot Calculus a
p)) = Calculus a
p
-- De Morgan's laws
reduce (CNot (COr Calculus a
p Calculus a
q)) = Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
CNot Calculus a
p Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`CAnd` Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
CNot Calculus a
q
reduce (CNot (CAnd Calculus a
p Calculus a
q)) = Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
CNot Calculus a
p Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`COr` Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
CNot Calculus a
q
-- Remaining CNot (i.e. CXor)
reduce (CNot Calculus a
p) = Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
CNot (Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
reduce Calculus a
p)
-- Distributive laws
reduce (COr (Calculus a
p `CAnd` Calculus a
q) Calculus a
r) = Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
CAnd (Calculus a
p Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`COr` Calculus a
r) (Calculus a
q Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`COr` Calculus a
r)
reduce (COr Calculus a
r (Calculus a
p `CAnd` Calculus a
q)) = Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
CAnd (Calculus a
r Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`COr` Calculus a
p) (Calculus a
r Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`COr` Calculus a
q)
-- Remaining COr, CAnd
reduce (Calculus a
p `COr` Calculus a
q) = Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
reduce Calculus a
p Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`COr` Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
reduce Calculus a
q
reduce (Calculus a
p `CAnd` Calculus a
q) = Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
reduce Calculus a
p Calculus a -> Calculus a -> Calculus a
forall a. Calculus a -> Calculus a -> Calculus a
`CAnd` Calculus a -> Calculus a
forall a. Calculus a -> Calculus a
reduce Calculus a
q
-- Base case, CNothing to reduce
reduce Calculus a
p = Calculus a
p