module DFAMin (minimizeDFA) where

import AbsSyn

import Control.Monad  (guard)
import Data.Bifunctor (second)
import Data.IntMap    (IntMap)
import Data.IntSet    (IntSet)

import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import qualified Data.List   as List
import qualified Data.Map    as Map

{- Note [Hopcroft's Algorithm]

DFA minimization is implemented using Hopcroft's algorithm. The following
definition is mostly copied from Wikipedia.

We assume the following definitions:
    - Q is the set of all states in our DFA
    - F is the subset of Q that contains all final (or "accepting") states
    - ∑ is the set of input symbols (for us, [0..255])

We use the phrase  "X refines Y into Y1 and Y2" to mean the following:
    - Y1 := Y ∩ X
    - Y2 := Y \ X
    - |Y1| > 0
    - |Y2| > 0

The algorithm itself is defined thusly:

    P := {F, Q \ F}
    W := {F, Q \ F}
    while (W is not empty) do
      choose and remove a set A from W
      for each c in Σ do
        let X be the set of states for which a transition on c leads to a state in A
        for each set Y in P that is refined by X into Y1 and Y2 do
            replace Y in P by the two sets Y1 and Y2
            if Y is in W
                replace Y in W by Y1 and Y2
            else
                if |Y1| <= |Y2|
                    add Y1 to W
                else
                    add Y2 to W


Our implementation differs slightly, as we perform several optimizations.

In the Wikipedia implementation, P and W are initialized to two subsets of Q,
specifically F and Q \ F. The exact subsets do not matter; what matters is the
following:
    - P and W should contain all Q states
    - equivalent states should all be in the same subset

As per the first requirement, it would be fine for P and W to be initialized as
a set that only contains Q. Using more fine-grained subsets reduces the amount
of work that needs to be done. The second requirement stems from the fact that
our partition "refining" can divide subsets, but we do not have a way to
re-merge subsets.

Our first optimization is that we use a more granular division of states in the
initial set. Specifically, we group all states by their list of "accepts", since
we know that for two states to be equivalent their list of "accepts" must be the
same: the resulting subsets therefore meet our two stated criteria.


Our second optimization relies on the observation that given that all states are
in W, then all states will appear in A; as a result, instead of starting with a
set P that contains all subsets, that we refine in parallel to W, we can instead
start with an empty set R, and add each A to R before iterating over P. This
makes updating R and W easier, and removes the need for the expensive "is Y in
W" check.


With those two optimizations, our implementation is therefore:

    R := {}
    W := {all "accept" subsets of Q}
    while (W is not empty) do
      choose and remove a set A from W
      add A to R
      for each c in Σ do
        let X be the set of states for which a transition on c leads to a state in A
        for each set Y in R that is refined by X into Y1 and Y2 do
            replace Y in R by the two sets Y1 and Y2
            if |Y1| <= |Y2|
                add Y1 to W
            else
                add Y2 to W
        for each set Y in W that is refined by X into Y1 and Y2 do
            replace Y in W by the two sets Y1 and Y2

-}

type OldSNum = Int -- ^ Old state number
type NewSNum = Int -- ^ New state number

-- | Reduce the number of states in the given DFA by grouping indistinguishable
-- states.
minimizeDFA :: forall a. Ord a => DFA OldSNum a -> DFA NewSNum a
minimizeDFA :: forall a. Ord a => DFA OldSNum a -> DFA OldSNum a
minimizeDFA dfa :: DFA OldSNum a
dfa@(DFA [OldSNum]
starts Map OldSNum (State OldSNum a)
statemap) = [OldSNum] -> Map OldSNum (State OldSNum a) -> DFA OldSNum a
forall s a. [s] -> Map s (State s a) -> DFA s a
DFA [OldSNum]
starts (Map OldSNum (State OldSNum a) -> DFA OldSNum a)
-> Map OldSNum (State OldSNum a) -> DFA OldSNum a
forall a b. (a -> b) -> a -> b
$ [(OldSNum, State OldSNum a)] -> Map OldSNum (State OldSNum a)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(OldSNum, State OldSNum a)]
new_states
  where
    -- Group the states into classes according to the language they accept.
    equiv_classes :: [EquivalenceClass]
    equiv_classes :: [EquivalenceClass]
