add an FAQ file
[packages/hoopl.git] / prototypes / Hoopl1.hs
1 {-# OPTIONS_GHC -Wall -fno-warn-incomplete-patterns #-}
2 -- With GHC 6.10 we get bogus incomplete-pattern warnings
3 -- It's fine in 6.12
4 {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, EmptyDataDecls,
5 PatternGuards, TypeFamilies #-}
6
7 -- This version uses type families to express the functional dependency
8 -- between the open/closed-ness of the input graph and the type of the
9 -- input fact expected for a graph of that shape
10
11 module Hoopl where
12
13 import qualified Data.IntMap as M
14 import qualified Data.IntSet as S
15
16 -----------------------------------------------------------------------------
17 -- Graphs
18 -----------------------------------------------------------------------------
19
20 data ZOpen
21 data ZClosed
22
23 type O = ZOpen
24 type C = ZClosed
25
26 -- Blocks are always non-empty
27 data Block n e x where
28 BUnit :: n e x -> Block n e x
29 BCat :: Block n e O -> Block n O x -> Block n e x
30
31 type Blocks n = [Block n C C]
32
33 data Graph n e x where
34 GNil :: Graph n O O
35 GUnit :: Block n e x -> Graph n e x
36 GMany { g_entry :: Block n e C
37 , g_blocks :: Blocks n
38 , g_exit :: Exit (Block n C x) x } :: Graph n e x
39
40 -- Invariant: if g_entry is closed,
41 -- its BlockId cannot be a target of
42 -- branches in the blocks
43
44 -- If a graph has a Tail, then that tail is the only
45 -- exit from the graph, even if the Tail is closed
46 -- See the definition of successors!
47
48 data Exit thing x where
49 NoTail :: Exit thing C
50 Tail :: thing -> Exit thing x
51
52 class Edges thing where
53 blockId :: thing C x -> BlockId
54 successors :: thing e C -> [BlockId]
55
56 instance Edges n => Edges (Block n) where
57 blockId (BUnit n) = blockId n
58 blockId (BCat b _) = blockId b
59 successors (BUnit n) = successors n
60 successors (BCat _ b) = successors b
61
62 instance Edges n => Edges (Graph n) where
63 blockId (GUnit b) = blockId b
64 blockId (GMany b _ _) = blockId b
65 successors (GUnit b) = successors b
66 successors (GMany _ _ (Tail b)) = successors b
67 successors (GMany b bs NoTail)
68 = blockSetElems (all_succs `minusBlockSet` all_blk_ids)
69 where
70 all_succs = mkBlockSet (successors b ++ concatMap successors bs)
71 all_blk_ids = mkBlockSet (map blockId bs)
72
73
74 gCat :: Graph n e O -> Graph n O x -> Graph n e x
75 gCat GNil g2 = g2
76 gCat g1 GNil = g1
77
78 gCat (GUnit b1) (GUnit b2)
79 = GUnit (b1 `BCat` b2)
80
81 gCat (GUnit b) (GMany e bs x)
82 = GMany (b `BCat` e) bs x
83
84 gCat (GMany e bs (Tail x)) (GUnit b2)
85 = GMany e bs (Tail (x `BCat` b2))
86
87 gCat (GMany e1 bs1 (Tail x1)) (GMany e2 bs2 x2)
88 = GMany e1 (x1 `BCat` e2 : bs1 ++ bs2) x2
89
90 gCatC :: Graph n e C -> Graph n C x -> Graph n e x
91 gCatC (GUnit b1) (GUnit b2) = GMany b1 [] (Tail b2)
92 gCatC (GUnit b1) (GMany e2 bs x2) = GMany b1 (e2:bs) x2
93 gCatC (GMany e bs NoTail) (GUnit b2) = GMany e bs (Tail b2)
94 gCatC (GMany e bs (Tail b1)) (GUnit b2) = GMany e (b1:bs) (Tail b2)
95 gCatC (GMany e1 bs1 NoTail) (GMany e2 bs2 x2) = GMany e1 (e2 : bs1 ++ bs2) x2
96 gCatC (GMany e1 bs1 (Tail x1)) (GMany e2 bs2 x2) = GMany e1 (x1 : e2 : bs1 ++ bs2) x2
97
98 type GraphWithFacts n f e x = (Graph n e x, FactBase f)
99 type BlocksWithFacts n f = (Blocks n, FactBase f)
100
101 gwfCat :: GraphWithFacts n f e O -> GraphWithFacts n f O x -> GraphWithFacts n f e x
102 gwfCat (g1,fb1) (g2,fb2) = (g1 `gCat` g2, fb1 `unionFactBase` fb2)
103
104 mkGMany :: GraphWithFacts n e C f
105 -> BlocksWithFacts n
106 -> Exit (GraphWithFacts n f C x) x
107 -> GraphWithFacts n e x
108 mkGMany (e,fb1) (bs,fb2) x = GMany b_e (bs_e ++ bs ++ bs_x) b_x
109 where
110 (b_e, bs_e) = mkHead e
111 (bs_x, b_x) = mkTail x
112
113 mkHead :: Graph n e C -> (Block n e C, Blocks n)
114 mkHead (GUnit b) = (b, [])
115 mkHead (GMany e bs NoTail) = (e, bs)
116 mkHead (GMany e bs (Tail b)) = (e, b:bs)
117
118 mkTail :: Exit (GraphWithFacts n C x) x
119 -> (BlocksWithFacts n, Exit (Block n C x) x)
120 mkTail NoTail = ([], NoTail)
121 mkTail (Tail (GUnit b, fb)) = ([], Tail b)
122 mkTail (Tail (GMany e bs x)) = (e:bs, x)
123
124 flattenG :: Graph n C C -> Blocks n
125 flattenG (GUnit b) = [b]
126 flattenG (GMany e bs NoTail) = e:bs
127 flattenG (GMany e bs (Tail x)) = e:x:bs
128
129 forwardBlockList :: Blocks n -> Blocks n
130 -- This produces a list of blocks in order suitable for forward analysis.
131 -- ToDo: Do a topological sort to improve convergence rate of fixpoint
132 -- This will require a (HavingSuccessors l) class constraint
133 forwardBlockList blks = blks
134
135 -----------------------------------------------------------------------------
136 -- DataflowLattice
137 -----------------------------------------------------------------------------
138
139 data DataflowLattice a = DataflowLattice {
140 fact_name :: String, -- Documentation
141 fact_bot :: a, -- Lattice bottom element
142 fact_add_to :: a -> a -> TxRes a, -- Lattice join plus change flag
143 fact_do_logging :: Bool -- log changes
144 }
145
146 data ChangeFlag = NoChange | SomeChange
147 data TxRes a = TxRes ChangeFlag a
148
149 -----------------------------------------------------------------------------
150 -- The main Hoopl API
151 -----------------------------------------------------------------------------
152
153 type ForwardTransfers n f
154 = forall e x. n e x -> InFact e f -> OutFact x f
155
156 type ForwardRewrites n f
157 = forall e x. n e x -> InFact e f -> Maybe (AGraph n e x)
158
159 type family InFact e f :: *
160 type instance InFact C f = InFactC f
161 type instance InFact O f = f
162
163 type family OutFact x f :: *
164 type instance OutFact C f = OutFactC f
165 type instance OutFact O f = f
166
167 type InFactC fact = BlockId -> fact
168 type OutFactC fact = [(BlockId, fact)]
169
170 data AGraph n e x = AGraph -- Stub for now
171
172
173 -----------------------------------------------------------------------------
174 -- TxFactBase: a FactBase with ChangeFlag information
175 -----------------------------------------------------------------------------
176
177 -- The TxFactBase is an accumulating parameter, threaded through all
178 -- the analysis/transformation of each block in the g_blocks of a grpah.
179 -- It carries a ChangeFlag with it, and a set of BlockIds
180 -- to monitor. Updates to other BlockIds don't affect the ChangeFlag
181 data TxFactBase n f
182 = TxFB { tfb_fbase :: FactBase f
183
184 , tfb_cha :: ChangeFlag
185 , tfb_bids :: BlockSet -- Update change flag iff these blocks change
186 -- These are BlockIds of the *original*
187 -- (not transformed) blocks
188
189 , tfb_blks :: BlocksWithFacts n f -- Transformed blocks
190 }
191
192 factBaseInFacts :: DataflowLattice f -> TxFactBase n f -> InFactC f
193 factBaseInFacts lattice (TxFB { tfb_fbase = fbase })
194 = lookupFact lattice fbase
195
196 factBaseOutFacts :: TxFactBase n f -> OutFactC f
197 factBaseOutFacts (TxFB { tfb_fbase = fbase, tfb_bids = bids })
198 = [ (bid, f) | (bid, f) <- factBaseList fbase
199 , not (bid `elemBlockSet` bids) ]
200 -- The successors of the Graph are the the BlockIds for which
201 -- we hvae facts, that are *not* in the blocks of the graph
202
203 updateFact :: DataflowLattice f -> (BlockId, f)
204 -> TxFactBase n f -> TxFactBase n f
205 -- Update a TxFactBase, setting the change flag iff
206 -- a) the new fact adds information...
207 -- b) for a block in the BlockSet in the TxFactBase
208 updateFact lat (bid, new_fact) tx_fb@(TxFB { tfb_fbase = fbase, tfb_bids = bids})
209 | NoChange <- cha2 = tx_fb
210 | bid `elemBlockSet` bids = tx_fb { tfb_fbase = new_fbase, tfb_cha = SomeChange }
211 | otherwise = tx_fb { tfb_fbase = new_fbase }
212 where
213 old_fact = lookupFact lat fbase bid
214 TxRes cha2 res_fact = fact_add_to lat old_fact new_fact
215 new_fbase = extendFactBase fbase bid res_fact
216
217 updateFacts :: Edges n
218 => DataflowLattice f
219 -> GFT_Block n f
220 -> Block n C C
221 -> Trans (TxFactBase n f) (TxFactBase n f)
222 updateFacts lat (GFT block_trans) blk
223 tx_fb@(TxFB { tfb_fbase = fbase, tfb_bids = bids, tfb_blks = blks })
224 = do { (graph, out_facts) <- block_trans blk (lookupFact lat fbase)
225 ; let tx_fb' = tx_fb { tfb_bids = extendBlockSet bids (blockId blk)
226 , tfb_blks = flattenG graph ++ blks }
227 ; return (foldr (updateFact lat) tx_fb' out_facts) }
228
229 -----------------------------------------------------------------------------
230 -- The Trans arrow
231 -----------------------------------------------------------------------------
232
233 type Trans a b = a -> FuelMonad b
234 -- Transform a into b, with facts of type f
235 -- Deals with optimsation fuel and unique supply too
236
237 (>>>) :: Trans a b -> Trans b c -> Trans a c
238 -- Compose two dataflow transfers in sequence
239 (dft1 >>> dft2) f = do { f1 <- dft1 f; f2 <- dft2 f1; return f2 }
240
241 liftTrans :: (a->b) -> Trans a b
242 liftTrans f x = return (f x)
243
244 idTrans :: Trans a a
245 idTrans x = return x
246
247 fixpointTrans :: forall n f.
248 Trans (TxFactBase n f) (TxFactBase n f)
249 -> Trans (OutFactC f) (TxFactBase n f)
250 fixpointTrans tx_fb_trans out_facts
251 = do { fuel <- getFuel
252 ; loop fuel (mkFactBase out_facts) }
253 where
254 loop :: Fuel -> Trans (FactBase f) (TxFactBase n f)
255 loop fuel fbase
256 = do { tx_fb <- tx_fb_trans (TxFB { tfb_fbase = fbase
257 , tfb_cha = NoChange
258 , tfb_blks = []
259 , tfb_bids = emptyBlockSet })
260 ; case tfb_cha tx_fb of
261 NoChange -> return tx_fb
262 SomeChange -> do { setFuel fuel; loop fuel (tfb_fbase tx_fb) } }
263
264 -----------------------------------------------------------------------------
265 -- Transfer functions
266 -----------------------------------------------------------------------------
267
268 -- Keys to the castle: a generic transfer function for each shape
269 -- Here's the idea: we start with single-n transfer functions,
270 -- move to basic-block transfer functions (we have exactly four shapes),
271 -- then finally to graph transfer functions (which requires iteration).
272
273 newtype GFT thing n f = GFT (GFTR thing n f)
274 type GFTR thing n f = forall e x. thing e x
275 -> InFact e f
276 -> FuelMonad (GraphWithFacts n e x f, OutFact x f)
277
278 type GFT_Node n f = GFT n n f
279 type GFT_Block n f = GFT (Block n) n f
280 type GFT_Graph n f = GFT (Graph n) n f
281 -----------------------------------------------------------------------------
282
283 gftNodeTransfer :: forall n f . ForwardTransfers n f -> GFT_Node n f
284 -- Lifts ForwardTransfers to GFT_Node; simple transfer only
285 gftNodeTransfer base_trans = GFT node_trans
286 where
287 node_trans :: GFTR n n f
288 node_trans node f = return (GUnit (BUnit node), base_trans node f)
289
290 gftNodeRewrite :: forall n f.
291 ForwardTransfers n f
292 -> ForwardRewrites n f
293 -> GFT_Graph n f
294 -> GFT_Node n f
295 -- Lifts (ForwardTransfers,ForwardRewrites) to GFT_Node;
296 -- this time we do rewriting as well.
297 -- The GFT_Graph parameters specifies what to do with the rewritten graph
298 gftNodeRewrite transfers rewrites (GFT graph_trans)
299 = GFT node_rewrite
300 where
301 node_trans :: GFTR n n f
302 node_trans node f = return (GUnit (BUnit node), transfers node f)
303
304 node_rewrite :: GFTR n n f
305 node_rewrite node f
306 = case rewrites node f of
307 Nothing -> node_trans node f
308 Just g -> do { out <- fuelExhausted
309 ; if out then
310 node_trans node f
311 else do { decrementFuel
312 ; g' <- graphOfAGraph g
313 ; graph_trans g' f } }
314
315 gftBlock :: forall n f. GFT_Node n f -> GFT_Block n f
316 -- Lift from nodes to blocks
317 gftBlock (GFT node_trans) = GFT block_trans
318 where
319 block_trans :: GFTR (Block n) n f
320 block_trans (BUnit node) f = node_trans node f
321 block_trans (BCat hd mids) f = do { (g1,f1) <- block_trans hd f
322 ; (g2,f2) <- block_trans mids f1
323 ; return (g1 `gwfCat` g2, f2) }
324
325
326 gftGraph :: forall n f. Edges n => DataflowLattice f -> GFT_Block n f -> GFT_Graph n f
327 -- Lift from blocks to graphs
328 gftGraph lattice gft_block@(GFT block_trans) = GFT graph_trans
329 where
330 graph_trans :: GFTR (Graph n) n f
331 graph_trans GNil f = return (GNil, f)
332 graph_trans (GUnit blk) f = block_trans blk f
333 graph_trans (GMany entry blocks exit) f
334 = do { (entry', f1) <- block_trans entry f
335 ; tx_fb <- ft_blocks blocks f1
336 ; (exit', f3) <- ft_exit exit tx_fb
337 ; return (mkGMany entry' (tfb_blks tx_fb) exit', f3) }
338
339 -- It's a bit disgusting that the TxFactBase has to be
340 -- preserved as far as the Exit block, becaues the TxFactBase
341 -- is really concerned with the fixpoint calculation
342 -- But I can't see any other tidy way to compute the
343 -- LastOutFacts in the NoTail case
344 ft_exit :: Exit (Block n C x) x
345 -> Trans (TxFactBase n f) (Exit (Graph n C x) x, OutFact x f)
346 ft_exit (Tail blk) f = do { (blk', f1) <- block_trans blk (factBaseInFacts lattice f)
347 ; return (Tail blk', f1) }
348 ft_exit NoTail f = return (NoTail, factBaseOutFacts f)
349
350 ft_block_once :: Block n C C -> Trans (TxFactBase n f) (TxFactBase n f)
351 ft_block_once blk = updateFacts lattice gft_block blk
352
353 ft_blocks_once :: Blocks n -> Trans (TxFactBase n f) (TxFactBase n f)
354 ft_blocks_once blks = foldr ((>>>) . ft_block_once) idTrans blks
355
356 ft_blocks :: [Block n C C] -> Trans (OutFactC f) (TxFactBase n f)
357 ft_blocks blocks = fixpointTrans (ft_blocks_once (forwardBlockList blocks))
358
359 ----------------------------------------------------------------
360 -- The pi├Ęce de resistance: cunning transfer functions
361 ----------------------------------------------------------------
362
363 pureAnalysis :: Edges n => DataflowLattice f -> ForwardTransfers n f -> GFT_Graph n f
364 pureAnalysis lattice = gftGraph lattice . gftBlock . gftNodeTransfer
365
366 analyseAndRewrite
367 :: forall n f. Edges n
368 => RewritingDepth
369 -> DataflowLattice f
370 -> ForwardTransfers n f
371 -> ForwardRewrites n f
372 -> GFT_Graph n f
373
374 data RewritingDepth = RewriteShallow | RewriteDeep
375 -- When a transformation proposes to rewrite a node,
376 -- you can either ask the system to
377 -- * "shallow": accept the new graph, analyse it without further rewriting
378 -- * "deep": recursively analyse-and-rewrite the new graph
379
380 analyseAndRewrite depth lattice transfers rewrites
381 = gft_graph_cunning
382 where
383 gft_graph_base, gft_graph_cunning, gft_graph_recurse :: GFT_Graph n f
384
385 gft_graph_base = gftGraph lattice (gftBlock gft_node_base)
386 gft_graph_cunning = gftGraph lattice (gftBlock gft_node_cunning)
387 gft_graph_recurse = case depth of
388 RewriteShallow -> gft_graph_base
389 RewriteDeep -> gft_graph_cunning
390
391 gft_node_base, gft_node_cunning :: GFT_Node n f
392 gft_node_base = gftNodeTransfer transfers
393 gft_node_cunning = gftNodeRewrite transfers rewrites gft_graph_recurse
394
395 -----------------------------------------------------------------------------
396 -- The fuel monad
397 -----------------------------------------------------------------------------
398
399 type Uniques = Int
400 type Fuel = Int
401
402 newtype FuelMonad a = FM { unFM :: Fuel -> Uniques -> (a, Fuel, Uniques) }
403
404 instance Monad FuelMonad where
405 return x = FM (\f u -> (x,f,u))
406 m >>= k = FM (\f u -> case unFM m f u of (r,f',u') -> unFM (k r) f' u')
407
408 fuelExhausted :: FuelMonad Bool
409 fuelExhausted = FM (\f u -> (f <= 0, f, u))
410
411 decrementFuel :: FuelMonad ()
412 decrementFuel = FM (\f u -> ((), f-1, u))
413
414 getFuel :: FuelMonad Fuel
415 getFuel = FM (\f u -> (f,f,u))
416
417 setFuel :: Fuel -> FuelMonad ()
418 setFuel f = FM (\_ u -> ((), f, u))
419
420 graphOfAGraph :: AGraph node e x -> FuelMonad (Graph node e x)
421 graphOfAGraph = error "urk" -- Stub
422
423 -----------------------------------------------------------------------------
424 -- BlockId, BlockEnv, BlockSet
425 -----------------------------------------------------------------------------
426
427 type BlockId = Int
428
429 mkBlockId :: Int -> BlockId
430 mkBlockId uniq = uniq
431
432 type FactBase a = M.IntMap a
433
434 mkFactBase :: [(BlockId, f)] -> FactBase f
435 mkFactBase prs = M.fromList prs
436
437 lookupFact :: DataflowLattice f -> FactBase f -> BlockId -> f
438 lookupFact lattice env blk_id
439 = case M.lookup blk_id env of
440 Just f -> f
441 Nothing -> fact_bot lattice
442
443 extendFactBase :: FactBase f -> BlockId -> f -> FactBase f
444 extendFactBase env blk_id f = M.insert blk_id f env
445
446 unionFactBase :: FactBase f -> FactBase f -> FactBase f
447 unionFactBase = M.union
448
449 factBaseList :: FactBase f -> [(BlockId, f)]
450 factBaseList env = M.toList env
451
452 type BlockSet = S.IntSet
453
454 emptyBlockSet :: BlockSet
455 emptyBlockSet = S.empty
456
457 extendBlockSet :: BlockSet -> BlockId -> BlockSet
458 extendBlockSet bids bid = S.insert bid bids
459
460 elemBlockSet :: BlockId -> BlockSet -> Bool
461 elemBlockSet bid bids = S.member bid bids
462
463 blockSetElems :: BlockSet -> [BlockId]
464 blockSetElems = S.toList
465
466 minusBlockSet :: BlockSet -> BlockSet -> BlockSet
467 minusBlockSet = S.difference
468
469 mkBlockSet :: [BlockId] -> BlockSet
470 mkBlockSet = S.fromList