{-# 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
(LatticeSyntax a -> LatticeSyntax a -> Bool)
-> (LatticeSyntax a -> LatticeSyntax a -> Bool)
-> Eq (LatticeSyntax a)
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, Eq (LatticeSyntax a)
Eq (LatticeSyntax a)
-> (LatticeSyntax a -> LatticeSyntax a -> Ordering)
-> (LatticeSyntax a -> LatticeSyntax a -> Bool)
-> (LatticeSyntax a -> LatticeSyntax a -> Bool)
-> (LatticeSyntax a -> LatticeSyntax a -> Bool)
-> (LatticeSyntax a -> LatticeSyntax a -> Bool)
-> (LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a)
-> (LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a)
-> Ord (LatticeSyntax a)
LatticeSyntax a -> LatticeSyntax a -> Bool
LatticeSyntax a -> LatticeSyntax a -> Ordering
LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
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
$cp1Ord :: forall a. Ord a => Eq (LatticeSyntax a)
Ord, ReadPrec [LatticeSyntax a]
ReadPrec (LatticeSyntax a)
Int -> ReadS (LatticeSyntax a)
ReadS [LatticeSyntax a]
(Int -> ReadS (LatticeSyntax a))
-> ReadS [LatticeSyntax a]
-> ReadPrec (LatticeSyntax a)
-> ReadPrec [LatticeSyntax a]
-> Read (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
[LatticeSyntax a] -> ShowS
LatticeSyntax a -> String
(Int -> LatticeSyntax a -> ShowS)
-> (LatticeSyntax a -> String)
-> ([LatticeSyntax a] -> ShowS)
-> Show (LatticeSyntax a)
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, a -> LatticeSyntax b -> LatticeSyntax a
(a -> b) -> LatticeSyntax a -> LatticeSyntax b
(forall a b. (a -> b) -> LatticeSyntax a -> LatticeSyntax b)
-> (forall a b. a -> LatticeSyntax b -> LatticeSyntax a)
-> Functor LatticeSyntax
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
<$ :: a -> LatticeSyntax b -> LatticeSyntax a
$c<$ :: forall a b. a -> LatticeSyntax b -> LatticeSyntax a
fmap :: (a -> b) -> LatticeSyntax a -> LatticeSyntax b
$cfmap :: forall a b. (a -> b) -> LatticeSyntax a -> LatticeSyntax b
Functor, LatticeSyntax a -> Bool
(a -> m) -> LatticeSyntax a -> m
(a -> b -> b) -> b -> LatticeSyntax a -> b
(forall m. Monoid m => LatticeSyntax m -> m)
-> (forall m a. Monoid m => (a -> m) -> LatticeSyntax a -> m)
-> (forall m a. Monoid m => (a -> m) -> LatticeSyntax a -> m)
-> (forall a b. (a -> b -> b) -> b -> LatticeSyntax a -> b)
-> (forall a b. (a -> b -> b) -> b -> LatticeSyntax a -> b)
-> (forall b a. (b -> a -> b) -> b -> LatticeSyntax a -> b)
-> (forall b a. (b -> a -> b) -> b -> LatticeSyntax a -> b)
-> (forall a. (a -> a -> a) -> LatticeSyntax a -> a)
-> (forall a. (a -> a -> a) -> LatticeSyntax a -> a)
-> (forall a. LatticeSyntax a -> [a])
-> (forall a. LatticeSyntax a -> Bool)
-> (forall a. LatticeSyntax a -> Int)
-> (forall a. Eq a => a -> LatticeSyntax a -> Bool)
-> (forall a. Ord a => LatticeSyntax a -> a)
-> (forall a. Ord a => LatticeSyntax a -> a)
-> (forall a. Num a => LatticeSyntax a -> a)
-> (forall a. Num a => LatticeSyntax a -> a)
-> Foldable LatticeSyntax
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 :: LatticeSyntax a -> a
$cproduct :: forall a. Num a => LatticeSyntax a -> a
sum :: LatticeSyntax a -> a
$csum :: forall a. Num a => LatticeSyntax a -> a
minimum :: LatticeSyntax a -> a
$cminimum :: forall a. Ord a => LatticeSyntax a -> a
maximum :: LatticeSyntax a -> a
$cmaximum :: forall a. Ord a => LatticeSyntax a -> a
elem :: a -> LatticeSyntax a -> Bool
$celem :: forall a. Eq a => a -> LatticeSyntax a -> Bool
length :: LatticeSyntax a -> Int
$clength :: forall a. LatticeSyntax a -> Int
null :: LatticeSyntax a -> Bool
$cnull :: forall a. LatticeSyntax a -> Bool
toList :: LatticeSyntax a -> [a]
$ctoList :: forall a. LatticeSyntax a -> [a]
foldl1 :: (a -> a -> a) -> LatticeSyntax a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> LatticeSyntax a -> a
foldr1 :: (a -> a -> a) -> LatticeSyntax a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> LatticeSyntax a -> a
foldl' :: (b -> a -> b) -> b -> LatticeSyntax a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> LatticeSyntax a -> b
foldl :: (b -> a -> b) -> b -> LatticeSyntax a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> LatticeSyntax a -> b
foldr' :: (a -> b -> b) -> b -> LatticeSyntax a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> LatticeSyntax a -> b
foldr :: (a -> b -> b) -> b -> LatticeSyntax a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> LatticeSyntax a -> b
foldMap' :: (a -> m) -> LatticeSyntax a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> LatticeSyntax a -> m
foldMap :: (a -> m) -> LatticeSyntax a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> LatticeSyntax a -> m
fold :: LatticeSyntax m -> m
$cfold :: forall m. Monoid m => LatticeSyntax m -> m
Foldable, Functor LatticeSyntax
Foldable LatticeSyntax
Functor LatticeSyntax
-> Foldable LatticeSyntax
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> LatticeSyntax a -> f (LatticeSyntax b))
-> (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 (m :: * -> *) a.
    Monad m =>
    LatticeSyntax (m a) -> m (LatticeSyntax a))
-> Traversable LatticeSyntax
(a -> f b) -> LatticeSyntax a -> f (LatticeSyntax b)
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 :: LatticeSyntax (m a) -> m (LatticeSyntax a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
LatticeSyntax (m a) -> m (LatticeSyntax a)
mapM :: (a -> m b) -> LatticeSyntax a -> m (LatticeSyntax b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LatticeSyntax a -> m (LatticeSyntax b)
sequenceA :: LatticeSyntax (f a) -> f (LatticeSyntax a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
LatticeSyntax (f a) -> f (LatticeSyntax a)
traverse :: (a -> f b) -> LatticeSyntax a -> f (LatticeSyntax b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LatticeSyntax a -> f (LatticeSyntax b)
$cp2Traversable :: Foldable LatticeSyntax
$cp1Traversable :: Functor LatticeSyntax
Traversable, Typeable, Typeable (LatticeSyntax a)
DataType
Constr
Typeable (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 (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (LatticeSyntax a))
-> (LatticeSyntax a -> Constr)
-> (LatticeSyntax a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (LatticeSyntax a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (LatticeSyntax a)))
-> ((forall b. Data b => b -> b)
    -> LatticeSyntax a -> LatticeSyntax a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LatticeSyntax a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LatticeSyntax a -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> LatticeSyntax a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LatticeSyntax a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> LatticeSyntax a -> m (LatticeSyntax a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LatticeSyntax a -> m (LatticeSyntax a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LatticeSyntax a -> m (LatticeSyntax a))
-> Data (LatticeSyntax a)
LatticeSyntax a -> DataType
LatticeSyntax a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (LatticeSyntax a))
(forall b. Data b => b -> b) -> LatticeSyntax a -> LatticeSyntax a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LatticeSyntax a -> c (LatticeSyntax a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (LatticeSyntax a)
forall a. Data a => Typeable (LatticeSyntax a)
forall a. Data a => LatticeSyntax a -> DataType
forall a. Data a => LatticeSyntax a -> Constr
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 u.
Int -> (forall d. Data d => d -> u) -> LatticeSyntax a -> u
forall u. (forall d. Data d => d -> u) -> LatticeSyntax a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LatticeSyntax a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LatticeSyntax a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LatticeSyntax a -> m (LatticeSyntax a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LatticeSyntax a -> m (LatticeSyntax 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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (LatticeSyntax a))
$cLMeet :: Constr
$cLJoin :: Constr
$cLBound :: Constr
$cLVar :: Constr
$tLatticeSyntax :: DataType
gmapMo :: (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 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 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 :: 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 d. Data d => d -> u) -> LatticeSyntax a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> LatticeSyntax a -> [u]
gmapQr :: (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 :: (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 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 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 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 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)
$cp1Data :: forall a. Data a => Typeable (LatticeSyntax a)
Data)

instance Applicative LatticeSyntax where
  pure :: a -> LatticeSyntax a
pure  = a -> LatticeSyntax a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: LatticeSyntax (a -> b) -> LatticeSyntax a -> LatticeSyntax 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 :: a -> LatticeSyntax a
return = a -> LatticeSyntax a
forall a. a -> LatticeSyntax a
LVar
  LVar a
x    >>= :: LatticeSyntax a -> (a -> LatticeSyntax b) -> LatticeSyntax b
>>= a -> LatticeSyntax b
f = a -> LatticeSyntax b
f a
x
  LBound Bool
b  >>= a -> LatticeSyntax b
_ = Bool -> LatticeSyntax b
forall a. Bool -> LatticeSyntax a
LBound Bool
b
  LJoin LatticeSyntax a
a LatticeSyntax a
b >>= a -> LatticeSyntax b
f = LatticeSyntax b -> LatticeSyntax b -> LatticeSyntax b
forall a. LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
LJoin (LatticeSyntax a
a LatticeSyntax a -> (a -> LatticeSyntax b) -> LatticeSyntax b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> LatticeSyntax b
f) (LatticeSyntax a
b LatticeSyntax a -> (a -> LatticeSyntax b) -> LatticeSyntax 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 = LatticeSyntax b -> LatticeSyntax b -> LatticeSyntax b
forall a. LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
LMeet (LatticeSyntax a
a LatticeSyntax a -> (a -> LatticeSyntax b) -> LatticeSyntax b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> LatticeSyntax b
f) (LatticeSyntax a
b LatticeSyntax a -> (a -> LatticeSyntax b) -> LatticeSyntax b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> LatticeSyntax b
f)

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

dual :: LatticeSyntax a -> LatticeSyntax a
dual :: LatticeSyntax a -> LatticeSyntax a
dual (LVar a
v) = a -> LatticeSyntax a
forall a. a -> LatticeSyntax a
LVar a
v
dual (LBound Bool
t) = Bool -> LatticeSyntax a
forall a. Bool -> LatticeSyntax a
LBound (Bool -> LatticeSyntax a) -> Bool -> LatticeSyntax a
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
t
dual (LJoin LatticeSyntax a
a LatticeSyntax a
b) = LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
forall a. LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
LMeet (LatticeSyntax a -> LatticeSyntax a
forall a. LatticeSyntax a -> LatticeSyntax a
dual LatticeSyntax a
a) (LatticeSyntax a -> LatticeSyntax a
forall a. LatticeSyntax a -> LatticeSyntax a
dual LatticeSyntax a
b)
dual (LMeet LatticeSyntax a
a LatticeSyntax a
b) = LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
forall a. LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
LJoin (LatticeSyntax a -> LatticeSyntax a
forall a. LatticeSyntax a -> LatticeSyntax a
dual LatticeSyntax a
a) (LatticeSyntax a -> LatticeSyntax 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 :: LatticeSyntax a -> LatticeSyntax a -> Bool
equivalent LatticeSyntax a
a LatticeSyntax a
b = ((Bool, Bool) -> Bool) -> [(Bool, Bool)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Bool -> Bool -> Bool) -> (Bool, Bool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==)) ([(Bool, Bool)] -> Bool)
-> (Eval a (Bool, Bool) -> [(Bool, Bool)])
-> Eval a (Bool, Bool)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eval a (Bool, Bool) -> [(Bool, Bool)]
forall v a. Eval v a -> [a]
runEval (Eval a (Bool, Bool) -> Bool) -> Eval a (Bool, Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ Eval a (Bool, Bool)
p
  where p :: Eval a (Bool, Bool)
p = (,) (Bool -> Bool -> (Bool, Bool))
-> Eval a Bool -> Eval a (Bool -> (Bool, Bool))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LatticeSyntax a -> Eval a Bool
forall v. Ord v => LatticeSyntax v -> Eval v Bool
evalLattice LatticeSyntax a
a Eval a (Bool -> (Bool, Bool)) -> Eval a Bool -> Eval a (Bool, Bool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> LatticeSyntax a -> Eval a Bool
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 :: LatticeSyntax a -> LatticeSyntax a -> Bool
preorder LatticeSyntax a
a LatticeSyntax a
b = (LatticeSyntax a
a LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
forall a. LatticeSyntax a -> LatticeSyntax a -> LatticeSyntax a
`LJoin` LatticeSyntax a
b) LatticeSyntax a -> LatticeSyntax a -> Bool
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 :: LatticeSyntax a -> Bool
satisfiable = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool)
-> (LatticeSyntax a -> [Bool]) -> LatticeSyntax a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eval a Bool -> [Bool]
forall v a. Eval v a -> [a]
runEval (Eval a Bool -> [Bool])
-> (LatticeSyntax a -> Eval a Bool) -> LatticeSyntax a -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LatticeSyntax a -> Eval a Bool
forall v. Ord v => LatticeSyntax v -> Eval v Bool
evalLattice

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

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

instance Applicative (Eval v) where
  pure :: a -> Eval v a
pure = a -> Eval v a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: Eval v (a -> b) -> Eval v a -> Eval v 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 :: Eval v a
empty = Eval v a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  <|> :: Eval v a -> Eval v a -> Eval v 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 :: a -> Eval v a
return = StateT (Map v Bool) [] a -> Eval v a
forall v a. StateT (Map v Bool) [] a -> Eval v a
Eval (StateT (Map v Bool) [] a -> Eval v a)
-> (a -> StateT (Map v Bool) [] a) -> a -> Eval v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> StateT (Map v Bool) [] a
forall (m :: * -> *) a. Monad m => a -> m a
return
  Eval StateT (Map v Bool) [] a
m >>= :: Eval v a -> (a -> Eval v b) -> Eval v b
>>= a -> Eval v b
k = StateT (Map v Bool) [] b -> Eval v b
forall v a. StateT (Map v Bool) [] a -> Eval v a
Eval (StateT (Map v Bool) [] b -> Eval v b)
-> StateT (Map v Bool) [] b -> Eval v b
forall a b. (a -> b) -> a -> b
$ StateT (Map v Bool) [] a
m StateT (Map v Bool) [] a
-> (a -> StateT (Map v Bool) [] b) -> StateT (Map v Bool) [] b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Eval v b -> StateT (Map v Bool) [] b
forall v a. Eval v a -> StateT (Map v Bool) [] a
unEval (Eval v b -> StateT (Map v Bool) [] b)
-> (a -> Eval v b) -> a -> StateT (Map v Bool) [] b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eval v b
k

instance MonadPlus (Eval v) where
  mzero :: Eval v a
mzero = StateT (Map v Bool) [] a -> Eval v a
forall v a. StateT (Map v Bool) [] a -> Eval v a
Eval StateT (Map v Bool) [] a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  Eval StateT (Map v Bool) [] a
a mplus :: Eval v a -> Eval v a -> Eval v a
`mplus` Eval StateT (Map v Bool) [] a
b = StateT (Map v Bool) [] a -> Eval v a
forall v a. StateT (Map v Bool) [] a -> Eval v a
Eval (StateT (Map v Bool) [] a -> Eval v a)
-> StateT (Map v Bool) [] a -> Eval v a
forall a b. (a -> b) -> a -> b
$ StateT (Map v Bool) [] a
a StateT (Map v Bool) [] a
-> StateT (Map v Bool) [] a -> StateT (Map v Bool) [] 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 :: Eval v a -> [a]
runEval Eval v a
act = StateT (Map v Bool) [] a -> Map v Bool -> [a]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Eval v a -> StateT (Map v Bool) [] a
forall v a. Eval v a -> StateT (Map v Bool) [] a
unEval Eval v a
act) Map v Bool
forall k a. Map k a
Map.empty

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

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