equiv_classes = DFA OldSNum a -> [EquivalenceClass]
forall a. Ord a => DFA OldSNum a -> [EquivalenceClass]
groupEquivalentStates DFA OldSNum a
dfa

    -- A map from new state numbers to a class of equivalent old states.
    numbered_states :: [(NewSNum, EquivalenceClass)]
    numbered_states :: [(OldSNum, EquivalenceClass)]
numbered_states = OldSNum
-> [OldSNum] -> [EquivalenceClass] -> [(OldSNum, EquivalenceClass)]
number ([OldSNum] -> OldSNum
forall a. [a] -> OldSNum
forall (t :: * -> *) a. Foldable t => t a -> OldSNum
length [OldSNum]
starts) [OldSNum]
starts [EquivalenceClass]
equiv_classes

    -- Assign each state in the minimized DFA a number, making
    -- sure that we assign the numbers [0..] to the start states.
    number :: NewSNum -> [NewSNum] -> [EquivalenceClass] -> [(NewSNum, EquivalenceClass)]
    number :: OldSNum
-> [OldSNum] -> [EquivalenceClass] -> [(OldSNum, EquivalenceClass)]
number OldSNum
_ [OldSNum]
_ [] = []
    number OldSNum
n [OldSNum]
unassigned_starts (EquivalenceClass
ss:[EquivalenceClass]
sss)
      | [OldSNum] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OldSNum]
starts_ss = (OldSNum
n,EquivalenceClass
ss) (OldSNum, EquivalenceClass)
-> [(OldSNum, EquivalenceClass)] -> [(OldSNum, EquivalenceClass)]
forall a. a -> [a] -> [a]
: OldSNum -> [(OldSNum, EquivalenceClass)]
continue (OldSNum
nOldSNum -> OldSNum -> OldSNum
forall a. Num a => a -> a -> a
+OldSNum
1)
      | Bool
otherwise      = (OldSNum -> (OldSNum, EquivalenceClass))
-> [OldSNum] -> [(OldSNum, EquivalenceClass)]
forall a b. (a -> b) -> [a] -> [b]
map (,EquivalenceClass
ss) [OldSNum]
starts_ss [(OldSNum, EquivalenceClass)]
-> [(OldSNum, EquivalenceClass)] -> [(OldSNum, EquivalenceClass)]
forall a. [a] -> [a] -> [a]
++ OldSNum -> [(OldSNum, EquivalenceClass)]
continue OldSNum
n
        -- if one of the states of the minimized DFA corresponds
        -- to multiple starts states, we just have to duplicate
        -- that state.
      where
        -- All the start states in ss (starts_ss) are assigned this equivalence class.
        -- The remaining ones are passed to the recursive call.
        ([OldSNum]
starts_ss, [OldSNum]
starts_other) = (OldSNum -> Bool) -> [OldSNum] -> ([OldSNum], [OldSNum])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (OldSNum -> EquivalenceClass -> Bool
`IntSet.member` EquivalenceClass
ss) [OldSNum]
unassigned_starts
        continue :: OldSNum -> [(OldSNum, EquivalenceClass)]
continue OldSNum
n' = OldSNum
-> [OldSNum] -> [EquivalenceClass] -> [(OldSNum, EquivalenceClass)]
number OldSNum
n' [OldSNum]
starts_other [EquivalenceClass]
sss

    -- Mapping new state numbers to their state description.
    new_states :: [(NewSNum, State NewSNum a)]
    new_states :: [(OldSNum, State OldSNum a)]
