module Data.OpenApi.Compare.Validate.Schema.DNF
( DNF (..),
Disjunct (..),
pattern SingleDisjunct,
pattern TopDNF,
pattern BottomDNF,
pattern LiteralDNF,
foldDNF,
forDNF,
)
where
import Algebra.Lattice
import Control.Applicative
import Data.Foldable
import qualified Data.Set as S
newtype DNF a = DNF (S.Set (Disjunct a))
deriving stock (DNF a -> DNF a -> Bool
(DNF a -> DNF a -> Bool) -> (DNF a -> DNF a -> Bool) -> Eq (DNF a)
forall a. Eq a => DNF a -> DNF a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DNF a -> DNF a -> Bool
$c/= :: forall a. Eq a => DNF a -> DNF a -> Bool
== :: DNF a -> DNF a -> Bool
$c== :: forall a. Eq a => DNF a -> DNF a -> Bool
Eq, Eq (DNF a)
Eq (DNF a)
-> (DNF a -> DNF a -> Ordering)
-> (DNF a -> DNF a -> Bool)
-> (DNF a -> DNF a -> Bool)
-> (DNF a -> DNF a -> Bool)
-> (DNF a -> DNF a -> Bool)
-> (DNF a -> DNF a -> DNF a)
-> (DNF a -> DNF a -> DNF a)
-> Ord (DNF a)
DNF a -> DNF a -> Bool
DNF a -> DNF a -> Ordering
DNF a -> DNF a -> DNF 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 (DNF a)
forall a. Ord a => DNF a -> DNF a -> Bool
forall a. Ord a => DNF a -> DNF a -> Ordering
forall a. Ord a => DNF a -> DNF a -> DNF a
min :: DNF a -> DNF a -> DNF a
$cmin :: forall a. Ord a => DNF a -> DNF a -> DNF a
max :: DNF a -> DNF a -> DNF a
$cmax :: forall a. Ord a => DNF a -> DNF a -> DNF a
>= :: DNF a -> DNF a -> Bool
$c>= :: forall a. Ord a => DNF a -> DNF a -> Bool
> :: DNF a -> DNF a -> Bool
$c> :: forall a. Ord a => DNF a -> DNF a -> Bool
<= :: DNF a -> DNF a -> Bool
$c<= :: forall a. Ord a => DNF a -> DNF a -> Bool
< :: DNF a -> DNF a -> Bool
$c< :: forall a. Ord a => DNF a -> DNF a -> Bool
compare :: DNF a -> DNF a -> Ordering
$ccompare :: forall a. Ord a => DNF a -> DNF a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (DNF a)
Ord, Int -> DNF a -> ShowS
[DNF a] -> ShowS
DNF a -> String
(Int -> DNF a -> ShowS)
-> (DNF a -> String) -> ([DNF a] -> ShowS) -> Show (DNF a)
forall a. Show a => Int -> DNF a -> ShowS
forall a. Show a => [DNF a] -> ShowS
forall a. Show a => DNF a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DNF a] -> ShowS
$cshowList :: forall a. Show a => [DNF a] -> ShowS
show :: DNF a -> String
$cshow :: forall a. Show a => DNF a -> String
showsPrec :: Int -> DNF a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DNF a -> ShowS
Show)
newtype Disjunct a = Disjunct (S.Set a)
deriving stock (Disjunct a -> Disjunct a -> Bool
(Disjunct a -> Disjunct a -> Bool)
-> (Disjunct a -> Disjunct a -> Bool) -> Eq (Disjunct a)
forall a. Eq a => Disjunct a -> Disjunct a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Disjunct a -> Disjunct a -> Bool
$c/= :: forall a. Eq a => Disjunct a -> Disjunct a -> Bool
== :: Disjunct a -> Disjunct a -> Bool
$c== :: forall a. Eq a => Disjunct a -> Disjunct a -> Bool
Eq, Eq (Disjunct a)
Eq (Disjunct a)
-> (Disjunct a -> Disjunct a -> Ordering)
-> (Disjunct a -> Disjunct a -> Bool)
-> (Disjunct a -> Disjunct a -> Bool)
-> (Disjunct a -> Disjunct a -> Bool)
-> (Disjunct a -> Disjunct a -> Bool)
-> (Disjunct a -> Disjunct a -> Disjunct a)
-> (Disjunct a -> Disjunct a -> Disjunct a)
-> Ord (Disjunct a)
Disjunct a -> Disjunct a -> Bool
Disjunct a -> Disjunct a -> Ordering
Disjunct a -> Disjunct a -> Disjunct 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 (Disjunct a)
forall a. Ord a => Disjunct a -> Disjunct a -> Bool
forall a. Ord a => Disjunct a -> Disjunct a -> Ordering
forall a. Ord a => Disjunct a -> Disjunct a -> Disjunct a
min :: Disjunct a -> Disjunct a -> Disjunct a
$cmin :: forall a. Ord a => Disjunct a -> Disjunct a -> Disjunct a
max :: Disjunct a -> Disjunct a -> Disjunct a
$cmax :: forall a. Ord a => Disjunct a -> Disjunct a -> Disjunct a
>= :: Disjunct a -> Disjunct a -> Bool
$c>= :: forall a. Ord a => Disjunct a -> Disjunct a -> Bool
> :: Disjunct a -> Disjunct a -> Bool
$c> :: forall a. Ord a => Disjunct a -> Disjunct a -> Bool
<= :: Disjunct a -> Disjunct a -> Bool
$c<= :: forall a. Ord a => Disjunct a -> Disjunct a -> Bool
< :: Disjunct a -> Disjunct a -> Bool
$c< :: forall a. Ord a => Disjunct a -> Disjunct a -> Bool
compare :: Disjunct a -> Disjunct a -> Ordering
$ccompare :: forall a. Ord a => Disjunct a -> Disjunct a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Disjunct a)
Ord, Int -> Disjunct a -> ShowS
[Disjunct a] -> ShowS
Disjunct a -> String
(Int -> Disjunct a -> ShowS)
-> (Disjunct a -> String)
-> ([Disjunct a] -> ShowS)
-> Show (Disjunct a)
forall a. Show a => Int -> Disjunct a -> ShowS
forall a. Show a => [Disjunct a] -> ShowS
forall a. Show a => Disjunct a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Disjunct a] -> ShowS
$cshowList :: forall a. Show a => [Disjunct a] -> ShowS
show :: Disjunct a -> String
$cshow :: forall a. Show a => Disjunct a -> String
showsPrec :: Int -> Disjunct a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Disjunct a -> ShowS
Show)
disjImplies :: Ord a => Disjunct a -> Disjunct a -> Bool
disjImplies :: Disjunct a -> Disjunct a -> Bool
disjImplies (Disjunct Set a
xs) (Disjunct Set a
ys) = Set a
ys Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set a
xs
disjConjunction :: Ord a => Disjunct a -> Disjunct a -> Disjunct a
disjConjunction :: Disjunct a -> Disjunct a -> Disjunct a
disjConjunction (Disjunct Set a
xs) (Disjunct Set a
ys) = Set a -> Disjunct a
forall a. Set a -> Disjunct a
Disjunct (Set a -> Disjunct a) -> Set a -> Disjunct a
forall a b. (a -> b) -> a -> b
$ Set a
xs Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Set a
ys
disjAdd :: Ord a => DNF a -> Disjunct a -> DNF a
disjAdd :: DNF a -> Disjunct a -> DNF a
disjAdd (DNF Set (Disjunct a)
yss) Disjunct a
xs
| (Disjunct a -> Bool) -> Set (Disjunct a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Disjunct a
xs Disjunct a -> Disjunct a -> Bool
forall a. Ord a => Disjunct a -> Disjunct a -> Bool
`disjImplies`) Set (Disjunct a)
yss = Set (Disjunct a) -> DNF a
forall a. Set (Disjunct a) -> DNF a
DNF Set (Disjunct a)
yss
| Bool
otherwise = Set (Disjunct a) -> DNF a
forall a. Set (Disjunct a) -> DNF a
DNF (Set (Disjunct a) -> DNF a) -> Set (Disjunct a) -> DNF a
forall a b. (a -> b) -> a -> b
$ Disjunct a -> Set (Disjunct a) -> Set (Disjunct a)
forall a. Ord a => a -> Set a -> Set a
S.insert Disjunct a
xs (Set (Disjunct a) -> Set (Disjunct a))
-> Set (Disjunct a) -> Set (Disjunct a)
forall a b. (a -> b) -> a -> b
$ (Disjunct a -> Bool) -> Set (Disjunct a) -> Set (Disjunct a)
forall a. (a -> Bool) -> Set a -> Set a
S.filter (Bool -> Bool
not (Bool -> Bool) -> (Disjunct a -> Bool) -> Disjunct a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Disjunct a -> Disjunct a -> Bool
forall a. Ord a => Disjunct a -> Disjunct a -> Bool
`disjImplies` Disjunct a
xs)) Set (Disjunct a)
yss
instance Ord a => Lattice (DNF a) where
DNF a
xss \/ :: DNF a -> DNF a -> DNF a
\/ DNF Set (Disjunct a)
yss = (DNF a -> Disjunct a -> DNF a)
-> DNF a -> Set (Disjunct a) -> DNF a
forall a b. (a -> b -> a) -> a -> Set b -> a
S.foldl' DNF a -> Disjunct a -> DNF a
forall a. Ord a => DNF a -> Disjunct a -> DNF a
disjAdd DNF a
xss Set (Disjunct a)
yss
DNF Set (Disjunct a)
xss /\ :: DNF a -> DNF a -> DNF a
/\ DNF Set (Disjunct a)
yss =
(DNF a -> Disjunct a -> DNF a) -> DNF a -> [Disjunct a] -> DNF a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' DNF a -> Disjunct a -> DNF a
forall a. Ord a => DNF a -> Disjunct a -> DNF a
disjAdd DNF a
forall a. BoundedJoinSemiLattice a => a
bottom ([Disjunct a] -> DNF a) -> [Disjunct a] -> DNF a
forall a b. (a -> b) -> a -> b
$
(Disjunct a -> Disjunct a -> Disjunct a)
-> [Disjunct a] -> [Disjunct a] -> [Disjunct a]
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Disjunct a -> Disjunct a -> Disjunct a
forall a. Ord a => Disjunct a -> Disjunct a -> Disjunct a
disjConjunction (Set (Disjunct a) -> [Disjunct a]
forall a. Set a -> [a]
S.toList Set (Disjunct a)
xss) (Set (Disjunct a) -> [Disjunct a]
forall a. Set a -> [a]
S.toList Set (Disjunct a)
yss)
pattern BottomDNF :: DNF a
pattern $bBottomDNF :: DNF a
$mBottomDNF :: forall r a. DNF a -> (Void# -> r) -> (Void# -> r) -> r
BottomDNF <-
DNF (S.null -> True)
where
BottomDNF = Set (Disjunct a) -> DNF a
forall a. Set (Disjunct a) -> DNF a
DNF Set (Disjunct a)
forall a. Set a
S.empty
isSingleton :: S.Set a -> Maybe a
isSingleton :: Set a -> Maybe a
isSingleton Set a
s
| Set a -> Int
forall a. Set a -> Int
S.size Set a
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = Set a -> Maybe a
forall a. Set a -> Maybe a
S.lookupMin Set a
s
| Bool
otherwise = Maybe a
forall a. Maybe a
Nothing
pattern SingleDisjunct :: Ord a => Disjunct a -> DNF a
pattern $bSingleDisjunct :: Disjunct a -> DNF a
$mSingleDisjunct :: forall r a.
Ord a =>
DNF a -> (Disjunct a -> r) -> (Void# -> r) -> r
SingleDisjunct xs <-
DNF (isSingleton -> Just xs)
where
SingleDisjunct Disjunct a
xs = Set (Disjunct a) -> DNF a
forall a. Set (Disjunct a) -> DNF a
DNF (Set (Disjunct a) -> DNF a) -> Set (Disjunct a) -> DNF a
forall a b. (a -> b) -> a -> b
$ Disjunct a -> Set (Disjunct a)
forall a. a -> Set a
S.singleton Disjunct a
xs
pattern TopDNF :: DNF a
pattern $bTopDNF :: DNF a
$mTopDNF :: forall r a. DNF a -> (Void# -> r) -> (Void# -> r) -> r
TopDNF <-
DNF (isSingleton -> Just (Disjunct (S.null -> True)))
where
TopDNF = Set (Disjunct a) -> DNF a
forall a. Set (Disjunct a) -> DNF a
DNF (Set (Disjunct a) -> DNF a) -> Set (Disjunct a) -> DNF a
forall a b. (a -> b) -> a -> b
$ Disjunct a -> Set (Disjunct a)
forall a. a -> Set a
S.singleton (Disjunct a -> Set (Disjunct a)) -> Disjunct a -> Set (Disjunct a)
forall a b. (a -> b) -> a -> b
$ Set a -> Disjunct a
forall a. Set a -> Disjunct a
Disjunct Set a
forall a. Set a
S.empty
pattern LiteralDNF :: Ord a => a -> DNF a
pattern $bLiteralDNF :: a -> DNF a
$mLiteralDNF :: forall r a. Ord a => DNF a -> (a -> r) -> (Void# -> r) -> r
LiteralDNF x <-
SingleDisjunct (Disjunct (isSingleton -> Just x))
where
LiteralDNF a
x = Disjunct a -> DNF a
forall a. Ord a => Disjunct a -> DNF a
SingleDisjunct (Disjunct a -> DNF a) -> Disjunct a -> DNF a
forall a b. (a -> b) -> a -> b
$ Set a -> Disjunct a
forall a. Set a -> Disjunct a
Disjunct (Set a -> Disjunct a) -> Set a -> Disjunct a
forall a b. (a -> b) -> a -> b
$ a -> Set a
forall a. a -> Set a
S.singleton a
x
instance Ord a => BoundedJoinSemiLattice (DNF a) where
bottom :: DNF a
bottom = DNF a
forall a. DNF a
BottomDNF
instance Ord a => BoundedMeetSemiLattice (DNF a) where
top :: DNF a
top = DNF a
forall a. DNF a
TopDNF
foldDisjunct :: BoundedMeetSemiLattice l => (a -> l) -> Disjunct a -> l
foldDisjunct :: (a -> l) -> Disjunct a -> l
foldDisjunct a -> l
f (Disjunct Set a
xs) = (l -> a -> l) -> l -> Set a -> l
forall a b. (a -> b -> a) -> a -> Set b -> a
S.foldl' (\l
y a
l -> l
y l -> l -> l
forall a. Lattice a => a -> a -> a
/\ a -> l
f a
l) l
forall a. BoundedMeetSemiLattice a => a
top Set a
xs
foldDNF :: BoundedLattice l => (a -> l) -> DNF a -> l
foldDNF :: (a -> l) -> DNF a -> l
foldDNF a -> l
f (DNF Set (Disjunct a)
xss) = (l -> Disjunct a -> l) -> l -> Set (Disjunct a) -> l
forall a b. (a -> b -> a) -> a -> Set b -> a
S.foldl' (\l
y Disjunct a
xs -> l
y l -> l -> l
forall a. Lattice a => a -> a -> a
\/ (a -> l) -> Disjunct a -> l
forall l a. BoundedMeetSemiLattice l => (a -> l) -> Disjunct a -> l
foldDisjunct a -> l
f Disjunct a
xs) l
forall a. BoundedJoinSemiLattice a => a
bottom Set (Disjunct a)
xss
newtype LiftA f a = LiftA {LiftA f a -> f a
getLiftA :: f a}
deriving newtype (a -> LiftA f b -> LiftA f a
(a -> b) -> LiftA f a -> LiftA f b
(forall a b. (a -> b) -> LiftA f a -> LiftA f b)
-> (forall a b. a -> LiftA f b -> LiftA f a) -> Functor (LiftA f)
forall a b. a -> LiftA f b -> LiftA f a
forall a b. (a -> b) -> LiftA f a -> LiftA f b
forall (f :: * -> *) a b. Functor f => a -> LiftA f b -> LiftA f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> LiftA f a -> LiftA f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> LiftA f b -> LiftA f a
$c<$ :: forall (f :: * -> *) a b. Functor f => a -> LiftA f b -> LiftA f a
fmap :: (a -> b) -> LiftA f a -> LiftA f b
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> LiftA f a -> LiftA f b
Functor, Functor (LiftA f)
a -> LiftA f a
Functor (LiftA f)
-> (forall a. a -> LiftA f a)
-> (forall a b. LiftA f (a -> b) -> LiftA f a -> LiftA f b)
-> (forall a b c.
(a -> b -> c) -> LiftA f a -> LiftA f b -> LiftA f c)
-> (forall a b. LiftA f a -> LiftA f b -> LiftA f b)
-> (forall a b. LiftA f a -> LiftA f b -> LiftA f a)
-> Applicative (LiftA f)
LiftA f a -> LiftA f b -> LiftA f b
LiftA f a -> LiftA f b -> LiftA f a
LiftA f (a -> b) -> LiftA f a -> LiftA f b
(a -> b -> c) -> LiftA f a -> LiftA f b -> LiftA f c
forall a. a -> LiftA f a
forall a b. LiftA f a -> LiftA f b -> LiftA f a
forall a b. LiftA f a -> LiftA f b -> LiftA f b
forall a b. LiftA f (a -> b) -> LiftA f a -> LiftA f b
forall a b c. (a -> b -> c) -> LiftA f a -> LiftA f b -> LiftA f c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (f :: * -> *). Applicative f => Functor (LiftA f)
forall (f :: * -> *) a. Applicative f => a -> LiftA f a
forall (f :: * -> *) a b.
Applicative f =>
LiftA f a -> LiftA f b -> LiftA f a
forall (f :: * -> *) a b.
Applicative f =>
LiftA f a -> LiftA f b -> LiftA f b
forall (f :: * -> *) a b.
Applicative f =>
LiftA f (a -> b) -> LiftA f a -> LiftA f b
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> LiftA f a -> LiftA f b -> LiftA f c
<* :: LiftA f a -> LiftA f b -> LiftA f a
$c<* :: forall (f :: * -> *) a b.
Applicative f =>
LiftA f a -> LiftA f b -> LiftA f a
*> :: LiftA f a -> LiftA f b -> LiftA f b
$c*> :: forall (f :: * -> *) a b.
Applicative f =>
LiftA f a -> LiftA f b -> LiftA f b
liftA2 :: (a -> b -> c) -> LiftA f a -> LiftA f b -> LiftA f c
$cliftA2 :: forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> LiftA f a -> LiftA f b -> LiftA f c
<*> :: LiftA f (a -> b) -> LiftA f a -> LiftA f b
$c<*> :: forall (f :: * -> *) a b.
Applicative f =>
LiftA f (a -> b) -> LiftA f a -> LiftA f b
pure :: a -> LiftA f a
$cpure :: forall (f :: * -> *) a. Applicative f => a -> LiftA f a
$cp1Applicative :: forall (f :: * -> *). Applicative f => Functor (LiftA f)
Applicative)
instance (Lattice a, Applicative f) => Lattice (LiftA f a) where
/\ :: LiftA f a -> LiftA f a -> LiftA f a
(/\) = (a -> a -> a) -> LiftA f a -> LiftA f a -> LiftA f a
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall a. Lattice a => a -> a -> a
(/\)
\/ :: LiftA f a -> LiftA f a -> LiftA f a
(\/) = (a -> a -> a) -> LiftA f a -> LiftA f a -> LiftA f a
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall a. Lattice a => a -> a -> a
(\/)
instance (BoundedJoinSemiLattice a, Applicative f) => BoundedJoinSemiLattice (LiftA f a) where
bottom :: LiftA f a
bottom = a -> LiftA f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
forall a. BoundedJoinSemiLattice a => a
bottom
instance (BoundedMeetSemiLattice a, Applicative f) => BoundedMeetSemiLattice (LiftA f a) where
top :: LiftA f a
top = a -> LiftA f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
forall a. BoundedMeetSemiLattice a => a
top
forDNF :: (BoundedLattice l, Applicative f) => (a -> f l) -> DNF a -> f l
forDNF :: (a -> f l) -> DNF a -> f l
forDNF a -> f l
f = LiftA f l -> f l
forall k (f :: k -> *) (a :: k). LiftA f a -> f a
getLiftA (LiftA f l -> f l) -> (DNF a -> LiftA f l) -> DNF a -> f l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> LiftA f l) -> DNF a -> LiftA f l
forall l a. BoundedLattice l => (a -> l) -> DNF a -> l
foldDNF (f l -> LiftA f l
forall k (f :: k -> *) (a :: k). f a -> LiftA f a
LiftA (f l -> LiftA f l) -> (a -> f l) -> a -> LiftA f l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f l
f)