{-# 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 = forall {a}.
Hashable a =>
[a] -> MultiSet a -> MultiSet a -> (MultiSet a, MultiSet a)
go (forall a. MultiSet a -> [a]
M.toList MultiSet x
ts0) 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 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 (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 (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
forall a. Eq a => Replace a -> Replace a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Replace a -> Replace a -> Bool
$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
Eq, 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
hash :: Replace a -> Int
$chash :: forall a. Hashable a => Replace a -> Int
hashWithSalt :: Int -> Replace a -> Int
$chashWithSalt :: forall a. Hashable a => Int -> Replace a -> Int
Hashable, 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
$cto :: forall a x. Rep (Replace a) x -> Replace a
$cfrom :: forall a x. Replace a -> Rep (Replace a) x
Generic, Int -> Replace a -> ShowS
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
showList :: [Replace a] -> ShowS
$cshowList :: forall a. Show a => [Replace a] -> ShowS
show :: Replace a -> String
$cshow :: forall a. Show a => Replace a -> String
showsPrec :: Int -> Replace a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Replace a -> ShowS
Show)

powerset :: [a] -> [[a]]
powerset :: forall a. [a] -> [[a]]
powerset []      = [[]]
powerset (a
x:[a]
xs) = [a
xforall a. a -> [a] -> [a]
:[a]
ps | [a]
ps <- forall a. [a] -> [[a]]
powerset [a]
xs] forall 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 forall a. Eq a => a -> a -> Bool
== Relation
GT then forall a. HashSet a
S.empty else forall a. Hashable a => a -> HashSet a
S.singleton forall a. HashSet a
S.empty
possibilities Relation
r [a]
xs     []    = if Relation
r forall a. Eq a => a -> a -> Bool
== Relation
EQ then forall a. HashSet a
S.empty else forall a. Hashable a => a -> HashSet a
S.singleton (forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> HashSet a -> Replace a
`Replace` forall a. HashSet a
S.empty)  [a]
xs)
possibilities Relation
_ []     (a
_:[a]
_) = forall a. HashSet a
S.empty
possibilities Relation
r (a
x:[a]
xs) [a]
ys    = if Relation
r forall a. Eq a => a -> a -> Bool
== Relation
EQ then HashSet (HashSet (Replace a))
eqs else forall a. (Eq a, Hashable 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 = forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions forall a b. (a -> b) -> a -> b
$ 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 = forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (forall a. a -> a -> Replace a
ReplaceOne a
x a
y)) (forall a.
(Hashable a, Eq a) =>
Relation -> [a] -> [a] -> HashSet (HashSet (Replace a))
possibilities Relation
r [a]
xs (forall a. Eq a => a -> [a] -> [a]
L.delete a
y [a]
ys))
  doms :: HashSet (HashSet (Replace a))
doms = forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map [a] -> HashSet (HashSet (Replace a))
go (forall a. [a] -> [[a]]
powerset forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
L.nub [a]
ys) where
    go :: [a] -> HashSet (HashSet (Replace a))
go [a]
ys' = forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map
      (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (forall a. a -> HashSet a -> Replace a
Replace a
x (forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [a]
ys')))
      (forall a.
(Hashable a, Eq a) =>
Relation -> [a] -> [a] -> HashSet (HashSet (Replace a))
possibilities Relation
GTE [a]
xs (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 forall a. Eq a => a -> a -> Bool
== forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m'
impl = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry MultiSet lifted -> MultiSet lifted -> m (oc base)
go (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 | forall a. MultiSet a -> Bool
M.null MultiSet lifted
ts Bool -> Bool -> Bool
&& forall a. MultiSet a -> Bool
M.null MultiSet lifted
us             = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Relation
r forall a. Eq a => a -> a -> Bool
== Relation
GT then 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 (forall a. MultiSet a -> Bool
M.null MultiSet lifted
ts) Bool -> Bool -> Bool
&& forall a. MultiSet a -> Bool
M.null MultiSet lifted
us       = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Relation
r forall a. Eq a => a -> a -> Bool
== Relation
EQ then 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 | forall a. MultiSet a -> Bool
M.null MultiSet lifted
ts       Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. MultiSet a -> Bool
M.null MultiSet lifted
us) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall a.
(Hashable a, Eq a) =>
Relation -> [a] -> [a] -> HashSet (HashSet (Replace a))
possibilities Relation
r (forall a. MultiSet a -> [a]
M.toList MultiSet lifted
ts) (forall a. MultiSet a -> [a]
M.toList MultiSet lifted
us)

      result :: m (oc base)
result =
        forall a. String -> a -> a
trace' (String
"There are " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. HashSet a -> Int
S.size HashSet (HashSet (Replace lifted))
pos) forall a. [a] -> [a] -> [a]
++ String
" possibilities") forall a b. (a -> b) -> a -> b
$
        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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM HashSet (Replace lifted) -> m (oc base)
posConstraints (forall a. HashSet a -> [a]
S.toList HashSet (HashSet (Replace lifted))
pos)

      posConstraints :: HashSet (Replace lifted) -> m (oc base)
posConstraints HashSet (Replace lifted)
pos1 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' m (oc base) -> Replace lifted -> m (oc base)
apply (forall (m :: * -> *) a. Monad m => a -> m a
return oc base
oc) (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
          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 forall a. HashSet a -> Bool
S.null HashSet lifted
ts'
            then forall (m :: * -> *) a. Monad m => a -> m a
return oc base
oc'
            else 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ConstraintGen oc base lifted m
underlying WQOConstraints oc m'
impl Relation
GT oc base
oc' lifted
t) (forall a. HashSet a -> [a]
S.toList HashSet lifted
ts')