{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TemplateHaskell #-} module Satyros.CNF.Formula ( FormulaLike(Formula, FormulaLike) , Formula , clauseLikesOfFormulaLike , clausesOfFormula , maxVariableInFormula ) where import Control.Lens (Iso', _Wrapped, makeWrapped) import GHC.Generics (Generic, Generic1) import Satyros.CNF.Clause (Clause, ClauseLike, maxVariableInClause) import Satyros.CNF.Literal (Literal) import Satyros.CNF.Variable (Variable) newtype FormulaLike a = FormulaLike { FormulaLike a -> [ClauseLike a] _clausesOfFormula :: [ClauseLike a] } deriving stock ((forall x. FormulaLike a -> Rep (FormulaLike a) x) -> (forall x. Rep (FormulaLike a) x -> FormulaLike a) -> Generic (FormulaLike a) forall x. Rep (FormulaLike a) x -> FormulaLike a forall x. FormulaLike a -> Rep (FormulaLike a) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall a x. Rep (FormulaLike a) x -> FormulaLike a forall a x. FormulaLike a -> Rep (FormulaLike a) x $cto :: forall a x. Rep (FormulaLike a) x -> FormulaLike a $cfrom :: forall a x. FormulaLike a -> Rep (FormulaLike a) x Generic, (forall a. FormulaLike a -> Rep1 FormulaLike a) -> (forall a. Rep1 FormulaLike a -> FormulaLike a) -> Generic1 FormulaLike forall a. Rep1 FormulaLike a -> FormulaLike a forall a. FormulaLike a -> Rep1 FormulaLike a forall k (f :: k -> *). (forall (a :: k). f a -> Rep1 f a) -> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f $cto1 :: forall a. Rep1 FormulaLike a -> FormulaLike a $cfrom1 :: forall a. FormulaLike a -> Rep1 FormulaLike a Generic1) deriving newtype (Int -> FormulaLike a -> ShowS [FormulaLike a] -> ShowS FormulaLike a -> String (Int -> FormulaLike a -> ShowS) -> (FormulaLike a -> String) -> ([FormulaLike a] -> ShowS) -> Show (FormulaLike a) forall a. Show a => Int -> FormulaLike a -> ShowS forall a. Show a => [FormulaLike a] -> ShowS forall a. Show a => FormulaLike a -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [FormulaLike a] -> ShowS $cshowList :: forall a. Show a => [FormulaLike a] -> ShowS show :: FormulaLike a -> String $cshow :: forall a. Show a => FormulaLike a -> String showsPrec :: Int -> FormulaLike a -> ShowS $cshowsPrec :: forall a. Show a => Int -> FormulaLike a -> ShowS Show, b -> FormulaLike a -> FormulaLike a NonEmpty (FormulaLike a) -> FormulaLike a FormulaLike a -> FormulaLike a -> FormulaLike a (FormulaLike a -> FormulaLike a -> FormulaLike a) -> (NonEmpty (FormulaLike a) -> FormulaLike a) -> (forall b. Integral b => b -> FormulaLike a -> FormulaLike a) -> Semigroup (FormulaLike a) forall b. Integral b => b -> FormulaLike a -> FormulaLike a forall a. NonEmpty (FormulaLike a) -> FormulaLike a forall a. FormulaLike a -> FormulaLike a -> FormulaLike a forall a. (a -> a -> a) -> (NonEmpty a -> a) -> (forall b. Integral b => b -> a -> a) -> Semigroup a forall a b. Integral b => b -> FormulaLike a -> FormulaLike a stimes :: b -> FormulaLike a -> FormulaLike a $cstimes :: forall a b. Integral b => b -> FormulaLike a -> FormulaLike a sconcat :: NonEmpty (FormulaLike a) -> FormulaLike a $csconcat :: forall a. NonEmpty (FormulaLike a) -> FormulaLike a <> :: FormulaLike a -> FormulaLike a -> FormulaLike a $c<> :: forall a. FormulaLike a -> FormulaLike a -> FormulaLike a Semigroup, Semigroup (FormulaLike a) FormulaLike a Semigroup (FormulaLike a) -> FormulaLike a -> (FormulaLike a -> FormulaLike a -> FormulaLike a) -> ([FormulaLike a] -> FormulaLike a) -> Monoid (FormulaLike a) [FormulaLike a] -> FormulaLike a FormulaLike a -> FormulaLike a -> FormulaLike a forall a. Semigroup (FormulaLike a) forall a. FormulaLike a forall a. Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a forall a. [FormulaLike a] -> FormulaLike a forall a. FormulaLike a -> FormulaLike a -> FormulaLike a mconcat :: [FormulaLike a] -> FormulaLike a $cmconcat :: forall a. [FormulaLike a] -> FormulaLike a mappend :: FormulaLike a -> FormulaLike a -> FormulaLike a $cmappend :: forall a. FormulaLike a -> FormulaLike a -> FormulaLike a mempty :: FormulaLike a $cmempty :: forall a. FormulaLike a $cp1Monoid :: forall a. Semigroup (FormulaLike a) Monoid) makeWrapped ''FormulaLike type Formula = FormulaLike Literal pattern Formula :: [Clause] -> Formula pattern $bFormula :: [Clause] -> Formula $mFormula :: forall r. Formula -> ([Clause] -> r) -> (Void# -> r) -> r Formula v = FormulaLike v {-# COMPLETE Formula #-} clauseLikesOfFormulaLike :: Iso' (FormulaLike a) [ClauseLike a] clauseLikesOfFormulaLike :: p [ClauseLike a] (f [ClauseLike a]) -> p (FormulaLike a) (f (FormulaLike a)) clauseLikesOfFormulaLike = p [ClauseLike a] (f [ClauseLike a]) -> p (FormulaLike a) (f (FormulaLike a)) forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t) _Wrapped {-# INLINE clauseLikesOfFormulaLike #-} clausesOfFormula :: Iso' Formula [Clause] clausesOfFormula :: p [Clause] (f [Clause]) -> p Formula (f Formula) clausesOfFormula = p [Clause] (f [Clause]) -> p Formula (f Formula) forall a. Iso' (FormulaLike a) [ClauseLike a] clauseLikesOfFormulaLike {-# INLINE clausesOfFormula #-} maxVariableInFormula :: Formula -> Variable maxVariableInFormula :: Formula -> Variable maxVariableInFormula = [Variable] -> Variable forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a maximum ([Variable] -> Variable) -> (Formula -> [Variable]) -> Formula -> Variable forall b c a. (b -> c) -> (a -> b) -> a -> c . (Clause -> Variable) -> [Clause] -> [Variable] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Clause -> Variable maxVariableInClause ([Clause] -> [Variable]) -> (Formula -> [Clause]) -> Formula -> [Variable] forall b c a. (b -> c) -> (a -> b) -> a -> c . Formula -> [Clause] forall a. FormulaLike a -> [ClauseLike a] _clausesOfFormula {-# INLINE maxVariableInFormula #-}