1 module FAmin 
    2 
    3 ( minBDFA
    4 , minTNFA
    5 )
    6 
    7 where
    8 
    9 
   10 import Set
   11 import FiniteMap
   12 
   13 import Options
   14 
   15 import Stuff
   16 
   17 import TA
   18 import FAtypes
   19 import Ids
   20 
   21 import FAconv
   22 
   23 import FAdet
   24 import FAhom
   25 
   26 -- amin stuff
   27 
   28 partFM :: Ord a => [[a]] -> FiniteMap a Int
   29 -- input is list of lists that constitute a partition
   30 -- output map each elem to the number of its class
   31 partFM p = 
   32     addListToFM_C 
   33         (\ _ _ -> error "partFM") -- paranoid: check uniq-ness
   34         emptyFM
   35         [ (v, k) | (k, vs) <- zip [0..] p, v <- vs ]
   36 
   37 -- items :: [a] -> [(Int, a, [a])]
   38 -- lists with dropped/picked nth element
   39 items [] = []
   40 items (x : xs) = (0, x, xs) : [ (n + 1, y, x : ys) | (n, y, ys) <- items xs ]
   41 
   42 refineFM :: (Show a, Ord a) =>
   43         FiniteMap a Int -> FiniteMap a Int -> FiniteMap a Int
   44 -- uses collectFM: result number range may have holes
   45 -- f must be a complete map, g may have holes
   46 refineFM f g =
   47     let fg = mapFM ( \ x fx -> 
   48                 (fx, lookupFM g x)) 
   49                 f
   50         p  = collectFM (eltsFM fg)
   51         h  = mapFM ( \ x fgx -> 
   52                 lookupWithDefaultFM p (error "refineFM.h") fgx ) 
   53                 fg
   54     in
   55 
   56 --      trace ("\nrefineFM.fg = " ++ show fg) $
   57 --      trace ("\nrefineFM.p  = " ++ show p ) $
   58 --      trace ("\nrefineFM.h  = " ++ show h ) $
   59 
   60         h           
   61 
   62 
   63 refineFMs :: (Show a, Ord a) => 
   64         FiniteMap a Int -> [ FiniteMap a Int ] -> FiniteMap a Int
   65 refineFMs p [] = p
   66 refineFMs p (f : fs) =
   67         if sizeFM p == cardinality (mkSet (eltsFM p))
   68         then p                   -- cannot be further refined
   69         else refineFMs (refineFM p f) fs   
   70     
   71 
   72 tconthrough :: (Show a, Ord a)
   73         => FiniteMap (STerm a) a -- transition table
   74         -> Set a            -- all variables
   75         -> FiniteMap a Int     -- a partition of all variables
   76         -> FiniteMap a Int     -- refinement of that partition
   77 
   78 tconthrough m all p =
   79     let tups (t, w) = 
   80                 [ ( ( stcon t, n, xs )
   81                   , (x, lookupWithDefaultFM p (error "tconthrough.w") w) )
   82                 | (n, x, xs) <- items (stargs t)
   83                 ]
   84 
   85         h = addListToFM_C 
   86                 (\ a b -> plusFM_C (error "tconthrough.h") a b) 
   87                 emptyFM 
   88                 [ (fun, unitFM x w) 
   89                 | tw <- fmToList m, (fun, (x, w)) <- tups tw 
   90                 ]
   91 
   92         q = refineFMs p (eltsFM h)
   93     in  
   94 
   95 --      trace ("\ntconthrough.p: " ++ show p) $
   96 --      trace ("\ntconthrough.h: " ++ show h) $
   97 --      trace ("\ntconthrough.q: " ++ show q) $
   98         
   99         q
  100 
  101 ------------------------------------------------------------------------
  102 
  103 minBDFA :: (Show a, Ord a) => Opts -> BDFA a -> BDFA Int
  104 minBDFA opts b @ (BDFA cons all starts moves) =
  105     let nostarts = all `minusSet` starts
  106         p = partFM [ setToList starts, setToList nostarts ]
  107         q = fixpoint (tconthrough moves all) p
  108         f = lookupWithDefaultFM q (error "bdfamin.f")
  109         c = homBDFA opts f b
  110     in  
  111 --      trace ("\nbdfamin.nostarts: " ++ show nostarts) $
  112 --      trace ("\nbdfamin.p: " ++ show p) $
  113 --      trace ("\nbdfamin.q: " ++ show q) $
  114 --      trace ("\nbdfamin.c: " ++ show c) $
  115         c
  116 
  117 
  118 minTNFA :: Opts -> TNFA Int -> TNFA Int
  119 minTNFA opts = bdfa2tnfa opts . minBDFA opts . tnfa2bdfa opts
  120 
  121 
  122