1 module FAmin
3 ( minBDFA
4 , minTNFA
5 )
7 where
10 import Set
11 import FiniteMap
13 import Options
15 import Stuff
17 import TA
18 import FAtypes
19 import Ids
21 import FAconv
24 import FAhom
26 -- amin stuff
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 =
33 (\ _ _ -> error "partFM") -- paranoid: check uniq-ness
34 emptyFM
35 [ (v, k) | (k, vs) <- zip [0..] p, v <- vs ]
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 ]
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
56 -- trace ("\nrefineFM.fg = " ++ show fg) \$
57 -- trace ("\nrefineFM.p = " ++ show p ) \$
58 -- trace ("\nrefineFM.h = " ++ show h ) \$
60 h
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
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
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 ]
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 ]
92 q = refineFMs p (eltsFM h)
93 in
95 -- trace ("\ntconthrough.p: " ++ show p) \$
96 -- trace ("\ntconthrough.h: " ++ show h) \$
97 -- trace ("\ntconthrough.q: " ++ show q) \$
99 q
101 ------------------------------------------------------------------------
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
118 minTNFA :: Opts -> TNFA Int -> TNFA Int
119 minTNFA opts = bdfa2tnfa opts . minBDFA opts . tnfa2bdfa opts