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