{-# 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
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
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, Condition c -> DataType
Condition c -> Constr
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 (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))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. 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 u. (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 :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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)
Data, 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 :: forall a. Condition a -> Condition a
cNot (Lit Bool
b)  = forall c. Bool -> Condition c
Lit (Bool -> Bool
not Bool
b)
cNot (CNot Condition a
c) = Condition a
c
cNot Condition a
c        = forall a. Condition a -> Condition a
CNot Condition a
c

-- | Boolean AND of two 'Condition' values.
cAnd :: Condition a -> Condition a -> Condition a
cAnd :: forall a. Condition a -> Condition a -> Condition a
cAnd (Lit Bool
False) Condition a
_           = forall c. Bool -> Condition c
Lit Bool
False
cAnd Condition a
_           (Lit Bool
False) = 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           = forall a. Condition a -> Condition a -> Condition a
CAnd Condition a
x Condition a
y

-- | Boolean OR of two 'Condition' values.
cOr :: Eq v => Condition v -> Condition v -> Condition v
cOr :: forall v. Eq v => Condition v -> Condition v -> Condition v
cOr  (Lit Bool
True)  Condition v
_           = forall c. Bool -> Condition c
Lit Bool
True
cOr  Condition v
_           (Lit Bool
True)  = 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 forall a. Eq a => a -> a -> Bool
== Condition v
d                   = forall c. Bool -> Condition c
Lit Bool
True
cOr  (CNot Condition v
c)    Condition v
d
  | Condition v
c forall a. Eq a => a -> a -> Bool
== Condition v
d                   = forall c. Bool -> Condition c
Lit Bool
True
cOr  Condition v
x           Condition v
y           = forall a. Condition a -> Condition a -> Condition a
COr Condition v
x Condition v
y

instance Functor Condition where
  a -> b
f fmap :: forall a b. (a -> b) -> Condition a -> Condition b
`fmap` Var a
c    = forall c. c -> Condition c
Var (a -> b
f a
c)
  a -> b
_ `fmap` Lit Bool
c    = forall c. Bool -> Condition c
Lit Bool
c
  a -> b
f `fmap` CNot Condition a
c   = forall a. Condition a -> Condition a
CNot (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  = forall a. Condition a -> Condition a -> Condition a
COr  (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Condition a
c) (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 = forall a. Condition a -> Condition a -> Condition a
CAnd (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Condition a
c) (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 :: forall m a. Monoid m => (a -> m) -> Condition a -> m
`foldMap` Var a
c    = a -> m
f a
c
  a -> m
_ `foldMap` Lit Bool
_    = forall a. Monoid a => a
mempty
  a -> m
f `foldMap` CNot Condition a
c   = 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  = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f Condition a
c forall a. Monoid a => a -> a -> a
`mappend` 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 = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f Condition a
c forall a. Monoid a => a -> a -> a
`mappend` 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 :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Condition a -> f (Condition b)
`traverse` Var a
c    = forall c. c -> Condition c
Var 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    = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall c. Bool -> Condition c
Lit Bool
c
  a -> f b
f `traverse` CNot Condition a
c   = forall a. Condition a -> Condition a
CNot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` 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  = forall a. Condition a -> Condition a -> Condition a
COr  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f 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 = forall a. Condition a -> Condition a -> Condition a
CAnd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f 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 :: forall c. c -> Condition c
pure  = forall c. c -> Condition c
Var
  <*> :: forall a 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 :: forall c. c -> Condition c
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  -- Terminating cases
  >>= :: forall a b. Condition a -> (a -> Condition b) -> Condition b
(>>=) (Lit Bool
x) a -> 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 = forall a. Condition a -> Condition a
CNot (Condition a
x 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 = forall a. Condition a -> Condition a -> Condition a
COr  (Condition a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Condition b
f) (Condition a
y 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 = forall a. Condition a -> Condition a -> Condition a
CAnd (Condition a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Condition b
f) (Condition a
y 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 = forall c. Bool -> Condition c
Lit Bool
False
  mappend :: Condition a -> Condition a -> Condition a
mappend = forall a. Semigroup a => a -> a -> a
(<>)

instance Semigroup (Condition a) where
  <> :: Condition a -> Condition a -> Condition a
(<>) = forall a. Condition a -> Condition a -> Condition a
COr

instance Alternative Condition where
  empty :: forall a. Condition a
empty = forall a. Monoid a => a
mempty
  <|> :: forall a. Condition a -> Condition a -> Condition a
(<|>) = forall a. Monoid a => a -> a -> a
mappend

instance MonadPlus Condition where
  mzero :: forall a. Condition a
mzero = forall a. Monoid a => a
mempty
  mplus :: forall a. Condition a -> Condition a -> Condition a
mplus = 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 = 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 :: forall c d.
Condition c -> (c -> Either d Bool) -> (Condition d, [d])
simplifyCondition Condition c
cond c -> Either d Bool
i = forall {a}. Condition a -> (Condition a, [a])
fv forall b c a. (b -> c) -> (a -> b) -> a -> c
. Condition c -> Condition d
walk 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   -> forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall c. c -> Condition c
Var forall c. Bool -> Condition c
Lit (c -> Either d Bool
i c
v)
      Lit Bool
b   -> 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 -> forall c. Bool -> Condition c
Lit Bool
False
                   Lit Bool
False -> forall c. Bool -> Condition c
Lit Bool
True
                   Condition d
c' -> forall a. Condition a -> Condition a
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
_)   -> forall c. Bool -> Condition c
Lit Bool
True
                   (Condition d
c', Lit Bool
False) -> Condition d
c'
                   (Condition d
_, Lit Bool
True)   -> forall c. Bool -> Condition c
Lit Bool
True
                   (Condition d
c',Condition d
d')         -> forall a. Condition a -> Condition a -> Condition a
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
_) -> forall c. Bool -> Condition c
Lit Bool
False
                    (Lit Bool
True, Condition d
d') -> Condition d
d'
                    (Condition d
_, Lit Bool
False) -> forall c. Bool -> Condition c
Lit Bool
False
                    (Condition d
c', Lit Bool
True) -> Condition d
c'
                    (Condition d
c',Condition d
d')        -> forall a. Condition a -> Condition a -> Condition a
CAnd Condition d
c' Condition d
d'
    -- gather free vars
    fv :: Condition a -> (Condition a, [a])
fv Condition a
c = (Condition a
c, 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 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 forall a. [a] -> [a] -> [a]
++ Condition a -> [a]
fv' Condition a
c2