{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# LANGUAGE PatternGuards #-}
module DFAMin (minimizeDFA) where

import AbsSyn

import Data.Map (Map)
import qualified Data.Map as Map
import Data.IntSet (IntSet)
import qualified Data.IntSet as IS
import Data.IntMap (IntMap)
import qualified Data.IntMap as IM
import Data.List as List


-- Hopcroft's Algorithm for DFA minimization (cut/pasted from Wikipedia):

-- P := {{all accepting states}, {all nonaccepting states}};
-- Q := {{all accepting states}};
-- while (Q is not empty) do
--      choose and remove a set A from Q
--      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 for which X ∩ Y is nonempty do
--                replace Y in P by the two sets X ∩ Y and Y \ X
--                if Y is in Q
--                     replace Y in Q by the same two sets
--                else
--                     add the smaller of the two sets to Q
--           end;
--      end;
-- end;

minimizeDFA :: Ord a => DFA Int a -> DFA Int a
minimizeDFA :: DFA Int a -> DFA Int a
minimizeDFA  dfa :: DFA Int a
dfa@DFA { dfa_start_states :: forall s a. DFA s a -> [s]
dfa_start_states = [Int]
starts,
                       dfa_states :: forall s a. DFA s a -> Map s (State s a)
dfa_states       = Map Int (State Int a)
statemap
                     }
  = DFA :: forall s a. [s] -> Map s (State s a) -> DFA s a
DFA { dfa_start_states :: [Int]
dfa_start_states = [Int]
starts,
          dfa_states :: Map Int (State Int a)
dfa_states       = [(Int, State Int a)] -> Map Int (State Int a)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int, State Int a)]
states }
  where
      equiv_classes :: [IntSet]
equiv_classes   = DFA Int a -> [IntSet]
forall a. Ord a => DFA Int a -> [IntSet]
groupEquivStates DFA Int a
dfa

      numbered_states :: [(Int, IntSet)]
numbered_states = Int -> [IntSet] -> [(Int, IntSet)]
number ([Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
starts) [IntSet]
equiv_classes

      -- assign each state in the minimized DFA a number, making
      -- sure that we assign the numbers [0..] to the start states.
      number :: Int -> [IntSet] -> [(Int, IntSet)]
number Int
_ [] = []
      number Int
n (IntSet
ss:[IntSet]
sss) =
        case (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> IntSet -> Bool
`IS.member` IntSet
ss) [Int]
starts of
          []      -> (Int
n,IntSet
ss) (Int, IntSet) -> [(Int, IntSet)] -> [(Int, IntSet)]
forall a. a -> [a] -> [a]
: Int -> [IntSet] -> [(Int, IntSet)]
number (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [IntSet]
sss
          [Int]
starts' -> [Int] -> [IntSet] -> [(Int, IntSet)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
starts' (IntSet -> [IntSet]
forall a. a -> [a]
repeat IntSet
ss) [(Int, IntSet)] -> [(Int, IntSet)] -> [(Int, IntSet)]
forall a. [a] -> [a] -> [a]
++ Int -> [IntSet] -> [(Int, IntSet)]
number Int
n [IntSet]
sss
          -- if one of the states of the minimized DFA corresponds
          -- to multiple starts states, we just have to duplicate
          -- that state.

      states :: [(Int, State Int a)]
states = [
                let old_states :: [State Int a]
old_states = (Int -> State Int a) -> [Int] -> [State Int a]
forall a b. (a -> b) -> [a] -> [b]
map (Map Int (State Int a) -> Int -> State Int a
forall k a. Ord k => Map k a -> k -> a
lookup Map Int (State Int a)
statemap) (IntSet -> [Int]
IS.toList IntSet
equiv)
                    accs :: [Accept a]
accs = (Accept a -> Accept a) -> [Accept a] -> [Accept a]
forall a b. (a -> b) -> [a] -> [b]
map Accept a -> Accept a
forall a. Accept a -> Accept a
fix_acc (State Int a -> [Accept a]
forall s a. State s a -> [Accept a]
state_acc ([State Int a] -> State Int a
forall a. [a] -> a
head [State Int a]
old_states))
                           -- accepts should all be the same
                    out :: IntMap Int
out  = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IM.fromList [ (Int
b, Int -> Int
get_new Int
old)
                                           | State [Accept a]
_ IntMap Int
out <- [State Int a]
old_states,
                                             (Int
b,Int
old) <- IntMap Int -> [(Int, Int)]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap Int
out ]
                in (Int
n, [Accept a] -> IntMap Int -> State Int a
forall s a. [Accept a] -> IntMap s -> State s a
State [Accept a]
accs IntMap Int
out)
               | (Int
n, IntSet
equiv) <- [(Int, IntSet)]
numbered_states
               ]

      fix_acc :: Accept a -> Accept a
fix_acc Accept a
acc = Accept a
acc { accRightCtx :: RightContext Int
accRightCtx = RightContext Int -> RightContext Int
fix_rctxt (Accept a -> RightContext Int
forall a. Accept a -> RightContext Int
accRightCtx Accept a
acc) }

      fix_rctxt :: RightContext Int -> RightContext Int
fix_rctxt (RightContextRExp Int
s) = Int -> RightContext Int
forall r. r -> RightContext r
RightContextRExp (Int -> Int
get_new Int
s)
      fix_rctxt RightContext Int
other = RightContext Int
other

      lookup :: Map k a -> k -> a
lookup Map k a
m k
k = a -> k -> Map k a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"minimizeDFA") k
k Map k a
m
      get_new :: Int -> Int