new_states = ((OldSNum, EquivalenceClass) -> (OldSNum, State OldSNum a))
-> [(OldSNum, EquivalenceClass)] -> [(OldSNum, State OldSNum a)]
forall a b. (a -> b) -> [a] -> [b]
map ((EquivalenceClass -> State OldSNum a)
-> (OldSNum, EquivalenceClass) -> (OldSNum, State OldSNum a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second EquivalenceClass -> State OldSNum a
class_to_new_state) [(OldSNum, EquivalenceClass)]
numbered_states

    -- Translate an equivalence class of old states into a new state description.
    class_to_new_state :: EquivalenceClass -> State NewSNum a
    class_to_new_state :: EquivalenceClass -> State OldSNum a
class_to_new_state =
        -- A new state is constructed from any of the old states in the equivalence class.
        -- It does not matter which old state we pick since by construction of the classes
        -- they have the same behavior, both in their output (accepts) and their transitions.
        -- Since IntSet does not have a method to give an arbitrary element
        -- (ideally the one that is fastest to retrieve)
        -- we use findMin (always succeeds because the IntSet is non-empty).
        State OldSNum a -> State OldSNum a
old_state_to_new_state (State OldSNum a -> State OldSNum a)
-> (EquivalenceClass -> State OldSNum a)
-> EquivalenceClass
-> State OldSNum a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map OldSNum (State OldSNum a) -> OldSNum -> State OldSNum a
forall {c}. Map OldSNum c -> OldSNum -> c
lookupOrPanic Map OldSNum (State OldSNum a)
statemap (OldSNum -> State OldSNum a)
-> (EquivalenceClass -> OldSNum)
-> EquivalenceClass
-> State OldSNum a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EquivalenceClass -> OldSNum
IntSet.findMin
      where
        lookupOrPanic :: Map OldSNum c -> OldSNum -> c
lookupOrPanic = (OldSNum -> Map OldSNum c -> c) -> Map OldSNum c -> OldSNum -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((OldSNum -> Map OldSNum c -> c) -> Map OldSNum c -> OldSNum -> c)
-> (OldSNum -> Map OldSNum c -> c) -> Map OldSNum c -> OldSNum -> c
forall a b. (a -> b) -> a -> b
$ c -> OldSNum -> Map OldSNum c -> c
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault c
forall {a}. a
panic
        panic :: a
panic = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"alex::DFAMin.minimizeDFA: panic: state not found"

    -- Convert all state numbers in the State structure to new ones.
    old_state_to_new_state :: State OldSNum a -> State NewSNum a
    old_state_to_new_state :: State OldSNum a -> State OldSNum a
old_state_to_new_state (State [Accept a]
old_accepts IntMap OldSNum
old_transitions) =
      [Accept a] -> IntMap OldSNum -> State OldSNum a
forall s a. [Accept a] -> IntMap s -> State s a
State ((Accept a -> Accept a) -> [Accept a] -> [Accept a]
forall a b. (a -> b) -> [a] -> [b]
map Accept a -> Accept a
fix_acc [Accept a]
old_accepts) ((OldSNum -> OldSNum) -> IntMap OldSNum -> IntMap OldSNum
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OldSNum -> OldSNum
get_new IntMap OldSNum
old_transitions)

    fix_acc :: Accept a -> Accept a
    fix_acc :: Accept a -> Accept a
fix_acc Accept a
acc = Accept a
acc { accRightCtx :: RightContext OldSNum
accRightCtx = (OldSNum -> OldSNum)
-> RightContext OldSNum -> RightContext OldSNum
forall a b. (a -> b) -> RightContext a -> RightContext b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OldSNum -> OldSNum
get_new (RightContext OldSNum -> RightContext OldSNum)
-> RightContext OldSNum -> RightContext OldSNum
forall a b. (a -> b) -> a -> b
$ Accept a -> RightContext OldSNum
forall a. Accept a -> RightContext OldSNum
accRightCtx Accept a
acc }

    get_new :: OldSNum -> NewSNum
    get_new :: OldSNum -> OldSNum
get_new OldSNum
k = OldSNum -> OldSNum -> IntMap OldSNum -> OldSNum
forall a. a -> OldSNum -> IntMap a -> a
IntMap.findWithDefault OldSNum
forall {a}. a
panic OldSNum
k IntMap OldSNum
old_to_new
      where
        panic :: a
panic = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"alex::DFAMin.minimizeDFA: panic: state not found"

    -- Memoized translation of old state numbers to new state numbers.
    old_to_new :: IntMap NewSNum
    old_to_new :: IntMap OldSNum
old_to_new = [(OldSNum, OldSNum)] -> IntMap OldSNum
forall a. [(OldSNum, a)] -> IntMap a
IntMap.fromList ([(OldSNum, OldSNum)] -> IntMap OldSNum)
-> [(OldSNum, OldSNum)] -> IntMap OldSNum
forall a b. (a -> b) -> a -> b
$ do
      (OldSNum
n,EquivalenceClass
ss) <- [(OldSNum, EquivalenceClass)]
numbered_states
      OldSNum
s <- EquivalenceClass -> [OldSNum]
IntSet.toList EquivalenceClass
ss
      (OldSNum, OldSNum) -> [(OldSNum, OldSNum)]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OldSNum
s,OldSNum
n)


