{-# 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)


-- types
type LBooleanFormula p = XRec p (BooleanFormula p)
data BooleanFormula p = Var (LIdP p) | And [LBooleanFormula p] | Or [LBooleanFormula p]
                      | Parens (LBooleanFormula p)

-- instances
deriving instance (Eq (LIdP p), Eq (LBooleanFormula p)) => Eq (BooleanFormula p)

-- smart constructors
-- see note [Simplification of BooleanFormulas]
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 []

-- Convert a Bool to a BooleanFormula
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

-- Make a conjunction, and try to simplify
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
  -- See Note [Simplification of BooleanFormulas]
  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
     -- assume that xs are already simplified
     -- otherwise we would need: fromAnd (And xs) = concat <$> traverse fromAnd xs
    (Or [])  -> Maybe [LBooleanFormula p]
forall a. Maybe a
Nothing
     -- in case of False we bail out, And [..,mkFalse,..] == mkFalse
    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
  -- See Note [Simplification of BooleanFormulas]
  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