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

-- | This module defines a constraint generator for a multiset
--   quasi-ordering. For more details, please see the definition
--   of @mul@ in section 4.2.1 of the paper.
module Language.REST.Internal.MultisetOrder (multisetOrder) where

import GHC.Generics
import qualified Data.List as L
import Prelude hiding (EQ, GT)
import Data.Hashable
import qualified Data.HashSet as S

import qualified Language.REST.Internal.MultiSet as M
import Language.REST.WQOConstraints as OC
import Language.REST.Types

type MultiSet = M.MultiSet

trace' :: String -> a -> a
-- trace' = trace
trace' :: forall a. String -> a -> a
trace' String
_ a
x = a
x

removeEQs :: (Eq x, Ord x, Hashable x) => MultiSet x -> MultiSet x -> (MultiSet x, MultiSet x)
removeEQs :: forall x.
(Eq x, Ord x, Hashable x) =>
MultiSet x -> MultiSet x -> (MultiSet x, MultiSet x)
removeEQs MultiSet x
ts0 = [x] -> MultiSet x -> MultiSet x -> (MultiSet x, MultiSet x)
forall {a}.
Hashable a =>
[a] -> MultiSet a -> MultiSet a -> (MultiSet a, MultiSet a)
go (MultiSet x -> [x]
forall a. MultiSet a -> [a]
M.toList MultiSet x
ts0) MultiSet x
forall a. MultiSet a
M.empty where
  go :: [a] -> MultiSet a -> MultiSet a -> (MultiSet a, MultiSet a)
go []       MultiSet a
ts MultiSet a
us                   = (MultiSet a
ts, MultiSet a
us)
  go (a
x : [a]
xs) MultiSet a
ts MultiSet a
us | a
x a -> MultiSet a -> Bool
forall a. (Eq a, Hashable a) => a -> MultiSet a -> Bool
`M.member` MultiSet a
us = [a] -> MultiSet a -> MultiSet a -> (MultiSet a, MultiSet a)
go [a]
xs MultiSet a
ts (a -> MultiSet a -> MultiSet a
forall a. (Hashable a, Eq a) => a -> MultiSet a -> MultiSet a
M.delete a
x MultiSet a
us)
  go (a
x : [a]
xs) MultiSet a
ts MultiSet a
us        = [a] -> MultiSet a -> MultiSet a -> (MultiSet a, MultiSet a)
go [a]
xs (a -> MultiSet a -> MultiSet a
forall a. (Eq a, Hashable a) => a -> MultiSet a -> MultiSet a
M.insert a
x MultiSet a
ts) MultiSet a
us

data Replace a =
    ReplaceOne a a
  | Replace a (S.HashSet a)
  deriving (Replace a -> Replace a -> Bool
(Replace a -> Replace a -> Bool)
-> (Replace a -> Replace a -> Bool) -> Eq (Replace a)
forall a. Eq a => Replace a -> Replace a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Replace a -> Replace a -> Bool
== :: Replace a -> Replace a -> Bool
$c/= :: forall a. Eq a => Replace a -> Replace a -> Bool
/= :: Replace a -> Replace a -> Bool
Eq, Eq (Replace a)
Eq (Replace a) =>
(Int -> Replace a -> Int)
-> (Replace a -> Int) -> Hashable (Replace a)
Int -> Replace a -> Int
Replace a -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall a. Hashable a => Eq (Replace a)
forall a. Hashable a => Int -> Replace a -> Int
forall a. Hashable a => Replace a -> Int
$chashWithSalt :: forall a. Hashable a => Int -> Replace a -> Int
hashWithSalt :: Int -> Replace a -> Int
$chash :: forall a. Hashable a => Replace a -> Int
hash :: Replace a -> Int
Hashable, (forall x. Replace a -> Rep (Replace a) x)
-> (forall x. Rep (Replace a) x -> Replace a)
-> Generic (Replace a)
forall x. Rep (Replace a) x -> Replace a
forall x. Replace a -> Rep (Replace a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Replace a) x -> Replace a
forall a x. Replace a -> Rep (Replace a) x
$cfrom :: forall a x. Replace a -> Rep (Replace a) x
from :: forall x. Replace a -> Rep (Replace a) x
$cto :: forall a x. Rep (Replace a) x -> Replace a
to :: forall x. Rep (Replace a) x -> Replace a
Generic, Int -> Replace a -> ShowS
[Replace a] -> ShowS
Replace a -> String
(Int -> Replace a -> ShowS)
-> (Replace a -> String)
-> ([Replace a] -> ShowS)
-> Show (Replace a)
forall a. Show a => Int -> Replace a -> ShowS
forall a. Show a => [Replace a] -> ShowS
forall a. Show a => Replace a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Replace a -> ShowS
showsPrec :: Int -> Replace a -> ShowS
$cshow :: forall a. Show a => Replace a -> String
show :: Replace a -> String
$cshowList :: forall a. Show a => [Replace a] -> ShowS
showList :: [Replace a] -> ShowS
Show)