-- | An equivalence class is a /non-empty/ set of states.
type EquivalenceClass = IntSet


-- | Creates the subsets of Q that are used to initialize W.
--
-- As per the two conditions listed in Note [Hopcroft's Algorithm], we have two
-- requirements: the union of all resulting sets must be equivalent to Q (the set
-- of all states), and all equivalent states must be in the same subsets.
--
-- We group states by their list of 'Accept'.
initialSubsets :: forall a. Ord a => DFA OldSNum a -> [EquivalenceClass]
initialSubsets :: forall a. Ord a => DFA OldSNum a -> [EquivalenceClass]
initialSubsets DFA OldSNum a
dfa = Map [Accept a] EquivalenceClass -> [EquivalenceClass]
forall k a. Map k a -> [a]
Map.elems (Map [Accept a] EquivalenceClass -> [EquivalenceClass])
-> Map [Accept a] EquivalenceClass -> [EquivalenceClass]
forall a b. (a -> b) -> a -> b
$ (EquivalenceClass -> EquivalenceClass -> EquivalenceClass)
-> [([Accept a], EquivalenceClass)]
-> Map [Accept a] EquivalenceClass
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith EquivalenceClass -> EquivalenceClass -> EquivalenceClass
IntSet.union ([([Accept a], EquivalenceClass)]
 -> Map [Accept a] EquivalenceClass)
-> [([Accept a], EquivalenceClass)]
-> Map [Accept a] EquivalenceClass
forall a b. (a -> b) -> a -> b
$ do
  (OldSNum
stateIndex, State [Accept a]
accepts IntMap OldSNum
_transitions) <- Map OldSNum (State OldSNum a) -> [(OldSNum, State OldSNum a)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map OldSNum (State OldSNum a) -> [(OldSNum, State OldSNum a)])
-> Map OldSNum (State OldSNum a) -> [(OldSNum, State OldSNum a)]
forall a b. (a -> b) -> a -> b
$ DFA OldSNum a -> Map OldSNum (State OldSNum a)
forall s a. DFA s a -> Map s (State s a)
dfa_states DFA OldSNum a
dfa
  ([Accept a], EquivalenceClass) -> [([Accept a], EquivalenceClass)]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Accept a]
accepts, OldSNum -> EquivalenceClass
IntSet.singleton OldSNum
stateIndex)


-- | Creates a cache of all reverse transitions for a given DFA.
--
-- To each token c in Σ, the resulting map associates a reverse map of
-- transitions. That is: for each c, we have a map that, to a state s,
-- associates the set of states that can reach s via c.
--
-- Given that the actual value of c is never actually required, we flatten the
-- result into a list.
generateReverseTransitionCache :: forall a. Ord a => DFA OldSNum a -> [IntMap EquivalenceClass]
generateReverseTransitionCache :: forall a. Ord a => DFA OldSNum a -> [IntMap EquivalenceClass]
generateReverseTransitionCache DFA OldSNum a
dfa = IntMap (IntMap EquivalenceClass) -> [IntMap EquivalenceClass]
forall a. IntMap a -> [a]
IntMap.elems (IntMap (IntMap EquivalenceClass) -> [IntMap EquivalenceClass])
-> IntMap (IntMap EquivalenceClass) -> [IntMap EquivalenceClass]
forall a b. (a -> b) -> a -> b
$
  (IntMap EquivalenceClass
 -> IntMap EquivalenceClass -> IntMap EquivalenceClass)
