{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

module Language.REST.Internal.WQO (
      empty
    , insert
    , insertMaybe
    , orderings
    , getRelation
    , merge
    , mergeAll
    , notStrongerThan
    , WQO
    , QORelation(..)
    , ExtendOrderingResult(..)
    , relevantTo
    , singleton
    , null
    , getPO
    , getECs
    , elems) where

import Prelude hiding (null, EQ, GT)
import GHC.Generics (Generic)
import qualified Data.Map as M
import Control.Monad
import Data.Hashable
import Data.Maybe
import qualified Data.List as L
import qualified Data.Set as S

import qualified Language.REST.Internal.EquivalenceClass as EC
import qualified Language.REST.Internal.PartialOrder as PO
import Language.REST.Internal.Orphans ()
import Language.REST.Op
import Language.REST.SMT

type PartialOrder     = PO.PartialOrder
type EquivalenceClass = EC.EquivalenceClass

data QORelation = QGT | QEQ deriving (Eq QORelation
QORelation -> QORelation -> Bool
QORelation -> QORelation -> Ordering
QORelation -> QORelation -> QORelation
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
min :: QORelation -> QORelation -> QORelation
$cmin :: QORelation -> QORelation -> QORelation
max :: QORelation -> QORelation -> QORelation
$cmax :: QORelation -> QORelation -> QORelation
>= :: QORelation -> QORelation -> Bool
$c>= :: QORelation -> QORelation -> Bool
> :: QORelation -> QORelation -> Bool
$c> :: QORelation -> QORelation -> Bool
<= :: QORelation -> QORelation -> Bool
$c<= :: QORelation -> QORelation -> Bool
< :: QORelation -> QORelation -> Bool
$c< :: QORelation -> QORelation -> Bool
compare :: QORelation -> QORelation -> Ordering
$ccompare :: QORelation -> QORelation -> Ordering
Ord, QORelation -> QORelation -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QORelation -> QORelation -> Bool
$c/= :: QORelation -> QORelation -> Bool
== :: QORelation -> QORelation -> Bool
$c== :: QORelation -> QORelation -> Bool
Eq, forall x. Rep QORelation x -> QORelation
forall x. QORelation -> Rep QORelation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep QORelation x -> QORelation
$cfrom :: forall x. QORelation -> Rep QORelation x
Generic, Eq QORelation
Int -> QORelation -> Int
QORelation -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: QORelation -> Int
$chash :: QORelation -> Int
hashWithSalt :: Int -> QORelation -> Int
$chashWithSalt :: Int -> QORelation -> Int
Hashable)

instance Show QORelation where
  show :: QORelation -> String
show QORelation
QGT = String
">"
  show QORelation
QEQ = String
"≈"

instance {-# OVERLAPPING #-} ToSMTVar a Int => ToSMT (WQO a) Bool where
  toSMT :: WQO a -> SMTExpr Bool
toSMT (WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
po) = [SMTExpr Bool] -> SMTExpr Bool
And forall a b. (a -> b) -> a -> b
$ [SMTExpr Bool]
ecsSMT forall a. [a] -> [a] -> [a]
++ [SMTExpr Bool]
posSMT where

    toSMT' :: a -> SMTExpr Int
    toSMT' :: a -> SMTExpr Int
toSMT' = forall a b. ToSMT a b => a -> SMTExpr b
toSMT

    ecsSMT :: [SMTExpr Bool]
ecsSMT = do
      EquivalenceClass a
ec <- forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
ecs
      let ecl :: [a]
ecl = forall a. EquivalenceClass a -> [a]
EC.toList EquivalenceClass a
ec
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ecl forall a. Ord a => a -> a -> Bool
>= Int
2
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [SMTExpr a] -> SMTExpr Bool
Equal (forall a b. (a -> b) -> [a] -> [b]
map a -> SMTExpr Int
toSMT' [a]
ecl)

    posSMT :: [SMTExpr Bool]
posSMT = do
      (EquivalenceClass a
ec, Set (EquivalenceClass a)
vs) <- forall k. PartialOrder k -> [(k, Set k)]
PO.toDescsList PartialOrder (EquivalenceClass a)
po
      EquivalenceClass a
var        <- forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
vs
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SMTExpr Int -> SMTExpr Int -> SMTExpr Bool
Greater (forall a b. ToSMT a b => a -> SMTExpr b
toSMT forall a b. (a -> b) -> a -> b
$ forall a. EquivalenceClass a -> a
EC.head EquivalenceClass a
ec) (forall a b. ToSMT a b => a -> SMTExpr b
toSMT forall a b. (a -> b) -> a -> b
$ forall a. EquivalenceClass a -> a
EC.head EquivalenceClass a
var)


getPO :: WQO a -> PartialOrder (EquivalenceClass a)
getPO :: forall a. WQO a -> PartialOrder (EquivalenceClass a)
getPO (WQO Set (EquivalenceClass a)
_ PartialOrder (EquivalenceClass a)
po)  = PartialOrder (EquivalenceClass a)
po

getECs :: WQO a -> S.Set (EquivalenceClass a)
getECs :: forall a. WQO a -> Set (EquivalenceClass a)
getECs (WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
_) = Set (EquivalenceClass a)
ecs

-- | Well-founded reflexive partial orders
data WQO a =
  -- Invariant: the first set contains all equivalence classes
  --
  -- The strict partial order describes the ordering of the
  -- equivalence classes in the first set.
  WQO (S.Set (EquivalenceClass a)) (PartialOrder (EquivalenceClass a))
  deriving (WQO a -> WQO a -> Bool
WQO a -> WQO a -> Ordering
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 (WQO a)
forall a. Ord a => WQO a -> WQO a -> Bool
forall a. Ord a => WQO a -> WQO a -> Ordering
forall a. Ord a => WQO a -> WQO a -> WQO a
min :: WQO a -> WQO a -> WQO a
$cmin :: forall a. Ord a => WQO a -> WQO a -> WQO a
max :: WQO a -> WQO a -> WQO a
$cmax :: forall a. Ord a => WQO a -> WQO a -> WQO a
>= :: WQO a -> WQO a -> Bool
$c>= :: forall a. Ord a => WQO a -> WQO a -> Bool
> :: WQO a -> WQO a -> Bool
$c> :: forall a. Ord a => WQO a -> WQO a -> Bool
<= :: WQO a -> WQO a -> Bool
$c<= :: forall a. Ord a => WQO a -> WQO a -> Bool
< :: WQO a -> WQO a -> Bool
$c< :: forall a. Ord a => WQO a -> WQO a -> Bool
compare :: WQO a -> WQO a -> Ordering
$ccompare :: forall a. Ord a => WQO a -> WQO a -> Ordering
Ord, WQO a -> WQO a -> Bool
forall a. Eq a => WQO a -> WQO a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WQO a -> WQO a -> Bool
$c/= :: forall a. Eq a => WQO a -> WQO a -> Bool
== :: WQO a -> WQO a -> Bool
$c== :: forall a. Eq a => WQO a -> WQO a -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (WQO a) x -> WQO a
forall a x. WQO a -> Rep (WQO a) x
$cto :: forall a x. Rep (WQO a) x -> WQO a
$cfrom :: forall a x. WQO a -> Rep (WQO a) x
Generic, forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall {a}. Hashable a => Eq (WQO a)
forall a. Hashable a => Int -> WQO a -> Int
forall a. Hashable a => WQO a -> Int
hash :: WQO a -> Int
$chash :: forall a. Hashable a => WQO a -> Int
hashWithSalt :: Int -> WQO a -> Int
$chashWithSalt :: forall a. Hashable a => Int -> WQO a -> Int
Hashable)

instance (Show a, Eq a, Hashable a) => Show (WQO a) where
    show :: WQO a -> String
show (WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
_)  | forall a. Set a -> Bool
S.null Set (EquivalenceClass a)
ecs  = String
"⊤"
    show (WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
po) = forall a. [a] -> [[a]] -> [a]
L.intercalate String
" ∧ " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [EquivalenceClass a]
ecs' forall a. [a] -> [a] -> [a]
++ [String]
po')
        where
            ecs' :: [EquivalenceClass a]
ecs'          = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. EquivalenceClass a -> Bool
EC.isSingleton) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
ecs
            po' :: [String]
po'           =
                [forall a. Show a => a -> String
show PartialOrder (EquivalenceClass a)
po | Bool -> Bool
not (forall a. Eq a => PartialOrder a -> Bool
PO.isEmpty PartialOrder (EquivalenceClass a)
po)]
            --         else [show $ PO.mapUnsafe ecHead po]
            -- ecHead (x, y) = (EC.head x, EC.head y)

null :: Eq a => WQO a -> Bool
null :: forall a. Eq a => WQO a -> Bool
null WQO a
wqo = WQO a
wqo forall a. Eq a => a -> a -> Bool
== forall a. WQO a
empty

empty :: WQO a
empty :: forall a. WQO a
empty = forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO forall a. Set a
S.empty forall a. PartialOrder a
PO.empty

singleton :: (Ord a, Eq a, Hashable a) => (a, a, QORelation) -> Maybe (WQO a)
singleton :: forall a.
(Ord a, Eq a, Hashable a) =>
(a, a, QORelation) -> Maybe (WQO a)
singleton = forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> (a, a, QORelation) -> Maybe (WQO a)
insertMaybe forall a. WQO a
empty

{-# INLINE elems #-}
elems :: (Ord a) => WQO a -> S.Set a
elems :: forall a. Ord a => WQO a -> Set a
elems (WQO Set (EquivalenceClass a)
ec PartialOrder (EquivalenceClass a)
_) = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. EquivalenceClass a -> Set a
EC.elems (forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
ec)

-- | @getEquivalenceClasses (>=) a b@ retrieves the equivanlence classes of
-- @a@ and @b@.
--
-- TODO: Why are these looked up in pairs and not individually?
{-# INLINE getEquivalenceClasses #-}
getEquivalenceClasses :: (Ord a, Eq a, Hashable a) => WQO a -> a -> a
  -> (Maybe (EquivalenceClass a), Maybe (EquivalenceClass a))
getEquivalenceClasses :: forall a.
(Ord a, Eq a, Hashable a) =>
WQO a
-> a
-> a
-> (Maybe (EquivalenceClass a), Maybe (EquivalenceClass a))
getEquivalenceClasses (WQO Set (EquivalenceClass a)
classes PartialOrder (EquivalenceClass a)
_) a
source a
target = (Maybe (EquivalenceClass a)
t, Maybe (EquivalenceClass a)
u)
  where
    t :: Maybe (EquivalenceClass a)
t = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> Bool
EC.isMember a
source) [EquivalenceClass a]
classes'
    u :: Maybe (EquivalenceClass a)
u = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> Bool
EC.isMember a
target) [EquivalenceClass a]
classes'
    classes' :: [EquivalenceClass a]
classes' = forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
classes

-- | Like @getEquivalenceClasses@ but only yields a result
-- if classes of equivalence are found for both elements.
{-# INLINE getEquivalenceClasses' #-}
getEquivalenceClasses'
  :: (Ord a, Hashable a)
  => WQO a
  -> a
  -> a
  -> Maybe (EC.EquivalenceClass a, EC.EquivalenceClass a)
getEquivalenceClasses' :: forall a.
(Ord a, Hashable a) =>
WQO a -> a -> a -> Maybe (EquivalenceClass a, EquivalenceClass a)
getEquivalenceClasses' (WQO Set (EquivalenceClass a)
classes PartialOrder (EquivalenceClass a)
_) a
source a
target =
  do
    EquivalenceClass a
t <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> Bool
EC.isMember a
source) [EquivalenceClass a]
classes'
    if forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> Bool
