{-# 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
Eq QORelation =>
(QORelation -> QORelation -> Ordering)
-> (QORelation -> QORelation -> Bool)
-> (QORelation -> QORelation -> Bool)
-> (QORelation -> QORelation -> Bool)
-> (QORelation -> QORelation -> Bool)
-> (QORelation -> QORelation -> QORelation)
-> (QORelation -> QORelation -> QORelation)
-> Ord 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
$ccompare :: QORelation -> QORelation -> Ordering
compare :: QORelation -> QORelation -> Ordering
$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
>= :: QORelation -> QORelation -> Bool
$cmax :: QORelation -> QORelation -> QORelation
max :: QORelation -> QORelation -> QORelation
$cmin :: QORelation -> QORelation -> QORelation
min :: QORelation -> QORelation -> QORelation
Ord, QORelation -> QORelation -> Bool
(QORelation -> QORelation -> Bool)
-> (QORelation -> QORelation -> Bool) -> Eq QORelation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QORelation -> QORelation -> Bool
== :: QORelation -> QORelation -> Bool
$c/= :: QORelation -> QORelation -> Bool
/= :: QORelation -> QORelation -> Bool
Eq, (forall x. QORelation -> Rep QORelation x)
-> (forall x. Rep QORelation x -> QORelation) -> Generic QORelation
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
$cfrom :: forall x. QORelation -> Rep QORelation x
from :: forall x. QORelation -> Rep QORelation x
$cto :: forall x. Rep QORelation x -> QORelation
to :: forall x. Rep QORelation x -> QORelation
Generic, Eq QORelation
Eq QORelation =>
(Int -> QORelation -> Int)
-> (QORelation -> Int) -> Hashable QORelation
Int -> QORelation -> Int
QORelation -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> QORelation -> Int
hashWithSalt :: Int -> QORelation -> Int
$chash :: QORelation -> Int
hash :: 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 ([SMTExpr Bool] -> SMTExpr Bool) -> [SMTExpr Bool] -> SMTExpr Bool
forall a b. (a -> b) -> a -> b
$ [SMTExpr Bool]
ecsSMT [SMTExpr Bool] -> [SMTExpr Bool] -> [SMTExpr Bool]
forall a. [a] -> [a] -> [a]
++ [SMTExpr Bool]
posSMT where

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

    ecsSMT :: [SMTExpr Bool]
ecsSMT = do
      EquivalenceClass a
ec <- Set (EquivalenceClass a) -> [EquivalenceClass a]
forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
ecs
      let ecl :: [a]
ecl = EquivalenceClass a -> [a]
forall a. EquivalenceClass a -> [a]
EC.toList EquivalenceClass a
ec
      Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ecl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
      SMTExpr Bool -> [SMTExpr Bool]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTExpr Bool -> [SMTExpr Bool]) -> SMTExpr Bool -> [SMTExpr Bool]
forall a b. (a -> b) -> a -> b
$ [SMTExpr Int] -> SMTExpr Bool
forall a1. [SMTExpr a1] -> SMTExpr Bool
Equal ((a -> SMTExpr Int) -> [a] -> [SMTExpr Int]
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) <- PartialOrder (EquivalenceClass a)
-> [(EquivalenceClass a, Set (EquivalenceClass a))]
forall k. PartialOrder k -> [(k, Set k)]
PO.toDescsList PartialOrder (EquivalenceClass a)
po
      EquivalenceClass a
var        <- Set (EquivalenceClass a) -> [EquivalenceClass a]
forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
vs
      SMTExpr Bool -> [SMTExpr Bool]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTExpr Bool -> [SMTExpr Bool]) -> SMTExpr Bool -> [SMTExpr Bool]