powerset :: [a] -> [[a]]
powerset :: forall a. [a] -> [[a]]
powerset []      = [[]]
powerset (a
x:[a]
xs) = [a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ps | [a]
ps <- [a] -> [[a]]
forall a. [a] -> [[a]]
powerset [a]
xs] [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [a] -> [[a]]
forall a. [a] -> [[a]]
powerset [a]
xs

possibilities :: (Hashable a, Eq a) => Relation -> [a] -> [a] -> S.HashSet (S.HashSet (Replace a))
possibilities :: forall a.
(Hashable a, Eq a) =>
Relation -> [a] -> [a] -> HashSet (HashSet (Replace a))
possibilities Relation
r []     []    = if Relation
r Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
GT then HashSet (HashSet (Replace a))
forall a. HashSet a
S.empty else HashSet (Replace a) -> HashSet (HashSet (Replace a))
forall a. Hashable a => a -> HashSet a
S.singleton HashSet (Replace a)
forall a. HashSet a
S.empty
possibilities Relation
r [a]
xs     []    = if Relation
r Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
EQ then HashSet (HashSet (Replace a))
forall a. HashSet a
S.empty else HashSet (Replace a) -> HashSet (HashSet (Replace a))
forall a. Hashable a => a -> HashSet a
S.singleton ([Replace a] -> HashSet (Replace a)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Replace a] -> HashSet (Replace a))
-> [Replace a] -> HashSet (Replace a)
forall a b. (a -> b) -> a -> b
$ (a -> Replace a) -> [a] -> [Replace a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> HashSet a -> Replace a
forall a. a -> HashSet a -> Replace a
`Replace` HashSet a
forall a. HashSet a
S.empty)  [a]
xs)
possibilities Relation
_ []     (a
_:[a]
_) = HashSet (HashSet (Replace a))
forall a. HashSet a
S.empty
possibilities Relation
r (a
x:[a]
xs) [a]
ys    = if Relation
r Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
EQ then HashSet (HashSet (Replace a))
eqs else HashSet (HashSet (Replace a))
-> HashSet (HashSet (Replace a)) -> HashSet (HashSet (Replace a))
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union HashSet (HashSet (Replace a))
eqs HashSet (HashSet (Replace a))
doms where
  eqs :: HashSet (HashSet (Replace a))
eqs = [HashSet (HashSet (Replace a))] -> HashSet (HashSet (Replace a))
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet (HashSet (Replace a))] -> HashSet (HashSet (Replace a)))
-> [HashSet (HashSet (Replace a))] -> HashSet (HashSet (Replace a))
forall a b. (a -> b) -> a -> b
$ (a -> HashSet (HashSet (Replace a)))
-> [a] -> [HashSet (HashSet (Replace a))]
forall a b. (a -> b) -> [a] -> [b]
map a -> HashSet (HashSet (Replace a))
go [a]
ys where
    go :: a -> HashSet (HashSet (Replace a))
go a
y = (HashSet (Replace a) -> HashSet (Replace a))
-> HashSet (HashSet (Replace a)) -> HashSet (HashSet (Replace a))
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (Replace a -> HashSet (Replace a) -> HashSet (Replace a)
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (a -> a -> Replace a
forall a. a -> a -> Replace a
ReplaceOne a
x a
y)) (Relation -> [a] -> [a] -> HashSet (HashSet (Replace a))
forall a.
(Hashable a, Eq a) =>
Relation -> [a] -> [a] -> HashSet (HashSet (Replace a))
possibilities Relation
r [a]
xs (a -> [a] -> [a]
forall a. Eq a => a -> [a] -> [a]
L.delete a
y [a]
ys))
  doms :: HashSet (HashSet (Replace a))