EC.isMember a
target EquivalenceClass a
t
      then forall (m :: * -> *) a. Monad m => a -> m a
return (EquivalenceClass a
t, EquivalenceClass a
t)
      else (EquivalenceClass a
t,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> Bool
EC.isMember a
target) [EquivalenceClass a]
classes'
  where
    classes' :: [EquivalenceClass a]
classes' = forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
classes

-- | @getRelation (>=) a b == QEQ@ iff @a >= b@
--   @getRelation (>=) a b == QGT@ iff @a > b@
{-# INLINE getRelation #-}
getRelation :: (Ord a, Eq a, Hashable a) => WQO a -> a -> a -> Maybe QORelation
getRelation :: forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> a -> a -> Maybe QORelation
getRelation WQO a
_ a
f a
g | a
f forall a. Eq a => a -> a -> Bool
== a
g = forall a. a -> Maybe a
Just QORelation
QEQ
getRelation wqo :: WQO a
wqo@(WQO Set (EquivalenceClass a)
_ PartialOrder (EquivalenceClass a)
po) a
source a
target
    | Just (EquivalenceClass a
s, EquivalenceClass a
t) <- forall a.
(Ord a, Hashable a) =>
WQO a -> a -> a -> Maybe (EquivalenceClass a, EquivalenceClass a)
getEquivalenceClasses' WQO a
wqo a
source a
target
    = if EquivalenceClass a
s forall a. Eq a => a -> a -> Bool
== EquivalenceClass a
t
        then forall a. a -> Maybe a
Just QORelation
QEQ
        else
            if forall a.
(Eq a, Ord a, Hashable a) =>
PartialOrder a -> a -> a -> Bool
PO.gt PartialOrder (EquivalenceClass a)
po EquivalenceClass a
s EquivalenceClass a
t
                then forall a. a -> Maybe a
Just QORelation
QGT
                else forall a. Maybe a
Nothing
    | Bool
otherwise = forall a. Maybe a
Nothing

-- | @expandEC (>=) ec x@ adds an element @x@ to the equivalence class
-- @ec@ of @(>=)@.
expandEC :: (Ord a, Eq a, Hashable a) => WQO a -> EquivalenceClass a -> a -> WQO a
expandEC :: forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> EquivalenceClass a -> a -> WQO a
expandEC (WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
po) EquivalenceClass a
ec a
x = forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
ecs' PartialOrder (EquivalenceClass a)
po'
    where
        ec' :: EquivalenceClass a
ec'  = forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> EquivalenceClass a
EC.insert a
x EquivalenceClass a
ec
        ecs' :: Set (EquivalenceClass a)
ecs' = forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
ec' forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
S.delete EquivalenceClass a
ec Set (EquivalenceClass a)
ecs
        po' :: PartialOrder (EquivalenceClass a)
po'  = forall a.
(Eq a, Ord a, Hashable a) =>
[a] -> a -> PartialOrder a -> PartialOrder a
PO.replaceUnsafe [EquivalenceClass a
ec] EquivalenceClass a
ec' PartialOrder (EquivalenceClass a)
po

-- | @mergeECs (>=) ec1 ec2@ combines the equivalence classes @ec1@ and @ec2@
-- of @(>=)@.
mergeECs :: (Ord a, Eq a, Hashable a) => WQO a -> EquivalenceClass a -> EquivalenceClass a -> WQO a
mergeECs :: forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> EquivalenceClass a -> EquivalenceClass a -> WQO a
mergeECs (WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
po) EquivalenceClass a
ec1 EquivalenceClass a
ec2 = forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
ecs' PartialOrder (EquivalenceClass a)
po'
    where
        ec' :: EquivalenceClass a
ec'  = forall a.
(Ord a, Eq a, Hashable a) =>
EquivalenceClass a -> EquivalenceClass a -> EquivalenceClass a
EC.union EquivalenceClass a
ec1 EquivalenceClass a
ec2
        ecs' :: Set (EquivalenceClass a)
ecs' = forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
ec' forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
S.delete EquivalenceClass a
ec2 forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
S.delete EquivalenceClass a
ec1 Set (EquivalenceClass a)
ecs
        po' :: PartialOrder (EquivalenceClass a)
po'  = forall a.
(Eq a, Ord a, Hashable a) =>
[a] -> a -> PartialOrder a -> PartialOrder a
PO.replaceUnsafe [EquivalenceClass a
ec1, EquivalenceClass a
ec2] EquivalenceClass a
ec' PartialOrder (EquivalenceClass a)
po

type ECMap a = M.Map (EquivalenceClass a) (EquivalenceClass a)

{-# SPECIALISE notStrongerThan :: WQO Op -> WQO Op -> Bool #-}
-- |  @w1 `notStrongerThan` w2@ if it is possible to extend @w1@ with additional
--    relations to obtain @w2@
notStrongerThan :: forall a . (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
notStrongerThan :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
notStrongerThan WQO a
w1 WQO a
w2 | WQO a
w1 forall a. Eq a => a -> a -> Bool
== WQO a
w2 = Bool
True
notStrongerThan (WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
po) (WQO Set (EquivalenceClass a)
ecs' PartialOrder (EquivalenceClass a)
po') = Bool
result where
  result :: Bool
result = case ECMap a -> [EquivalenceClass a] -> Maybe (ECMap a)
mkEcsMap forall k a. Map k a
M.empty (forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
ecs) of
    Just ECMap a
ecsMap -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall {a}.
Ord a =>
Map a (EquivalenceClass a) -> (a, Set (EquivalenceClass a)) -> Bool
gt ECMap a
ecsMap) (forall k. PartialOrder k -> [(k, Set k)]
PO.toDescsList PartialOrder (EquivalenceClass a)
po)
    Maybe (ECMap a)
Nothing     -> Bool
False

  mkEcsMap :: ECMap a -> [EquivalenceClass a] -> Maybe (ECMap a)
  mkEcsMap :: ECMap a -> [EquivalenceClass a] -> Maybe (ECMap a)
mkEcsMap ECMap a
buf []        = forall a. a -> Maybe a
Just ECMap a
buf
  mkEcsMap ECMap a
buf (EquivalenceClass a
ec:[EquivalenceClass a]
rest) =
    do
      EquivalenceClass a
ec' <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (EquivalenceClass a
ec forall a. Ord a => EquivalenceClass a -> EquivalenceClass a -> Bool
`EC.isSubsetOf`) (forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
ecs')
      ECMap a -> [EquivalenceClass a] -> Maybe (ECMap a)
mkEcsMap (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert EquivalenceClass a
ec EquivalenceClass a
ec' ECMap a
buf) [EquivalenceClass a]
rest
  gt :: Map a (EquivalenceClass a) -> (a, Set (EquivalenceClass a)) -> Bool
gt Map a (EquivalenceClass a)
ecsMap (a
ec, Set (EquivalenceClass a)
descs) =
    let
      Just EquivalenceClass a
ec' = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
ec Map a (EquivalenceClass a)
ecsMap
    in
      Set (EquivalenceClass a)
descs forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` forall a. Ord a => a -> PartialOrder a -> Set a
PO.descendents EquivalenceClass a
ec' PartialOrder (EquivalenceClass a)
po'




mergeAll :: forall a. (Show a, Ord a, Eq a, Hashable a) => [WQO a] -> Maybe (WQO a)
mergeAll :: forall a.
(Show a, Ord a, Eq a, Hashable a) =>
[WQO a] -> Maybe (WQO a)
mergeAll []            = forall a. a -> Maybe a
Just forall a. WQO a
empty
mergeAll [WQO a
x]           = forall a. a -> Maybe a
Just WQO a
x
mergeAll (WQO a
x : WQO a
x' : [WQO a]
xs) = do
  WQO a
y <- forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
merge WQO a
x WQO a
x'
  forall a.
(Show a, Ord a, Eq a, Hashable a) =>
[WQO a] -> Maybe (WQO a)
mergeAll (WQO a
y forall a. a -> [a] -> [a]
: [WQO a]
xs)

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

{-# INLINE merge #-}
merge :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Maybe (WQO a)
merge :: forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
merge lhs :: WQO a
lhs@(WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
po) rhs :: WQO a
rhs@(WQO Set (EquivalenceClass a)
ecs' PartialOrder (EquivalenceClass a)
po') | forall a. Ord a => Set a -> Set a -> Bool
S.disjoint (forall a. Ord a => WQO a -> Set a
elems WQO a
lhs) (forall a. Ord a => WQO a -> Set a
elems WQO a
rhs)
  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO (forall a. Ord a => Set a -> Set a -> Set a
S.union Set (EquivalenceClass a)
ecs Set (EquivalenceClass a)
ecs') (forall a.
Ord a =>
PartialOrder a -> PartialOrder a -> PartialOrder a
PO.unionDisjointUnsafe PartialOrder (EquivalenceClass a)
po PartialOrder (EquivalenceClass a)
po')
merge WQO a
lhs WQO a
rhs  =
  if forall a. Set a -> Int
S.size (forall a. Ord a => WQO a -> Set a
elems WQO a
lhs) forall a. Ord a => a -> a -> Bool
>= forall a. Set a -> Int
S.size (forall a. Ord a => WQO a -> Set a
elems WQO a
rhs)
  then forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
merge' WQO a
lhs WQO a
rhs
  else forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
merge' WQO a
rhs WQO a
lhs

{-# SPECIALISE merge' :: WQO Op -> WQO Op -> Maybe (WQO Op) #-}
merge' :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Maybe (WQO a)
merge' :: forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
merge' WQO a
lhs rhs :: WQO a
rhs@(WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
po) = forall a. String -> a -> a
trace' String
message Maybe (WQO a)
result where

    message :: String
message = String
"Merge " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Hashable a => a -> Int
hash WQO a
lhs) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Hashable a => a -> Int
hash WQO a
rhs)

    withEQs' :: Maybe (WQO a)
withEQs' = forall {a}.
(Ord a, Hashable a) =>
WQO a -> [(a, a, QORelation)] -> Maybe (WQO a)
go WQO a
lhs [(a, a, QORelation)]
ecsFacts

    result :: Maybe (WQO a)
result = do
      WQO a
withEQs <- Maybe (WQO a)
withEQs'
      forall {a}.
(Ord a, Hashable a) =>
WQO a -> [(a, a, QORelation)] -> Maybe (WQO a)
go WQO a
withEQs [(a, a, QORelation)]
poFacts

    ecsFacts :: [(a, a, QORelation)]
    ecsFacts :: [(a, a, QORelation)]
ecsFacts = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {b}. EquivalenceClass b -> [(b, b, QORelation)]
ecFacts (forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
ecs)

    ecFacts :: EquivalenceClass b -> [(b, b, QORelation)]
ecFacts EquivalenceClass b
ec =
        let
            xs :: [b]
xs = forall a. EquivalenceClass a -> [a]
EC.toList EquivalenceClass b
ec
        in
            forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ b
a b
b -> (b
a, b
b, QORelation
QEQ)) [b]
xs (forall a. [a] -> [a]
tail [b]
xs)

    poFacts :: [(a, a, QORelation)]
    poFacts :: [(a, a, QORelation)]
poFacts =
        forall a b. (a -> b) -> [a] -> [b]
map (\(EquivalenceClass a
a, EquivalenceClass a
b) -> (forall a. [a] -> a
head (forall a. EquivalenceClass a -> [a]
EC.toList EquivalenceClass a
a), forall a. [a] -> a
head (forall a. EquivalenceClass a -> [a]
EC.toList EquivalenceClass a
b), QORelation
QGT)) (forall a. PartialOrder a -> [(a, a)]
PO.toList PartialOrder (EquivalenceClass a)
po)

    go :: WQO a -> [(a, a, QORelation)] -> Maybe (WQO a)
go WQO a
r []       = forall a. a -> Maybe a
Just WQO a
r
    go WQO a
r ((a, a, QORelation)
x : [(a, a, QORelation)]
xs) =
      do
        WQO a
r' <- forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> (a, a, QORelation) -> Maybe (WQO a)
insertMaybe WQO a
r (a, a, QORelation)
x
        WQO a -> [(a, a, QORelation)] -> Maybe (WQO a)
go WQO a
r' [(a, a, QORelation)]
xs


data ExtendOrderingResult a =
    ValidExtension (WQO a)
  | AlreadyImplied
  | Contradicts

-- | @relevantTo wqo as bs@ returns a new WQO that contains only the necessary
--   relations to relate elements from @as@ with elements in @bs@ as they are
--   related in @wqo@.
relevantTo :: (Ord a, Eq a, Hashable a) => WQO a -> S.Set a -> S.Set a -> WQO a
relevantTo :: forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> Set a -> Set a -> WQO a
relevantTo WQO a
wqo0 Set a
as Set a
bs = WQO a -> [(a, a)] -> WQO a
go forall a. WQO a
empty [(a, a)]
cartesianProduct where

  cartesianProduct :: [(a, a)]
cartesianProduct = do
    a
x <- forall a. Set a -> [a]
S.toList Set a
as
    a
y <- forall a. Set a -> [a]
S.toList Set a
bs
    forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, a
y)

  get :: WQO a -> ExtendOrderingResult a -> WQO a
get WQO a
_ (ValidExtension WQO a
w) = WQO a
w
  get WQO a
w ExtendOrderingResult a
AlreadyImplied     = WQO a
w
  get WQO a
_ ExtendOrderingResult a
_                  = forall a. HasCallStack => a
undefined

  go :: WQO a -> [(a, a)] -> WQO a
go WQO a
wqo []                     = WQO a
wqo
  go WQO a
wqo ((a
f, a
g) : [(a, a)]
xs) | a
f forall a. Eq a => a -> a -> Bool
== a
g = WQO a -> [(a, a)] -> WQO a
go WQO a
wqo [(a, a)]
xs
  go WQO a
wqo ((a
f, a
g) : [(a, a)]
xs) | Just QORelation
r  <- forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> a -> a -> Maybe QORelation
getRelation WQO a
wqo0 a
f a
g
                       , WQO a
wqo'    <- forall {a}. WQO a -> ExtendOrderingResult a -> WQO a
get WQO a
wqo forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
insert WQO a
wqo (a
f, a
g, QORelation
r)
                       = WQO a -> [(a, a)] -> WQO a
go WQO a
wqo' [(a, a)]
xs
  go WQO a
wqo ((a
f, a
g) : [(a, a)]
xs) | Just QORelation
r  <- forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> a -> a -> Maybe QORelation
getRelation WQO a
wqo0 a
g a
f
                       , WQO a
wqo'    <- forall {a}. WQO a -> ExtendOrderingResult a -> WQO a
get WQO a
wqo forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
insert WQO a
wqo (a
g, a
f, QORelation
r)
                       = WQO a -> [(a, a)] -> WQO a
go WQO a
wqo' [(a, a)]
xs
  go WQO a
wqo ((a, a)
_ : [(a, a)]
xs)       = WQO a -> [(a, a)] -> WQO a
go WQO a
wqo [(a, a)]
xs

{-# INLINE insertMaybe #-}
{-# SPECIALISE insertMaybe :: WQO Op -> (Op, Op, QORelation) -> Maybe (WQO Op) #-}
insertMaybe :: (Ord a, Eq a, Hashable a) => WQO a -> (a, a, QORelation) -> Maybe (WQO a)
insertMaybe :: forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> (a, a, QORelation) -> Maybe (WQO a)
insertMaybe WQO a
wqo (a, a, QORelation)
t = case forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
insert WQO a
wqo (a, a, QORelation)
t of
  ValidExtension WQO a
wqo' -> forall a. a -> Maybe a
Just WQO a
wqo'
  ExtendOrderingResult a
AlreadyImplied      -> forall a. a -> Maybe a
Just WQO a
wqo
  ExtendOrderingResult a
Contradicts         -> forall a. Maybe a
Nothing



{-# SPECIALISE insert :: WQO Op -> (Op, Op, QORelation) -> ExtendOrderingResult Op #-}
insert :: (Ord a, Eq a, Hashable a) => WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
insert :: forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
insert WQO a
_   (a
f, a
g, QORelation
QGT)  | a
f forall a. Eq a => a -> a -> Bool
== a
g = forall a. ExtendOrderingResult a
Contradicts
insert WQO a
wqo (a
f, a
g, QORelation
r)    | Just QORelation
r' <- forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> a -> a -> Maybe QORelation
getRelation WQO a
wqo a
f a
g
                        = if QORelation
r forall a. Eq a => a -> a -> Bool
== QORelation
r' then forall a. ExtendOrderingResult a
AlreadyImplied else forall a. ExtendOrderingResult a
Contradicts
insert WQO a
wqo (a
f, a
g, QORelation
_)    | forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> a -> a -> Maybe QORelation
getRelation WQO a
wqo a
g a
f = forall a. ExtendOrderingResult a
Contradicts

insert wqo :: WQO a
wqo@(WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
po) (a
f, a
g, QORelation
QEQ) = forall a. WQO a -> ExtendOrderingResult a
ValidExtension forall a b. (a -> b) -> a -> b
$
    case forall a.
(Ord a, Eq a, Hashable a) =>
WQO a
-> a
-> a
-> (Maybe (EquivalenceClass a), Maybe (EquivalenceClass a))
getEquivalenceClasses WQO a
wqo a
f a
g of
        (Maybe (EquivalenceClass a)
Nothing, Maybe (EquivalenceClass a)
Nothing) ->
            let
                ecs' :: Set (EquivalenceClass a)
ecs' = forall a. Ord a => a -> Set a -> Set a
S.insert (forall a. (Ord a, Eq a, Hashable a) => [a] -> EquivalenceClass a
EC.fromList [a
f, a
g]) Set (EquivalenceClass a)
ecs
            in
                forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
ecs' PartialOrder (EquivalenceClass a)
po
        (Just EquivalenceClass a
ec, Maybe (EquivalenceClass a)
Nothing)   -> forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> EquivalenceClass a -> a -> WQO a
expandEC WQO a
wqo EquivalenceClass a
ec a
g
        (Maybe (EquivalenceClass a)
Nothing, Just EquivalenceClass a
ec)   -> forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> EquivalenceClass a -> a -> WQO a
expandEC WQO a
wqo EquivalenceClass a
ec a
f
        (Just EquivalenceClass a
ec1, Just EquivalenceClass a
ec2) -> forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> EquivalenceClass a -> EquivalenceClass a -> WQO a
mergeECs WQO a
wqo EquivalenceClass a
ec1 EquivalenceClass a
ec2

insert wqo :: WQO a
wqo@(WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
po) (a
f, a
g, QORelation
QGT) = forall a. WQO a -> ExtendOrderingResult a
ValidExtension forall a b. (a -> b) -> a -> b
$
    case forall a.
(Ord a, Eq a, Hashable a) =>
WQO a
-> a
-> a
-> (Maybe (EquivalenceClass a), Maybe (EquivalenceClass a))
getEquivalenceClasses WQO a
wqo a
f a
g of
        (Maybe (EquivalenceClass a)
Nothing, Maybe (EquivalenceClass a)
Nothing) ->
            let
                f' :: EquivalenceClass a
f'       = forall a. (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a
EC.singleton a
f
                g' :: EquivalenceClass a
g'       = forall a. (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a
EC.singleton a
g
                ecs' :: Set (EquivalenceClass a)
ecs'     = forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
f' forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
g' Set (EquivalenceClass a)
ecs
                Just PartialOrder (EquivalenceClass a)
po' = forall a.
(Eq a, Ord a, Hashable a) =>
PartialOrder a -> a -> a -> Maybe (PartialOrder a)
PO.insert PartialOrder (EquivalenceClass a)
po EquivalenceClass a
f' EquivalenceClass a
g'
            in
                forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
ecs' PartialOrder (EquivalenceClass a)
po'
        (Just EquivalenceClass a
ec, Maybe (EquivalenceClass a)
Nothing)   ->
            let
                g' :: EquivalenceClass a
g'       = forall a. (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a
EC.singleton a
g
                ecs' :: Set (EquivalenceClass a)
ecs'     = forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
g' Set (EquivalenceClass a)
ecs
                Just PartialOrder (EquivalenceClass a)
po' = forall a.
(Eq a, Ord a, Hashable a) =>
PartialOrder a -> a -> a -> Maybe (PartialOrder a)
PO.insert PartialOrder (EquivalenceClass a)
po EquivalenceClass a
ec EquivalenceClass a
g'
            in
                forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
ecs' PartialOrder (EquivalenceClass a)
po'

        (Maybe (EquivalenceClass a)
Nothing, Just EquivalenceClass a
ec) ->
            let
                f' :: EquivalenceClass a
f'       = forall a. (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a
EC.singleton a
f
                ecs' :: Set (EquivalenceClass a)
ecs'     = forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
f' Set (EquivalenceClass a)
ecs
                Just PartialOrder (EquivalenceClass a)
po' = forall a.
(Eq a, Ord a, Hashable a) =>
PartialOrder a -> a -> a -> Maybe (PartialOrder a)
PO.insert PartialOrder (EquivalenceClass a)
po EquivalenceClass a
f' EquivalenceClass a
ec
            in
                forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
ecs' PartialOrder (EquivalenceClass a)
po'
        (Just EquivalenceClass a
ec1, Just EquivalenceClass a
ec2) ->
            forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
ecs (forall a. Ord a => PartialOrder a -> a -> a -> PartialOrder a
PO.insertUnsafe PartialOrder (EquivalenceClass a)
po EquivalenceClass a
ec1 EquivalenceClass a
ec2)

-- | Generates all the possible orderings of the elements in the given set.
orderings :: forall a. (Ord a, Eq a, Hashable a) => S.Set a -> S.Set (WQO a)
orderings :: forall a. (Ord a, Eq a, Hashable a) => Set a -> Set (WQO a)
orderings Set a
ops = Set (WQO a) -> Set (WQO a) -> Set (WQO a)
go forall a. Set a
S.empty (forall a. a -> Set a
S.singleton forall a. WQO a
empty) where

  insert' :: WQO a -> (a, a, QORelation) -> Maybe (WQO a)
insert' WQO a
w (a, a, QORelation)
t | ValidExtension WQO a
w' <- forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
insert WQO a
w (a, a, QORelation)
t = forall a. a -> Maybe a
Just WQO a
w'
  insert' WQO a
_ (a, a, QORelation)
_                                   = forall a. Maybe a
Nothing

  go :: S.Set (WQO a) -> S.Set (WQO a) -> S.Set (WQO a)
  go :: Set (WQO a) -> Set (WQO a) -> Set (WQO a)
go Set (WQO a)
seen Set (WQO a)
acc | forall a. Set a -> Bool
S.null Set (WQO a)
acc = Set (WQO a)
seen
  go Set (WQO a)
seen Set (WQO a)
acc =
    let
      ordering :: WQO a
ordering  = forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList Set (WQO a)
acc
      acc' :: Set (WQO a)
acc'      = forall a. Ord a => a -> Set a -> Set a
S.delete WQO a
ordering Set (WQO a)
acc
      seen' :: Set (WQO a)
seen'     = forall a. Ord a => a -> Set a -> Set a
S.insert WQO a
ordering Set (WQO a)
seen
      newOrderings :: Set (WQO a)
newOrderings =
        forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ do
          a
f <- forall a. Set a -> [a]
S.toList Set a
ops
          a
g <- forall a. Set a -> [a]
S.toList (forall a. Ord a => a -> Set a -> Set a
S.delete a
f Set a
ops)
          QORelation
o <- [QORelation
QEQ, QORelation
QGT]
          forall a. Maybe a -> [a]
maybeToList (forall {a}.
(Ord a, Hashable a) =>
WQO a -> (a, a, QORelation) -> Maybe (WQO a)
insert' WQO a
ordering (a
f,a
g, QORelation
o))
      newOrderings' :: Set (WQO a)
newOrderings' = forall a. Ord a => Set a -> Set a -> Set a
S.difference Set (WQO a)
newOrderings Set (WQO a)
seen
    in
      Set (WQO a) -> Set (WQO a) -> Set (WQO a)
go Set (WQO a)
seen' (forall a. Ord a => Set a -> Set a -> Set a
S.union Set (WQO a)
acc' Set (WQO a)
newOrderings')