{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}

module Distribution.Types.Condition
  ( Condition (..)
  , cNot
  , cAnd
  , cOr
  , simplifyCondition
  ) where

import Distribution.Compat.Prelude
import 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
$cshowsPrec :: forall c. Show c => Int -> Condition c -> ShowS
showsPrec :: Int -> Condition c -> ShowS
$cshow :: forall c. Show c => Condition c -> String
show :: Condition c -> String
$cshowList :: forall c. Show c => [Condition c] -> ShowS
showList :: [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
$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
/= :: Condition c -> Condition c -> Bool
Eq, Typeable, Typeable (Condition c)
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 -> Constr
Condition c -> DataType
(forall b. Data b => b -> b) -> Condition c -> Condition c
forall c. Data c => Typeable (Condition c)
forall c. Data c => Condition c -> Constr
forall c. Data c => Condition c -> DataType
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))
$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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Condition c -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Condition c)
$ctoConstr :: forall c. Data c => Condition c -> Constr
toConstr :: Condition c -> Constr
$cdataTypeOf :: forall c. Data c => Condition c -> DataType
dataTypeOf :: Condition c -> DataType
$cdataCast1 :: forall c (t :: * -> *) (c :: * -> *).
(Data c, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Condition c))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Condition c))
$cgmapT :: forall c.
Data c =>
(forall b. Data b => b -> b) -> Condition c -> Condition c
gmapT :: (forall b. Data b => b -> b) -> Condition c -> Condition c
$cgmapQl :: 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
$cgmapQr :: forall c r r'.
Data c =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Condition c -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Condition c -> r
$cgmapQ :: forall c u.
Data c =>
(forall d. Data d => d -> u) -> Condition c -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Condition c -> u
$cgmapM :: forall c (m :: * -> *).
(Data c, Monad 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)
$cgmapMp :: 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)
$cgmapMo :: forall c (m :: * -> *).
(Data c, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Condition c -> m (Condition c)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Condition c -> m (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
$cfrom :: forall c x. Condition c -> Rep (Condition c) x
from :: forall x. Condition c -> Rep (Condition c) x
$cto :: forall c x. Rep (Condition c) x -> Condition c
to :: forall x. Rep (Condition c) x -> Condition c
Generic)

-- | Boolean negation of a 'Condition' value.
cNot :: Condition a -> Condition a
cNot :: forall a. 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 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
_ = 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 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
_ = 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 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 = 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 a. Condition a -> Condition a
CNot ((a -> b) -> Condition a -> Condition b
forall a b. (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 a. Condition a -> Condition a -> Condition a
COr ((a -> b) -> Condition a -> Condition b
forall a b. (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 a b. (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 a. Condition a -> Condition a -> Condition a
CAnd ((a -> b) -> Condition a -> Condition b
forall a b. (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 a b. (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 :: forall m a. Monoid m => (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 m a. Monoid m => (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 m a. Monoid m => (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 m a. Monoid m => (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 m a. Monoid m => (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 m a. Monoid m => (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 :: forall (f :: * -> *) a b.
Applicative f =>
(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 a b. (a -> b) -> f a -> f 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 a. a -> f a
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 a. Condition a -> Condition a
CNot (Condition b -> Condition b) -> f (Condition b) -> f (Condition b)
forall a b. (a -> b) -> f a -> f 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Condition a -> f (Condition 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 a. Condition a -> Condition a -> Condition a
COr (Condition b -> Condition b -> Condition b)
-> f (Condition b) -> f (Condition b -> Condition b)
forall a b. (a -> b) -> f a -> f 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Condition a -> f (Condition b)
traverse a -> f b
f Condition a
c f (Condition b -> Condition b)
-> f (Condition b) -> f (Condition b)
forall a b. f (a -> b) -> f a -> f 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Condition a -> f (Condition 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 a. Condition a -> Condition a -> Condition a
CAnd (Condition b -> Condition b -> Condition b)
-> f (Condition b) -> f (Condition b -> Condition b)
forall a b. (a -> b) -> f a -> f 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Condition a -> f (Condition b)
traverse a -> f b
f Condition a
c f (Condition b -> Condition b)
-> f (Condition b) -> f (Condition b)
forall a b. f (a -> b) -> f a -> f 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Condition a -> f (Condition b)
traverse a -> f b
f Condition a
d

instance Applicative Condition where
  pure :: forall c. c -> Condition c
pure = a -> Condition a
forall c. c -> Condition c
Var
  <*> :: forall a b. 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 :: forall c. c -> Condition c
return = a -> Condition a
forall c. c -> Condition c
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
_ = 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 a. Condition a -> Condition a
CNot (Condition a
x Condition a -> (a -> Condition b) -> Condition b
forall a b. 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 a. Condition a -> Condition a -> Condition a
COr (Condition a
x Condition a -> (a -> Condition b) -> Condition b
forall a b. 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 a b. 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 a. Condition a -> Condition a -> Condition a
CAnd (Condition a
x Condition a -> (a -> Condition b) -> Condition b
forall a b. 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 a b. 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 a. Condition a -> Condition a -> Condition a
COr

instance Alternative Condition where
  empty :: forall a. Condition a
empty = Condition a
forall a. Monoid a => a
mempty
  <|> :: forall a. 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 :: forall a. Condition a
mzero = Condition a
forall a. Monoid a => a
mempty
  mplus :: forall a. 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 :: forall c d.
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 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
_) -> 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 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
_) -> 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 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, 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