{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns    #-}
module Satyros.CNF.Literal
  ( Literal(Literal)
  , negateLiteral
  , literalToVariable
  , literalToPositivity
  ) where

import           Control.Lens           ((#))
import           GHC.Generics           (Generic)
import           Satyros.CNF.Positivity (Positivity (Negative, Positive),
                                         isPositive)
import           Satyros.CNF.Variable   (Variable (Variable))
import           Satyros.Util           (intToWord, wordToInt)

newtype Literal = LiteralInternal Int
  deriving stock ((forall x. Literal -> Rep Literal x)
-> (forall x. Rep Literal x -> Literal) -> Generic Literal
forall x. Rep Literal x -> Literal
forall x. Literal -> Rep Literal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Literal x -> Literal
$cfrom :: forall x. Literal -> Rep Literal x
Generic, Literal -> Literal -> Bool
(Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool) -> Eq Literal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Literal -> Literal -> Bool
$c/= :: Literal -> Literal -> Bool
== :: Literal -> Literal -> Bool
$c== :: Literal -> Literal -> Bool
Eq, Eq Literal
Eq Literal
-> (Literal -> Literal -> Ordering)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Literal)
-> (Literal -> Literal -> Literal)
-> Ord Literal
Literal -> Literal -> Bool
Literal -> Literal -> Ordering
Literal -> Literal -> Literal
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Literal -> Literal -> Literal
$cmin :: Literal -> Literal -> Literal
max :: Literal -> Literal -> Literal
$cmax :: Literal -> Literal -> Literal
>= :: Literal -> Literal -> Bool
$c>= :: Literal -> Literal -> Bool
> :: Literal -> Literal -> Bool
$c> :: Literal -> Literal -> Bool
<= :: Literal -> Literal -> Bool
$c<= :: Literal -> Literal -> Bool
< :: Literal -> Literal -> Bool
$c< :: Literal -> Literal -> Bool
compare :: Literal -> Literal -> Ordering
$ccompare :: Literal -> Literal -> Ordering
$cp1Ord :: Eq Literal
Ord)
  deriving newtype (Int -> Literal -> ShowS
[Literal] -> ShowS
Literal -> String
(Int -> Literal -> ShowS)
-> (Literal -> String) -> ([Literal] -> ShowS) -> Show Literal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Literal] -> ShowS
$cshowList :: [Literal] -> ShowS
show :: Literal -> String
$cshow :: Literal -> String
showsPrec :: Int -> Literal -> ShowS
$cshowsPrec :: Int -> Literal -> ShowS
Show)

pattern Literal :: Positivity -> Variable -> Literal
pattern $bLiteral :: Positivity -> Variable -> Literal
$mLiteral :: forall r.
Literal -> (Positivity -> Variable -> r) -> (Void# -> r) -> r
Literal a b <- (matchLiteral -> (a, b)) where
  Literal Positivity
Positive (Variable Word
b) = Int -> Literal
LiteralInternal (Word -> Int
wordToInt Word
b)
  Literal Positivity
Negative (Variable Word
b) = Int -> Literal
LiteralInternal (- Word -> Int
wordToInt Word
b)
{-# COMPLETE Literal #-}

matchLiteral :: Literal -> (Positivity, Variable)
matchLiteral :: Literal -> (Positivity, Variable)
matchLiteral Literal
l = (Literal -> Positivity
literalToPositivity Literal
l, Literal -> Variable
literalToVariable Literal
l)
{-# INLINE matchLiteral #-}

negateLiteral :: Literal -> Literal
negateLiteral :: Literal -> Literal
negateLiteral (LiteralInternal Int
n) = Int -> Literal
LiteralInternal (- Int
n)
{-# INLINE negateLiteral #-}

literalToVariable :: Literal -> Variable
literalToVariable :: Literal -> Variable
literalToVariable (LiteralInternal Int
n) = Word -> Variable
Variable (Int -> Word
intToWord (Int -> Int
forall a. Num a => a -> a
abs Int
n))
{-# INLINE literalToVariable #-}

literalToPositivity :: Literal -> Positivity
literalToPositivity :: Literal -> Positivity
literalToPositivity (LiteralInternal Int
n) = Tagged Bool (Identity Bool)
-> Tagged Positivity (Identity Positivity)
Iso' Positivity Bool
isPositive (Tagged Bool (Identity Bool)
 -> Tagged Positivity (Identity Positivity))
-> Bool -> Positivity
forall t b. AReview t b -> b -> t
# (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0)
{-# INLINE literalToPositivity #-}