add an FAQ file
[packages/hoopl.git] / prototypes / Hoopl4.hs
1 {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, EmptyDataDecls, PatternGuards, TypeFamilies #-}
2
3 module Hoopl4 where
4
5 import qualified Data.IntMap as M
6 import qualified Data.IntSet as S
7
8 -----------------------------------------------------------------------------
9 -- Graphs
10 -----------------------------------------------------------------------------
11
12 data ZOpen
13 data ZClosed
14
15 type O = ZOpen
16 type C = ZClosed
17
18 -- Blocks are always non-empty
19 data Block n e x where
20 BUnit :: n e x -> Block n e x
21 BCat :: Block n e O -> Block n O x -> Block n e x
22
23 type BlockGraph n = BlockMap (Block n C C)
24
25 data Graph n e x where
26 GNil :: Graph n O O
27 GUnit :: Block n e O -> Graph n e O
28 GMany :: Block n e C -> BlockGraph n
29 -> Tail n x -> Graph n e x
30
31 -- If a graph has a Tail, then that tail is the only
32 -- exit from the graph, even if the Tail is closed
33 -- See the definition of successors!
34
35 data Tail n x where
36 NoTail :: Tail n C
37 Tail :: BlockId -> Block n C O -> Tail n O
38
39 class LiftNode x where
40 liftNode :: n e x -> Graph n e x
41 instance LiftNode ZClosed where
42 liftNode n = GMany (BUnit n) noBlocks NoTail
43 instance LiftNode ZOpen where
44 liftNode n = GUnit (BUnit n)
45
46 {- Edges is not currently used
47 class Edges thing where
48 successors :: thing e C -> [BlockId]
49
50 instance Edges n => Edges (Block n) where
51 successors (BUnit n) = successors n
52 successors (BCat _ b) = successors b
53
54 instance Edges n => Edges (Graph n) where
55 successors (GMany b bs NoTail)
56 = blockSetElems (all_succs `minusBlockSet` all_blk_ids)
57 where
58 (bids, blks) = unzip (blocksToList bs)
59 all_succs = mkBlockSet (successors b ++ [bid | b <- blks, bid <- successors b])
60 all_blk_ids = mkBlockSet bids
61 -}
62
63 ecGraph :: Graph n e C -> (Block n e C, BlockGraph n)
64 ecGraph (GMany b bs NoTail) = (b, bs)
65
66 cxGraph :: BlockId -> Graph n C O -> (BlockGraph n, Tail n O)
67 cxGraph bid (GUnit b) = (noBlocks, Tail bid b)
68 cxGraph bid (GMany be bs tail) = (addBlock bid be bs, tail)
69
70 flattenG :: BlockId -> Graph n C C -> BlockGraph n
71 flattenG bid (GMany e bs NoTail) = addBlock bid e bs
72
73 gCat :: Graph n e O -> Graph n O x -> Graph n e x
74 gCat GNil g2 = g2
75 gCat g1 GNil = g1
76
77 gCat (GUnit b1) (GUnit b2)
78 = GUnit (b1 `BCat` b2)
79
80 gCat (GUnit b) (GMany e bs x)
81 = GMany (b `BCat` e) bs x
82
83 gCat (GMany e bs (Tail bid x)) (GUnit b2)
84 = GMany e bs (Tail bid (x `BCat` b2))
85
86 gCat (GMany e1 bs1 (Tail bid x1)) (GMany e2 bs2 x2)
87 = GMany e1 (addBlock bid (x1 `BCat` e2) bs1 `unionBlocks` bs2) x2
88
89 forwardBlockList, backwardBlockList :: BlockGraph n -> [(BlockId,Block n C C)]
90 -- This produces a list of blocks in order suitable for forward analysis.
91 -- ToDo: Do a topological sort to improve convergence rate of fixpoint
92 -- This will require a (HavingSuccessors l) class constraint
93 forwardBlockList blks = blocksToList blks
94 backwardBlockList blks = blocksToList blks
95
96 -----------------------------------------------------------------------------
97 -- DataflowLattice
98 -----------------------------------------------------------------------------
99
100 data DataflowLattice a = DataflowLattice {
101 fact_name :: String, -- Documentation
102 fact_bot :: a, -- Lattice bottom element
103 fact_extend :: a -> a -> (ChangeFlag,a), -- Lattice join plus change flag
104 fact_do_logging :: Bool -- log changes
105 }
106
107 data ChangeFlag = NoChange | SomeChange
108
109 -----------------------------------------------------------------------------
110 -- The main Hoopl API
111 -----------------------------------------------------------------------------
112
113 type ForwardTransfers n f
114 = forall e x. f -> n e x -> TailFactF x f
115
116 type ForwardRewrites n f
117 = forall e x. f -> n e x -> Maybe (AGraph n e x)
118
119 type family TailFactF x f :: *
120 type instance TailFactF C f = [(BlockId, f)]
121 type instance TailFactF O f = f
122
123 data AGraph n e x = AGraph -- Stub for now
124
125
126 -----------------------------------------------------------------------------
127 -- TxFactBase: a FactBase with ChangeFlag information
128 -----------------------------------------------------------------------------
129
130 -- The TxFactBase is an accumulating parameter, threaded through all
131 -- the analysis/transformation of each block in the g_blocks of a grpah.
132 -- It carries a ChangeFlag with it, and a set of BlockIds
133 -- to monitor. Updates to other BlockIds don't affect the ChangeFlag
134 data TxFactBase n fact
135 = TxFB { tfb_fbase :: FactBase fact
136
137 , tfb_cha :: ChangeFlag
138 , tfb_bids :: BlockSet -- Update change flag iff these blocks change
139 -- These are BlockIds of the *original*
140 -- (not transformed) blocks
141
142 , tfb_blks :: BlockGraph n -- Transformed blocks
143 }
144
145 factBaseInFacts :: DataflowLattice f -> TxFactBase n f -> BlockId -> f
146 factBaseInFacts lattice (TxFB { tfb_fbase = fbase }) bid
147 = lookupFact lattice fbase bid
148
149 factBaseOutFacts :: TxFactBase n f -> [(BlockId,f)]
150 factBaseOutFacts (TxFB { tfb_fbase = fbase, tfb_bids = bids })
151 = [ (bid, f) | (bid, f) <- factBaseList fbase
152 , not (bid `elemBlockSet` bids) ]
153 -- The successors of the Graph are the the BlockIds for which
154 -- we hvae facts, that are *not* in the blocks of the graph
155
156 updateFact :: DataflowLattice f -> (BlockId, f)
157 -> TxFactBase n f -> TxFactBase n f
158 -- Update a TxFactBase, setting the change flag iff
159 -- a) the new fact adds information...
160 -- b) for a block in the BlockSet in the TxFactBase
161 updateFact lat (bid, new_fact) tx_fb@(TxFB { tfb_fbase = fbase, tfb_bids = bids})
162 | NoChange <- cha2 = tx_fb
163 | bid `elemBlockSet` bids = tx_fb { tfb_fbase = new_fbase, tfb_cha = SomeChange }
164 | otherwise = tx_fb { tfb_fbase = new_fbase }
165 where
166 old_fact = lookupFact lat fbase bid
167 (cha2, res_fact) = fact_extend lat old_fact new_fact
168 new_fbase = extendFactBase fbase bid res_fact
169
170 updateFacts :: DataflowLattice f
171 -> BlockId
172 -> (FactBase f -> FuelMonad ([(BlockId,f)], Graph n C C))
173 -> TxFactBase n f -> FuelMonad (TxFactBase n f)
174 -- Works regardless of direction
175 updateFacts lat bid fb_trans
176 tx_fb@(TxFB { tfb_fbase = fbase, tfb_bids = bids, tfb_blks = blks })
177 = do { (out_facts, graph) <- fb_trans fbase
178 ; let tx_fb' = tx_fb { tfb_bids = extendBlockSet bids bid
179 , tfb_blks = flattenG bid graph `unionBlocks` blks }
180 ; return (foldr (updateFact lat) tx_fb' out_facts) }
181
182 -----------------------------------------------------------------------------
183 -- The Trans arrow
184 -----------------------------------------------------------------------------
185
186 fixpoint :: forall n f.
187 (TxFactBase n f -> FuelMonad (TxFactBase n f))
188 -> (FactBase f -> FuelMonad (TxFactBase n f))
189 fixpoint tx_fb_trans init_fbase
190 = do { fuel <- getFuel
191 ; loop fuel init_fbase }
192 where
193 loop :: Fuel -> FactBase f -> FuelMonad (TxFactBase n f)
194 loop fuel fbase
195 = do { tx_fb <- tx_fb_trans (TxFB { tfb_fbase = fbase
196 , tfb_cha = NoChange
197 , tfb_blks = noBlocks
198 , tfb_bids = emptyBlockSet })
199 ; case tfb_cha tx_fb of
200 NoChange -> return tx_fb
201 SomeChange -> do { setFuel fuel; loop fuel (tfb_fbase tx_fb) } }
202
203 -----------------------------------------------------------------------------
204 -- Transfer functions
205 -----------------------------------------------------------------------------
206
207 -- Keys to the castle: a generic transfer function for each shape
208 -- Here's the idea: we start with single-n transfer functions,
209 -- move to basic-block transfer functions (we have exactly four shapes),
210 -- then finally to graph transfer functions (which requires iteration).
211
212 type ARF thing n f = forall e x. LiftNode x
213 => f -> thing e x
214 -> FuelMonad (TailFactF x f, Graph n e x)
215
216 type ARF_Node n f = ARF n n f
217 type ARF_Block n f = ARF (Block n) n f
218 type ARF_Graph n f = ARF (Graph n) n f
219 -----------------------------------------------------------------------------
220
221 arfNodeTransfer :: forall n f. ForwardTransfers n f -> ARF_Node n f
222 -- Lifts ForwardTransfers to ARF_Node; simple transfer only
223 arfNodeTransfer transfer_fn f node
224 = return (transfer_fn f node, liftNode node)
225
226 arfNodeRewrite :: forall n f.
227 ForwardTransfers n f
228 -> ForwardRewrites n f
229 -> ARF_Graph n f
230 -> ARF_Node n f
231 -- Lifts (ForwardTransfers,ForwardRewrites) to ARF_Node;
232 -- this time we do rewriting as well.
233 -- The ARF_Graph parameters specifies what to do with the rewritten graph
234 arfNodeRewrite transfer_fn rewrite_fn graph_trans f node
235 = do { mb_g <- withFuel (rewrite_fn f node)
236 ; case mb_g of
237 Nothing -> arfNodeTransfer transfer_fn f node
238 Just ag -> do { g <- graphOfAGraph ag
239 ; graph_trans f g } }
240
241 arfBlock :: forall n f. ARF_Node n f -> ARF_Block n f
242 -- Lift from nodes to blocks
243 arfBlock arf_node f (BUnit node) = arf_node f node
244 arfBlock arf_node f (BCat hd mids) = do { (f1,g1) <- arfBlock arf_node f hd
245 ; (f2,g2) <- arfBlock arf_node f1 mids
246 ; return (f2, g1 `gCat` g2) }
247
248 arfGraph :: forall n f. DataflowLattice f -> ARF_Block n f -> ARF_Graph n f
249 -- Lift from blocks to graphs
250 arfGraph lattice arf_block f GNil = return (f, GNil)
251 arfGraph lattice arf_block f (GUnit blk) = arf_block f blk
252 arfGraph lattice arf_block f (GMany entry blocks exit)
253 = do { (f1, entry_g) <- arf_block f entry
254 ; tx_fb <- ft_blocks blocks (mkFactBase f1)
255 ; (f3, bs2, exit') <- ft_exit tx_fb exit
256 ; let (entry', bs1) = ecGraph entry_g
257 final_bs = bs1 `unionBlocks` tfb_blks tx_fb `unionBlocks` bs2
258 ; return (f3, GMany entry' final_bs exit') }
259 where
260 -- It's a bit disgusting that the TxFactBase has to be
261 -- preserved as far as the Tail block, becaues the TxFactBase
262 -- is really concerned with the fixpoint calculation
263 -- But I can't see any other tidy way to compute the
264 -- LastOutFacts in the NoTail case
265 ft_exit :: TxFactBase n f -> Tail n x
266 -> FuelMonad (TailFactF x f, BlockGraph n, Tail n x)
267 ft_exit f (Tail bid blk)
268 = do { (f1, g) <- arf_block (factBaseInFacts lattice f bid) blk
269 ; let (bs, exit) = cxGraph bid g
270 ; return (f1, bs, exit) }
271 ft_exit f NoTail
272 = return (factBaseOutFacts f, noBlocks, NoTail)
273
274 ft_block_once :: (BlockId, Block n C C) -> TxFactBase n f
275 -> FuelMonad (TxFactBase n f)
276 ft_block_once (bid, b) = updateFacts lattice bid $ \fbase ->
277 arf_block (lookupFact lattice fbase bid) b
278
279 ft_blocks_once :: [(BlockId, Block n C C)]
280 -> TxFactBase n f -> FuelMonad (TxFactBase n f)
281 ft_blocks_once [] tx_fb = return tx_fb
282 ft_blocks_once (b:bs) tx_fb = do { tx_fb1 <- ft_block_once b tx_fb
283 ; ft_blocks_once bs tx_fb1 }
284
285 ft_blocks :: BlockGraph n -> FactBase f -> FuelMonad (TxFactBase n f)
286 ft_blocks blocks = fixpoint (ft_blocks_once (forwardBlockList blocks))
287
288 ----------------------------------------------------------------
289 -- The pi├Ęce de resistance: cunning transfer functions
290 ----------------------------------------------------------------
291
292 pureAnalysis :: DataflowLattice f -> ForwardTransfers n f -> ARF_Graph n f
293 pureAnalysis lattice f = arfGraph lattice (arfBlock (arfNodeTransfer f))
294
295 analyseAndRewriteFwd
296 :: forall n f.
297 DataflowLattice f
298 -> ForwardTransfers n f
299 -> ForwardRewrites n f
300 -> RewritingDepth
301 -> ARF_Graph n f
302
303 data RewritingDepth = RewriteShallow | RewriteDeep
304 -- When a transformation proposes to rewrite a node,
305 -- you can either ask the system to
306 -- * "shallow": accept the new graph, analyse it without further rewriting
307 -- * "deep": recursively analyse-and-rewrite the new graph
308
309 analyseAndRewriteFwd lattice transfers rewrites depth
310 = anal_rewrite
311 where
312 anal_rewrite, anal_only, arf_rec :: ARF_Graph n f
313
314 anal_rewrite = arfGraph lattice $ arfBlock $
315 arfNodeRewrite transfers rewrites arf_rec
316
317 anal_only = arfGraph lattice $ arfBlock $
318 arfNodeTransfer transfers
319
320 arf_rec = case depth of
321 RewriteShallow -> anal_only
322 RewriteDeep -> anal_rewrite
323
324 -----------------------------------------------------------------------------
325 -- Backward rewriting
326 -----------------------------------------------------------------------------
327
328 type BackwardTransfers n f
329 = forall e x. TailFactB x f -> n e x -> f
330 type BackwardRewrites n f
331 = forall e x. TailFactB x f -> n e x -> Maybe (AGraph n e x)
332
333 type ARB thing n f = forall e x. LiftNode x
334 => TailFactB x f -> thing e x
335 -> FuelMonad (f, Graph n e x)
336
337 type family TailFactB x f :: *
338 type instance TailFactB C f = FactBase f
339 type instance TailFactB O f = f
340
341 type ARB_Node n f = ARB n n f
342 type ARB_Block n f = ARB (Block n) n f
343 type ARB_Graph n f = ARB (Graph n) n f
344
345 arbNodeTransfer :: forall n f . BackwardTransfers n f -> ARB_Node n f
346 -- Lifts BackwardTransfers to ARB_Node; simple transfer only
347 arbNodeTransfer transfer_fn f node
348 = return (transfer_fn f node, liftNode node)
349
350 arbNodeRewrite :: forall n f.
351 BackwardTransfers n f
352 -> BackwardRewrites n f
353 -> ARB_Graph n f
354 -> ARB_Node n f
355 -- Lifts (BackwardTransfers,BackwardRewrites) to ARB_Node;
356 -- this time we do rewriting as well.
357 -- The ARB_Graph parameters specifies what to do with the rewritten graph
358 arbNodeRewrite transfer_fn rewrite_fn graph_trans f node
359 = do { mb_g <- withFuel (rewrite_fn f node)
360 ; case mb_g of
361 Nothing -> arbNodeTransfer transfer_fn f node
362 Just ag -> do { g <- graphOfAGraph ag
363 ; graph_trans f g } }
364
365 arbBlock :: forall n f. ARB_Node n f -> ARB_Block n f
366 -- Lift from nodes to blocks
367 arbBlock arb_node f (BUnit node) = arb_node f node
368 arbBlock arb_node f (BCat b1 b2) = do { (f2,g2) <- arbBlock arb_node f b2
369 ; (f1,g1) <- arbBlock arb_node f2 b1
370 ; return (f1, g1 `gCat` g2) }
371
372 arbGraph :: forall n f. DataflowLattice f -> ARB_Block n f -> ARB_Graph n f
373 arbGraph lattice arb_block f GNil = return (f, GNil)
374 arbGraph lattice arb_block f (GUnit blk) = arb_block f blk
375 arbGraph lattice arb_block f (GMany entry blocks exit)
376 = do { (f1, bs2, exit') <- bt_exit f exit
377 ; tx_fb <- bt_blocks blocks f1
378 ; (f3, entry_g) <- arb_block (tfb_fbase tx_fb) entry
379 ; let (entry', bs1) = ecGraph entry_g
380 final_bs = bs1 `unionBlocks` tfb_blks tx_fb `unionBlocks` bs2
381 ; return (f3, GMany entry' final_bs exit') }
382 where
383 -- It's a bit disgusting that the TxFactBase has to be
384 -- preserved as far as the Tail block, becaues the TxFactBase
385 -- is really concerned with the fixpoint calculation
386 -- But I can't see any other tidy way to compute the
387 -- LastOutFacts in the NoTail case
388 bt_exit :: TailFactB x f -> Tail n x
389 -> FuelMonad (FactBase f, BlockGraph n, Tail n x)
390 bt_exit f (Tail bid blk)
391 = do { (f1, g) <- arb_block f blk
392 ; let (bs, exit) = cxGraph bid g
393 ; return (mkFactBase [(bid,f1)], bs, exit) }
394 bt_exit f NoTail
395 = return (f, noBlocks, NoTail)
396
397 bt_block_once :: (BlockId, Block n C C) -> TxFactBase n f
398 -> FuelMonad (TxFactBase n f)
399 bt_block_once (bid, b) = updateFacts lattice bid $ \fbase ->
400 do { (f, g) <- arb_block fbase b
401 ; return ([(bid,f)], g) }
402
403 bt_blocks_once :: [(BlockId,Block n C C)]
404 -> TxFactBase n f -> FuelMonad (TxFactBase n f)
405 bt_blocks_once [] tx_fb = return tx_fb
406 bt_blocks_once (b:bs) tx_fb = do { tx_fb' <- bt_block_once b tx_fb
407 ; bt_blocks_once bs tx_fb' }
408
409 bt_blocks :: BlockGraph n -> FactBase f -> FuelMonad (TxFactBase n f)
410 bt_blocks blocks = fixpoint (bt_blocks_once (backwardBlockList blocks))
411
412 analyseAndRewriteBwd
413 :: forall n f.
414 DataflowLattice f
415 -> BackwardTransfers n f
416 -> BackwardRewrites n f
417 -> RewritingDepth
418 -> ARB_Graph n f
419
420 analyseAndRewriteBwd lattice transfers rewrites depth
421 = anal_rewrite
422 where
423 anal_rewrite, anal_only, arb_rec :: ARB_Graph n f
424
425 anal_rewrite = arbGraph lattice $ arbBlock $
426 arbNodeRewrite transfers rewrites arb_rec
427
428 anal_only = arbGraph lattice $ arbBlock $
429 arbNodeTransfer transfers
430
431 arb_rec = case depth of
432 RewriteShallow -> anal_only
433 RewriteDeep -> anal_rewrite
434
435
436 -----------------------------------------------------------------------------
437 -- The fuel monad
438 -----------------------------------------------------------------------------
439
440 type Uniques = Int
441 type Fuel = Int
442
443 newtype FuelMonad a = FM { unFM :: Fuel -> Uniques -> (a, Fuel, Uniques) }
444
445 instance Monad FuelMonad where
446 return x = FM (\f u -> (x,f,u))
447 m >>= k = FM (\f u -> case unFM m f u of (r,f',u') -> unFM (k r) f' u')
448
449 withFuel :: Maybe a -> FuelMonad (Maybe a)
450 withFuel Nothing = return Nothing
451 withFuel (Just r) = FM (\f u -> if f==0 then (Nothing, f, u)
452 else (Just r, f-1, u))
453
454 getFuel :: FuelMonad Fuel
455 getFuel = FM (\f u -> (f,f,u))
456
457 setFuel :: Fuel -> FuelMonad ()
458 setFuel f = FM (\_ u -> ((), f, u))
459
460 graphOfAGraph :: AGraph node e x -> FuelMonad (Graph node e x)
461 graphOfAGraph = error "urk" -- Stub
462
463 -----------------------------------------------------------------------------
464 -- BlockId, FactBase, BlockSet
465 -----------------------------------------------------------------------------
466
467 type BlockId = Int
468
469 mkBlockId :: Int -> BlockId
470 mkBlockId uniq = uniq
471
472 ----------------------
473 type BlockMap a = M.IntMap a
474
475 noBlocks :: BlockGraph n
476 noBlocks = M.empty
477
478 addBlock :: BlockId -> Block n C C -> BlockGraph n -> BlockGraph n
479 addBlock = M.insert
480
481 unionBlocks :: BlockGraph n -> BlockGraph n -> BlockGraph n
482 unionBlocks = M.union
483
484 blocksToList :: BlockGraph n -> [(BlockId,Block n C C)]
485 blocksToList = M.toList
486
487 ----------------------
488 type FactBase a = M.IntMap a
489
490 mkFactBase :: [(BlockId, f)] -> FactBase f
491 mkFactBase prs = M.fromList prs
492
493 lookupFact :: DataflowLattice f -> FactBase f -> BlockId -> f
494 lookupFact lattice env blk_id
495 = case M.lookup blk_id env of
496 Just f -> f
497 Nothing -> fact_bot lattice
498
499 extendFactBase :: FactBase f -> BlockId -> f -> FactBase f
500 extendFactBase env blk_id f = M.insert blk_id f env
501
502 unionFactBase :: FactBase f -> FactBase f -> FactBase f
503 unionFactBase = M.union
504
505 factBaseList :: FactBase f -> [(BlockId, f)]
506 factBaseList env = M.toList env
507
508
509 ----------------------
510 type BlockSet = S.IntSet
511
512 emptyBlockSet :: BlockSet
513 emptyBlockSet = S.empty
514
515 extendBlockSet :: BlockSet -> BlockId -> BlockSet
516 extendBlockSet bids bid = S.insert bid bids
517
518 elemBlockSet :: BlockId -> BlockSet -> Bool
519 elemBlockSet bid bids = S.member bid bids
520
521 blockSetElems :: BlockSet -> [BlockId]
522 blockSetElems = S.toList
523
524 minusBlockSet :: BlockSet -> BlockSet -> BlockSet
525 minusBlockSet = S.difference
526
527 mkBlockSet :: [BlockId] -> BlockSet
528 mkBlockSet = S.fromList