module MyhillNerode
where

import DFA
import PrintDFA
import Transform
import Auxfuns
import List

--  Parition:  division of a set into a set of parts that are disjoint and cover the set

--  rep:  takes a partition and an element and returns the part of which it is a member
rep :: (Eq a) => [[a]] -> a -> [a]
rep (q:qs) p
   | p `elem` q = q
   | otherwise = rep qs p
rep [] p = error "rep"

--  image:  parition-over-Q -> delta -> part -> symbol -> image of q as a part
image :: (Eq q) => [[q]] -> (q -> t -> q) -> [q] -> t -> [(q, [q])]
image qs d p w = map (\q -> (q, rep qs $ d q w)) p


--  inducedP:  returns partition induced by a mapping, given as a graph
inducedP :: (Ord a, Eq t) => [(a, t)] -> [[a]]
inducedP f = inducedPA [] f
    where inducedPA :: (Ord q, Eq t) => [(t, [q])] -> [(q, t)] -> [[q]]
          inducedPA inv [] = map (\(k,v) -> canonical v) inv
          inducedPA inv ((p,fp):f) = inducedPA (insertByCons inv fp p) f

--  refineP:  partitions a part of a partition based on delta
--          N.B. the partition returned is a parition of part p of parition qs
refineP :: (Ord q) => [[q]] -> (q -> t -> q) -> [q] -> t -> [[q]]
refineP qs d p w = inducedP $ image qs d p w

--  step:  Refines the partition based on induced map by symbol w
step :: (Ord q) => [[q]] -> (q -> t -> q) -> t -> [[q]]
step qs d w = concat [refineP qs d p w | p <- qs]

--  iter:  Refines the partition based on induced map by a set of symbols ws
iter :: (Ord q) => [[q]] -> (q -> t -> q) -> [t] -> [[q]]
iter qs d [] = qs
iter qs d (w:ws) = iter (step qs d w) d ws

--  mhCore:  
--  Assumptions:  
--     1.  All states are reachable.  
--     2.  The set of final and non-final states are non-empty.
--  Note worklist is pessimistic.  This has guaranteed worst case behavior.
--   However, optimizing is non-trivial as d' is not well defined until bigQ' is stable

mhCore :: (Ord q) => DFA q t -> DFA [q] t
mhCore (DFA { states = bigQ, symbols = sigma, delta = d, start = q0, final = f})
    = let notf = [ q | q <- bigQ, not $ elem q f]
          p0 = [f,notf]                                 -- initial partition
          worklist = concat $ map (\_ -> sigma) bigQ    -- symbols on which to refine partition (|Q| copies of Sigma)
          bigQ' = iter p0 d worklist                    -- the final partition (new state space)
          d' (p:_) a = rep bigQ' (d p a)                -- lifting of delta to new state space
          [q0'] = filter (elem q0) bigQ'                -- lifting of q0
          f' = filter (\(p:_) -> elem p f) bigQ'        -- lifting of f
      in DFA { states = bigQ', symbols = sigma, delta = d', start = q0', final = f' }

mh m = let m' = reachableDFA m
           q' = states m'
           empty = DFA { states = [q'], 
                         symbols = symbols m', 
                         delta = \_ _ -> q',
                         start = q', 
                         final = [] }
           sigmastar = empty { final = [q'] }
       in if null $ final m' then empty
          else if all (\q -> elem q (final m')) q' then sigmastar
               else mhCore m'