bfa1cb103793608525eead9bdb23acd6673d875f
[nofib.git] / real / rx / src / FAmin.hs
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