{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Language.Haskell.Syntax.BooleanFormula(
BooleanFormula(..), LBooleanFormula,
mkVar, mkFalse, mkTrue, mkBool, mkAnd, mkOr
) where
import Prelude hiding ( init, last )
import Data.List ( nub )
import Language.Haskell.Syntax.Extension (XRec, UnXRec (..), LIdP)
type LBooleanFormula p = XRec p (BooleanFormula p)
data BooleanFormula p = Var (LIdP p) | And [LBooleanFormula p] | Or [LBooleanFormula p]
| Parens (LBooleanFormula p)
deriving instance (Eq (LIdP p), Eq (LBooleanFormula p)) => Eq (BooleanFormula p)
mkVar :: LIdP p -> BooleanFormula p
mkVar :: forall p. LIdP p -> BooleanFormula p
mkVar = LIdP p -> BooleanFormula p
forall p. LIdP p -> BooleanFormula p
Var
mkFalse, mkTrue :: BooleanFormula p
mkFalse :: forall p. BooleanFormula p
mkFalse = [LBooleanFormula p] -> BooleanFormula p
forall p. [LBooleanFormula p] -> BooleanFormula p
Or []
mkTrue :: forall p. BooleanFormula p
mkTrue = [LBooleanFormula p] -> BooleanFormula p
forall p. [LBooleanFormula p] -> BooleanFormula p
And []
mkBool :: Bool -> BooleanFormula p
mkBool :: forall p. Bool -> BooleanFormula p
mkBool Bool
False = BooleanFormula p
forall p. BooleanFormula p
mkFalse
mkBool Bool
True = BooleanFormula p
forall p. BooleanFormula p
mkTrue
mkAnd :: forall p. (UnXRec p, Eq (LIdP p), Eq (LBooleanFormula p)) => [LBooleanFormula p] -> BooleanFormula p
mkAnd :: forall p.
(UnXRec p, Eq (LIdP p), Eq (LBooleanFormula p)) =>
[LBooleanFormula p] -> BooleanFormula p
mkAnd = BooleanFormula p
-> ([[LBooleanFormula p]] -> BooleanFormula p)
-> Maybe [[LBooleanFormula p]]
-> BooleanFormula p
forall b a. b -> (a -> b) -> Maybe a -> b
maybe BooleanFormula p
forall p. BooleanFormula p
mkFalse ([LBooleanFormula p] -> BooleanFormula p
mkAnd' ([LBooleanFormula p] -> BooleanFormula p)
-> ([[LBooleanFormula p]] -> [LBooleanFormula p])
-> [[LBooleanFormula p]]
-> BooleanFormula p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LBooleanFormula p] -> [LBooleanFormula p]
forall a. Eq a => [a] -> [a]
nub ([LBooleanFormula p] -> [LBooleanFormula p])
-> ([[LBooleanFormula p]] -> [LBooleanFormula p])
-> [[LBooleanFormula p]]
-> [LBooleanFormula p]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[LBooleanFormula p]] -> [LBooleanFormula p]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) (Maybe [[LBooleanFormula p]] -> BooleanFormula p)
-> ([LBooleanFormula p] -> Maybe [[LBooleanFormula p]])
-> [LBooleanFormula p]
-> BooleanFormula p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LBooleanFormula p -> Maybe [LBooleanFormula p])
-> [LBooleanFormula p] -> Maybe [[LBooleanFormula p]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM LBooleanFormula p -> Maybe [LBooleanFormula p]
fromAnd
where
fromAnd :: LBooleanFormula p -> Maybe [LBooleanFormula p]
fromAnd :: LBooleanFormula p -> Maybe [LBooleanFormula p]
fromAnd LBooleanFormula p
bf = case forall p a. UnXRec p => XRec p a -> a
unXRec @p LBooleanFormula p
bf of
(And [LBooleanFormula p]
xs) -> [LBooleanFormula p] -> Maybe [LBooleanFormula p]
forall a. a -> Maybe a
Just [LBooleanFormula p]
xs
(Or []) -> Maybe [LBooleanFormula p]
forall a. Maybe a
Nothing
BooleanFormula p
_ -> [LBooleanFormula p] -> Maybe [LBooleanFormula p]
forall a. a -> Maybe a
Just [LBooleanFormula p
bf]
mkAnd' :: [LBooleanFormula p] -> BooleanFormula p
mkAnd' [LBooleanFormula p
x] = forall p a. UnXRec p => XRec p a -> a
unXRec @p LBooleanFormula p
x
mkAnd' [LBooleanFormula p]
xs = [LBooleanFormula p] -> BooleanFormula p
forall p. [LBooleanFormula p] -> BooleanFormula p
And [LBooleanFormula p]
xs
mkOr :: forall p. (UnXRec p, Eq (LIdP p), Eq (LBooleanFormula p)) => [LBooleanFormula p] -> BooleanFormula p
mkOr :: forall p.
(UnXRec p, Eq (LIdP p), Eq (LBooleanFormula p)) =>
[LBooleanFormula p] -> BooleanFormula p
mkOr = BooleanFormula p
-> ([[LBooleanFormula p]] -> BooleanFormula p)
-> Maybe [[LBooleanFormula p]]
-> BooleanFormula p
forall b a. b -> (a -> b) -> Maybe a -> b
maybe BooleanFormula p
forall p. BooleanFormula p
mkTrue ([LBooleanFormula p] -> BooleanFormula p
mkOr' ([LBooleanFormula p] -> BooleanFormula p)
-> ([[LBooleanFormula p]] -> [LBooleanFormula p])
-> [[LBooleanFormula p]]
-> BooleanFormula p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LBooleanFormula p] -> [LBooleanFormula p]
forall a. Eq a => [a] -> [a]
nub ([LBooleanFormula p] -> [LBooleanFormula p])
-> ([[LBooleanFormula p]] -> [LBooleanFormula p])
-> [[LBooleanFormula p]]
-> [LBooleanFormula p]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[LBooleanFormula p]] -> [LBooleanFormula p]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) (Maybe [[LBooleanFormula p]] -> BooleanFormula p)
-> ([LBooleanFormula p] -> Maybe [[LBooleanFormula p]])
-> [LBooleanFormula p]
-> BooleanFormula p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LBooleanFormula p -> Maybe [LBooleanFormula p])
-> [LBooleanFormula p] -> Maybe [[LBooleanFormula p]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM LBooleanFormula p -> Maybe [LBooleanFormula p]
fromOr
where
fromOr :: LBooleanFormula p -> Maybe [LBooleanFormula p]
fromOr LBooleanFormula p
bf = case forall p a. UnXRec p => XRec p a -> a
unXRec @p LBooleanFormula p
bf of
(Or [LBooleanFormula p]
xs) -> [LBooleanFormula p] -> Maybe [LBooleanFormula p]
forall a. a -> Maybe a
Just [LBooleanFormula p]
xs
(And []) -> Maybe [LBooleanFormula p]
forall a. Maybe a
Nothing
BooleanFormula p
_ -> [LBooleanFormula p] -> Maybe [LBooleanFormula p]
forall a. a -> Maybe a
Just [LBooleanFormula p
bf]
mkOr' :: [LBooleanFormula p] -> BooleanFormula p
mkOr' [LBooleanFormula p
x] = forall p a. UnXRec p => XRec p a -> a
unXRec @p LBooleanFormula p
x
mkOr' [LBooleanFormula p]
xs = [LBooleanFormula p] -> BooleanFormula p
forall p. [LBooleanFormula p] -> BooleanFormula p
Or [LBooleanFormula p]
xs