{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Language.REST.WQOConstraints.Strict (
      strictOC
    , strictOC'
    , addConstraint
    , difference
    , getOrdering
    , intersect
    , isSatisfiable
    , isUnsatisfiable
    , noConstraints
    , notStrongerThan
    , permits
    , relevantConstraints
    , union
    , unsatisfiable
    , singleton
    , StrictOC
    , elems
    ) 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

-- Represents a set of constraints on a WQO on type `a`

-- The constraints are represented as a set ws of WQOs
-- The constraints permit any WQO w that is a valid extension of some (w' in wqos)


data StrictOC a = StrictOC (S.Set (WQO a))
  deriving (StrictOC a -> StrictOC a -> Bool
(StrictOC a -> StrictOC a -> Bool)
-> (StrictOC a -> StrictOC a -> Bool) -> Eq (StrictOC a)
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, Eq (StrictOC a)
Eq (StrictOC a)
-> (StrictOC a -> StrictOC a -> Ordering)
-> (StrictOC a -> StrictOC a -> Bool)
-> (StrictOC a -> StrictOC a -> Bool)
-> (StrictOC a -> StrictOC a -> Bool)
-> (StrictOC a -> StrictOC a -> Bool)
-> (StrictOC a -> StrictOC a -> StrictOC a)
-> (StrictOC a -> StrictOC a -> StrictOC a)
-> Ord (StrictOC a)
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
$cp1Ord :: forall a. Ord a => Eq (StrictOC a)
Ord, (forall x. StrictOC a -> Rep (StrictOC a) x)
-> (forall x. Rep (StrictOC a) x -> StrictOC a)
-> Generic (StrictOC a)
forall x. Rep (StrictOC a) x -> StrictOC a
forall x. StrictOC a -> Rep (StrictOC a) x
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, Int -> StrictOC a -> Int
StrictOC a -> Int
(Int -> StrictOC a -> Int)
-> (StrictOC a -> Int) -> Hashable (StrictOC a)
forall a. Hashable a => Int -> StrictOC a -> Int
forall a. Hashable a => StrictOC a -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
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) | Set (WQO a) -> Bool
forall a. Set a -> Bool
S.null Set (WQO a)
cs             = String
"unsatisfiable"
  show (StrictOC Set (WQO a)
cs) | WQO a -> Set (WQO a) -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member WQO a
forall a. WQO a
WQO.empty Set (WQO a)
cs = String
"no constraints"
  show (StrictOC Set (WQO a)
cs) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
" ∨ \n" ((WQO a -> String) -> [WQO a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map WQO a -> String
forall a. Show a => a -> String
show (Set (WQO a) -> [WQO a]
forall a. Set a -> [a]
S.toList Set (WQO a)
cs))
    -- where
      -- show' o@(OpOrdering s) = if S.size s > 1 then printf "(%s)" (show o) else show o

getOrdering :: StrictOC a -> Maybe (WQO a)
getOrdering :: StrictOC a -> Maybe (WQO a)
getOrdering (StrictOC Set (WQO a)
o) =
  [WQO a] -> Maybe (WQO a)
forall a. [a] -> Maybe a
listToMaybe (Set (WQO a) -> [WQO a]
forall a. Set a -> [a]
S.toList Set (WQO a)
o)

elems :: Ord a => StrictOC a -> S.Set a
elems :: StrictOC a -> Set a
elems (StrictOC Set (WQO a)
sets) = [Set a] -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set a] -> Set a) -> [Set a] -> Set a
forall a b. (a -> b) -> a -> b
$ (WQO a -> Set a) -> [WQO a] -> [Set a]
forall a b. (a -> b) -> [a] -> [b]
map WQO a -> Set a
forall a. Ord a => WQO a -> Set a
WQO.elems (Set (WQO a) -> [WQO a]
forall a. Set a -> [a]
S.toList Set (WQO a)
sets)

noConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a
noConstraints :: StrictOC a
noConstraints = Set (WQO a) -> StrictOC a
forall a. Set (WQO a) -> StrictOC a
StrictOC (WQO a -> Set (WQO a)
forall a. a -> Set a
S.singleton (WQO a
forall a. WQO a
WQO.empty))

unsatisfiable :: StrictOC a
unsatisfiable :: StrictOC a
unsatisfiable = Set (WQO a) -> StrictOC a
forall a. Set (WQO a) -> StrictOC a
StrictOC Set (WQO a)
forall a. Set a
S.empty

isUnsatisfiable :: Eq a => StrictOC a -> Bool
isUnsatisfiable :: StrictOC a -> Bool
isUnsatisfiable StrictOC a
c = StrictOC a
c StrictOC a -> StrictOC a -> Bool
forall a. Eq a => a -> a -> Bool
== StrictOC a
forall a. StrictOC a
unsatisfiable

isSatisfiable :: Eq a => StrictOC a -> Bool
isSatisfiable :: StrictOC a -> Bool
isSatisfiable StrictOC a
c = StrictOC a
c StrictOC a -> StrictOC a -> Bool
forall a. Eq a => a -> a -> Bool
/= StrictOC a
forall a. StrictOC a
unsatisfiable

notStrongerThan :: forall m a. (Monad m, Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> m Bool
notStrongerThan :: StrictOC a -> StrictOC a -> m Bool
notStrongerThan (StrictOC Set (WQO a)
_lhs) (StrictOC Set (WQO a)
_rhs) = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- The difference of two constraints `a` and `b` is new constraints such that
-- intersect (diff a b) b = a
difference :: (Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a
difference :: StrictOC a -> StrictOC a -> StrictOC a
difference (StrictOC Set (WQO a)
lhs) (StrictOC Set (WQO a)
rhs) =
    Set (WQO a) -> StrictOC a
forall a. Set (WQO a) -> StrictOC a
StrictOC (Set (WQO a) -> Set (WQO a) -> Set (WQO a)
forall a. Ord a => Set a -> Set a -> Set a
S.difference Set (WQO a)
lhs Set (WQO a)
rhs)

-- The union  of two constraints `a` and `b` is new constraints that only
-- permits an ordering if permitted by either `a` or `b`
union :: (Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a
union :: StrictOC a -> StrictOC a -> StrictOC a
union (StrictOC Set (WQO a)
lhs) (StrictOC Set (WQO a)
rhs) =
  Set (WQO a) -> StrictOC a
forall a. (Eq a, Ord a, Hashable a) => Set (WQO a) -> StrictOC a
fromSet (Set (WQO a) -> StrictOC a) -> Set (WQO a) -> StrictOC a
forall a b. (a -> b) -> a -> b
$ Set (WQO a) -> Set (WQO a) -> Set (WQO a)
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 :: Set (WQO a) -> StrictOC a
fromSet Set (WQO a)
oc = -- StrictOC oc
  Set (WQO a) -> StrictOC a
forall a. Set (WQO a) -> StrictOC a
StrictOC (Set (WQO a) -> StrictOC a) -> Set (WQO a) -> StrictOC a
forall a b. (a -> b) -> a -> b
$ [WQO a] -> [WQO a] -> Set (WQO a)
forall a. (Ord a, Hashable a) => [WQO a] -> [WQO a] -> Set (WQO a)
go [] ((WQO a -> Int) -> [WQO a] -> [WQO a]
forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn (Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Set a -> Int) -> (WQO a -> Set a) -> WQO a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WQO a -> Set a
forall a. Ord a => WQO a -> Set a
WQO.elems) ([WQO a] -> [WQO a]) -> [WQO a] -> [WQO a]
forall a b. (a -> b) -> a -> b
$ Set (WQO a) -> [WQO a]
forall a. Set a -> [a]
S.toList Set (WQO a)
oc)
  where
    go :: [WQO a] -> [WQO a] -> Set (WQO a)
go [WQO a]
include []       = [WQO a] -> Set (WQO a)
forall a. Ord a => [a] -> Set a
S.fromList [WQO a]
include
    go [WQO a]
include (WQO a
x : [WQO a]
xs) =
        if (WQO a -> Bool) -> [WQO a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (WQO a -> WQO a -> Bool
forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
`WQO.notStrongerThan` WQO a
x) ([WQO a]
include [WQO a] -> [WQO a] -> [WQO a]
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 WQO a -> [WQO a] -> [WQO a]
forall a. a -> [a] -> [a]
: [WQO a]
include) [WQO a]
xs


-- The intersection of two constraints `a` and `b` is new constraints that only
-- permits the orderings permitted by both `a` and `b`
intersect :: (Show a, Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a
intersect :: StrictOC a -> StrictOC a -> StrictOC a
intersect (StrictOC Set (WQO a)
lhs) (StrictOC Set (WQO a)
rhs) = StrictOC a
result
  -- trace (printf "%s intersect %s yields %s" (show lhs) (show rhs) (show result)) result
    where
      result :: StrictOC a
result = Set (WQO a) -> StrictOC a
forall a. (Eq a, Ord a, Hashable a) => Set (WQO a) -> StrictOC a
fromSet (Set (WQO a) -> StrictOC a) -> Set (WQO a) -> StrictOC a
forall a b. (a -> b) -> a -> b
$ [WQO a] -> Set (WQO a)
forall a. Ord a => [a] -> Set a
S.fromList ([WQO a] -> Set (WQO a)) -> [WQO a] -> Set (WQO a)
forall a b. (a -> b) -> a -> b
$
        do
          WQO a
lhs' <- Set (WQO a) -> [WQO a]
forall a. Set a -> [a]
S.toList Set (WQO a)
lhs
          WQO a
rhs' <- Set (WQO a) -> [WQO a]
forall a. Set a -> [a]
S.toList Set (WQO a)
rhs
          Maybe (WQO a) -> [WQO a]
forall a. Maybe a -> [a]
maybeToList (WQO a -> WQO a -> Maybe (WQO a)
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 :: WQO a -> StrictOC a -> StrictOC a
addConstraint WQO a
c (StrictOC Set (WQO a)
oc) = Set (WQO a) -> StrictOC a
forall a. Set (WQO a) -> StrictOC a
StrictOC (Set (WQO a) -> StrictOC a) -> Set (WQO a) -> StrictOC a
forall a b. (a -> b) -> a -> b
$ [WQO a] -> Set (WQO a)
forall a. Ord a => [a] -> Set a
S.fromList ([WQO a] -> Set (WQO a)) -> [WQO a] -> Set (WQO a)
forall a b. (a -> b) -> a -> b
$ do
  WQO a
c'  <-  Set (WQO a) -> [WQO a]
forall a. Set a -> [a]
S.toList Set (WQO a)
oc
  Maybe (WQO a) -> [WQO a]
forall a. Maybe a -> [a]
maybeToList (Maybe (WQO a) -> [WQO a]) -> Maybe (WQO a) -> [WQO a]
forall a b. (a -> b) -> a -> b
$ WQO a -> WQO a -> Maybe (WQO a)
forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
c WQO a
c'

singleton :: (Eq a, Ord a, Hashable a) => WQO a -> StrictOC a
singleton :: WQO a -> StrictOC a
singleton WQO a
c = WQO a -> StrictOC a -> StrictOC a
forall a.
(Eq a, Ord a, Hashable a) =>
WQO a -> StrictOC a -> StrictOC a
addConstraint WQO a
c StrictOC a
forall a. (Eq a, Ord a, Hashable a) => StrictOC a
noConstraints

relevantConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a -> S.Set a -> S.Set a -> StrictOC a
relevantConstraints :: StrictOC a -> Set a -> Set a -> StrictOC a
relevantConstraints (StrictOC Set (WQO a)
oc0) Set a
as Set a
bs = [WQO a] -> StrictOC a -> StrictOC a
go (Set (WQO a) -> [WQO a]
forall a. Set a -> [a]
S.toList Set (WQO a)
oc0) StrictOC a
forall a. StrictOC a
unsatisfiable
  where
    go :: [WQO a] -> StrictOC a -> StrictOC a
    go :: [WQO a] -> StrictOC a -> StrictOC a
go []          StrictOC a
oc   = StrictOC a
oc
    go (WQO a
o : [WQO a]
rest) StrictOC a
exist =
      let
        o' :: WQO a
o' = WQO a -> Set a -> Set a -> WQO a
forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> Set a -> Set a -> WQO a
WQO.relevantTo WQO a
o Set a
as Set a
bs
      in
        if WQO a -> Bool
forall a. Eq a => WQO a -> Bool
WQO.null WQO a
o'
        then StrictOC a
forall a. (Eq a, Ord a, Hashable a) => StrictOC a
noConstraints
        else [WQO a] -> StrictOC a -> StrictOC a
go [WQO a]
rest (StrictOC a -> StrictOC a -> StrictOC a
forall a.
(Eq a, Ord a, Hashable a) =>
StrictOC a -> StrictOC a -> StrictOC a
union (WQO a -> StrictOC a
forall a. (Eq a, Ord a, Hashable a) => WQO a -> StrictOC a
singleton WQO a
o) StrictOC a
exist)

permits :: (Eq a, Ord a, Hashable a) => StrictOC a -> WQO a -> Bool
permits :: StrictOC a -> WQO a -> Bool
permits (StrictOC Set (WQO a)
permitted) WQO a
desired =
  (WQO a -> Bool) -> [WQO a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (WQO a -> WQO a -> Bool
forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
`WQO.notStrongerThan` WQO a
desired) (Set (WQO a) -> [WQO a]
forall a. Set a -> [a]
S.toList Set (WQO a)
permitted)

strictOC :: Monad m => OC.WQOConstraints StrictOC m
strictOC :: WQOConstraints StrictOC m
strictOC = (forall a.
 (Eq a, Ord a, Hashable a) =>
 WQO a -> StrictOC a -> StrictOC a)
-> (forall a.
    (Show a, Eq a, Ord a, Hashable a) =>
    StrictOC a -> StrictOC a -> StrictOC a)
-> (forall a.
    (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
    StrictOC a -> m Bool)
-> (forall a.
    (ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
    StrictOC a -> StrictOC a -> m Bool)
-> (forall a. (Eq a, Ord a, Hashable a) => StrictOC a)
-> (forall a.
    (Show a, Eq a, Ord a, Hashable a) =>
    StrictOC a -> WQO a -> Bool)
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    StrictOC a -> Set a -> Set a -> StrictOC a)
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    StrictOC a -> StrictOC a -> StrictOC a)
-> (forall a. StrictOC a)
-> (forall a. (Eq a, Ord a, Hashable a) => StrictOC a -> Set a)
-> (forall a. StrictOC a -> Maybe (WQO a))
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    StrictOC a -> StrictOC a)
-> WQOConstraints StrictOC m
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 -> Set a -> Set a -> impl a)
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    impl a -> impl a -> impl a)
-> (forall a. impl a)
-> (forall a. (Eq a, Ord a, Hashable a) => impl a -> Set a)
-> (forall a. impl a -> Maybe (WQO a))
-> (forall a. (Eq a, Ord a, Hashable a) => impl a -> impl 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
  (Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> (StrictOC a -> Bool) -> StrictOC a -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictOC a -> Bool
forall a. Eq a => StrictOC a -> Bool
isSatisfiable)
  forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
StrictOC a -> StrictOC a -> m Bool
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
forall a.
(Show a, Eq a, Ord a, Hashable a) =>
StrictOC a -> WQO a -> Bool
permits
  forall a.
(Eq a, Ord a, Hashable a) =>
StrictOC a -> Set a -> Set a -> StrictOC a
relevantConstraints
  forall a.
(Eq a, Ord a, Hashable a) =>
StrictOC a -> StrictOC a -> StrictOC a
union
  forall a. StrictOC a
unsatisfiable
  forall a. (Eq a, Ord a, Hashable a) => StrictOC a -> Set a
forall a. Ord a => StrictOC a -> Set a
elems
  forall a. StrictOC a -> Maybe (WQO a)
getOrdering
  forall a. a -> a
forall a. (Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a
id

strictOC' :: OC.WQOConstraints StrictOC Identity
strictOC' :: WQOConstraints StrictOC Identity
strictOC' = WQOConstraints StrictOC Identity
forall (m :: * -> *). Monad m => WQOConstraints StrictOC m
strictOC