{-# 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 #-}