1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
module Mu where
import Data.Map( Map, (!) )
import qualified Data.Map as M
import Data.Set( Set )
import qualified Data.Set as S
import Graph
--------------------------------------------------------------------------------
-- naive implementation of fixpoint computation
mu0 :: (Ord x, Eq a) => a -> [(x, [x], [a] -> a)] -> [x] -> [a]
mu0 bot defs zs = [ done!z | z <- zs ]
where
xs = [ x | (x, _, _) <- defs ]
done = iter [ bot | _ <- xs ]
iter as
| as == as' = tab
| otherwise = iter as'
where
tab = M.fromList (xs `zip` as)
as' = [ f [ tab!y | y <- ys ]
| (_,(_, ys, f)) <- as `zip` defs
]
--------------------------------------------------------------------------------
-- scc-based implementation of fixpoint computation
{-
a --^ initial/bottom value (smallest element) in the fixpoint computation
-> [( x, [x] --^ A single category, its arguments
, [a] -> a) --^ function that takes as its argument a list of values that we want to compute for the [x]
]
-> [x] --^ All categories that you want to see the answer for
-> [a] --^ Values for the given categories
-}
mu :: (Ord x, Eq a) => a -> [(x, [x], [a] -> a)] -> [x] -> [a]
mu bot defs zs = [ vtab?z | z <- zs ]
where
ftab = M.fromList [ (x,f) | (x,_,f) <- defs ]
graph = reach (M.fromList [ (x,xs) | (x,xs,_) <- defs ]) zs
vtab = foldl compute M.empty (scc graph)
compute vtab t = fix (-1) vtab (map (vtab ?) xs)
where
xs = S.toList (backs t)
fix 0 vtab _ = vtab
fix n vtab as
| as' == as = vtab'
| otherwise = fix (n-1) vtab' as'
where
(_,vtab') = eval t vtab
as' = map (vtab' ?) xs
eval (Cut x) vtab = (vtab?x, vtab)
eval (Node x ts) vtab = (a, M.insert x a vtab')
where
(as, vtab') = evalList ts vtab
a = (ftab!x) as
evalList [] vtab = ([], vtab)
evalList (t:ts) vtab = (a:as, vtab'')
where
(a, vtab') = eval t vtab
(as,vtab'') = evalList ts vtab'
vtab ? x = case M.lookup x vtab of
Nothing -> bot
Just a -> a
--------------------------------------------------------------------------------
-- diff/scc-based implementation of fixpoint computation
muDiff :: (Ord x, Eq a)
=> a -> (a->Bool) -> (a->a->a) -> (a->a->a)
-> [(x, [x], [a] -> a)]
-> [x] -> [a]
muDiff bot isBot diff apply defs zs = [ vtab?z | z <- zs ]
where
ftab = M.fromList [ (x,f) | (x,_,f) <- defs ]
graph = reach (M.fromList [ (x,xs) | (x,xs,_) <- defs ]) zs
vtab = foldl compute M.empty (scc graph)
compute vtab t = fix vtab M.empty
where
xs = S.toList (backs t)
fix dtab vtab
| all isBot ds = vtab'
| otherwise = fix (M.fromList (xs `zip` ds)) vtab'
where
dtab' = eval t dtab
vtab' = foldr (\(x,d) -> M.alter (Just . apply' d) x) vtab (M.toList dtab')
ds = map (dtab' ?) xs
apply' d Nothing = apply d bot
apply' d (Just a) = apply d a
eval (Cut x) tab = tab
eval (Node x ts) tab = M.insert x d tab'
where
tab' = foldl (flip eval) tab ts
d = (ftab!x) [ tab'?x | x <- map top ts ] `diff` (vtab?x)
vtab ? x = case M.lookup x vtab of
Nothing -> bot
Just a -> a
--------------------------------------------------------------------------------
|
