{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} module Distribution.Types.Condition ( Condition(..), cNot, cAnd, cOr, simplifyCondition, ) where import Prelude () import Distribution.Compat.Prelude -- | A boolean expression parameterized over the variable type used. data Condition c = Var c | Lit Bool | CNot (Condition c) | COr (Condition c) (Condition c) | CAnd (Condition c) (Condition c) deriving (Int -> Condition c -> ShowS [Condition c] -> ShowS Condition c -> String (Int -> Condition c -> ShowS) -> (Condition c -> String) -> ([Condition c] -> ShowS) -> Show (Condition c) forall c. Show c => Int -> Condition c -> ShowS forall c. Show c => [Condition c] -> ShowS forall c. Show c => Condition c -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Condition c] -> ShowS $cshowList :: forall c. Show c => [Condition c] -> ShowS show :: Condition c -> String $cshow :: forall c. Show c => Condition c -> String showsPrec :: Int -> Condition c -> ShowS $cshowsPrec :: forall c. Show c => Int -> Condition c -> ShowS Show, Condition c -> Condition c -> Bool (Condition c -> Condition c -> Bool) -> (Condition c -> Condition c -> Bool) -> Eq (Condition c) forall c. Eq c => Condition c -> Condition c -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Condition c -> Condition c -> Bool $c/= :: forall c. Eq c => Condition c -> Condition c -> Bool == :: Condition c -> Condition c -> Bool $c== :: forall c. Eq c => Condition c -> Condition c -> Bool Eq, Typeable, Typeable (Condition c) DataType Constr Typeable (Condition c) -> (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Condition c -> c (Condition c)) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Condition c)) -> (Condition c -> Constr) -> (Condition c -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Condition c))) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Condition c))) -> ((forall b. Data b => b -> b) -> Condition c -> Condition c) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Condition c -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Condition c -> r) -> (forall u. (forall d. Data d => d -> u) -> Condition c -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> Condition c -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Condition c -> m (Condition c)) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Condition c -> m (Condition c)) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Condition c -> m (Condition c)) -> Data (Condition c) Condition c -> DataType Condition c -> Constr (forall d. Data d => c (t d)) -> Maybe (c (Condition c)) (forall b. Data b => b -> b) -> Condition c -> Condition c (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Condition c -> c (Condition c) (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Condition c) forall c. Data c => Typeable (Condition c) forall c. Data c => Condition c -> DataType forall c. Data c => Condition c -> Constr forall c. Data c => (forall b. Data b => b -> b) -> Condition c -> Condition c forall c u. Data c => Int -> (forall d. Data d => d -> u) -> Condition c -> u forall c u. Data c => (forall d. Data d => d -> u) -> Condition c -> [u] forall c r r'. Data c => (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Condition c -> r forall c r r'. Data c => (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Condition c -> r forall c (m :: * -> *). (Data c, Monad m) => (forall d. Data d => d -> m d) -> Condition c -> m (Condition c) forall c (m :: * -> *). (Data c, MonadPlus m) => (forall d. Data d => d -> m d) -> Condition c -> m (Condition c) forall c (c :: * -> *). Data c => (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Condition c) forall c (c :: * -> *). Data c => (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Condition c -> c (Condition c) forall c (t :: * -> *) (c :: * -> *). (Data c, Typeable t) => (forall d. Data d => c (t d)) -> Maybe (c (Condition c)) forall c (t :: * -> * -> *) (c :: * -> *). (Data c, Typeable t) => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Condition c)) forall a. Typeable a -> (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> Condition c -> u forall u. (forall d. Data d => d -> u) -> Condition c -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Condition c -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Condition c -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Condition c -> m (Condition c) forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Condition c -> m (Condition c) forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Condition c) forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Condition c -> c (Condition c) forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Condition c)) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Condition c)) $cCAnd :: Constr $cCOr :: Constr $cCNot :: Constr $cLit :: Constr $cVar :: Constr $tCondition :: DataType gmapMo :: (forall d. Data d => d -> m d) -> Condition c -> m (Condition c) $cgmapMo :: forall c (m :: * -> *). (Data c, MonadPlus m) => (forall d. Data d => d -> m d) -> Condition c -> m (Condition c) gmapMp :: (forall d. Data d => d -> m d) -> Condition c -> m (Condition c) $cgmapMp :: forall c (m :: * -> *). (Data c, MonadPlus m) => (forall d. Data d => d -> m d) -> Condition c -> m (Condition c) gmapM :: (forall d. Data d => d -> m d) -> Condition c -> m (Condition c) $cgmapM :: forall c (m :: * -> *). (Data c, Monad m) => (forall d. Data d => d -> m d) -> Condition c -> m (Condition c) gmapQi :: Int -> (forall d. Data d => d -> u) -> Condition c -> u $cgmapQi :: forall c u. Data c => Int -> (forall d. Data d => d -> u) -> Condition c -> u gmapQ :: (forall d. Data d => d -> u) -> Condition c -> [u] $cgmapQ :: forall c u. Data c => (forall d. Data d => d -> u) -> Condition c -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Condition c -> r $cgmapQr :: forall c r r'. Data c => (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Condition c -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Condition c -> r $cgmapQl :: forall c r r'. Data c => (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Condition c -> r gmapT :: (forall b. Data b => b -> b) -> Condition c -> Condition c $cgmapT :: forall c. Data c => (forall b. Data b => b -> b) -> Condition c -> Condition c dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Condition c)) $cdataCast2 :: forall c (t :: * -> * -> *) (c :: * -> *). (Data c, Typeable t) => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Condition c)) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Condition c)) $cdataCast1 :: forall c (t :: * -> *) (c :: * -> *). (Data c, Typeable t) => (forall d. Data d => c (t d)) -> Maybe (c (Condition c)) dataTypeOf :: Condition c -> DataType $cdataTypeOf :: forall c. Data c => Condition c -> DataType toConstr :: Condition c -> Constr $ctoConstr :: forall c. Data c => Condition c -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Condition c) $cgunfold :: forall c (c :: * -> *). Data c => (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Condition c) gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Condition c -> c (Condition c) $cgfoldl :: forall c (c :: * -> *). Data c => (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Condition c -> c (Condition c) $cp1Data :: forall c. Data c => Typeable (Condition c) Data, (forall x. Condition c -> Rep (Condition c) x) -> (forall x. Rep (Condition c) x -> Condition c) -> Generic (Condition c) forall x. Rep (Condition c) x -> Condition c forall x. Condition c -> Rep (Condition c) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall c x. Rep (Condition c) x -> Condition c forall c x. Condition c -> Rep (Condition c) x $cto :: forall c x. Rep (Condition c) x -> Condition c $cfrom :: forall c x. Condition c -> Rep (Condition c) x Generic) -- | Boolean negation of a 'Condition' value. cNot :: Condition a -> Condition a cNot :: Condition a -> Condition a cNot (Lit Bool b) = Bool -> Condition a forall c. Bool -> Condition c Lit (Bool -> Bool not Bool b) cNot (CNot Condition a c) = Condition a c cNot Condition a c = Condition a -> Condition a forall c. Condition c -> Condition c CNot Condition a c -- | Boolean AND of two 'Condtion' values. cAnd :: Condition a -> Condition a -> Condition a cAnd :: Condition a -> Condition a -> Condition a cAnd (Lit Bool False) Condition a _ = Bool -> Condition a forall c. Bool -> Condition c Lit Bool False cAnd Condition a _ (Lit Bool False) = Bool -> Condition a forall c. Bool -> Condition c Lit Bool False cAnd (Lit Bool True) Condition a x = Condition a x cAnd Condition a x (Lit Bool True) = Condition a x cAnd Condition a x Condition a y = Condition a -> Condition a -> Condition a forall c. Condition c -> Condition c -> Condition c CAnd Condition a x Condition a y -- | Boolean OR of two 'Condition' values. cOr :: Eq v => Condition v -> Condition v -> Condition v cOr :: Condition v -> Condition v -> Condition v cOr (Lit Bool True) Condition v _ = Bool -> Condition v forall c. Bool -> Condition c Lit Bool True cOr Condition v _ (Lit Bool True) = Bool -> Condition v forall c. Bool -> Condition c Lit Bool True cOr (Lit Bool False) Condition v x = Condition v x cOr Condition v x (Lit Bool False) = Condition v x cOr Condition v c (CNot Condition v d) | Condition v c Condition v -> Condition v -> Bool forall a. Eq a => a -> a -> Bool == Condition v d = Bool -> Condition v forall c. Bool -> Condition c Lit Bool True cOr (CNot Condition v c) Condition v d | Condition v c Condition v -> Condition v -> Bool forall a. Eq a => a -> a -> Bool == Condition v d = Bool -> Condition v forall c. Bool -> Condition c Lit Bool True cOr Condition v x Condition v y = Condition v -> Condition v -> Condition v forall c. Condition c -> Condition c -> Condition c COr Condition v x Condition v y instance Functor Condition where a -> b f fmap :: (a -> b) -> Condition a -> Condition b `fmap` Var a c = b -> Condition b forall c. c -> Condition c Var (a -> b f a c) a -> b _ `fmap` Lit Bool c = Bool -> Condition b forall c. Bool -> Condition c Lit Bool c a -> b f `fmap` CNot Condition a c = Condition b -> Condition b forall c. Condition c -> Condition c CNot ((a -> b) -> Condition a -> Condition b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap a -> b f Condition a c) a -> b f `fmap` COr Condition a c Condition a d = Condition b -> Condition b -> Condition b forall c. Condition c -> Condition c -> Condition c COr ((a -> b) -> Condition a -> Condition b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap a -> b f Condition a c) ((a -> b) -> Condition a -> Condition b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap a -> b f Condition a d) a -> b f `fmap` CAnd Condition a c Condition a d = Condition b -> Condition b -> Condition b forall c. Condition c -> Condition c -> Condition c CAnd ((a -> b) -> Condition a -> Condition b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap a -> b f Condition a c) ((a -> b) -> Condition a -> Condition b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap a -> b f Condition a d) instance Foldable Condition where a -> m f foldMap :: (a -> m) -> Condition a -> m `foldMap` Var a c = a -> m f a c a -> m _ `foldMap` Lit Bool _ = m forall a. Monoid a => a mempty a -> m f `foldMap` CNot Condition a c = (a -> m) -> Condition a -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap a -> m f Condition a c a -> m f `foldMap` COr Condition a c Condition a d = (a -> m) -> Condition a -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap a -> m f Condition a c m -> m -> m forall a. Monoid a => a -> a -> a `mappend` (a -> m) -> Condition a -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap a -> m f Condition a d a -> m f `foldMap` CAnd Condition a c Condition a d = (a -> m) -> Condition a -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap a -> m f Condition a c m -> m -> m forall a. Monoid a => a -> a -> a `mappend` (a -> m) -> Condition a -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap a -> m f Condition a d instance Traversable Condition where a -> f b f traverse :: (a -> f b) -> Condition a -> f (Condition b) `traverse` Var a c = b -> Condition b forall c. c -> Condition c Var (b -> Condition b) -> f b -> f (Condition b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b `fmap` a -> f b f a c a -> f b _ `traverse` Lit Bool c = Condition b -> f (Condition b) forall (f :: * -> *) a. Applicative f => a -> f a pure (Condition b -> f (Condition b)) -> Condition b -> f (Condition b) forall a b. (a -> b) -> a -> b $ Bool -> Condition b forall c. Bool -> Condition c Lit Bool c a -> f b f `traverse` CNot Condition a c = Condition b -> Condition b forall c. Condition c -> Condition c CNot (Condition b -> Condition b) -> f (Condition b) -> f (Condition b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b `fmap` (a -> f b) -> Condition a -> f (Condition b) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse a -> f b f Condition a c a -> f b f `traverse` COr Condition a c Condition a d = Condition b -> Condition b -> Condition b forall c. Condition c -> Condition c -> Condition c COr (Condition b -> Condition b -> Condition b) -> f (Condition b) -> f (Condition b -> Condition b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b `fmap` (a -> f b) -> Condition a -> f (Condition b) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse a -> f b f Condition a c f (Condition b -> Condition b) -> f (Condition b) -> f (Condition b) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> (a -> f b) -> Condition a -> f (Condition b) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse a -> f b f Condition a d a -> f b f `traverse` CAnd Condition a c Condition a d = Condition b -> Condition b -> Condition b forall c. Condition c -> Condition c -> Condition c CAnd (Condition b -> Condition b -> Condition b) -> f (Condition b) -> f (Condition b -> Condition b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b `fmap` (a -> f b) -> Condition a -> f (Condition b) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse a -> f b f Condition a c f (Condition b -> Condition b) -> f (Condition b) -> f (Condition b) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> (a -> f b) -> Condition a -> f (Condition b) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse a -> f b f Condition a d instance Applicative Condition where pure :: a -> Condition a pure = a -> Condition a forall c. c -> Condition c Var <*> :: Condition (a -> b) -> Condition a -> Condition b (<*>) = Condition (a -> b) -> Condition a -> Condition b forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b ap instance Monad Condition where return :: a -> Condition a return = a -> Condition a forall (f :: * -> *) a. Applicative f => a -> f a pure -- Terminating cases >>= :: Condition a -> (a -> Condition b) -> Condition b (>>=) (Lit Bool x) a -> Condition b _ = Bool -> Condition b forall c. Bool -> Condition c Lit Bool x (>>=) (Var a x) a -> Condition b f = a -> Condition b f a x -- Recursing cases (>>=) (CNot Condition a x ) a -> Condition b f = Condition b -> Condition b forall c. Condition c -> Condition c CNot (Condition a x Condition a -> (a -> Condition b) -> Condition b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= a -> Condition b f) (>>=) (COr Condition a x Condition a y) a -> Condition b f = Condition b -> Condition b -> Condition b forall c. Condition c -> Condition c -> Condition c COr (Condition a x Condition a -> (a -> Condition b) -> Condition b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= a -> Condition b f) (Condition a y Condition a -> (a -> Condition b) -> Condition b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= a -> Condition b f) (>>=) (CAnd Condition a x Condition a y) a -> Condition b f = Condition b -> Condition b -> Condition b forall c. Condition c -> Condition c -> Condition c CAnd (Condition a x Condition a -> (a -> Condition b) -> Condition b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= a -> Condition b f) (Condition a y Condition a -> (a -> Condition b) -> Condition b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= a -> Condition b f) instance Monoid (Condition a) where mempty :: Condition a mempty = Bool -> Condition a forall c. Bool -> Condition c Lit Bool False mappend :: Condition a -> Condition a -> Condition a mappend = Condition a -> Condition a -> Condition a forall a. Semigroup a => a -> a -> a (<>) instance Semigroup (Condition a) where <> :: Condition a -> Condition a -> Condition a (<>) = Condition a -> Condition a -> Condition a forall c. Condition c -> Condition c -> Condition c COr instance Alternative Condition where empty :: Condition a empty = Condition a forall a. Monoid a => a mempty <|> :: Condition a -> Condition a -> Condition a (<|>) = Condition a -> Condition a -> Condition a forall a. Monoid a => a -> a -> a mappend instance MonadPlus Condition where mzero :: Condition a mzero = Condition a forall a. Monoid a => a mempty mplus :: Condition a -> Condition a -> Condition a mplus = Condition a -> Condition a -> Condition a forall a. Monoid a => a -> a -> a mappend instance Binary c => Binary (Condition c) instance Structured c => Structured (Condition c) instance NFData c => NFData (Condition c) where rnf :: Condition c -> () rnf = Condition c -> () forall a. (Generic a, GNFData (Rep a)) => a -> () genericRnf -- | Simplify the condition and return its free variables. simplifyCondition :: Condition c -> (c -> Either d Bool) -- ^ (partial) variable assignment -> (Condition d, [d]) simplifyCondition :: Condition c -> (c -> Either d Bool) -> (Condition d, [d]) simplifyCondition Condition c cond c -> Either d Bool i = Condition d -> (Condition d, [d]) forall a. Condition a -> (Condition a, [a]) fv (Condition d -> (Condition d, [d])) -> (Condition c -> Condition d) -> Condition c -> (Condition d, [d]) forall b c a. (b -> c) -> (a -> b) -> a -> c . Condition c -> Condition d walk (Condition c -> (Condition d, [d])) -> Condition c -> (Condition d, [d]) forall a b. (a -> b) -> a -> b $ Condition c cond where walk :: Condition c -> Condition d walk Condition c cnd = case Condition c cnd of Var c v -> (d -> Condition d) -> (Bool -> Condition d) -> Either d Bool -> Condition d forall a c b. (a -> c) -> (b -> c) -> Either a b -> c either d -> Condition d forall c. c -> Condition c Var Bool -> Condition d forall c. Bool -> Condition c Lit (c -> Either d Bool i c v) Lit Bool b -> Bool -> Condition d forall c. Bool -> Condition c Lit Bool b CNot Condition c c -> case Condition c -> Condition d walk Condition c c of Lit Bool True -> Bool -> Condition d forall c. Bool -> Condition c Lit Bool False Lit Bool False -> Bool -> Condition d forall c. Bool -> Condition c Lit Bool True Condition d c' -> Condition d -> Condition d forall c. Condition c -> Condition c CNot Condition d c' COr Condition c c Condition c d -> case (Condition c -> Condition d walk Condition c c, Condition c -> Condition d walk Condition c d) of (Lit Bool False, Condition d d') -> Condition d d' (Lit Bool True, Condition d _) -> Bool -> Condition d forall c. Bool -> Condition c Lit Bool True (Condition d c', Lit Bool False) -> Condition d c' (Condition d _, Lit Bool True) -> Bool -> Condition d forall c. Bool -> Condition c Lit Bool True (Condition d c',Condition d d') -> Condition d -> Condition d -> Condition d forall c. Condition c -> Condition c -> Condition c COr Condition d c' Condition d d' CAnd Condition c c Condition c d -> case (Condition c -> Condition d walk Condition c c, Condition c -> Condition d walk Condition c d) of (Lit Bool False, Condition d _) -> Bool -> Condition d forall c. Bool -> Condition c Lit Bool False (Lit Bool True, Condition d d') -> Condition d d' (Condition d _, Lit Bool False) -> Bool -> Condition d forall c. Bool -> Condition c Lit Bool False (Condition d c', Lit Bool True) -> Condition d c' (Condition d c',Condition d d') -> Condition d -> Condition d -> Condition d forall c. Condition c -> Condition c -> Condition c CAnd Condition d c' Condition d d' -- gather free vars fv :: Condition a -> (Condition a, [a]) fv Condition a c = (Condition a c, Condition a -> [a] forall a. Condition a -> [a] fv' Condition a c) fv' :: Condition a -> [a] fv' Condition a c = case Condition a c of Var a v -> [a v] Lit Bool _ -> [] CNot Condition a c' -> Condition a -> [a] fv' Condition a c' COr Condition a c1 Condition a c2 -> Condition a -> [a] fv' Condition a c1 [a] -> [a] -> [a] forall a. [a] -> [a] -> [a] ++ Condition a -> [a] fv' Condition a c2 CAnd Condition a c1 Condition a c2 -> Condition a -> [a] fv' Condition a c1 [a] -> [a] -> [a] forall a. [a] -> [a] -> [a] ++ Condition a -> [a] fv' Condition a c2