{-# LANGUAGE CPP                #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFoldable     #-}
{-# LANGUAGE DeriveFunctor      #-}
{-# LANGUAGE DeriveTraversable  #-}
-- |
--
-- Inspired by <http://www.well-typed.com/blog/2014/12/simple-smt-solver/ Simple SMT Solver>.
--
-- In future this module will probably be moved into separate package.
module Distribution.SPDX.Extra.Internal
  (LatticeSyntax(..), dual, freeVars, equivalent, preorder, satisfiable) where

import Control.Applicative
import Control.Monad
import Control.Monad.Trans.State.Strict
import Data.Data
import Data.Foldable
import Data.Traversable
import Prelude                          hiding (all, or)

import qualified Data.Map.Strict as Map

data LatticeSyntax a = LVar a
                     | LBound Bool
                     | LJoin (LatticeSyntax a) (LatticeSyntax a)
                     | LMeet (LatticeSyntax a) (LatticeSyntax a)
  deriving (LatticeSyntax a -> LatticeSyntax a -> Bool
forall a. Eq a => LatticeSyntax a -> LatticeSyntax a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LatticeSyntax a -> LatticeSyntax a -> Bool
$c/= :: forall a. Eq a => LatticeSyntax a -> LatticeSyntax a -> Bool
== :: LatticeSyntax a -> LatticeSyntax a -> Bool
$c== :: forall a. Eq a => LatticeSyntax a -> LatticeSyntax a -> Bool
Eq, LatticeSyntax a -> LatticeSyntax a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (LatticeSyntax a)
forall a. Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
forall a. Ord a => LatticeSyntax a -> LatticeSyntax a -> Ordering
forall a.
Ord a =>
LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
min :: LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
$cmin :: forall a.
Ord a =>
LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
max :: LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
$cmax :: forall a.
Ord a =>
LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
>= :: LatticeSyntax a -> LatticeSyntax a -> Bool
$c>= :: forall a. Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
> :: LatticeSyntax a -> LatticeSyntax a -> Bool
$c> :: forall a. Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
<= :: LatticeSyntax a -> LatticeSyntax a -> Bool
$c<= :: forall a. Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
< :: LatticeSyntax a -> LatticeSyntax a -> Bool
$c< :: forall a. Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
compare :: LatticeSyntax a -> LatticeSyntax a -> Ordering
$ccompare :: forall a. Ord a => LatticeSyntax a -> LatticeSyntax a -> Ordering
Ord, ReadPrec [LatticeSyntax a]
ReadPrec (LatticeSyntax a)
ReadS [LatticeSyntax a]
forall a. Read a => ReadPrec [LatticeSyntax a]
forall a. Read a => ReadPrec (LatticeSyntax a)
forall a. Read a => Int -> ReadS (LatticeSyntax a)
forall a. Read a => ReadS [LatticeSyntax a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [LatticeSyntax a]
$creadListPrec :: forall a. Read a => ReadPrec [LatticeSyntax a]
readPrec :: ReadPrec (LatticeSyntax a)
$creadPrec :: forall a. Read a => ReadPrec (LatticeSyntax a)
readList :: ReadS [LatticeSyntax a]
$creadList :: forall a. Read a => ReadS [LatticeSyntax a]
readsPrec :: Int -> ReadS (LatticeSyntax a)
$creadsPrec :: forall a. Read a => Int -> ReadS (LatticeSyntax a)
Read, Int -> LatticeSyntax a -> ShowS
forall a. Show a => Int -> LatticeSyntax a -> ShowS
forall a. Show a => [LatticeSyntax a] -> ShowS
forall a. Show a => LatticeSyntax a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LatticeSyntax a] -> ShowS
$cshowList :: forall a. Show a => [LatticeSyntax a] -> ShowS
show :: LatticeSyntax a -> String
$cshow :: forall a. Show a => LatticeSyntax a -> String
showsPrec :: Int -> LatticeSyntax a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> LatticeSyntax a -> ShowS
Show, forall a b. a -> LatticeSyntax b -> LatticeSyntax a
forall a b. (a -> b) -> LatticeSyntax a -> LatticeSyntax b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> LatticeSyntax b -> LatticeSyntax a
$c<$ :: forall a b. a -> LatticeSyntax b -> LatticeSyntax a
fmap :: forall a b. (a -> b) -> LatticeSyntax a -> LatticeSyntax b
$cfmap :: forall a b. (a -> b) -> LatticeSyntax a -> LatticeSyntax b
Functor, forall a. Eq a => a -> LatticeSyntax a -> Bool
forall a. Num a => LatticeSyntax a -> a
forall a. Ord a => LatticeSyntax a -> a
forall m. Monoid m => LatticeSyntax m -> m
forall a. LatticeSyntax a -> Bool
forall a. LatticeSyntax a -> Int
forall a. LatticeSyntax a -> [a]
forall a. (a -> a -> a) -> LatticeSyntax a -> a
forall m a. Monoid m => (a -> m) -> LatticeSyntax a -> m
forall b a. (b -> a -> b) -> b -> LatticeSyntax a -> b
forall a b. (a -> b -> b) -> b -> LatticeSyntax a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => LatticeSyntax a -> a
$cproduct :: forall a. Num a => LatticeSyntax a -> a
sum :: forall a. Num a => LatticeSyntax a -> a
$csum :: forall a. Num a => LatticeSyntax a -> a
minimum :: forall a. Ord a => LatticeSyntax a -> a
$cminimum :: forall a. Ord a => LatticeSyntax a -> a
maximum :: forall a. Ord a => LatticeSyntax a -> a
$cmaximum :: forall a. Ord a => LatticeSyntax a -> a
elem :: forall a. Eq a => a -> LatticeSyntax a -> Bool
$celem :: forall a. Eq a => a -> LatticeSyntax a -> Bool
length :: forall a. LatticeSyntax a -> Int
$clength :: forall a. LatticeSyntax a -> Int
null :: forall a. LatticeSyntax a -> Bool
$cnull :: forall a. LatticeSyntax a -> Bool
toList :: forall a. LatticeSyntax a -> [a]
$ctoList :: forall a. LatticeSyntax a -> [a]
foldl1 :: forall a. (a -> a -> a) -> LatticeSyntax a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> LatticeSyntax a -> a
foldr1 :: forall a. (a -> a -> a) -> LatticeSyntax a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> LatticeSyntax a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> LatticeSyntax a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> LatticeSyntax a -> b
foldl :: forall b a. (b -> a -> b) -> b -> LatticeSyntax a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> LatticeSyntax a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> LatticeSyntax a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> LatticeSyntax a -> b
foldr :: forall a b. (a -> b -> b) -> b -> LatticeSyntax a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> LatticeSyntax a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> LatticeSyntax a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> LatticeSyntax a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> LatticeSyntax a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> LatticeSyntax a -> m
fold :: forall m. Monoid m => LatticeSyntax m -> m
$cfold :: forall m. Monoid m => LatticeSyntax m -> m
Foldable, Functor LatticeSyntax
Foldable LatticeSyntax
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
LatticeSyntax (m a) -> m (LatticeSyntax a)
forall (f :: * -> *) a.
Applicative f =>
LatticeSyntax (f a) -> f (LatticeSyntax a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LatticeSyntax a -> m (LatticeSyntax b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LatticeSyntax a -> f (LatticeSyntax b)
sequence :: forall (m :: * -> *) a.
Monad m =>
LatticeSyntax (m a) -> m (LatticeSyntax a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
LatticeSyntax (m a) -> m (LatticeSyntax a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LatticeSyntax a -> m (LatticeSyntax b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LatticeSyntax a -> m (LatticeSyntax b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
LatticeSyntax (f a) -> f (LatticeSyntax a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
LatticeSyntax (f a) -> f (LatticeSyntax a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LatticeSyntax a -> f (LatticeSyntax b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LatticeSyntax a -> f (LatticeSyntax b)
Traversable, Typeable, LatticeSyntax a -> Constr
LatticeSyntax a -> DataType
forall {a}. Data a => Typeable (LatticeSyntax a)
forall a. Data a => LatticeSyntax a -> Constr
forall a. Data a => LatticeSyntax a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b) -> LatticeSyntax a -> LatticeSyntax a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> LatticeSyntax a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> LatticeSyntax a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LatticeSyntax a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LatticeSyntax a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> LatticeSyntax a -> m (LatticeSyntax a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> LatticeSyntax a -> m (LatticeSyntax a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (LatticeSyntax a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LatticeSyntax a -> c (LatticeSyntax a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (LatticeSyntax a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (LatticeSyntax a))
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 (LatticeSyntax a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LatticeSyntax a -> c (LatticeSyntax a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (LatticeSyntax a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LatticeSyntax a -> m (LatticeSyntax a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> LatticeSyntax a -> m (LatticeSyntax a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LatticeSyntax a -> m (LatticeSyntax a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> LatticeSyntax a -> m (LatticeSyntax a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LatticeSyntax a -> m (LatticeSyntax a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> LatticeSyntax a -> m (LatticeSyntax a)
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> LatticeSyntax a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> LatticeSyntax a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> LatticeSyntax a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> LatticeSyntax a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LatticeSyntax a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LatticeSyntax a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LatticeSyntax a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LatticeSyntax a -> r
gmapT :: (forall b. Data b => b -> b) -> LatticeSyntax a -> LatticeSyntax a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> LatticeSyntax a -> LatticeSyntax a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (LatticeSyntax a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (LatticeSyntax a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (LatticeSyntax a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (LatticeSyntax a))
dataTypeOf :: LatticeSyntax a -> DataType
$cdataTypeOf :: forall a. Data a => LatticeSyntax a -> DataType
toConstr :: LatticeSyntax a -> Constr
$ctoConstr :: forall a. Data a => LatticeSyntax a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (LatticeSyntax a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (LatticeSyntax a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LatticeSyntax a -> c (LatticeSyntax a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LatticeSyntax a -> c (LatticeSyntax a)
Data)

instance Applicative LatticeSyntax where
  pure :: forall a. a -> LatticeSyntax a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b.
LatticeSyntax (a -> b) -> LatticeSyntax a -> LatticeSyntax b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad LatticeSyntax where
  return :: forall a. a -> LatticeSyntax a
return = forall a. a -> LatticeSyntax a
LVar
  LVar a
x    >>= :: forall a b.
LatticeSyntax a -> (a -> LatticeSyntax b) -> LatticeSyntax b
>>= a -> LatticeSyntax b
f = a -> LatticeSyntax b
f a
x
  LBound Bool
b  >>= a -> LatticeSyntax b
_ = forall a. Bool -> LatticeSyntax a
LBound Bool
b
  LJoin LatticeSyntax a
a LatticeSyntax a
b >>= a -> LatticeSyntax b
f = forall a. LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
LJoin (LatticeSyntax a
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> LatticeSyntax b
f) (LatticeSyntax a
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> LatticeSyntax b
f)
  LMeet LatticeSyntax a
a LatticeSyntax a
b >>= a -> LatticeSyntax b
f = forall a. LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
LMeet (LatticeSyntax a
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> LatticeSyntax b
f) (LatticeSyntax a
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> LatticeSyntax b
f)

freeVars :: LatticeSyntax a -> [a]
freeVars :: forall a. LatticeSyntax a -> [a]
freeVars = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

dual :: LatticeSyntax a -> LatticeSyntax a
dual :: forall a. LatticeSyntax a -> LatticeSyntax a
dual (LVar a
v) = forall a. a -> LatticeSyntax a
LVar a
v
dual (LBound Bool
t) = forall a. Bool -> LatticeSyntax a
LBound forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
t
dual (LJoin LatticeSyntax a
a LatticeSyntax a
b) = forall a. LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
LMeet (forall a. LatticeSyntax a -> LatticeSyntax a
dual LatticeSyntax a
a) (forall a. LatticeSyntax a -> LatticeSyntax a
dual LatticeSyntax a
b)
dual (LMeet LatticeSyntax a
a LatticeSyntax a
b) = forall a. LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
LJoin (forall a. LatticeSyntax a -> LatticeSyntax a
dual LatticeSyntax a
a) (forall a. LatticeSyntax a -> LatticeSyntax a
dual LatticeSyntax a
b)

-- | Test for equivalence.
--
-- >>> equivalent (LMeet (LVar 'a') (LVar 'b')) (LMeet (LVar 'b') (LVar 'a'))
-- True
--
-- >>> equivalent (LVar 'a') (LMeet (LVar 'a') (LVar 'a'))
-- True
--
-- >>> equivalent (LMeet (LVar 'a') (LVar 'b')) (LMeet (LVar 'b') (LVar 'b'))
-- False
equivalent :: Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
equivalent :: forall a. Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
equivalent LatticeSyntax a
a LatticeSyntax a
b = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Eq a => a -> a -> Bool
(==)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v a. Eval v a -> [a]
runEval forall a b. (a -> b) -> a -> b
$ Eval a (Bool, Bool)
p
  where p :: Eval a (Bool, Bool)
p = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall v. Ord v => LatticeSyntax v -> Eval v Bool
evalLattice LatticeSyntax a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall v. Ord v => LatticeSyntax v -> Eval v Bool
evalLattice LatticeSyntax a
b

-- | Test for preorder.
--
-- @ a ≤ b ⇔ a ∨ b ≡ b ⇔ a ≡ a ∧ b @
--
-- >>> preorder (LVar 'a' `LMeet` LVar 'b') (LVar 'a')
-- True
--
-- >>> preorder (LVar 'a') (LVar 'a' `LMeet` LVar 'b')
-- False
preorder :: Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
preorder :: forall a. Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
preorder LatticeSyntax a
a LatticeSyntax a
b = (LatticeSyntax a
a forall a. LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
`LJoin` LatticeSyntax a
b) forall a. Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
`equivalent` LatticeSyntax a
b

-- | Return `True` if for some variable assigment expression evaluates to `True`.
satisfiable :: Ord a => LatticeSyntax a -> Bool
satisfiable :: forall a. Ord a => LatticeSyntax a -> Bool
satisfiable = forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v a. Eval v a -> [a]
runEval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. Ord v => LatticeSyntax v -> Eval v Bool
evalLattice

newtype Eval v a = Eval { forall v a. Eval v a -> StateT (Map v Bool) [] a
unEval :: StateT (Map.Map v Bool) [] a }

instance Functor (Eval v) where
  fmap :: forall a b. (a -> b) -> Eval v a -> Eval v b
fmap = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Applicative (Eval v) where
  pure :: forall a. a -> Eval v a
pure = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. Eval v (a -> b) -> Eval v a -> Eval v b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Alternative (Eval v) where
  empty :: forall a. Eval v a
empty = forall (m :: * -> *) a. MonadPlus m => m a
mzero
  <|> :: forall a. Eval v a -> Eval v a -> Eval v a
(<|>) = forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus

instance Monad (Eval v) where
  return :: forall a. a -> Eval v a
return = forall v a. StateT (Map v Bool) [] a -> Eval v a
Eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return
  Eval StateT (Map v Bool) [] a
m >>= :: forall a b. Eval v a -> (a -> Eval v b) -> Eval v b
>>= a -> Eval v b
k = forall v a. StateT (Map v Bool) [] a -> Eval v a
Eval forall a b. (a -> b) -> a -> b
$ StateT (Map v Bool) [] a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall v a. Eval v a -> StateT (Map v Bool) [] a
unEval forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eval v b
k

instance MonadPlus (Eval v) where
  mzero :: forall a. Eval v a
mzero = forall v a. StateT (Map v Bool) [] a -> Eval v a
Eval forall (m :: * -> *) a. MonadPlus m => m a
mzero
  Eval StateT (Map v Bool) [] a
a mplus :: forall a. Eval v a -> Eval v a -> Eval v a
`mplus` Eval StateT (Map v Bool) [] a
b = forall v a. StateT (Map v Bool) [] a -> Eval v a
Eval forall a b. (a -> b) -> a -> b
$ StateT (Map v Bool) [] a
a forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` StateT (Map v Bool) [] a
b

runEval :: Eval v a -> [a]
runEval :: forall v a. Eval v a -> [a]
runEval Eval v a
act = forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall v a. Eval v a -> StateT (Map v Bool) [] a
unEval Eval v a
act) forall k a. Map k a
Map.empty

evalLattice :: Ord v => LatticeSyntax v -> Eval v Bool
evalLattice :: forall v. Ord v => LatticeSyntax v -> Eval v Bool
evalLattice (LVar v
v)    = forall v. Ord v => v -> Eval v Bool
guess v
v
evalLattice (LBound Bool
b)  = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
evalLattice (LJoin LatticeSyntax v
a LatticeSyntax v
b) = forall v. Ord v => LatticeSyntax v -> Eval v Bool
evalLattice LatticeSyntax v
a forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
||^ forall v. Ord v => LatticeSyntax v -> Eval v Bool
evalLattice LatticeSyntax v
b
evalLattice (LMeet LatticeSyntax v
a LatticeSyntax v
b) = forall v. Ord v => LatticeSyntax v -> Eval v Bool
evalLattice LatticeSyntax v
a forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
&&^ forall v. Ord v => LatticeSyntax v -> Eval v Bool
evalLattice LatticeSyntax v
b

guess :: Ord v => v -> Eval v Bool
guess :: forall v. Ord v => v -> Eval v Bool
guess v
v = forall v a. StateT (Map v Bool) [] a -> Eval v a
Eval forall a b. (a -> b) -> a -> b
$ do
  Map v Bool
st <- forall (m :: * -> *) s. Monad m => StateT s m s
get
  let remember :: Bool -> StateT (Map v Bool) m Bool
remember Bool
b = forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert v
v Bool
b Map v Bool
st) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v Bool
st of
    Just Bool
b  -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
    Maybe Bool
Nothing -> forall {m :: * -> *}. Monad m => Bool -> StateT (Map v Bool) m Bool
remember Bool
True forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {m :: * -> *}. Monad m => Bool -> StateT (Map v Bool) m Bool
remember Bool
False

-- From Control.Monad.Extra of extra

-- | Like @if@, but where the test can be monadic.
ifM :: Monad m => m Bool -> m a -> m a -> m a
ifM :: forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
b m a
t m a
f = do Bool
b' <- m Bool
b; if Bool
b' then m a
t else m a
f

-- | The lazy '||' operator lifted to a monad. If the first
--   argument evaluates to 'True' the second argument will not
--   be evaluated.
--
-- > Just True  ||^ undefined  == Just True
-- > Just False ||^ Just True  == Just True
-- > Just False ||^ Just False == Just False
(||^) :: Monad m => m Bool -> m Bool -> m Bool
||^ :: forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
(||^) m Bool
a m Bool
b = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
a (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) m Bool
b

-- | The lazy '&&' operator lifted to a monad. If the first
--   argument evaluates to 'False' the second argument will not
--   be evaluated.
--
-- > Just False &&^ undefined  == Just False
-- > Just True  &&^ Just True  == Just True
-- > Just True  &&^ Just False == Just False
(&&^) :: Monad m => m Bool -> m Bool -> m Bool
&&^ :: forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
(&&^) m Bool
a m Bool
b = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
a m Bool
b (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)