doms = [HashSet (HashSet (Replace a))] -> HashSet (HashSet (Replace a))
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet (HashSet (Replace a))] -> HashSet (HashSet (Replace a)))
-> [HashSet (HashSet (Replace a))] -> HashSet (HashSet (Replace a))
forall a b. (a -> b) -> a -> b
$ ([a] -> HashSet (HashSet (Replace a)))
-> [[a]] -> [HashSet (HashSet (Replace a))]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> HashSet (HashSet (Replace a))
go ([a] -> [[a]]
forall a. [a] -> [[a]]
powerset ([a] -> [[a]]) -> [a] -> [[a]]
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. Eq a => [a] -> [a]
L.nub [a]
ys) where
    go :: [a] -> HashSet (HashSet (Replace a))
go [a]
ys' = (HashSet (Replace a) -> HashSet (Replace a))
-> HashSet (HashSet (Replace a)) -> HashSet (HashSet (Replace a))
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map
      (Replace a -> HashSet (Replace a) -> HashSet (Replace a)
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (a -> HashSet a -> Replace a
forall a. a -> HashSet a -> Replace a
Replace a
x ([a] -> HashSet a
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [a]
ys')))
      (Relation -> [a] -> [a] -> HashSet (HashSet (Replace a))
forall a.
(Hashable a, Eq a) =>
Relation -> [a] -> [a] -> HashSet (HashSet (Replace a))
possibilities Relation
GTE [a]
xs ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> [a] -> Bool) -> [a] -> a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [a]
ys') [a]
ys))


-- | Given a [constraint generator]("Language.REST.WQOConstraints#t:ConstraintGen") @cgen@ that generates constraints a WQO on
--   @base@ implied by a relation between elements of @lifted@, @'multisetOrder' cgen@
--   yields a constraint generator on elements of base implied by a relation between
--   multisets of @lifted@.
multisetOrder :: forall oc base lifted m . (Ord lifted, Ord base, Show base, Eq base, Hashable base, Hashable lifted, Eq lifted, Show (oc base), Eq (oc base),  Monad m) =>
     ConstraintGen oc base lifted m
  -> ConstraintGen oc base (MultiSet lifted) m
multisetOrder :: forall (oc :: * -> *) base lifted (m :: * -> *).
(Ord lifted, Ord base, Show base, Eq base, Hashable base,
 Hashable lifted, Eq lifted, Show (oc base), Eq (oc base),
 Monad m) =>
ConstraintGen oc base lifted m
-> ConstraintGen oc base (MultiSet lifted) m
multisetOrder ConstraintGen oc base lifted m
_          WQOConstraints oc m'
impl Relation
_ oc base
oc MultiSet lifted
_   MultiSet lifted
_   | oc base
oc oc base -> oc base -> Bool
forall a. Eq a => a -> a -> Bool
== WQOConstraints oc m' -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m'
impl = oc base -> m (oc base)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (oc base -> m (oc base)) -> oc base -> m (oc base)
forall a b. (a -> b) -> a -> b
$ WQOConstraints oc m' -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m'
impl
multisetOrder ConstraintGen oc base lifted m
underlying WQOConstraints oc m'
impl Relation
r oc base
oc MultiSet lifted
ts0 MultiSet lifted
us0 = (MultiSet lifted -> MultiSet lifted -> m (oc base))
-> (MultiSet lifted, MultiSet lifted) -> m (oc base)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry MultiSet lifted -> MultiSet lifted -> m (oc base)
go (MultiSet lifted
-> MultiSet lifted -> (MultiSet lifted, MultiSet lifted)
forall x.
(Eq x, Ord x, Hashable x) =>
MultiSet x -> MultiSet x -> (MultiSet x, MultiSet x)
removeEQs MultiSet lifted
ts0 MultiSet lifted
us0) where
  go :: MultiSet lifted -> MultiSet lifted -> m (oc base)
  go :: MultiSet lifted -> MultiSet lifted -> m (oc base)
go MultiSet lifted
ts MultiSet lifted
us | MultiSet lifted -> Bool
forall a. MultiSet a -> Bool
M.null MultiSet lifted
ts Bool -> Bool -> Bool
&& MultiSet lifted -> Bool
forall a. MultiSet a -> Bool
M.null MultiSet lifted
us             = oc base -> m (oc base)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (oc base -> m (oc base)) -> oc base -> m (oc base)
forall a b. (a -> b) -> a -> b
$ if Relation
r Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
GT then WQOConstraints oc m' -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m'
impl else oc base
oc
  go MultiSet lifted
ts MultiSet lifted
us | Bool -> Bool
not (MultiSet lifted -> Bool
forall a. MultiSet a -> Bool
M.null MultiSet lifted
ts) Bool -> Bool -> Bool
&& MultiSet lifted -> Bool
forall a. MultiSet a -> Bool
M.null MultiSet lifted
us       = oc base -> m (oc base)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (oc base -> m (oc base)) -> oc base -> m (oc base)
forall a b. (a -> b) -> a -> b
$ if Relation
r Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
EQ then WQOConstraints oc m' -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m'
impl else oc base
oc
  go MultiSet lifted
ts MultiSet lifted
us | MultiSet lifted -> Bool
forall a. MultiSet a -> Bool
M.null MultiSet lifted
ts       Bool -> Bool -> Bool
&& Bool -> Bool
not (MultiSet lifted -> Bool
forall a. MultiSet a -> Bool
M.null MultiSet lifted
us) = oc base -> m (oc base)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (oc base -> m (oc base)) -> oc base -> m (oc base)
forall a b. (a -> b) -> a -> b
$ WQOConstraints oc m' -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m'
impl
  go MultiSet lifted
ts MultiSet lifted
us = m (oc base)
result
    where

      pos :: HashSet (HashSet (Replace lifted))
pos = Relation
-> [lifted] -> [lifted] -> HashSet (HashSet (Replace lifted))
forall a.
(Hashable a, Eq a) =>
Relation -> [a] -> [a] -> HashSet (HashSet (Replace a))
possibilities Relation
r (MultiSet lifted -> [lifted]
forall a. MultiSet a -> [a]
M.toList MultiSet lifted
ts) (MultiSet lifted -> [lifted]
forall a. MultiSet a -> [a]
M.toList MultiSet lifted
us)

      result :: m (oc base)
result =
        String -> m (oc base) -> m (oc base)
forall a. String -> a -> a
trace' (String
"There are " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (HashSet (HashSet (Replace lifted)) -> Int
forall a. HashSet a -> Int
S.size HashSet (HashSet (Replace lifted))
pos) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" possibilities") (m (oc base) -> m (oc base)) -> m (oc base) -> m (oc base)
forall a b. (a -> b) -> a -> b
$
        WQOConstraints oc m' -> [oc base] -> oc base
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a, Show a, Show (oc a)) =>
WQOConstraints oc m -> [oc a] -> oc a
unionAll WQOConstraints oc m'
impl ([oc base] -> oc base) -> m [oc base] -> m (oc base)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (HashSet (Replace lifted) -> m (oc base))
-> [HashSet (Replace lifted)] -> m [oc base]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM HashSet (Replace lifted) -> m (oc base)
posConstraints (HashSet (HashSet (Replace lifted)) -> [HashSet (Replace lifted)]
forall a. HashSet a -> [a]
S.toList HashSet (HashSet (Replace lifted))
pos)

      posConstraints :: HashSet (Replace lifted) -> m (oc base)
