{-# 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 b :: Bool
b)  = Bool -> Condition a
forall c. Bool -> Condition c
Lit (Bool -> Bool
not Bool
b)
cNot (CNot c :: Condition a
c) = Condition a
c
cNot c :: 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 False) _           = Bool -> Condition a
forall c. Bool -> Condition c
Lit Bool
False
cAnd _           (Lit False) = Bool -> Condition a
forall c. Bool -> Condition c
Lit Bool
False
cAnd (Lit True)  x :: Condition a
x           = Condition a
x
cAnd x :: Condition a
x           (Lit True)  = Condition a
x
cAnd x :: Condition a
x           y :: 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 True)  _           = Bool -> Condition v
forall c. Bool -> Condition c
Lit Bool
True
cOr  _           (Lit True)  = Bool -> Condition v
forall c. Bool -> Condition c
Lit Bool
True
cOr  (Lit False) x :: Condition v
x           = Condition v
x
cOr  x :: Condition v
x           (Lit False) = Condition v
x
cOr  c :: Condition v
c           (CNot d :: 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 c :: Condition v
c)    d :: 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  x :: Condition v
x           y :: 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
  f :: a -> b
f fmap :: (a -> b) -> Condition a -> Condition b
`fmap` Var c :: a
c    = b -> Condition b
forall c. c -> Condition c
Var (a -> b
f a
c)
  _ `fmap` Lit c :: Bool
c    = Bool -> Condition b
forall c. Bool -> Condition c
Lit Bool
c
  f :: a -> b
f `fmap` CNot c :: 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)
  f :: a -> b
f `fmap` COr c :: Condition a
c d :: 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)
  f :: a -> b
f `fmap` CAnd c :: Condition a
c d :: 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
  f :: a -> m
f foldMap :: (a -> m) -> Condition a -> m
`foldMap` Var c :: a
c    = a -> m
f a
c
  _ `foldMap` Lit _    = m
forall a. Monoid a => a
mempty
  f :: a -> m
f `foldMap` CNot c :: 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
  f :: a -> m
f `foldMap` COr c :: Condition a
c d :: 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
  f :: a -> m
f `foldMap` CAnd c :: Condition a
c d :: 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
  f :: a -> f b
f traverse :: (a -> f b) -> Condition a -> f (Condition b)
`traverse` Var c :: 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
  _ `traverse` Lit c :: 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
  f :: a -> f b
f `traverse` CNot c :: 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
  f :: a -> f b
f `traverse` COr c :: Condition a
c d :: 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
  f :: a -> f b
f `traverse` CAnd c :: Condition a
c d :: 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 x :: Bool
x) _ = Bool -> Condition b
forall c. Bool -> Condition c
Lit Bool
x
  (>>=) (Var x :: a
x) f :: a -> Condition b
f = a -> Condition b
f a
x
  -- Recursing cases
  (>>=) (CNot  x :: Condition a
x  ) f :: 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   x :: Condition a
x y :: Condition a
y) f :: 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  x :: Condition a
x y :: Condition a
y) f :: 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 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 cond :: Condition c
cond i :: 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 cnd :: Condition c
cnd = case Condition c
cnd of
      Var v :: 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 b :: Bool
b   -> Bool -> Condition d
forall c. Bool -> Condition c
Lit Bool
b
      CNot c :: Condition c
c  -> case Condition c -> Condition d
walk Condition c
c of
                   Lit True -> Bool -> Condition d
forall c. Bool -> Condition c
Lit Bool
False
                   Lit False -> Bool -> Condition d
forall c. Bool -> Condition c
Lit Bool
True
                   c' :: Condition d
c' -> Condition d -> Condition d
forall c. Condition c -> Condition c
CNot Condition d
c'
      COr c :: Condition c
c d :: Condition c
d -> case (Condition c -> Condition d
walk Condition c
c, Condition c -> Condition d
walk Condition c
d) of
                   (Lit False, d' :: Condition d
d') -> Condition d
d'
                   (Lit True, _)   -> Bool -> Condition d
forall c. Bool -> Condition c
Lit Bool
True
                   (c' :: Condition d
c', Lit False) -> Condition d
c'
                   (_, Lit True)   -> Bool -> Condition d
forall c. Bool -> Condition c
Lit Bool
True
                   (c' :: Condition d
c',d' :: 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 c :: Condition c
c d :: Condition c
d -> case (Condition c -> Condition d
walk Condition c
c, Condition c -> Condition d
walk Condition c
d) of
                    (Lit False, _) -> Bool -> Condition d
forall c. Bool -> Condition c
Lit Bool
False
                    (Lit True, d' :: Condition d
d') -> Condition d
d'
                    (_, Lit False) -> Bool -> Condition d
forall c. Bool -> Condition c
Lit Bool
False
                    (c' :: Condition d
c', Lit True) -> Condition d
c'
                    (c' :: Condition d
c',d' :: 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 c :: Condition a
c = (Condition a
c, Condition a -> [a]
forall a. Condition a -> [a]
fv' Condition a
c)
    fv' :: Condition a -> [a]
fv' c :: Condition a
c = case Condition a
c of
      Var v :: a
v     -> [a
v]
      Lit _      -> []
      CNot c' :: Condition a
c'    -> Condition a -> [a]
fv' Condition a
c'
      COr c1 :: Condition a
c1 c2 :: 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 c1 :: Condition a
c1 c2 :: 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