{-# 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
data WQO a =
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)]
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)
{-# 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
{-# 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
{-# 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 :: (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 :: (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 #-}
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 :: (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)
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')