-> [(OldSNum, IntMap EquivalenceClass)]
-> IntMap (IntMap EquivalenceClass)
forall a. (a -> a -> a) -> [(OldSNum, a)] -> IntMap a
IntMap.fromListWith ((EquivalenceClass -> EquivalenceClass -> EquivalenceClass)
-> IntMap EquivalenceClass
-> IntMap EquivalenceClass
-> IntMap EquivalenceClass
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith EquivalenceClass -> EquivalenceClass -> EquivalenceClass
IntSet.union) ([(OldSNum, IntMap EquivalenceClass)]
 -> IntMap (IntMap EquivalenceClass))
-> [(OldSNum, IntMap EquivalenceClass)]
-> IntMap (IntMap EquivalenceClass)
forall a b. (a -> b) -> a -> b
$ do
    (OldSNum
sourceState, State [Accept a]
_accepts IntMap OldSNum
transitions) <- Map OldSNum (State OldSNum a) -> [(OldSNum, State OldSNum a)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map OldSNum (State OldSNum a) -> [(OldSNum, State OldSNum a)])
-> Map OldSNum (State OldSNum a) -> [(OldSNum, State OldSNum a)]
forall a b. (a -> b) -> a -> b
$ DFA OldSNum a -> Map OldSNum (State OldSNum a)
forall s a. DFA s a -> Map s (State s a)
dfa_states DFA OldSNum a
dfa
    (OldSNum
token, OldSNum
targetState) <- IntMap OldSNum -> [(OldSNum, OldSNum)]
forall a. IntMap a -> [(OldSNum, a)]
IntMap.toList IntMap OldSNum
transitions
    (OldSNum, IntMap EquivalenceClass)
-> [(OldSNum, IntMap EquivalenceClass)]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OldSNum
token, OldSNum -> EquivalenceClass -> IntMap EquivalenceClass
forall a. OldSNum -> a -> IntMap a
IntMap.singleton OldSNum
targetState (OldSNum -> EquivalenceClass
IntSet.singleton OldSNum
sourceState))


-- | Given two sets X and Y, compute their intersection and difference.
-- Only returns both if both are non-empty, otherwise return neither.
refine
  :: EquivalenceClass
  -> EquivalenceClass
  -> Maybe (EquivalenceClass, EquivalenceClass)
refine :: EquivalenceClass
-> EquivalenceClass -> Maybe (EquivalenceClass, EquivalenceClass)
refine EquivalenceClass
x EquivalenceClass
y =
  if EquivalenceClass -> Bool
IntSet.null EquivalenceClass
intersection Bool -> Bool -> Bool
|| EquivalenceClass -> Bool
IntSet.null EquivalenceClass
difference
    then Maybe (EquivalenceClass, EquivalenceClass)
forall a. Maybe a
Nothing
    else (EquivalenceClass, EquivalenceClass)
-> Maybe (EquivalenceClass, EquivalenceClass)
forall a. a -> Maybe a
Just (EquivalenceClass
intersection, EquivalenceClass
difference)
  where
    intersection :: EquivalenceClass
intersection = EquivalenceClass -> EquivalenceClass -> EquivalenceClass
IntSet.intersection EquivalenceClass
y EquivalenceClass
x
    difference :: EquivalenceClass
difference   = EquivalenceClass -> EquivalenceClass -> EquivalenceClass
IntSet.difference   EquivalenceClass
y EquivalenceClass
x


