{-# LANGUAGE OverloadedStrings #-}
module Data.ECTA.Internal.Paths (
Path(.., EmptyPath, ConsPath)
, unPath
, path
, Pathable(..)
, pathHeadUnsafe
, pathTailUnsafe
, isSubpath
, isStrictSubpath
, substSubpath
, smallestNonempty
, largestNonempty
, getMaxNonemptyIndex
, PathTrie(..)
, isEmptyPathTrie
, isTerminalPathTrie
, toPathTrie
, fromPathTrie
, pathTrieDescend
, PathEClass(PathEClass, ..)
, unPathEClass
, hasSubsumingMember
, completedSubsumptionOrdering
, EqConstraints(.., EmptyConstraints)
, rawMkEqConstraints
, unsafeGetEclasses
, hasSubsumingMemberListBased
, isContradicting
, mkEqConstraints
, combineEqConstraints
, eqConstraintsDescend
, constraintsAreContradictory
, constraintsImply
, subsumptionOrderedEclasses
, unsafeSubsumptionOrderedEclasses
) where
import Prelude hiding ( round )
import Data.Function ( on )
import Data.Hashable ( Hashable )
import Data.List ( isSubsequenceOf, nub, sort, sortBy )
import Data.Monoid ( Any(..) )
import Data.Semigroup ( Max(..) )
import qualified Data.Text as Text
import Data.Vector ( Vector )
import qualified Data.Vector as Vector
import Data.Vector.Instances ()
import GHC.Exts ( inline )
import GHC.Generics ( Generic )
import Data.Equivalence.Monad ( runEquivM, equate, desc, classes )
import Data.Memoization ( MemoCacheTag(..), memo2 )
import Data.Text.Extended.Pretty
import Utility.Fixpoint
flipOrdering :: Ordering -> Ordering
flipOrdering :: Ordering -> Ordering
flipOrdering Ordering
GT = Ordering
LT
flipOrdering Ordering
LT = Ordering
GT
flipOrdering Ordering
EQ = Ordering
EQ
data Path = Path ![Int]
deriving (Path -> Path -> Bool
(Path -> Path -> Bool) -> (Path -> Path -> Bool) -> Eq Path
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Path -> Path -> Bool
$c/= :: Path -> Path -> Bool
== :: Path -> Path -> Bool
$c== :: Path -> Path -> Bool
Eq, Eq Path
Eq Path
-> (Path -> Path -> Ordering)
-> (Path -> Path -> Bool)
-> (Path -> Path -> Bool)
-> (Path -> Path -> Bool)
-> (Path -> Path -> Bool)
-> (Path -> Path -> Path)
-> (Path -> Path -> Path)
-> Ord Path
Path -> Path -> Bool
Path -> Path -> Ordering
Path -> Path -> Path
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 :: Path -> Path -> Path
$cmin :: Path -> Path -> Path
max :: Path -> Path -> Path
$cmax :: Path -> Path -> Path
>= :: Path -> Path -> Bool
$c>= :: Path -> Path -> Bool
> :: Path -> Path -> Bool
$c> :: Path -> Path -> Bool
<= :: Path -> Path -> Bool
$c<= :: Path -> Path -> Bool
< :: Path -> Path -> Bool
$c< :: Path -> Path -> Bool
compare :: Path -> Path -> Ordering
$ccompare :: Path -> Path -> Ordering
$cp1Ord :: Eq Path
Ord, Int -> Path -> ShowS
[Path] -> ShowS
Path -> String
(Int -> Path -> ShowS)
-> (Path -> String) -> ([Path] -> ShowS) -> Show Path
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Path] -> ShowS
$cshowList :: [Path] -> ShowS
show :: Path -> String
$cshow :: Path -> String
showsPrec :: Int -> Path -> ShowS
$cshowsPrec :: Int -> Path -> ShowS
Show, (forall x. Path -> Rep Path x)
-> (forall x. Rep Path x -> Path) -> Generic Path
forall x. Rep Path x -> Path
forall x. Path -> Rep Path x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Path x -> Path
$cfrom :: forall x. Path -> Rep Path x
Generic)
unPath :: Path -> [Int]
unPath :: Path -> [Int]
unPath (Path [Int]
p) = [Int]
p
instance Hashable Path
path :: [Int] -> Path
path :: [Int] -> Path
path = [Int] -> Path
Path
{-# COMPLETE EmptyPath, ConsPath #-}
pattern EmptyPath :: Path
pattern $bEmptyPath :: Path
$mEmptyPath :: forall r. Path -> (Void# -> r) -> (Void# -> r) -> r
EmptyPath = Path []
pattern ConsPath :: Int -> Path -> Path
pattern $bConsPath :: Int -> Path -> Path
$mConsPath :: forall r. Path -> (Int -> Path -> r) -> (Void# -> r) -> r
ConsPath p ps <- Path (p : (Path -> ps)) where
ConsPath Int
p (Path [Int]
ps) = [Int] -> Path
Path (Int
p Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
ps)
pathHeadUnsafe :: Path -> Int
pathHeadUnsafe :: Path -> Int
pathHeadUnsafe (Path [Int]
ps) = [Int] -> Int
forall a. [a] -> a
head [Int]
ps
pathTailUnsafe :: Path -> Path
pathTailUnsafe :: Path -> Path
pathTailUnsafe (Path [Int]
ps) = [Int] -> Path
Path ([Int] -> [Int]
forall a. [a] -> [a]
tail [Int]
ps)
instance Pretty Path where
pretty :: Path -> Text
pretty (Path [Int]
ps) = Text -> [Text] -> Text
Text.intercalate Text
"." ((Int -> Text) -> [Int] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Text
Text.pack (String -> Text) -> (Int -> String) -> Int -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) [Int]
ps)
isSubpath :: Path -> Path -> Bool
isSubpath :: Path -> Path -> Bool
isSubpath Path
EmptyPath Path
_ = Bool
True
isSubpath (ConsPath Int
p1 Path
ps1) (ConsPath Int
p2 Path
ps2)
| Int
p1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
p2 = Path -> Path -> Bool
isSubpath Path
ps1 Path
ps2
isSubpath Path
_ Path
_ = Bool
False
isStrictSubpath :: Path -> Path -> Bool
isStrictSubpath :: Path -> Path -> Bool
isStrictSubpath Path
EmptyPath Path
EmptyPath = Bool
False
isStrictSubpath Path
EmptyPath Path
_ = Bool
True
isStrictSubpath (ConsPath Int
p1 Path
ps1) (ConsPath Int
p2 Path
ps2)
| Int
p1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
p2 = Path -> Path -> Bool
isStrictSubpath Path
ps1 Path
ps2
isStrictSubpath Path
_ Path
_ = Bool
False
substSubpath :: Path -> Path -> Path -> Path
substSubpath :: Path -> Path -> Path -> Path
substSubpath Path
replacement Path
toReplace Path
target = [Int] -> Path
Path ([Int] -> Path) -> [Int] -> Path
forall a b. (a -> b) -> a -> b
$ (Path -> [Int]
unPath Path
replacement) [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
drop ([Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Path -> [Int]
unPath Path
toReplace) (Path -> [Int]
unPath Path
target)
class Pathable t t' | t -> t' where
type Emptyable t'
getPath :: Path -> t -> Emptyable t'
getAllAtPath :: Path -> t -> [t']
modifyAtPath :: (t' -> t') -> Path -> t -> t
smallestNonempty :: Vector PathTrie -> Int
smallestNonempty :: Vector PathTrie -> Int
smallestNonempty Vector PathTrie
v = (Int -> PathTrie -> Int -> Int) -> Int -> Vector PathTrie -> Int
forall a b. (Int -> a -> b -> b) -> b -> Vector a -> b
Vector.ifoldr (\Int
i PathTrie
pt Int
oldMin -> case PathTrie
pt of
PathTrie
EmptyPathTrie -> Int
oldMin
PathTrie
_ -> Int
i)
Int
forall a. Bounded a => a
maxBound
Vector PathTrie
v
largestNonempty :: Vector PathTrie -> Int
largestNonempty :: Vector PathTrie -> Int
largestNonempty Vector PathTrie
v = (Int -> Int -> PathTrie -> Int) -> Int -> Vector PathTrie -> Int
forall a b. (a -> Int -> b -> a) -> a -> Vector b -> a
Vector.ifoldl (\Int
oldMin Int
i PathTrie
pt -> case PathTrie
pt of
PathTrie
EmptyPathTrie -> Int
oldMin
PathTrie
_ -> Int
i)
Int
forall a. Bounded a => a
minBound
Vector PathTrie
v
getMaxNonemptyIndex :: PathTrie -> Maybe Int
getMaxNonemptyIndex :: PathTrie -> Maybe Int
getMaxNonemptyIndex PathTrie
EmptyPathTrie = Maybe Int
forall a. Maybe a
Nothing
getMaxNonemptyIndex PathTrie
TerminalPathTrie = Maybe Int
forall a. Maybe a
Nothing
getMaxNonemptyIndex (PathTrieSingleChild Int
i PathTrie
_) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
getMaxNonemptyIndex (PathTrie Vector PathTrie
vec) = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Vector PathTrie -> Int
largestNonempty Vector PathTrie
vec
data PathTrie = EmptyPathTrie
| TerminalPathTrie
| PathTrieSingleChild {-# UNPACK #-} !Int !PathTrie
| PathTrie !(Vector PathTrie)
deriving ( PathTrie -> PathTrie -> Bool
(PathTrie -> PathTrie -> Bool)
-> (PathTrie -> PathTrie -> Bool) -> Eq PathTrie
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PathTrie -> PathTrie -> Bool
$c/= :: PathTrie -> PathTrie -> Bool
== :: PathTrie -> PathTrie -> Bool
$c== :: PathTrie -> PathTrie -> Bool
Eq, Int -> PathTrie -> ShowS
[PathTrie] -> ShowS
PathTrie -> String
(Int -> PathTrie -> ShowS)
-> (PathTrie -> String) -> ([PathTrie] -> ShowS) -> Show PathTrie
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PathTrie] -> ShowS
$cshowList :: [PathTrie] -> ShowS
show :: PathTrie -> String
$cshow :: PathTrie -> String
showsPrec :: Int -> PathTrie -> ShowS
$cshowsPrec :: Int -> PathTrie -> ShowS
Show, (forall x. PathTrie -> Rep PathTrie x)
-> (forall x. Rep PathTrie x -> PathTrie) -> Generic PathTrie
forall x. Rep PathTrie x -> PathTrie
forall x. PathTrie -> Rep PathTrie x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PathTrie x -> PathTrie
$cfrom :: forall x. PathTrie -> Rep PathTrie x
Generic )
instance Hashable PathTrie
isEmptyPathTrie :: PathTrie -> Bool
isEmptyPathTrie :: PathTrie -> Bool
isEmptyPathTrie PathTrie
EmptyPathTrie = Bool
True
isEmptyPathTrie PathTrie
_ = Bool
False
isTerminalPathTrie :: PathTrie -> Bool
isTerminalPathTrie :: PathTrie -> Bool
isTerminalPathTrie PathTrie
TerminalPathTrie = Bool
True
isTerminalPathTrie PathTrie
_ = Bool
False
comparePathTrieVectors :: Vector PathTrie -> Vector PathTrie -> Ordering
comparePathTrieVectors :: Vector PathTrie -> Vector PathTrie -> Ordering
comparePathTrieVectors Vector PathTrie
v1 Vector PathTrie
v2 = (Int -> Ordering -> Ordering) -> Ordering -> [Int] -> Ordering
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Int
i Ordering
res -> let (PathTrie
t1, PathTrie
t2) = (Vector PathTrie
v1 Vector PathTrie -> Int -> PathTrie
forall a. Vector a -> Int -> a
`Vector.unsafeIndex` Int
i, Vector PathTrie
v2 Vector PathTrie -> Int -> PathTrie
forall a. Vector a -> Int -> a
`Vector.unsafeIndex` Int
i)
in case (PathTrie -> Bool
isEmptyPathTrie PathTrie
t1, PathTrie -> Bool
isEmptyPathTrie PathTrie
t2) of
(Bool
False, Bool
True) -> Ordering
LT
(Bool
True, Bool
False) -> Ordering
GT
(Bool
True, Bool
True) -> Ordering
res
(Bool
False, Bool
False) -> case PathTrie -> PathTrie -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PathTrie
t1 PathTrie
t2 of
Ordering
LT -> Ordering
LT
Ordering
GT -> Ordering
GT
Ordering
EQ -> Ordering
res)
Ordering
valueIfComponentsMatch
[Int
0..(Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Vector PathTrie -> Int
forall a. Vector a -> Int
Vector.length Vector PathTrie
v1) (Vector PathTrie -> Int
forall a. Vector a -> Int
Vector.length Vector PathTrie
v2) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
where
valueIfComponentsMatch :: Ordering
valueIfComponentsMatch = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Vector PathTrie -> Int
forall a. Vector a -> Int
Vector.length Vector PathTrie
v1) (Vector PathTrie -> Int
forall a. Vector a -> Int
Vector.length Vector PathTrie
v2)
instance Ord PathTrie where
compare :: PathTrie -> PathTrie -> Ordering
compare PathTrie
EmptyPathTrie PathTrie
EmptyPathTrie = Ordering
EQ
compare PathTrie
EmptyPathTrie PathTrie
_ = Ordering
LT
compare PathTrie
_ PathTrie
EmptyPathTrie = Ordering
GT
compare PathTrie
TerminalPathTrie PathTrie
TerminalPathTrie = Ordering
EQ
compare PathTrie
TerminalPathTrie PathTrie
_ = Ordering
LT
compare PathTrie
_ PathTrie
TerminalPathTrie = Ordering
GT
compare (PathTrieSingleChild Int
i1 PathTrie
pt1) (PathTrieSingleChild Int
i2 PathTrie
pt2)
| Int
i1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i2 = Ordering
LT
| Int
i1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i2 = Ordering
GT
| Bool
otherwise = PathTrie -> PathTrie -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PathTrie
pt1 PathTrie
pt2
compare (PathTrieSingleChild Int
i1 PathTrie
pt1) (PathTrie Vector PathTrie
v2) = let i2 :: Int
i2 = Vector PathTrie -> Int
smallestNonempty Vector PathTrie
v2 in
case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
i1 Int
i2 of
Ordering
LT -> Ordering
LT
Ordering
GT -> Ordering
GT
Ordering
EQ -> case PathTrie -> PathTrie -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PathTrie
pt1 (Vector PathTrie
v2 Vector PathTrie -> Int -> PathTrie
forall a. Vector a -> Int -> a
`Vector.unsafeIndex` Int
i2) of
Ordering
LT -> Ordering
LT
Ordering
GT -> Ordering
GT
Ordering
EQ -> Ordering
LT
compare a :: PathTrie
a@(PathTrie Vector PathTrie
_) b :: PathTrie
b@(PathTrieSingleChild Int
_ PathTrie
_) = Ordering -> Ordering
flipOrdering (Ordering -> Ordering) -> Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ (PathTrie -> PathTrie -> Ordering)
-> PathTrie -> PathTrie -> Ordering
forall a. a -> a
inline PathTrie -> PathTrie -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PathTrie
b PathTrie
a
compare (PathTrie Vector PathTrie
v1) (PathTrie Vector PathTrie
v2) = Vector PathTrie -> Vector PathTrie -> Ordering
comparePathTrieVectors Vector PathTrie
v1 Vector PathTrie
v2
toPathTrie :: [Path] -> PathTrie
toPathTrie :: [Path] -> PathTrie
toPathTrie [] = PathTrie
EmptyPathTrie
toPathTrie [Path
EmptyPath] = PathTrie
TerminalPathTrie
toPathTrie [Path]
ps = if (Path -> Bool) -> [Path] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Path
p -> Path -> Int
pathHeadUnsafe Path
p Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Path -> Int
pathHeadUnsafe ([Path] -> Path
forall a. [a] -> a
head [Path]
ps)) [Path]
ps then
Int -> PathTrie -> PathTrie
PathTrieSingleChild (Path -> Int
pathHeadUnsafe (Path -> Int) -> Path -> Int
forall a b. (a -> b) -> a -> b
$ [Path] -> Path
forall a. [a] -> a
head [Path]
ps) ([Path] -> PathTrie
toPathTrie ([Path] -> PathTrie) -> [Path] -> PathTrie
forall a b. (a -> b) -> a -> b
$ (Path -> Path) -> [Path] -> [Path]
forall a b. (a -> b) -> [a] -> [b]
map Path -> Path
pathTailUnsafe [Path]
ps)
else
Vector PathTrie -> PathTrie
PathTrie Vector PathTrie
vec
where
maxIndex :: Int
maxIndex = Max Int -> Int
forall a. Max a -> a
getMax (Max Int -> Int) -> Max Int -> Int
forall a b. (a -> b) -> a -> b
$ (Path -> Max Int) -> [Path] -> Max Int
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> Max Int
forall a. a -> Max a
Max (Int -> Max Int) -> (Path -> Int) -> Path -> Max Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Path -> Int
pathHeadUnsafe) [Path]
ps
pathsStartingWith :: Int -> [Path] -> [Path]
pathsStartingWith :: Int -> [Path] -> [Path]
pathsStartingWith Int
i = (Path -> [Path]) -> [Path] -> [Path]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\case Path
EmptyPath -> []
ConsPath Int
j Path
p -> if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j then [Path
p] else [])
vec :: Vector PathTrie
vec = Int -> (Int -> PathTrie) -> Vector PathTrie
forall a. Int -> (Int -> a) -> Vector a
Vector.generate (Int
maxIndex Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (\Int
i -> [Path] -> PathTrie
toPathTrie ([Path] -> PathTrie) -> [Path] -> PathTrie
forall a b. (a -> b) -> a -> b
$ Int -> [Path] -> [Path]
pathsStartingWith Int
i [Path]
ps)
fromPathTrie :: PathTrie -> [Path]
fromPathTrie :: PathTrie -> [Path]
fromPathTrie PathTrie
EmptyPathTrie = []
fromPathTrie PathTrie
TerminalPathTrie = [Path
EmptyPath]
fromPathTrie (PathTrieSingleChild Int
i PathTrie
pt) = (Path -> Path) -> [Path] -> [Path]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Path -> Path
ConsPath Int
i) ([Path] -> [Path]) -> [Path] -> [Path]
forall a b. (a -> b) -> a -> b
$ PathTrie -> [Path]
fromPathTrie PathTrie
pt
fromPathTrie (PathTrie Vector PathTrie
v) = (Int -> PathTrie -> [Path] -> [Path])
-> [Path] -> Vector PathTrie -> [Path]
forall a b. (Int -> a -> b -> b) -> b -> Vector a -> b
Vector.ifoldr (\Int
i PathTrie
pt [Path]
acc -> (Path -> Path) -> [Path] -> [Path]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Path -> Path
ConsPath Int
i) (PathTrie -> [Path]
fromPathTrie PathTrie
pt) [Path] -> [Path] -> [Path]
forall a. [a] -> [a] -> [a]
++ [Path]
acc) [] Vector PathTrie
v
pathTrieDescend :: PathTrie -> Int -> PathTrie
pathTrieDescend :: PathTrie -> Int -> PathTrie
pathTrieDescend PathTrie
EmptyPathTrie Int
_ = PathTrie
EmptyPathTrie
pathTrieDescend PathTrie
TerminalPathTrie Int
_ = PathTrie
EmptyPathTrie
pathTrieDescend (PathTrie Vector PathTrie
v) Int
i = if Vector PathTrie -> Int
forall a. Vector a -> Int
Vector.length Vector PathTrie
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i then
Vector PathTrie
v Vector PathTrie -> Int -> PathTrie
forall a. Vector a -> Int -> a
`Vector.unsafeIndex` Int
i
else
PathTrie
EmptyPathTrie
pathTrieDescend (PathTrieSingleChild Int
j PathTrie
pt') Int
i
| Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = PathTrie
pt'
| Bool
otherwise = PathTrie
EmptyPathTrie
data PathEClass = PathEClass' { PathEClass -> PathTrie
getPathTrie :: !PathTrie
, PathEClass -> [Path]
getOrigPaths :: [Path]
}
deriving ( Int -> PathEClass -> ShowS
[PathEClass] -> ShowS
PathEClass -> String
(Int -> PathEClass -> ShowS)
-> (PathEClass -> String)
-> ([PathEClass] -> ShowS)
-> Show PathEClass
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PathEClass] -> ShowS
$cshowList :: [PathEClass] -> ShowS
show :: PathEClass -> String
$cshow :: PathEClass -> String
showsPrec :: Int -> PathEClass -> ShowS
$cshowsPrec :: Int -> PathEClass -> ShowS
Show, (forall x. PathEClass -> Rep PathEClass x)
-> (forall x. Rep PathEClass x -> PathEClass) -> Generic PathEClass
forall x. Rep PathEClass x -> PathEClass
forall x. PathEClass -> Rep PathEClass x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PathEClass x -> PathEClass
$cfrom :: forall x. PathEClass -> Rep PathEClass x
Generic )
instance Eq PathEClass where
== :: PathEClass -> PathEClass -> Bool
(==) = PathTrie -> PathTrie -> Bool
forall a. Eq a => a -> a -> Bool
(==) (PathTrie -> PathTrie -> Bool)
-> (PathEClass -> PathTrie) -> PathEClass -> PathEClass -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` PathEClass -> PathTrie
getPathTrie
instance Ord PathEClass where
compare :: PathEClass -> PathEClass -> Ordering
compare = PathTrie -> PathTrie -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (PathTrie -> PathTrie -> Ordering)
-> (PathEClass -> PathTrie) -> PathEClass -> PathEClass -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` PathEClass -> PathTrie
getPathTrie
pattern PathEClass :: [Path] -> PathEClass
pattern $bPathEClass :: [Path] -> PathEClass
$mPathEClass :: forall r. PathEClass -> ([Path] -> r) -> (Void# -> r) -> r
PathEClass ps <- PathEClass' _ ps where
PathEClass [Path]
ps = PathTrie -> [Path] -> PathEClass
PathEClass' ([Path] -> PathTrie
toPathTrie ([Path] -> PathTrie) -> [Path] -> PathTrie
forall a b. (a -> b) -> a -> b
$ [Path] -> [Path]
forall a. Eq a => [a] -> [a]
nub [Path]
ps) ([Path] -> [Path]
forall a. Ord a => [a] -> [a]
sort ([Path] -> [Path]) -> [Path] -> [Path]
forall a b. (a -> b) -> a -> b
$ [Path] -> [Path]
forall a. Eq a => [a] -> [a]
nub [Path]
ps)
unPathEClass :: PathEClass -> [Path]
unPathEClass :: PathEClass -> [Path]
unPathEClass (PathEClass' PathTrie
_ [Path]
paths) = [Path]
paths
instance Pretty PathEClass where
pretty :: PathEClass -> Text
pretty PathEClass
pec = Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (Text -> [Text] -> Text
Text.intercalate Text
"=" ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Path -> Text) -> [Path] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Path -> Text
forall a. Pretty a => a -> Text
pretty ([Path] -> [Text]) -> [Path] -> [Text]
forall a b. (a -> b) -> a -> b
$ PathEClass -> [Path]
unPathEClass PathEClass
pec) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
instance Hashable PathEClass
mkPathEClassFromPathTrie :: PathTrie -> PathEClass
mkPathEClassFromPathTrie :: PathTrie -> PathEClass
mkPathEClassFromPathTrie PathTrie
pt = PathTrie -> [Path] -> PathEClass
PathEClass' PathTrie
pt (PathTrie -> [Path]
fromPathTrie PathTrie
pt)
pathEClassDescend :: PathEClass -> Int -> PathEClass
pathEClassDescend :: PathEClass -> Int -> PathEClass
pathEClassDescend (PathEClass' PathTrie
pt [Path]
_) Int
i = PathTrie -> PathEClass
mkPathEClassFromPathTrie (PathTrie -> PathEClass) -> PathTrie -> PathEClass
forall a b. (a -> b) -> a -> b
$ PathTrie -> Int -> PathTrie
pathTrieDescend PathTrie
pt Int
i
hasSubsumingMember :: PathEClass -> PathEClass -> Bool
hasSubsumingMember :: PathEClass -> PathEClass -> Bool
hasSubsumingMember PathEClass
pec1 PathEClass
pec2 = PathTrie -> PathTrie -> Bool
go (PathEClass -> PathTrie
getPathTrie PathEClass
pec1) (PathEClass -> PathTrie
getPathTrie PathEClass
pec2)
where
go :: PathTrie -> PathTrie -> Bool
go :: PathTrie -> PathTrie -> Bool
go PathTrie
EmptyPathTrie PathTrie
_ = Bool
False
go PathTrie
_ PathTrie
EmptyPathTrie = Bool
False
go PathTrie
TerminalPathTrie PathTrie
TerminalPathTrie = Bool
False
go PathTrie
TerminalPathTrie PathTrie
_ = Bool
True
go PathTrie
_ PathTrie
TerminalPathTrie = Bool
False
go (PathTrieSingleChild Int
i1 PathTrie
pt1) (PathTrieSingleChild Int
i2 PathTrie
pt2) = if Int
i1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i2 then
PathTrie -> PathTrie -> Bool
go PathTrie
pt1 PathTrie
pt2
else
Bool
False
go (PathTrieSingleChild Int
i1 PathTrie
pt1) (PathTrie Vector PathTrie
v2) = case Vector PathTrie
v2 Vector PathTrie -> Int -> Maybe PathTrie
forall a. Vector a -> Int -> Maybe a
Vector.!? Int
i1 of
Maybe PathTrie
Nothing -> Bool
False
Just PathTrie
pt2 -> PathTrie -> PathTrie -> Bool
go PathTrie
pt1 PathTrie
pt2
go (PathTrie Vector PathTrie
v1) (PathTrieSingleChild Int
i2 PathTrie
pt2) = case Vector PathTrie
v1 Vector PathTrie -> Int -> Maybe PathTrie
forall a. Vector a -> Int -> Maybe a
Vector.!? Int
i2 of
Maybe PathTrie
Nothing -> Bool
False
Just PathTrie
pt1 -> PathTrie -> PathTrie -> Bool
go PathTrie
pt1 PathTrie
pt2
go (PathTrie Vector PathTrie
v1) (PathTrie Vector PathTrie
v2) = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Int
i -> PathTrie -> PathTrie -> Bool
go (Vector PathTrie
v1 Vector PathTrie -> Int -> PathTrie
forall a. Vector a -> Int -> a
`Vector.unsafeIndex` Int
i) (Vector PathTrie
v2 Vector PathTrie -> Int -> PathTrie
forall a. Vector a -> Int -> a
`Vector.unsafeIndex` Int
i))
[Int
0..(Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Vector PathTrie -> Int
forall a. Vector a -> Int
Vector.length Vector PathTrie
v1) (Vector PathTrie -> Int
forall a. Vector a -> Int
Vector.length Vector PathTrie
v2) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
completedSubsumptionOrdering :: PathEClass -> PathEClass -> Ordering
completedSubsumptionOrdering :: PathEClass -> PathEClass -> Ordering
completedSubsumptionOrdering PathEClass
pec1 PathEClass
pec2
| PathEClass -> PathEClass -> Bool
hasSubsumingMember PathEClass
pec1 PathEClass
pec2 = Ordering
LT
| PathEClass -> PathEClass -> Bool
hasSubsumingMember PathEClass
pec2 PathEClass
pec1 = Ordering
GT
| Bool
otherwise = PathEClass -> PathEClass -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PathEClass
pec2 PathEClass
pec1
data EqConstraints = EqConstraints { EqConstraints -> [PathEClass]
getEclasses :: [PathEClass]
}
| EqContradiction
deriving ( EqConstraints -> EqConstraints -> Bool
(EqConstraints -> EqConstraints -> Bool)
-> (EqConstraints -> EqConstraints -> Bool) -> Eq EqConstraints
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EqConstraints -> EqConstraints -> Bool
$c/= :: EqConstraints -> EqConstraints -> Bool
== :: EqConstraints -> EqConstraints -> Bool
$c== :: EqConstraints -> EqConstraints -> Bool
Eq, Eq EqConstraints
Eq EqConstraints
-> (EqConstraints -> EqConstraints -> Ordering)
-> (EqConstraints -> EqConstraints -> Bool)
-> (EqConstraints -> EqConstraints -> Bool)
-> (EqConstraints -> EqConstraints -> Bool)
-> (EqConstraints -> EqConstraints -> Bool)
-> (EqConstraints -> EqConstraints -> EqConstraints)
-> (EqConstraints -> EqConstraints -> EqConstraints)
-> Ord EqConstraints
EqConstraints -> EqConstraints -> Bool
EqConstraints -> EqConstraints -> Ordering
EqConstraints -> EqConstraints -> EqConstraints
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 :: EqConstraints -> EqConstraints -> EqConstraints
$cmin :: EqConstraints -> EqConstraints -> EqConstraints
max :: EqConstraints -> EqConstraints -> EqConstraints
$cmax :: EqConstraints -> EqConstraints -> EqConstraints
>= :: EqConstraints -> EqConstraints -> Bool
$c>= :: EqConstraints -> EqConstraints -> Bool
> :: EqConstraints -> EqConstraints -> Bool
$c> :: EqConstraints -> EqConstraints -> Bool
<= :: EqConstraints -> EqConstraints -> Bool
$c<= :: EqConstraints -> EqConstraints -> Bool
< :: EqConstraints -> EqConstraints -> Bool
$c< :: EqConstraints -> EqConstraints -> Bool
compare :: EqConstraints -> EqConstraints -> Ordering
$ccompare :: EqConstraints -> EqConstraints -> Ordering
$cp1Ord :: Eq EqConstraints
Ord, Int -> EqConstraints -> ShowS
[EqConstraints] -> ShowS
EqConstraints -> String
(Int -> EqConstraints -> ShowS)
-> (EqConstraints -> String)
-> ([EqConstraints] -> ShowS)
-> Show EqConstraints
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EqConstraints] -> ShowS
$cshowList :: [EqConstraints] -> ShowS
show :: EqConstraints -> String
$cshow :: EqConstraints -> String
showsPrec :: Int -> EqConstraints -> ShowS
$cshowsPrec :: Int -> EqConstraints -> ShowS
Show, (forall x. EqConstraints -> Rep EqConstraints x)
-> (forall x. Rep EqConstraints x -> EqConstraints)
-> Generic EqConstraints
forall x. Rep EqConstraints x -> EqConstraints
forall x. EqConstraints -> Rep EqConstraints x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep EqConstraints x -> EqConstraints
$cfrom :: forall x. EqConstraints -> Rep EqConstraints x
Generic )
instance Hashable EqConstraints
instance Pretty EqConstraints where
pretty :: EqConstraints -> Text
pretty EqConstraints
ecs = Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (Text -> [Text] -> Text
Text.intercalate Text
"," ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (PathEClass -> Text) -> [PathEClass] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map PathEClass -> Text
forall a. Pretty a => a -> Text
pretty (EqConstraints -> [PathEClass]
getEclasses EqConstraints
ecs)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
ecsGetPaths :: EqConstraints -> [[Path]]
ecsGetPaths :: EqConstraints -> [[Path]]
ecsGetPaths = (PathEClass -> [Path]) -> [PathEClass] -> [[Path]]
forall a b. (a -> b) -> [a] -> [b]
map PathEClass -> [Path]
unPathEClass ([PathEClass] -> [[Path]])
-> (EqConstraints -> [PathEClass]) -> EqConstraints -> [[Path]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqConstraints -> [PathEClass]
getEclasses
pattern EmptyConstraints :: EqConstraints
pattern $bEmptyConstraints :: EqConstraints
$mEmptyConstraints :: forall r. EqConstraints -> (Void# -> r) -> (Void# -> r) -> r
EmptyConstraints = EqConstraints []
unsafeGetEclasses :: EqConstraints -> [PathEClass]
unsafeGetEclasses :: EqConstraints -> [PathEClass]
unsafeGetEclasses EqConstraints
EqContradiction = String -> [PathEClass]
forall a. HasCallStack => String -> a
error String
"unsafeGetEclasses: Illegal argument 'EqContradiction'"
unsafeGetEclasses EqConstraints
ecs = EqConstraints -> [PathEClass]
getEclasses EqConstraints
ecs
rawMkEqConstraints :: [[Path]] -> EqConstraints
rawMkEqConstraints :: [[Path]] -> EqConstraints
rawMkEqConstraints = [PathEClass] -> EqConstraints
EqConstraints ([PathEClass] -> EqConstraints)
-> ([[Path]] -> [PathEClass]) -> [[Path]] -> EqConstraints
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Path] -> PathEClass) -> [[Path]] -> [PathEClass]
forall a b. (a -> b) -> [a] -> [b]
map [Path] -> PathEClass
PathEClass
constraintsAreContradictory :: EqConstraints -> Bool
constraintsAreContradictory :: EqConstraints -> Bool
constraintsAreContradictory = (EqConstraints -> EqConstraints -> Bool
forall a. Eq a => a -> a -> Bool
== EqConstraints
EqContradiction)
hasSubsumingMemberListBased :: [Path] -> [Path] -> Bool
hasSubsumingMemberListBased :: [Path] -> [Path] -> Bool
hasSubsumingMemberListBased [Path]
ps1 [Path]
ps2 = Any -> Bool
getAny (Any -> Bool) -> Any -> Bool
forall a b. (a -> b) -> a -> b
$ [Any] -> Any
forall a. Monoid a => [a] -> a
mconcat [Bool -> Any
Any (Path -> Path -> Bool
isStrictSubpath Path
p1 Path
p2) | Path
p1 <- [Path]
ps1
, Path
p2 <- [Path]
ps2]
isContradicting :: [[Path]] -> Bool
isContradicting :: [[Path]] -> Bool
isContradicting [[Path]]
cs = ([Path] -> Bool) -> [[Path]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\[Path]
pec -> [Path] -> [Path] -> Bool
hasSubsumingMemberListBased [Path]
pec [Path]
pec) [[Path]]
cs
mkEqConstraints :: [[Path]] -> EqConstraints
mkEqConstraints :: [[Path]] -> EqConstraints
mkEqConstraints [[Path]]
initialConstraints = case Maybe [[Path]]
completedConstraints of
Maybe [[Path]]
Nothing -> EqConstraints
EqContradiction
Just [[Path]]
cs -> [PathEClass] -> EqConstraints
EqConstraints ([PathEClass] -> EqConstraints) -> [PathEClass] -> EqConstraints
forall a b. (a -> b) -> a -> b
$ [PathEClass] -> [PathEClass]
forall a. Ord a => [a] -> [a]
sort ([PathEClass] -> [PathEClass]) -> [PathEClass] -> [PathEClass]
forall a b. (a -> b) -> a -> b
$ ([Path] -> PathEClass) -> [[Path]] -> [PathEClass]
forall a b. (a -> b) -> [a] -> [b]
map [Path] -> PathEClass
PathEClass [[Path]]
cs
where
removeTrivial :: (Eq a) => [[a]] -> [[a]]
removeTrivial :: [[a]] -> [[a]]
removeTrivial = ([a] -> Bool) -> [[a]] -> [[a]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\[a]
x -> [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) ([[a]] -> [[a]]) -> ([[a]] -> [[a]]) -> [[a]] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> [a]
forall a. Eq a => [a] -> [a]
nub
completedConstraints :: Maybe [[Path]]
completedConstraints = ([[Path]] -> Maybe [[Path]]) -> [[Path]] -> Maybe [[Path]]
forall a. Eq a => (a -> Maybe a) -> a -> Maybe a
fixMaybe [[Path]] -> Maybe [[Path]]
round ([[Path]] -> Maybe [[Path]]) -> [[Path]] -> Maybe [[Path]]
forall a b. (a -> b) -> a -> b
$ [[Path]] -> [[Path]]
forall a. Ord a => [[a]] -> [[a]]
complete ([[Path]] -> [[Path]]) -> [[Path]] -> [[Path]]
forall a b. (a -> b) -> a -> b
$ [[Path]] -> [[Path]]
forall a. Eq a => [[a]] -> [[a]]
removeTrivial [[Path]]
initialConstraints
round :: [[Path]] -> Maybe [[Path]]
round :: [[Path]] -> Maybe [[Path]]
round [[Path]]
cs = let cs' :: [[Path]]
cs' = [[Path]] -> [[Path]]
addCongruences [[Path]]
cs
cs'' :: [[Path]]
cs'' = [[Path]] -> [[Path]]
forall a. Ord a => [[a]] -> [[a]]
complete [[Path]]
cs'
in if [[Path]] -> Bool
isContradicting [[Path]]
cs'' then
Maybe [[Path]]
forall a. Maybe a
Nothing
else
[[Path]] -> Maybe [[Path]]
forall a. a -> Maybe a
Just [[Path]]
cs''
addCongruences :: [[Path]] -> [[Path]]
addCongruences :: [[Path]] -> [[Path]]
addCongruences [[Path]]
cs = [[Path]]
cs [[Path]] -> [[Path]] -> [[Path]]
forall a. [a] -> [a] -> [a]
++ [(Path -> Path) -> [Path] -> [Path]
forall a b. (a -> b) -> [a] -> [b]
map (\Path
z -> Path -> Path -> Path -> Path
substSubpath Path
z Path
x Path
y) [Path]
left | [Path]
left <- [[Path]]
cs, [Path]
right <- [[Path]]
cs, Path
x <- [Path]
left, Path
y <- [Path]
right, Path -> Path -> Bool
isStrictSubpath Path
x Path
y]
assertEquivs :: [a] -> m [()]
assertEquivs [a]
xs = (a -> m ()) -> [a] -> m [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\a
y -> a -> a -> m ()
forall c v d (m :: * -> *). MonadEquiv c v d m => v -> v -> m ()
equate ([a] -> a
forall a. [a] -> a
head [a]
xs) a
y) ([a] -> [a]
forall a. [a] -> [a]
tail [a]
xs)
complete :: (Ord a) => [[a]] -> [[a]]
complete :: [[a]] -> [[a]]
complete [[a]]
initialClasses = (a -> [a])
-> ([a] -> [a] -> [a]) -> (forall s. EquivM s [a] a [[a]]) -> [[a]]
forall v c a.
(v -> c) -> (c -> c -> c) -> (forall s. EquivM s c v a) -> a
runEquivM (a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[]) [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++) ((forall s. EquivM s [a] a [[a]]) -> [[a]])
-> (forall s. EquivM s [a] a [[a]]) -> [[a]]
forall a b. (a -> b) -> a -> b
$ do
([a] -> EquivT s [a] a Identity [()])
-> [[a]] -> EquivT s [a] a Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [a] -> EquivT s [a] a Identity [()]
forall (m :: * -> *) c a d. MonadEquiv c a d m => [a] -> m [()]
assertEquivs [[a]]
initialClasses
(Class s [a] a -> EquivT s [a] a Identity [a])
-> [Class s [a] a] -> EquivM s [a] a [[a]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Class s [a] a -> EquivT s [a] a Identity [a]
forall c v d (m :: * -> *). MonadEquiv c v d m => c -> m d
desc ([Class s [a] a] -> EquivM s [a] a [[a]])
-> EquivT s [a] a Identity [Class s [a] a] -> EquivM s [a] a [[a]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< EquivT s [a] a Identity [Class s [a] a]
forall c v d (m :: * -> *). MonadEquiv c v d m => m [c]
classes
combineEqConstraints :: EqConstraints -> EqConstraints -> EqConstraints
combineEqConstraints :: EqConstraints -> EqConstraints -> EqConstraints
combineEqConstraints = MemoCacheTag
-> (EqConstraints -> EqConstraints -> EqConstraints)
-> EqConstraints
-> EqConstraints
-> EqConstraints
forall a b c.
(Eq a, Hashable a, Eq b, Hashable b) =>
MemoCacheTag -> (a -> b -> c) -> a -> b -> c
memo2 (Text -> MemoCacheTag
NameTag Text
"combineEqConstraints") EqConstraints -> EqConstraints -> EqConstraints
go
where
go :: EqConstraints -> EqConstraints -> EqConstraints
go EqConstraints
EqContradiction EqConstraints
_ = EqConstraints
EqContradiction
go EqConstraints
_ EqConstraints
EqContradiction = EqConstraints
EqContradiction
go EqConstraints
ec1 EqConstraints
ec2 = [[Path]] -> EqConstraints
mkEqConstraints ([[Path]] -> EqConstraints) -> [[Path]] -> EqConstraints
forall a b. (a -> b) -> a -> b
$ EqConstraints -> [[Path]]
ecsGetPaths EqConstraints
ec1 [[Path]] -> [[Path]] -> [[Path]]
forall a. [a] -> [a] -> [a]
++ EqConstraints -> [[Path]]
ecsGetPaths EqConstraints
ec2
{-# NOINLINE combineEqConstraints #-}
eqConstraintsDescend :: EqConstraints -> Int -> EqConstraints
eqConstraintsDescend :: EqConstraints -> Int -> EqConstraints
eqConstraintsDescend EqConstraints
EqContradiction Int
_ = EqConstraints
EqContradiction
eqConstraintsDescend EqConstraints
ecs Int
i = [PathEClass] -> EqConstraints
EqConstraints ([PathEClass] -> EqConstraints) -> [PathEClass] -> EqConstraints
forall a b. (a -> b) -> a -> b
$ [PathEClass] -> [PathEClass]
forall a. Ord a => [a] -> [a]
sort ([PathEClass] -> [PathEClass]) -> [PathEClass] -> [PathEClass]
forall a b. (a -> b) -> a -> b
$ (PathEClass -> PathEClass) -> [PathEClass] -> [PathEClass]
forall a b. (a -> b) -> [a] -> [b]
map (PathEClass -> Int -> PathEClass
`pathEClassDescend` Int
i) (EqConstraints -> [PathEClass]
getEclasses EqConstraints
ecs)
constraintsImply :: EqConstraints -> EqConstraints -> Bool
constraintsImply :: EqConstraints -> EqConstraints -> Bool
constraintsImply EqConstraints
EqContradiction EqConstraints
_ = Bool
True
constraintsImply EqConstraints
_ EqConstraints
EqContradiction = Bool
False
constraintsImply EqConstraints
ecs1 EqConstraints
ecs2 = ([Path] -> Bool) -> [[Path]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[Path]
cs -> ([Path] -> Bool) -> [[Path]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Path] -> [Path] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSubsequenceOf [Path]
cs) (EqConstraints -> [[Path]]
ecsGetPaths EqConstraints
ecs1)) (EqConstraints -> [[Path]]
ecsGetPaths EqConstraints
ecs2)
subsumptionOrderedEclasses :: EqConstraints -> Maybe [PathEClass]
subsumptionOrderedEclasses :: EqConstraints -> Maybe [PathEClass]
subsumptionOrderedEclasses EqConstraints
ecs = case EqConstraints
ecs of
EqConstraints
EqContradiction -> Maybe [PathEClass]
forall a. Maybe a
Nothing
EqConstraints [PathEClass]
pecs -> [PathEClass] -> Maybe [PathEClass]
forall a. a -> Maybe a
Just ([PathEClass] -> Maybe [PathEClass])
-> [PathEClass] -> Maybe [PathEClass]
forall a b. (a -> b) -> a -> b
$ (PathEClass -> PathEClass -> Ordering)
-> [PathEClass] -> [PathEClass]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy PathEClass -> PathEClass -> Ordering
completedSubsumptionOrdering [PathEClass]
pecs
unsafeSubsumptionOrderedEclasses :: EqConstraints -> [PathEClass]
unsafeSubsumptionOrderedEclasses :: EqConstraints -> [PathEClass]
unsafeSubsumptionOrderedEclasses (EqConstraints [PathEClass]
pecs) = (PathEClass -> PathEClass -> Ordering)
-> [PathEClass] -> [PathEClass]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy PathEClass -> PathEClass -> Ordering
completedSubsumptionOrdering [PathEClass]
pecs
unsafeSubsumptionOrderedEclasses EqConstraints
EqContradiction = String -> [PathEClass]
forall a. HasCallStack => String -> a
error (String -> [PathEClass]) -> String -> [PathEClass]
forall a b. (a -> b) -> a -> b
$ String
"unsafeSubsumptionOrderedEclasses: unexpected EqContradiction"