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

-- | A boolean formula (without "not") represented as a Disjunctive Normal Form:
-- the formula is a disjunction of a set of clauses, each of which is a
-- conjunction of a set of some elementary formulas.
-- Invariant: no two disjuncts imply eachother
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)

-- A disjunct is a thing that is to be disjuncted. Itself it is a conjunction of some literals.
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)