-- | Given a DFA, compute all sets of equivalent states.
--
-- See Note [Hopcroft's Algorithm] for details.
groupEquivalentStates :: forall a. Ord a => DFA OldSNum a -> [EquivalenceClass]
groupEquivalentStates :: forall a. Ord a => DFA OldSNum a -> [EquivalenceClass]
groupEquivalentStates DFA OldSNum a
dfa = ([EquivalenceClass], [EquivalenceClass]) -> [EquivalenceClass]
outerLoop ([], DFA OldSNum a -> [EquivalenceClass]
forall a. Ord a => DFA OldSNum a -> [EquivalenceClass]
initialSubsets DFA OldSNum a
dfa)
  where
    reverseTransitionCache :: [IntMap EquivalenceClass]
    reverseTransitionCache :: [IntMap EquivalenceClass]
reverseTransitionCache = DFA OldSNum a -> [IntMap EquivalenceClass]
forall a. Ord a => DFA OldSNum a -> [IntMap EquivalenceClass]
generateReverseTransitionCache DFA OldSNum a
dfa

    -- While W isn't empty, pick an A from W, add it to R
    -- and iterate on X for each c in ∑.
    outerLoop :: ([EquivalenceClass], [EquivalenceClass]) -> [EquivalenceClass]
    outerLoop :: ([EquivalenceClass], [EquivalenceClass]) -> [EquivalenceClass]
outerLoop ([EquivalenceClass]
r,  []) = [EquivalenceClass]
r
    outerLoop ([EquivalenceClass]
r, EquivalenceClass
a:[EquivalenceClass]
w) = ([EquivalenceClass], [EquivalenceClass]) -> [EquivalenceClass]
outerLoop (([EquivalenceClass], [EquivalenceClass]) -> [EquivalenceClass])
-> ([EquivalenceClass], [EquivalenceClass]) -> [EquivalenceClass]
forall a b. (a -> b) -> a -> b
$ (([EquivalenceClass], [EquivalenceClass])
 -> EquivalenceClass -> ([EquivalenceClass], [EquivalenceClass]))
-> ([EquivalenceClass], [EquivalenceClass])
-> [EquivalenceClass]
-> ([EquivalenceClass], [EquivalenceClass])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' ([EquivalenceClass], [EquivalenceClass])
-> EquivalenceClass -> ([EquivalenceClass], [EquivalenceClass])
forall {t :: * -> *} {t :: * -> *}.
(Foldable t, Foldable t) =>
(t EquivalenceClass, t EquivalenceClass)
-> EquivalenceClass -> ([EquivalenceClass], [EquivalenceClass])
refineWithX (EquivalenceClass
aEquivalenceClass -> [EquivalenceClass] -> [EquivalenceClass]
forall a. a -> [a] -> [a]
:[EquivalenceClass]
r,[EquivalenceClass]
w) ([EquivalenceClass] -> ([EquivalenceClass], [EquivalenceClass]))
-> [EquivalenceClass] -> ([EquivalenceClass], [EquivalenceClass])
forall a b. (a -> b) -> a -> b
$ do
      IntMap EquivalenceClass
allPreviousStates <- [IntMap EquivalenceClass]
reverseTransitionCache
      let x :: EquivalenceClass
x = [EquivalenceClass] -> EquivalenceClass
forall (f :: * -> *).
Foldable f =>
f EquivalenceClass -> EquivalenceClass
IntSet.unions ([EquivalenceClass] -> EquivalenceClass)
-> [EquivalenceClass] -> EquivalenceClass
forall a b. (a -> b) -> a -> b
$ do
            (OldSNum
target, EquivalenceClass
sources) <- IntMap EquivalenceClass -> [(OldSNum, EquivalenceClass)]
forall a. IntMap a -> [(OldSNum, a)]
IntMap.toList IntMap EquivalenceClass
allPreviousStates
            Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ OldSNum
target OldSNum -> EquivalenceClass -> Bool
`IntSet.member` EquivalenceClass
a
            EquivalenceClass -> [EquivalenceClass]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure EquivalenceClass
sources
      Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ EquivalenceClass -> Bool
IntSet.null EquivalenceClass
x
      EquivalenceClass -> [EquivalenceClass]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure EquivalenceClass
x

    -- Given X, refine values in R, then refine values in W, building
    -- the new values of R and W along the way.
    refineWithX :: (t EquivalenceClass, t EquivalenceClass)
-> EquivalenceClass -> ([EquivalenceClass], [EquivalenceClass])
refineWithX (t EquivalenceClass
r, t EquivalenceClass
w) EquivalenceClass
x =
      let ([EquivalenceClass]
r', [EquivalenceClass]
w') = (([EquivalenceClass], [EquivalenceClass])
 -> EquivalenceClass -> ([EquivalenceClass], [EquivalenceClass]))
-> ([EquivalenceClass], [EquivalenceClass])
-> t EquivalenceClass
-> ([EquivalenceClass], [EquivalenceClass])
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (EquivalenceClass
-> ([EquivalenceClass], [EquivalenceClass])
-> EquivalenceClass
-> ([EquivalenceClass], [EquivalenceClass])
processR EquivalenceClass
x) ([], []) t EquivalenceClass
r
      in  ([EquivalenceClass]
r', ([EquivalenceClass] -> EquivalenceClass -> [EquivalenceClass])
-> [EquivalenceClass] -> t EquivalenceClass -> [EquivalenceClass]
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (EquivalenceClass
-> [EquivalenceClass] -> EquivalenceClass -> [EquivalenceClass]
processW EquivalenceClass
x) [EquivalenceClass]
w' t EquivalenceClass
w)

    processR :: EquivalenceClass
-> ([EquivalenceClass], [EquivalenceClass])
-> EquivalenceClass
-> ([EquivalenceClass], [EquivalenceClass])
processR EquivalenceClass
x ([EquivalenceClass]
r', [EquivalenceClass]
w') EquivalenceClass
y = case EquivalenceClass
-> EquivalenceClass -> Maybe (EquivalenceClass, EquivalenceClass)
refine EquivalenceClass
x EquivalenceClass
y of
      Maybe (EquivalenceClass, EquivalenceClass)
Nothing -> (EquivalenceClass
yEquivalenceClass -> [EquivalenceClass] -> [EquivalenceClass]
forall a. a -> [a] -> [a]
:[EquivalenceClass]
r', [EquivalenceClass]
w')
      Just (EquivalenceClass
y1, EquivalenceClass
y2)
        | EquivalenceClass -> OldSNum
IntSet.size EquivalenceClass
y1 OldSNum -> OldSNum -> Bool
forall a. Ord a => a -> a -> Bool
<= EquivalenceClass -> OldSNum
IntSet.size EquivalenceClass
y2 -> (EquivalenceClass
y2EquivalenceClass -> [EquivalenceClass] -> [EquivalenceClass]
forall a. a -> [a] -> [a]
:[EquivalenceClass]
r', EquivalenceClass
y1EquivalenceClass -> [EquivalenceClass] -> [EquivalenceClass]
forall a. a -> [a] -> [a]
:[EquivalenceClass]
w')
        | Bool
otherwise                        -> (EquivalenceClass
y1EquivalenceClass -> [EquivalenceClass] -> [EquivalenceClass]
forall a. a -> [a] -> [a]
:[EquivalenceClass]
r', EquivalenceClass
y2EquivalenceClass -> [EquivalenceClass] -> [EquivalenceClass]
forall a. a -> [a] -> [a]
:[EquivalenceClass]
w')

    processW :: EquivalenceClass
-> [EquivalenceClass] -> EquivalenceClass -> [EquivalenceClass]
processW EquivalenceClass
x [EquivalenceClass]
w' EquivalenceClass
y = case EquivalenceClass
-> EquivalenceClass -> Maybe (EquivalenceClass, EquivalenceClass)
refine EquivalenceClass
x EquivalenceClass
y of
      Maybe (EquivalenceClass, EquivalenceClass)
Nothing       -> EquivalenceClass
yEquivalenceClass -> [EquivalenceClass] -> [EquivalenceClass]
forall a. a -> [a] -> [a]
:[EquivalenceClass]
w'
      Just (EquivalenceClass
y1, EquivalenceClass
y2) -> EquivalenceClass
y1EquivalenceClass -> [EquivalenceClass] -> [EquivalenceClass]
forall a. a -> [a] -> [a]
:EquivalenceClass
y2EquivalenceClass -> [EquivalenceClass] -> [EquivalenceClass]
forall a. a -> [a] -> [a]
:[EquivalenceClass]
w'