{-# LANGUAGE OverloadedStrings #-}

-- | Representations of paths in an FTA, data structures for
--   equality constraints over paths, algorithms for saturating these constraints

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

-------------------------------------------------------


-----------------------------------------------------------------------
--------------------------- Misc / general ----------------------------
-----------------------------------------------------------------------

flipOrdering :: Ordering -> Ordering
flipOrdering :: Ordering -> Ordering
flipOrdering Ordering
GT = Ordering
LT
flipOrdering Ordering
LT = Ordering
GT
flipOrdering Ordering
EQ = Ordering
EQ

-----------------------------------------------------------------------
-------------------------------- Paths --------------------------------
-----------------------------------------------------------------------

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


-- | Read `substSubpath p1 p2 p3` as `[p1/p2]p3`
--
-- `substSubpath replacement toReplace target` takes `toReplace`, a prefix of target,
--  and returns a new path in which `toReplace` has been replaced by `replacement`.
--
--  Undefined if toReplace is not a prefix of target
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)


--------------------------------------------------------------------------
---------------------------- Using paths ---------------------------------
--------------------------------------------------------------------------

-- | TODO: Should this be redone as a lens-library traversal?
-- | TODO: I am unhappy about this Emptyable design; makes one question whether
--         this should be a typeclass at all. (Terms/ECTAs differ in that
--         there is always an ECTA Node that represents the value at a path)
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


-----------------------------------------------------------------------
---------------------------- Path tries -------------------------------
-----------------------------------------------------------------------

---------------------
------- Generic-ish utility functions
---------------------

-- | Precondition: A nonempty cell exists
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


-- | Precondition: A nonempty cell exists
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

---------------------
------- Path tries
---------------------

data PathTrie = EmptyPathTrie
              | TerminalPathTrie
              | PathTrieSingleChild {-# UNPACK #-} !Int !PathTrie
              | PathTrie !(Vector PathTrie) -- Invariant: Must have at least two nonempty nodes
  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 -- v2 must have a second nonempty
  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 -- TODO: Check whether this inlining is effective
  compare (PathTrie Vector PathTrie
v1)                (PathTrie Vector PathTrie
v2)                = Vector PathTrie -> Vector PathTrie -> Ordering
comparePathTrieVectors Vector PathTrie
v1 Vector PathTrie
v2


-- | Precondition: No path in the input is a subpath of another
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

    -- TODO: Inefficient to use this; many passes. over the list.
    -- This may not be used in a place where perf matters, though
    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

--------------------------------------------------------------------------
---------------------- Equality constraints over paths -------------------
--------------------------------------------------------------------------

---------------------------
---------- Path E-classes
---------------------------

data PathEClass = PathEClass' { PathEClass -> PathTrie
getPathTrie  :: !PathTrie
                              , PathEClass -> [Path]
getOrigPaths ::  [Path]   -- Intentionally lazy because
                                                          -- not available when calling `mkPathEClassFromPathTrie`
                              }
  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

-- | TODO: This pattern (and the caching of the original path list) is a temporary affair
--         until we convert all clients of PathEclass to fully be based on tries
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)]


-- | Extends the subsumption ordering to a total ordering by using the default lexicographic
--   comparison for incomparable elements.
-- | TODO: Optimization opportunity: Redundant work in the hasSubsumingMember calls
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
                       --   This next line is some hacky magic. Basically, it means that for the
                       --   Hoogle+/TermSearch workload, where there is no subsumption,
                       --   constraints will be evaluated in left-to-right order (instead of the default
                       --   right-to-left), which for that particular workload produces better
                       --   constraint-propagation
                       | Bool
otherwise                    = PathEClass -> PathEClass -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PathEClass
pec2 PathEClass
pec1

--------------------------------
---------- Equality constraints
--------------------------------

data EqConstraints = EqConstraints { EqConstraints -> [PathEClass]
getEclasses :: [PathEClass] -- ^ Must be sorted
                                   }
                   | 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
"}"

--------- Destructors and patterns

-- | Unsafe. Internal use only
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)

--------- Construction


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]

-- | The real contradiction condition is a cycle in the subsumption ordering.
--   But, after congruence closure, this will reduce into a self-cycle in the subsumption ordering.
--
--   TODO; Prove this.
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

-- Contains an inefficient implementation of the congruence closure algorithm
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

    -- Reason for the extra "complete" in this line:
    -- The first simplification done to the constraints is eclass-completion,
    -- to remove redundancy and shrink things before the very inefficienc
    -- addCongruences step (important in tests; less so in realistic input).
    -- The last simplification must also be completion, to give a valid value.
    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

---------- Operations

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)

-- A faster implementation would be: Merge the eclasses of both, run mkEqConstraints (or at least do eclass completion),
-- check result equal to ecs2
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"