posConstraints HashSet (Replace lifted)
pos1 = (m (oc base) -> Replace lifted -> m (oc base))
-> m (oc base) -> [Replace lifted] -> m (oc base)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' m (oc base) -> Replace lifted -> m (oc base)
apply (oc base -> m (oc base)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return oc base
oc) (HashSet (Replace lifted) -> [Replace lifted]
forall a. HashSet a -> [a]
S.toList HashSet (Replace lifted)
pos1) where
        apply :: m (oc base) -> Replace lifted -> m (oc base)
apply m (oc base)
moc (ReplaceOne lifted
t lifted
u) = do
          oc base
oc' <- m (oc base)
moc
          WQOConstraints oc m'
-> Relation -> oc base -> lifted -> lifted -> m (oc base)
ConstraintGen oc base lifted m
underlying WQOConstraints oc m'
impl Relation
EQ oc base
oc' lifted
t lifted
u
        apply m (oc base)
moc (Replace lifted
t HashSet lifted
ts') = do
          oc base
oc' <- m (oc base)
moc
          if HashSet lifted -> Bool
forall a. HashSet a -> Bool
S.null HashSet lifted
ts'
            then oc base -> m (oc base)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return oc base
oc'
            else WQOConstraints oc m' -> [oc base] -> oc base
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a, Show a, Show (oc a)) =>
WQOConstraints oc m -> [oc a] -> oc a
intersectAll WQOConstraints oc m'
impl ([oc base] -> oc base) -> m [oc base] -> m (oc base)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (lifted -> m (oc base)) -> [lifted] -> m [oc base]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (WQOConstraints oc m'
-> Relation -> oc base -> lifted -> lifted -> m (oc base)
ConstraintGen oc base lifted m
underlying WQOConstraints oc m'
impl Relation
GT oc base
oc' lifted
t) (HashSet lifted -> [lifted]
forall a. HashSet a -> [a]
S.toList HashSet lifted
ts')