{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Language.REST.WQOConstraints.Strict (
strictOC
, strictOC'
, difference
, isUnsatisfiable
, noConstraints
, permits
, StrictOC
) where
import Control.Monad.Identity
import GHC.Generics (Generic)
import Data.Hashable
import Data.Maybe
import qualified Data.List as L
import qualified Data.Set as S
import qualified Language.REST.WQOConstraints as OC
import qualified Language.REST.Internal.WQO as WQO
type WQO = WQO.WQO
newtype StrictOC a = StrictOC (S.Set (WQO a))
deriving (StrictOC a -> StrictOC a -> Bool
forall a. Eq a => StrictOC a -> StrictOC a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StrictOC a -> StrictOC a -> Bool
$c/= :: forall a. Eq a => StrictOC a -> StrictOC a -> Bool
== :: StrictOC a -> StrictOC a -> Bool
$c== :: forall a. Eq a => StrictOC a -> StrictOC a -> Bool
Eq, StrictOC a -> StrictOC a -> Bool
StrictOC a -> StrictOC a -> Ordering
StrictOC a -> StrictOC a -> StrictOC 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 (StrictOC a)
forall a. Ord a => StrictOC a -> StrictOC a -> Bool
forall a. Ord a => StrictOC a -> StrictOC a -> Ordering
forall a. Ord a => StrictOC a -> StrictOC a -> StrictOC a
min :: StrictOC a -> StrictOC a -> StrictOC a
$cmin :: forall a. Ord a => StrictOC a -> StrictOC a -> StrictOC a
max :: StrictOC a -> StrictOC a -> StrictOC a
$cmax :: forall a. Ord a => StrictOC a -> StrictOC a -> StrictOC a
>= :: StrictOC a -> StrictOC a -> Bool
$c>= :: forall a. Ord a => StrictOC a -> StrictOC a -> Bool
> :: StrictOC a -> StrictOC a -> Bool
$c> :: forall a. Ord a => StrictOC a -> StrictOC a -> Bool
<= :: StrictOC a -> StrictOC a -> Bool
$c<= :: forall a. Ord a => StrictOC a -> StrictOC a -> Bool
< :: StrictOC a -> StrictOC a -> Bool
$c< :: forall a. Ord a => StrictOC a -> StrictOC a -> Bool
compare :: StrictOC a -> StrictOC a -> Ordering
$ccompare :: forall a. Ord a => StrictOC a -> StrictOC a -> Ordering
Ord, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (StrictOC a) x -> StrictOC a
forall a x. StrictOC a -> Rep (StrictOC a) x
$cto :: forall a x. Rep (StrictOC a) x -> StrictOC a
$cfrom :: forall a x. StrictOC a -> Rep (StrictOC a) x
Generic, forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall {a}. Hashable a => Eq (StrictOC a)
forall a. Hashable a => Int -> StrictOC a -> Int
forall a. Hashable a => StrictOC a -> Int
hash :: StrictOC a -> Int
$chash :: forall a. Hashable a => StrictOC a -> Int
hashWithSalt :: Int -> StrictOC a -> Int
$chashWithSalt :: forall a. Hashable a => Int -> StrictOC a -> Int
Hashable)
instance (Show a, Eq a, Ord a, Hashable a) => Show (StrictOC a) where
show :: StrictOC a -> String
show (StrictOC Set (WQO a)
cs) | forall a. Set a -> Bool
S.null Set (WQO a)
cs = String
"unsatisfiable"
show (StrictOC Set (WQO a)
cs) | forall a. Ord a => a -> Set a -> Bool
S.member forall a. WQO a
WQO.empty Set (WQO a)
cs = String
"no constraints"
show (StrictOC Set (WQO a)
cs) = forall a. [a] -> [[a]] -> [a]
L.intercalate String
" ∨ \n" (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show (forall a. Set a -> [a]
S.toList Set (WQO a)
cs))
getOrdering :: StrictOC a -> Maybe (WQO a)
getOrdering :: forall a. StrictOC a -> Maybe (WQO a)
getOrdering (StrictOC Set (WQO a)
o) =
forall a. [a] -> Maybe a
listToMaybe (forall a. Set a -> [a]
S.toList Set (WQO a)
o)
noConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a
noConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a
noConstraints = forall a. Set (WQO a) -> StrictOC a
StrictOC (forall a. a -> Set a
S.singleton forall a. WQO a
WQO.empty)
unsatisfiable :: StrictOC a
unsatisfiable :: forall a. StrictOC a
unsatisfiable = forall a. Set (WQO a) -> StrictOC a
StrictOC forall a. Set a
S.empty
isUnsatisfiable :: Eq a => StrictOC a -> Bool
isUnsatisfiable :: forall a. Eq a => StrictOC a -> Bool
isUnsatisfiable StrictOC a
c = StrictOC a
c forall a. Eq a => a -> a -> Bool
== forall a. StrictOC a
unsatisfiable
isSatisfiable :: Eq a => StrictOC a -> Bool
isSatisfiable :: forall a. Eq a => StrictOC a -> Bool
isSatisfiable StrictOC a
c = StrictOC a
c forall a. Eq a => a -> a -> Bool
/= forall a. StrictOC a
unsatisfiable
notStrongerThan :: forall m a. (Monad m, Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> m Bool
notStrongerThan :: forall (m :: * -> *) a.
(Monad m, Eq a, Ord a, Hashable a) =>
StrictOC a -> StrictOC a -> m Bool
notStrongerThan (StrictOC Set (WQO a)
_lhs) (StrictOC Set (WQO a)
_rhs) = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
difference :: (Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a
difference :: forall a.
(Eq a, Ord a, Hashable a) =>
StrictOC a -> StrictOC a -> StrictOC a
difference (StrictOC Set (WQO a)
lhs) (StrictOC Set (WQO a)
rhs) =
forall a. Set (WQO a) -> StrictOC a
StrictOC (forall a. Ord a => Set a -> Set a -> Set a
S.difference Set (WQO a)
lhs Set (WQO a)
rhs)
union :: (Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a
union :: forall a.
(Eq a, Ord a, Hashable a) =>
StrictOC a -> StrictOC a -> StrictOC a
union (StrictOC Set (WQO a)
lhs) (StrictOC Set (WQO a)
rhs) =
forall a. (Eq a, Ord a, Hashable a) => Set (WQO a) -> StrictOC a
fromSet forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
S.union Set (WQO a)
lhs Set (WQO a)
rhs
fromSet :: (Eq a, Ord a, Hashable a) => S.Set (WQO a) -> StrictOC a
fromSet :: forall a. (Eq a, Ord a, Hashable a) => Set (WQO a) -> StrictOC a
fromSet Set (WQO a)
oc =
forall a. Set (WQO a) -> StrictOC a
StrictOC forall a b. (a -> b) -> a -> b
$ forall {a}.
(Ord a, Hashable a) =>
[WQO a] -> [WQO a] -> Set (WQO a)
go [] (forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => WQO a -> Set a
WQO.elems) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList Set (WQO a)
oc)
where
go :: [WQO a] -> [WQO a] -> Set (WQO a)
go [WQO a]
include [] = forall a. Ord a => [a] -> Set a
S.fromList [WQO a]
include
go [WQO a]
include (WQO a
x : [WQO a]
xs) =
if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
`WQO.notStrongerThan` WQO a
x) ([WQO a]
include forall a. [a] -> [a] -> [a]
++ [WQO a]
xs)
then [WQO a] -> [WQO a] -> Set (WQO a)
go [WQO a]
include [WQO a]
xs
else [WQO a] -> [WQO a] -> Set (WQO a)
go (WQO a
x forall a. a -> [a] -> [a]
: [WQO a]
include) [WQO a]
xs
intersect :: (Show a, Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a
intersect :: forall a.
(Show a, Eq a, Ord a, Hashable a) =>
StrictOC a -> StrictOC a -> StrictOC a
intersect (StrictOC Set (WQO a)
lhs) (StrictOC Set (WQO a)
rhs) = StrictOC a
result
where
result :: StrictOC a
result = forall a. (Eq a, Ord a, Hashable a) => Set (WQO a) -> StrictOC a
fromSet forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$
do
WQO a
lhs' <- forall a. Set a -> [a]
S.toList Set (WQO a)
lhs
WQO a
rhs' <- forall a. Set a -> [a]
S.toList Set (WQO a)
rhs
forall a. Maybe a -> [a]
maybeToList (forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
lhs' WQO a
rhs')
addConstraint :: (Eq a, Ord a, Hashable a) => WQO a -> StrictOC a -> StrictOC a
addConstraint :: forall a.
(Eq a, Ord a, Hashable a) =>
WQO a -> StrictOC a -> StrictOC a
addConstraint WQO a
c (StrictOC Set (WQO a)
oc) = forall a. Set (WQO a) -> StrictOC a
StrictOC forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ do
WQO a
c' <- forall a. Set a -> [a]
S.toList Set (WQO a)
oc
forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
c WQO a
c'
permits :: (Eq a, Ord a, Hashable a) => StrictOC a -> WQO a -> Bool
permits :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a -> WQO a -> Bool
permits (StrictOC Set (WQO a)
permitted) WQO a
desired =
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
`WQO.notStrongerThan` WQO a
desired) (forall a. Set a -> [a]
S.toList Set (WQO a)
permitted)
strictOC :: Monad m => OC.WQOConstraints StrictOC m
strictOC :: forall (m :: * -> *). Monad m => WQOConstraints StrictOC m
strictOC = forall (impl :: * -> *) (m :: * -> *).
(forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a)
-> (forall a.
(Show a, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a)
-> (forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
impl a -> m Bool)
-> (forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> m Bool)
-> (forall a. (Eq a, Ord a, Hashable a) => impl a)
-> (forall a.
(Show a, Eq a, Ord a, Hashable a) =>
impl a -> WQO a -> Bool)
-> (forall a.
(Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a)
-> (forall a. impl a)
-> (forall a. impl a -> Maybe (WQO a))
-> WQOConstraints impl m
OC.OC
forall a.
(Eq a, Ord a, Hashable a) =>
WQO a -> StrictOC a -> StrictOC a
addConstraint
forall a.
(Show a, Eq a, Ord a, Hashable a) =>
StrictOC a -> StrictOC a -> StrictOC a
intersect
(forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => StrictOC a -> Bool
isSatisfiable)
forall (m :: * -> *) a.
(Monad m, Eq a, Ord a, Hashable a) =>
StrictOC a -> StrictOC a -> m Bool
notStrongerThan
forall a. (Eq a, Ord a, Hashable a) => StrictOC a
noConstraints
forall a. (Eq a, Ord a, Hashable a) => StrictOC a -> WQO a -> Bool
permits
forall a.
(Eq a, Ord a, Hashable a) =>
StrictOC a -> StrictOC a -> StrictOC a
union
forall a. StrictOC a
unsatisfiable
forall a. StrictOC a -> Maybe (WQO a)
getOrdering
strictOC' :: OC.WQOConstraints StrictOC Identity
strictOC' :: WQOConstraints StrictOC Identity
strictOC' = forall (m :: * -> *). Monad m => WQOConstraints StrictOC m
strictOC