forall a b. (a -> b) -> a -> b
$ SMTExpr Int -> SMTExpr Int -> SMTExpr Bool
Greater (a -> SMTExpr Int
forall a b. ToSMT a b => a -> SMTExpr b
toSMT (a -> SMTExpr Int) -> a -> SMTExpr Int
forall a b. (a -> b) -> a -> b
$ EquivalenceClass a -> a
forall a. EquivalenceClass a -> a
EC.head EquivalenceClass a
ec) (a -> SMTExpr Int
forall a b. ToSMT a b => a -> SMTExpr b
toSMT (a -> SMTExpr Int) -> a -> SMTExpr Int
forall a b. (a -> b) -> a -> b
$ EquivalenceClass a -> a
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 (Eq (WQO a)
Eq (WQO a) =>
(WQO a -> WQO a -> Ordering)
-> (WQO a -> WQO a -> Bool)
-> (WQO a -> WQO a -> Bool)
-> (WQO a -> WQO a -> Bool)
-> (WQO a -> WQO a -> Bool)
-> (WQO a -> WQO a -> WQO a)
-> (WQO a -> WQO a -> WQO a)
-> Ord (WQO a)
WQO a -> WQO a -> Bool
WQO a -> WQO a -> Ordering
WQO a -> WQO a -> WQO 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 (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
$ccompare :: forall a. Ord a => WQO a -> WQO a -> Ordering
compare :: WQO a -> WQO a -> Ordering
$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
>= :: WQO a -> WQO a -> Bool
$cmax :: forall a. Ord a => WQO a -> WQO a -> WQO a
max :: WQO a -> WQO a -> WQO a
$cmin :: forall a. Ord a => WQO a -> WQO a -> WQO a
min :: WQO a -> WQO a -> WQO a
Ord, WQO a -> WQO a -> Bool
(WQO a -> WQO a -> Bool) -> (WQO a -> WQO a -> Bool) -> Eq (WQO a)
forall a. Eq a => WQO a -> WQO a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: WQO a -> WQO a -> Bool
Eq, (forall x. WQO a -> Rep (WQO a) x)
-> (forall x. Rep (WQO a) x -> WQO a) -> Generic (WQO a)
forall x. Rep (WQO a) x -> WQO a
forall x. WQO a -> Rep (WQO a) x
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
$cfrom :: forall a x. WQO a -> Rep (WQO a) x
from :: forall x. WQO a -> Rep (WQO a) x
$cto :: forall a x. Rep (WQO a) x -> WQO a
to :: forall x. Rep (WQO a) x -> WQO a
Generic, Eq (WQO a)
Eq (WQO a) =>
(Int -> WQO a -> Int) -> (WQO a -> Int) -> Hashable (WQO a)
Int -> WQO a -> Int
WQO a -> Int
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
$chashWithSalt :: forall a. Hashable a => Int -> WQO a -> Int
hashWithSalt :: Int -> WQO a -> Int
$chash :: forall a. Hashable a => WQO a -> Int
hash :: 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)
_)  | Set (EquivalenceClass a) -> Bool
forall a. Set a -> Bool
S.null Set (EquivalenceClass a)
ecs  = String
"⊤"
    show (WQO Set (EquivalenceClass a)
ecs PartialOrder (EquivalenceClass a)
po) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
" ∧ " ((EquivalenceClass a -> String) -> [EquivalenceClass a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map EquivalenceClass a -> String
forall a. Show a => a -> String
show [EquivalenceClass a]
ecs' [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
po')
        where
            ecs' :: [EquivalenceClass a]
ecs'          = (EquivalenceClass a -> Bool)
-> [EquivalenceClass a] -> [EquivalenceClass a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (EquivalenceClass a -> Bool) -> EquivalenceClass a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EquivalenceClass a -> Bool
forall a. EquivalenceClass a -> Bool
EC.isSingleton) ([EquivalenceClass a] -> [EquivalenceClass a])
-> [EquivalenceClass a] -> [EquivalenceClass a]
forall a b. (a -> b) -> a -> b
$ Set (EquivalenceClass a) -> [EquivalenceClass a]
forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
ecs
            po' :: [String]
po'           =
                [PartialOrder (EquivalenceClass a) -> String
forall a. Show a => a -> String
show PartialOrder (EquivalenceClass a)
po | Bool -> Bool
not (PartialOrder (EquivalenceClass a) -> Bool
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 WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
empty

empty :: WQO a
empty :: forall a. WQO a
empty = Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
forall a. Set a
S.empty PartialOrder (EquivalenceClass a)
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 = WQO a -> (a, a, QORelation) -> Maybe (WQO a)
forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> (a, a, QORelation) -> Maybe (WQO a)
insertMaybe WQO a
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)
_) = [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
$ (EquivalenceClass a -> Set a) -> [EquivalenceClass a] -> [Set a]
forall a b. (a -> b) -> [a] -> [b]
map EquivalenceClass a -> Set a
forall a. EquivalenceClass a -> Set a
EC.elems (Set (EquivalenceClass a) -> [EquivalenceClass a]
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 = (EquivalenceClass a -> Bool)
-> [EquivalenceClass a] -> Maybe (EquivalenceClass a)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (a -> EquivalenceClass a -> Bool
forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> Bool
EC.isMember a
source) [EquivalenceClass a]
classes'
    u :: Maybe (EquivalenceClass a)
u = (EquivalenceClass a -> Bool)
-> [EquivalenceClass a] -> Maybe (EquivalenceClass a)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (a -> EquivalenceClass a -> Bool
forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> Bool
EC.isMember a
target) [EquivalenceClass a]
classes'
    classes' :: [EquivalenceClass a]
classes' = Set (EquivalenceClass a) -> [EquivalenceClass a]
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 <- (EquivalenceClass a -> Bool)
-> [EquivalenceClass a] -> Maybe (EquivalenceClass a)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (a -> EquivalenceClass a -> Bool
forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> Bool
EC.isMember a
source) [EquivalenceClass a]
classes'
    if a -> EquivalenceClass a -> Bool
forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> Bool
EC.isMember a
target EquivalenceClass a
t
      then (EquivalenceClass a, EquivalenceClass a)
-> Maybe (EquivalenceClass a, EquivalenceClass a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (EquivalenceClass a
t, EquivalenceClass a
t)
      else (EquivalenceClass a
t,) (EquivalenceClass a -> (EquivalenceClass a, EquivalenceClass a))
-> Maybe (EquivalenceClass a)
-> Maybe (EquivalenceClass a, EquivalenceClass a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (EquivalenceClass a -> Bool)
-> [EquivalenceClass a] -> Maybe (EquivalenceClass a)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (a -> EquivalenceClass a -> Bool
forall a.
(Ord a, Eq a, Hashable a) =>
a -> EquivalenceClass a -> Bool
EC.isMember a
target) [EquivalenceClass a]
classes'
  where
    classes' :: [EquivalenceClass a]
classes' = Set (EquivalenceClass a) -> [EquivalenceClass a]
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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
g = QORelation -> Maybe QORelation
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) <- WQO a -> a -> a -> Maybe (EquivalenceClass a, EquivalenceClass a)
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 EquivalenceClass a -> EquivalenceClass a -> Bool
forall a. Eq a => a -> a -> Bool
== EquivalenceClass a
t
        then QORelation -> Maybe QORelation
forall a. a -> Maybe a
Just QORelation
QEQ
        else
            if PartialOrder (EquivalenceClass a)
-> EquivalenceClass a -> EquivalenceClass a -> Bool
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 QORelation -> Maybe QORelation
forall a. a -> Maybe a
Just QORelation
QGT
                else Maybe QORelation
forall a. Maybe a
Nothing
    | Bool
otherwise = Maybe QORelation
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 = Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
ecs' PartialOrder (EquivalenceClass a)
po'
    where
        ec' :: EquivalenceClass a
ec'  = a -> EquivalenceClass a -> EquivalenceClass a
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' = EquivalenceClass a
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
ec' (Set (EquivalenceClass a) -> Set (EquivalenceClass a))
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a b. (a -> b) -> a -> b
$ EquivalenceClass a
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => a -> Set a -> Set a
S.delete EquivalenceClass a
ec Set (EquivalenceClass a)
ecs
        po' :: PartialOrder (EquivalenceClass a)
po'  = [EquivalenceClass a]
-> EquivalenceClass a
-> PartialOrder (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a)
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 = Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
ecs' PartialOrder (EquivalenceClass a)
po'
    where
        ec' :: EquivalenceClass a
ec'  = EquivalenceClass a -> EquivalenceClass a -> EquivalenceClass a
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' = EquivalenceClass a
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
ec' (Set (EquivalenceClass a) -> Set (EquivalenceClass a))
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a b. (a -> b) -> a -> b
$ EquivalenceClass a
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => a -> Set a -> Set a
S.delete EquivalenceClass a
ec2 (Set (EquivalenceClass a) -> Set (EquivalenceClass a))
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a b. (a -> b) -> a -> b
$ EquivalenceClass a
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => a -> Set a -> Set a
S.delete EquivalenceClass a
ec1 Set (EquivalenceClass a)
ecs
        po' :: PartialOrder (EquivalenceClass a)
po'  = [EquivalenceClass a]
-> EquivalenceClass a
-> PartialOrder (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a)
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 WQO a -> WQO a -> Bool
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 ECMap a
forall k a. Map k a
M.empty (Set (EquivalenceClass a) -> [EquivalenceClass a]
forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
ecs) of
    Just ECMap a
ecsMap -> ((EquivalenceClass a, Set (EquivalenceClass a)) -> Bool)
-> [(EquivalenceClass a, Set (EquivalenceClass a))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ECMap a -> (EquivalenceClass a, Set (EquivalenceClass a)) -> Bool
forall {a}.
Ord a =>
Map a (EquivalenceClass a) -> (a, Set (EquivalenceClass a)) -> Bool
gt ECMap a
ecsMap) (PartialOrder (EquivalenceClass a)
-> [(EquivalenceClass a, Set (EquivalenceClass a))]
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 []        = ECMap a -> Maybe (ECMap a)
forall a. a -> Maybe a
Just ECMap a
buf
  mkEcsMap ECMap a
buf (EquivalenceClass a
ec:[EquivalenceClass a]
rest) =
    do
      EquivalenceClass a
ec' <- (EquivalenceClass a -> Bool)
-> [EquivalenceClass a] -> Maybe (EquivalenceClass a)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (EquivalenceClass a
ec EquivalenceClass a -> EquivalenceClass a -> Bool
forall a. Ord a => EquivalenceClass a -> EquivalenceClass a -> Bool
`EC.isSubsetOf`) (Set (EquivalenceClass a) -> [EquivalenceClass a]
forall a. Set a -> [a]
S.toList Set (EquivalenceClass a)
ecs')
      ECMap a -> [EquivalenceClass a] -> Maybe (ECMap a)
mkEcsMap (EquivalenceClass a -> EquivalenceClass a -> ECMap a -> ECMap a
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' = a -> Map a (EquivalenceClass a) -> Maybe (EquivalenceClass a)
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 Set (EquivalenceClass a) -> Set (EquivalenceClass a) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` EquivalenceClass a
-> PartialOrder (EquivalenceClass a) -> Set (EquivalenceClass a)
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 []            = WQO a -> Maybe (WQO a)
forall a. a -> Maybe a
Just WQO a
forall a. WQO a
empty
mergeAll [WQO a
x]           = WQO a -> Maybe (WQO a)
forall a. a -> Maybe a
Just WQO a
x
mergeAll (WQO a
x : WQO a
x' : [WQO a]
xs) = do
  WQO a
y <- WQO a -> WQO a -> Maybe (WQO a)
forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
merge WQO a
x WQO a
x'
  [WQO a] -> Maybe (WQO a)
forall a.
(Show a, Ord a, Eq a, Hashable a) =>
[WQO a] -> Maybe (WQO a)
mergeAll (WQO a
y WQO a -> [WQO a] -> [WQO a]
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') | Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
S.disjoint (WQO a -> Set a
forall a. Ord a => WQO a -> Set a
elems WQO a
lhs) (WQO a -> Set a
forall a. Ord a => WQO a -> Set a
elems WQO a
rhs)
  = WQO a -> Maybe (WQO a)
forall a. a -> Maybe a
Just (WQO a -> Maybe (WQO a)) -> WQO a -> Maybe (WQO a)
forall a b. (a -> b) -> a -> b
$ Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO (Set (EquivalenceClass a)
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (EquivalenceClass a)
ecs Set (EquivalenceClass a)
ecs') (PartialOrder (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a)
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 Set a -> Int
forall a. Set a -> Int
S.size (WQO a -> Set a
forall a. Ord a => WQO a -> Set a
elems WQO a
lhs) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Set a -> Int
forall a. Set a -> Int
S.size (WQO a -> Set a
forall a. Ord a => WQO a -> Set a
elems WQO a
rhs)
  then WQO a -> WQO a -> Maybe (WQO a)
forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
merge' WQO a
lhs WQO a
rhs
  else WQO a -> WQO a -> Maybe (WQO a)
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) = String -> Maybe (WQO a) -> Maybe (WQO a)
forall a. String -> a -> a
trace' String
message Maybe (WQO a)
result where

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

    withEQs' :: Maybe (WQO a)
withEQs' = WQO a -> [(a, a, QORelation)] -> Maybe (WQO a)
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'
      WQO a -> [(a, a, QORelation)] -> Maybe (WQO a)
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 = (EquivalenceClass a -> [(a, a, QORelation)])
-> [EquivalenceClass a] -> [(a, a, QORelation)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap EquivalenceClass a -> [(a, a, QORelation)]
forall {b}. EquivalenceClass b -> [(b, b, QORelation)]
ecFacts (Set (EquivalenceClass a) -> [EquivalenceClass a]
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 = EquivalenceClass b -> [b]
forall a. EquivalenceClass a -> [a]
EC.toList EquivalenceClass b
ec
        in
            (b -> b -> (b, b, QORelation))
-> [b] -> [b] -> [(b, b, QORelation)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ b
a b
b -> (b
a, b
b, QORelation
QEQ)) [b]
xs ([b] -> [b]
forall a. HasCallStack => [a] -> [a]
tail [b]
xs)

    poFacts :: [(a, a, QORelation)]
    poFacts :: [(a, a, QORelation)]
poFacts =
        ((EquivalenceClass a, EquivalenceClass a) -> (a, a, QORelation))
-> [(EquivalenceClass a, EquivalenceClass a)]
-> [(a, a, QORelation)]
forall a b. (a -> b) -> [a] -> [b]
map (\(EquivalenceClass a
a, EquivalenceClass a
b) -> ([a] -> a
forall a. HasCallStack => [a] -> a
head (EquivalenceClass a -> [a]
forall a. EquivalenceClass a -> [a]
EC.toList EquivalenceClass a
a), [a] -> a
forall a. HasCallStack => [a] -> a
head (EquivalenceClass a -> [a]
forall a. EquivalenceClass a -> [a]
EC.toList EquivalenceClass a
b), QORelation
QGT)) (PartialOrder (EquivalenceClass a)
-> [(EquivalenceClass a, EquivalenceClass a)]
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 []       = WQO a -> Maybe (WQO a)
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' <- WQO a -> (a, a, QORelation) -> Maybe (WQO a)
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 WQO a
forall a. WQO a
empty [(a, a)]
cartesianProduct where

  cartesianProduct :: [(a, a)]
cartesianProduct = do
    a
x <- Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
as
    a
y <- Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
bs
    (a, a) -> [(a, a)]
forall a. a -> [a]
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
_                  = WQO 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 a -> a -> Bool
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  <- WQO a -> a -> a -> Maybe QORelation
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'    <- WQO a -> ExtendOrderingResult a -> WQO a
forall {a}. WQO a -> ExtendOrderingResult a -> WQO a
get WQO a
wqo (ExtendOrderingResult a -> WQO a)
-> ExtendOrderingResult a -> WQO a
forall a b. (a -> b) -> a -> b
$ WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
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  <- WQO a -> a -> a -> Maybe QORelation
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'    <- WQO a -> ExtendOrderingResult a -> WQO a
forall {a}. WQO a -> ExtendOrderingResult a -> WQO a
get WQO a
wqo (ExtendOrderingResult a -> WQO a)
-> ExtendOrderingResult a -> WQO a
forall a b. (a -> b) -> a -> b
$ WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
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 WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
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' -> WQO a -> Maybe (WQO a)
forall a. a -> Maybe a
Just WQO a
wqo'
  ExtendOrderingResult a
AlreadyImplied      -> WQO a -> Maybe (WQO a)
forall a. a -> Maybe a
Just WQO a
wqo
  ExtendOrderingResult a
Contradicts         -> Maybe (WQO a)
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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
g = ExtendOrderingResult a
forall a. ExtendOrderingResult a
Contradicts
insert WQO a
wqo (a
f, a
g, QORelation
r)    | Just QORelation
r' <- WQO a -> a -> a -> Maybe QORelation
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 QORelation -> QORelation -> Bool
forall a. Eq a => a -> a -> Bool
== QORelation
r' then ExtendOrderingResult a
forall a. ExtendOrderingResult a
AlreadyImplied else ExtendOrderingResult a
forall a. ExtendOrderingResult a
Contradicts
insert WQO a
wqo (a
f, a
g, QORelation
_)    | Maybe QORelation -> Bool
forall a. Maybe a -> Bool
isJust (Maybe QORelation -> Bool) -> Maybe QORelation -> Bool
forall a b. (a -> b) -> a -> b
$ WQO a -> a -> a -> Maybe QORelation
forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> a -> a -> Maybe QORelation
getRelation WQO a
wqo a
g a
f = ExtendOrderingResult a
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) = WQO a -> ExtendOrderingResult a
forall a. WQO a -> ExtendOrderingResult a
ValidExtension (WQO a -> ExtendOrderingResult a)
-> WQO a -> ExtendOrderingResult a
forall a b. (a -> b) -> a -> b
$
    case WQO a
-> a
-> a
-> (Maybe (EquivalenceClass a), Maybe (EquivalenceClass a))
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' = EquivalenceClass a
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => a -> Set a -> Set a
S.insert ([a] -> EquivalenceClass a
forall a. (Ord a, Eq a, Hashable a) => [a] -> EquivalenceClass a
EC.fromList [a
f, a
g]) Set (EquivalenceClass a)
ecs
            in
                Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
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)   -> WQO a -> EquivalenceClass a -> a -> WQO a
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)   -> WQO a -> EquivalenceClass a -> a -> WQO a
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) -> WQO a -> EquivalenceClass a -> EquivalenceClass a -> WQO a
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) = WQO a -> ExtendOrderingResult a
forall a. WQO a -> ExtendOrderingResult a
ValidExtension (WQO a -> ExtendOrderingResult a)
-> WQO a -> ExtendOrderingResult a
forall a b. (a -> b) -> a -> b
$
    case WQO a
-> a
-> a
-> (Maybe (EquivalenceClass a), Maybe (EquivalenceClass a))
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'       = a -> EquivalenceClass a
forall a. (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a
EC.singleton a
f
                g' :: EquivalenceClass a
g'       = a -> EquivalenceClass a
forall a. (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a
EC.singleton a
g
                ecs' :: Set (EquivalenceClass a)
ecs'     = EquivalenceClass a
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
f' (Set (EquivalenceClass a) -> Set (EquivalenceClass a))
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a b. (a -> b) -> a -> b
$ EquivalenceClass a
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
g' Set (EquivalenceClass a)
ecs
                Just PartialOrder (EquivalenceClass a)
po' = PartialOrder (EquivalenceClass a)
-> EquivalenceClass a
-> EquivalenceClass a
-> Maybe (PartialOrder (EquivalenceClass a))
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
                Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
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'       = a -> EquivalenceClass a
forall a. (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a
EC.singleton a
g
                ecs' :: Set (EquivalenceClass a)
ecs'     = EquivalenceClass a
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
g' Set (EquivalenceClass a)
ecs
                Just PartialOrder (EquivalenceClass a)
po' = PartialOrder (EquivalenceClass a)
-> EquivalenceClass a
-> EquivalenceClass a
-> Maybe (PartialOrder (EquivalenceClass a))
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
                Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
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'       = a -> EquivalenceClass a
forall a. (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a
EC.singleton a
f
                ecs' :: Set (EquivalenceClass a)
ecs'     = EquivalenceClass a
-> Set (EquivalenceClass a) -> Set (EquivalenceClass a)
forall a. Ord a => a -> Set a -> Set a
S.insert EquivalenceClass a
f' Set (EquivalenceClass a)
ecs
                Just PartialOrder (EquivalenceClass a)
po' = PartialOrder (EquivalenceClass a)
-> EquivalenceClass a
-> EquivalenceClass a
-> Maybe (PartialOrder (EquivalenceClass a))
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
                Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
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) ->
            Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
forall a.
Set (EquivalenceClass a)
-> PartialOrder (EquivalenceClass a) -> WQO a
WQO Set (EquivalenceClass a)
ecs (PartialOrder (EquivalenceClass a)
-> EquivalenceClass a
-> EquivalenceClass a
-> PartialOrder (EquivalenceClass a)
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 Set (WQO a)
forall a. Set a
S.empty (WQO a -> Set (WQO a)
forall a. a -> Set a
S.singleton WQO a
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' <- WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> (a, a, QORelation) -> ExtendOrderingResult a
insert WQO a
w (a, a, QORelation)
t = WQO a -> Maybe (WQO a)
forall a. a -> Maybe a
Just WQO a
w'
  insert' WQO a
_ (a, a, QORelation)
_                                   = Maybe (WQO a)
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 | Set (WQO a) -> Bool
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  = [WQO a] -> WQO a
forall a. HasCallStack => [a] -> a
head ([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)
acc
      acc' :: Set (WQO a)
acc'      = WQO a -> Set (WQO a) -> Set (WQO a)
forall a. Ord a => a -> Set a -> Set a
S.delete WQO a
ordering Set (WQO a)
acc
      seen' :: Set (WQO a)
seen'     = WQO a -> Set (WQO a) -> Set (WQO a)
forall a. Ord a => a -> Set a -> Set a
S.insert WQO a
ordering Set (WQO a)
seen
      newOrderings :: Set (WQO a)
newOrderings =
        [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
          a
f <- Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
ops
          a
g <- Set a -> [a]
forall a. Set a -> [a]
S.toList (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
S.delete a
f Set a
ops)
          QORelation
o <- [QORelation
QEQ, QORelation
QGT]
          Maybe (WQO a) -> [WQO a]
forall a. Maybe a -> [a]
maybeToList (WQO a -> (a, a, QORelation) -> Maybe (WQO a)
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' = Set (WQO a) -> Set (WQO a) -> Set (WQO a)
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' (Set (WQO a) -> Set (WQO a) -> Set (WQO a)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (WQO a)
acc' Set (WQO a)
newOrderings')