get_new = Map Int Int -> Int -> Int
forall k a. Ord k => Map k a -> k -> a
lookup Map Int Int
old_to_new

      old_to_new :: Map Int Int
      old_to_new :: Map Int Int
old_to_new = [(Int, Int)] -> Map Int Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Int
s,Int
n) | (Int
n,IntSet
ss) <- [(Int, IntSet)]
numbered_states,
                                          Int
s <- IntSet -> [Int]
IS.toList IntSet
ss ]


groupEquivStates :: (Ord a) => DFA Int a -> [IntSet]
groupEquivStates :: DFA Int a -> [IntSet]
groupEquivStates DFA { dfa_states :: forall s a. DFA s a -> Map s (State s a)
dfa_states = Map Int (State Int a)
statemap }
  = [IntSet] -> [IntSet] -> [IntSet]
go [IntSet]
init_p [IntSet]
init_q
  where
    (Map Int (State Int a)
accepting, Map Int (State Int a)
nonaccepting) = (State Int a -> Bool)
-> Map Int (State Int a)
-> (Map Int (State Int a), Map Int (State Int a))
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition State Int a -> Bool
forall s a. State s a -> Bool
acc Map Int (State Int a)
statemap
       where acc :: State s a -> Bool
acc (State [Accept a]
as IntMap s
_) = Bool -> Bool
not ([Accept a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
List.null [Accept a]
as)

    nonaccepting_states :: IntSet
nonaccepting_states = [Int] -> IntSet
IS.fromList (Map Int (State Int a) -> [Int]
forall k a. Map k a -> [k]
Map.keys Map Int (State Int a)
nonaccepting)

    -- group the accepting states into equivalence classes
    accept_map :: Map [Accept a] [Int]
accept_map = {-# SCC "accept_map" #-}
      (Map [Accept a] [Int]
 -> (Int, State Int a) -> Map [Accept a] [Int])
-> Map [Accept a] [Int]
-> [(Int, State Int a)]
-> Map [Accept a] [Int]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Map [Accept a] [Int]
m (Int
n,State Int a
s) -> ([Int] -> [Int] -> [Int])
-> [Accept a]
-> [Int]
-> Map [Accept a] [Int]
-> Map [Accept a] [Int]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
(++) (State Int a -> [Accept a]
forall s a. State s a -> [Accept a]
state_acc State Int a
s) [Int
n] Map [Accept a] [Int]
m)
             Map [Accept a] [Int]
forall k a. Map k a
Map.empty
             (Map Int (State Int a) -> [(Int, State Int a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Int (State Int a)
accepting)

    -- accept_groups :: Ord s => [Set s]
    accept_groups :: [IntSet]
accept_groups = ([Int] -> IntSet) -> [[Int]] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> IntSet
IS.fromList (Map [Accept a] [Int] -> [[Int]]
forall k a. Map k a -> [a]
Map.elems Map [Accept a] [Int]
accept_map)

    init_p :: [IntSet]
init_p = IntSet
nonaccepting_states IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
: [IntSet]
accept_groups
    init_q :: [IntSet]
init_q = [IntSet]
accept_groups

    -- map token T to
    --   a map from state S to the list of states that transition to
    --   S on token T
    -- This is a cache of the information needed to compute x below
    bigmap :: IntMap (IntMap [SNum])
    bigmap :: IntMap (IntMap [Int])
bigmap = (IntMap [Int] -> IntMap [Int] -> IntMap [Int])
-> [(Int, IntMap [Int])] -> IntMap (IntMap [Int])
forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IM.fromListWith (([Int] -> [Int] -> [Int])
-> IntMap [Int] -> IntMap [Int] -> IntMap [Int]
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IM.unionWith [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
(++))
                [ (Int
i, Int -> [Int] -> IntMap [Int]
forall a. Int -> a -> IntMap a
IM.singleton Int
to [Int
from])
                | (Int
from, State Int a
state) <- Map Int (State Int a) -> [(Int, State Int a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Int (State Int a)
statemap,
                  (Int
i,Int
to) <- IntMap Int -> [(Int, Int)]
forall a. IntMap a -> [(Int, a)]
IM.toList (State Int a -> IntMap Int
forall s a. State s a -> IntMap s
state_out State Int a
state) ]

    -- incoming I A = the set of states that transition to a state in
    -- A on token I.
    incoming :: Int -> IntSet -> IntSet
    incoming :: Int -> IntSet -> IntSet
incoming Int
i IntSet
a = [Int] -> IntSet
IS.fromList ([[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Int]]
ss)
       where
         map1 :: IntMap [Int]
map1 = IntMap [Int] -> Int -> IntMap (IntMap [Int]) -> IntMap [Int]
forall a. a -> Int -> IntMap a -> a
IM.findWithDefault IntMap [Int]
forall a. IntMap a
IM.empty Int
i IntMap (IntMap [Int])
bigmap
         ss :: [[Int]]
ss = [ [Int] -> Int -> IntMap [Int] -> [Int]
forall a. a -> Int -> IntMap a -> a
IM.findWithDefault [] Int
s IntMap [Int]
map1
              | Int
s <- IntSet -> [Int]
IS.toList IntSet
a ]

    -- The outer loop: recurse on each set in Q
    go :: [IntSet] -> [IntSet] -> [IntSet]
go [IntSet]
p [] = [IntSet]
p
    go [IntSet]
p (IntSet
a:[IntSet]
q) = Int -> [IntSet] -> [IntSet] -> [IntSet]
go1 Int
0 [IntSet]
p [IntSet]
q
     where
       -- recurse on each token (0..255)
       go1 :: Int -> [IntSet] -> [IntSet] -> [IntSet]
go1 Int
256 [IntSet]
p [IntSet]
q = [IntSet] -> [IntSet] -> [IntSet]
go [IntSet]
p [IntSet]
q
       go1 Int
i   [IntSet]
p [IntSet]
q = Int -> [IntSet] -> [IntSet] -> [IntSet]
go1 (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [IntSet]
p' [IntSet]
q'
          where
            ([IntSet]
p',[IntSet]
q') = [IntSet] -> [IntSet] -> [IntSet] -> ([IntSet], [IntSet])
go2 [IntSet]
p [] [IntSet]
q

            x :: IntSet
x = Int -> IntSet -> IntSet
incoming Int
i IntSet
a

            -- recurse on each set in P
            go2 :: [IntSet] -> [IntSet] -> [IntSet] -> ([IntSet], [IntSet])
go2 []    [IntSet]
p' [IntSet]
q = ([IntSet]
p',[IntSet]
q)
            go2 (IntSet
y:[IntSet]
p) [IntSet]
p' [IntSet]
q
              | IntSet -> Bool
IS.null IntSet
i Bool -> Bool -> Bool
|| IntSet -> Bool
IS.null IntSet
d = [IntSet] -> [IntSet] -> [IntSet] -> ([IntSet], [IntSet])
go2 [IntSet]
p (IntSet
yIntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
:[IntSet]
p') [IntSet]
q
              | Bool
otherwise              = [IntSet] -> [IntSet] -> [IntSet] -> ([IntSet], [IntSet])
go2 [IntSet]
p (IntSet
iIntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
:IntSet
dIntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
:[IntSet]
p') [IntSet]
q1
              where
                    i :: IntSet
i = IntSet -> IntSet -> IntSet
IS.intersection IntSet
x IntSet
y
                    d :: IntSet
d = IntSet -> IntSet -> IntSet
IS.difference IntSet
y IntSet
x

                    q1 :: [IntSet]
q1 = [IntSet] -> [IntSet]
replaceyin [IntSet]
q
                           where
                             replaceyin :: [IntSet] -> [IntSet]
replaceyin [] =
                                if IntSet -> Int
IS.size IntSet
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< IntSet -> Int
IS.size IntSet
d then [IntSet
i] else [IntSet
d]
                             replaceyin (IntSet
z:[IntSet]
zs)
                                | IntSet
z IntSet -> IntSet -> Bool
forall a. Eq a => a -> a -> Bool
== IntSet
y    = IntSet
i IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
: IntSet
d IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
: [IntSet]
zs
                                | Bool
otherwise = IntSet
z IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
: [IntSet] -> [IntSet]
replaceyin [IntSet]
zs