refactoring 'fixpoint' and other code for display in paper
[packages/hoopl.git] / src / Compiler / Hoopl / Dataflow.hs
1 {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, EmptyDataDecls, PatternGuards, TypeFamilies, MultiParamTypeClasses #-}
2
3 module Compiler.Hoopl.Dataflow
4 ( DataflowLattice(..), JoinFun, OldFact(..), NewFact(..), Fact
5 , ChangeFlag(..), changeIf
6 , FwdPass(..), FwdTransfer, mkFTransfer, mkFTransfer3, getFTransfer3
7 , FwdRew(..), FwdRewrite, mkFRewrite, mkFRewrite3, getFRewrite3
8 , BwdPass(..), BwdTransfer, mkBTransfer, mkBTransfer3, getBTransfer3
9 , BwdRew(..), BwdRewrite, mkBRewrite, mkBRewrite3, getBRewrite3
10 , analyzeAndRewriteFwd, analyzeAndRewriteBwd
11 )
12 where
13
14 import Control.Monad
15 import Data.Maybe
16
17 import Compiler.Hoopl.Collections
18 import Compiler.Hoopl.Fuel
19 import Compiler.Hoopl.Graph
20 import qualified Compiler.Hoopl.GraphUtil as U
21 import Compiler.Hoopl.Label
22 import Compiler.Hoopl.Util
23
24 -----------------------------------------------------------------------------
25 -- DataflowLattice
26 -----------------------------------------------------------------------------
27
28 data DataflowLattice a = DataflowLattice
29 { fact_name :: String -- Documentation
30 , fact_bot :: a -- Lattice bottom element
31 , fact_join :: JoinFun a -- Lattice join plus change flag
32 -- (changes iff result > old fact)
33 }
34 -- ^ A transfer function might want to use the logging flag
35 -- to control debugging, as in for example, it updates just one element
36 -- in a big finite map. We don't want Hoopl to show the whole fact,
37 -- and only the transfer function knows exactly what changed.
38
39 type JoinFun a = Label -> OldFact a -> NewFact a -> (ChangeFlag, a)
40 -- the label argument is for debugging purposes only
41 newtype OldFact a = OldFact a
42 newtype NewFact a = NewFact a
43
44 data ChangeFlag = NoChange | SomeChange deriving (Eq, Ord)
45 changeIf :: Bool -> ChangeFlag
46 changeIf changed = if changed then SomeChange else NoChange
47
48 -----------------------------------------------------------------------------
49 -- Analyze and rewrite forward: the interface
50 -----------------------------------------------------------------------------
51
52 data FwdPass m n f
53 = FwdPass { fp_lattice :: DataflowLattice f
54 , fp_transfer :: FwdTransfer n f
55 , fp_rewrite :: FwdRewrite m n f }
56
57 newtype FwdTransfer n f
58 = FwdTransfer3 { getFTransfer3 ::
59 ( n C O -> f -> f
60 , n O O -> f -> f
61 , n O C -> f -> FactBase f
62 ) }
63
64 newtype FwdRewrite m n f
65 = FwdRewrite3 { getFRewrite3 ::
66 ( n C O -> f -> m (Maybe (FwdRew m n f C O))
67 , n O O -> f -> m (Maybe (FwdRew m n f O O))
68 , n O C -> f -> m (Maybe (FwdRew m n f O C))
69 ) }
70 data FwdRew m n f e x = FwdRew (Graph n e x) (FwdRewrite m n f)
71
72 -- result of a rewrite is a new graph and a (possibly) new rewrite function
73
74 mkFTransfer3 :: (n C O -> f -> f)
75 -> (n O O -> f -> f)
76 -> (n O C -> f -> FactBase f)
77 -> FwdTransfer n f
78 mkFTransfer3 f m l = FwdTransfer3 (f, m, l)
79
80 mkFTransfer :: (forall e x . n e x -> f -> Fact x f) -> FwdTransfer n f
81 mkFTransfer f = FwdTransfer3 (f, f, f)
82
83 mkFRewrite3 :: (n C O -> f -> m (Maybe (FwdRew m n f C O)))
84 -> (n O O -> f -> m (Maybe (FwdRew m n f O O)))
85 -> (n O C -> f -> m (Maybe (FwdRew m n f O C)))
86 -> FwdRewrite m n f
87 mkFRewrite3 f m l = FwdRewrite3 (f, m, l)
88
89 mkFRewrite :: (forall e x . n e x -> f -> m (Maybe (FwdRew m n f e x)))
90 -> FwdRewrite m n f
91 mkFRewrite f = FwdRewrite3 (f, f, f)
92
93
94 type family Fact x f :: *
95 type instance Fact C f = FactBase f
96 type instance Fact O f = f
97
98 -- | if the graph being analyzed is open at the entry, there must
99 -- be no other entry point, or all goes horribly wrong...
100 analyzeAndRewriteFwd
101 :: forall m n f e x entries. (FuelMonad m, NonLocal n, LabelsPtr entries)
102 => FwdPass m n f
103 -> MaybeC e entries
104 -> Graph n e x -> Fact e f
105 -> m (Graph n e x, FactBase f, MaybeO x f)
106 analyzeAndRewriteFwd pass entries g f =
107 do (rg, fout) <- arfGraph pass (fmap targetLabels entries) g f
108 let (g', fb) = normalizeGraph rg
109 return (g', fb, distinguishedExitFact g' fout)
110
111 distinguishedExitFact :: forall n e x f . Graph n e x -> Fact x f -> MaybeO x f
112 distinguishedExitFact g f = maybe g
113 where maybe :: Graph n e x -> MaybeO x f
114 maybe GNil = JustO f
115 maybe (GUnit {}) = JustO f
116 maybe (GMany _ _ x) = case x of NothingO -> NothingO
117 JustO _ -> JustO f
118
119 ----------------------------------------------------------------
120 -- Forward Implementation
121 ----------------------------------------------------------------
122
123 type Entries e = MaybeC e [Label]
124
125 arfGraph :: forall m n f e x .
126 (NonLocal n, FuelMonad m) => FwdPass m n f ->
127 Entries e -> Graph n e x -> Fact e f -> m (DG f n e x, Fact x f)
128 arfGraph pass entries = graph
129 where
130 {- nested type synonyms would be so lovely here
131 type ARF thing = forall e x . thing e x -> f -> m (DG f n e x, Fact x f)
132 type ARFX thing = forall e x . thing e x -> Fact e f -> m (DG f n e x, Fact x f)
133 -}
134 graph :: Graph n e x -> Fact e f -> m (DG f n e x, Fact x f)
135 block :: forall e x . Block n e x -> f -> m (DG f n e x, Fact x f)
136 node :: forall e x . (ShapeLifter e x)
137 => n e x -> f -> m (DG f n e x, Fact x f)
138 body :: [Label] -> Body n -> Fact C f -> m (DG f n C C, Fact C f)
139 -- Outgoing factbase is restricted to Labels *not* in
140 -- in the Body; the facts for Labels *in*
141 -- the Body are in the 'DG f n C C'
142 cat :: forall m e a x info info' info''. Monad m =>
143 (info -> m (DG f n e a, info'))
144 -> (info' -> m (DG f n a x, info''))
145 -> (info -> m (DG f n e x, info''))
146
147 graph GNil = \f -> return (dgnil, f)
148 graph (GUnit blk) = block blk
149 graph (GMany e bdy x) = (e `ebcat` bdy) `cat` exit x
150 where
151 ebcat :: MaybeO e (Block n O C) -> Body n -> Fact e f -> m (DG f n e C, Fact C f)
152 exit :: MaybeO x (Block n C O) -> Fact C f -> m (DG f n C x, Fact x f)
153 exit (JustO blk) = arfx block blk
154 exit NothingO = \fb -> return (dgnilC, fb)
155 ebcat entry bdy = c entries entry
156 where c :: MaybeC e [Label] -> MaybeO e (Block n O C)
157 -> Fact e f -> m (DG f n e C, Fact C f)
158 c NothingC (JustO entry) = block entry `cat` body (successors entry) bdy
159 c (JustC entries) NothingO = body entries bdy
160 c _ _ = error "bogus GADT pattern match failure"
161
162 -- Lift from nodes to blocks
163 block (BFirst n) = node n
164 block (BMiddle n) = node n
165 block (BLast n) = node n
166 block (BCat b1 b2) = block b1 `cat` block b2
167 block (BHead h n) = block h `cat` node n
168 block (BTail n t) = node n `cat` block t
169 block (BClosed h t)= block h `cat` block t
170
171 node n f
172 = do { fwdres <- frewrite pass n f >>= withFuel
173 ; case fwdres of
174 Nothing -> return (toDg f (toBlock n),
175 ftransfer pass n f)
176 Just (FwdRew g rw) ->
177 let pass' = pass { fp_rewrite = rw }
178 in arfGraph pass' (maybeEntry n) g (fwdEntryFact n f) }
179
180 -- | Compose fact transformers and concatenate the resulting
181 -- rewritten graphs.
182 {-# INLINE cat #-}
183 cat ft1 ft2 f = do { (g1,f1) <- ft1 f
184 ; (g2,f2) <- ft2 f1
185 ; return (g1 `dgCat` g2, f2) }
186
187 arfx :: forall thing x .
188 NonLocal thing
189 => (thing C x -> f -> m (DG f n C x, Fact x f))
190 -> (thing C x -> Fact C f -> m (DG f n C x, Fact x f))
191 arfx arf thing fb =
192 arf thing $ fromJust $ lookupFact (entryLabel thing) $ joinInFacts lattice fb
193 where lattice = fp_lattice pass
194 -- joinInFacts adds debugging information
195
196
197 -- Outgoing factbase is restricted to Labels *not* in
198 -- in the Body; the facts for Labels *in*
199 -- the Body are in the 'DG f n C C'
200 body entries blockmap init_fbase
201 = fixpoint True lattice do_block blocks init_fbase
202 where
203 blocks = forwardBlockList entries blockmap
204 lattice = fp_lattice pass
205 do_block b fb = do (g, fb) <- block b entryFact
206 return (g, mapToList fb)
207 where entryFact = getFact lattice (entryLabel b) fb
208
209
210 -- Join all the incoming facts with bottom.
211 -- We know the results _shouldn't change_, but the transfer
212 -- functions might, for example, generate some debugging traces.
213 joinInFacts :: DataflowLattice f -> FactBase f -> FactBase f
214 joinInFacts (DataflowLattice {fact_bot = bot, fact_join = fj}) fb =
215 mkFactBase $ map botJoin $ mapToList fb
216 where botJoin (l, f) = (l, snd $ fj l (OldFact bot) (NewFact f))
217
218 forwardBlockList :: (NonLocal n, LabelsPtr entry)
219 => entry -> Body n -> [Block n C C]
220 -- This produces a list of blocks in order suitable for forward analysis,
221 -- along with the list of Labels it may depend on for facts.
222 forwardBlockList entries (Body blks) = postorder_dfs_from blks entries
223
224 -----------------------------------------------------------------------------
225 -- Backward analysis and rewriting: the interface
226 -----------------------------------------------------------------------------
227
228 data BwdPass m n f
229 = BwdPass { bp_lattice :: DataflowLattice f
230 , bp_transfer :: BwdTransfer n f
231 , bp_rewrite :: BwdRewrite m n f }
232
233 newtype BwdTransfer n f
234 = BwdTransfer3 { getBTransfer3 ::
235 ( n C O -> f -> f
236 , n O O -> f -> f
237 , n O C -> FactBase f -> f
238 ) }
239 newtype BwdRewrite m n f
240 = BwdRewrite3 { getBRewrite3 ::
241 ( n C O -> f -> m (Maybe (BwdRew m n f C O))
242 , n O O -> f -> m (Maybe (BwdRew m n f O O))
243 , n O C -> FactBase f -> m (Maybe (BwdRew m n f O C))
244 ) }
245 data BwdRew m n f e x = BwdRew (Graph n e x) (BwdRewrite m n f)
246
247
248 mkBTransfer3 :: (n C O -> f -> f) -> (n O O -> f -> f) ->
249 (n O C -> FactBase f -> f) -> BwdTransfer n f
250 mkBTransfer3 f m l = BwdTransfer3 (f, m, l)
251
252 mkBTransfer :: (forall e x . n e x -> Fact x f -> f) -> BwdTransfer n f
253 mkBTransfer f = BwdTransfer3 (f, f, f)
254
255 mkBRewrite3 :: (n C O -> f -> m (Maybe (BwdRew m n f C O)))
256 -> (n O O -> f -> m (Maybe (BwdRew m n f O O)))
257 -> (n O C -> FactBase f -> m (Maybe (BwdRew m n f O C)))
258 -> BwdRewrite m n f
259 mkBRewrite3 f m l = BwdRewrite3 (f, m, l)
260
261 mkBRewrite :: (forall e x . n e x -> Fact x f -> m (Maybe (BwdRew m n f e x)))
262 -> BwdRewrite m n f
263 mkBRewrite f = BwdRewrite3 (f, f, f)
264
265
266 -----------------------------------------------------------------------------
267 -- Backward implementation
268 -----------------------------------------------------------------------------
269
270 arbGraph :: forall m n f e x .
271 (NonLocal n, FuelMonad m) => BwdPass m n f ->
272 Entries e -> Graph n e x -> Fact x f -> m (DG f n e x, Fact e f)
273 arbGraph pass entries = graph
274 where
275 {- nested type synonyms would be so lovely here
276 type ARB thing = forall e x . thing e x -> Fact x f -> m (DG f n e x, f)
277 type ARBX thing = forall e x . thing e x -> Fact x f -> m (DG f n e x, Fact e f)
278 -}
279 graph :: Graph n e x -> Fact x f -> m (DG f n e x, Fact e f)
280 block :: forall e x . Block n e x -> Fact x f -> m (DG f n e x, f)
281 node :: forall e x . (ShapeLifter e x)
282 => n e x -> Fact x f -> m (DG f n e x, f)
283 body :: [Label] -> Body n -> Fact C f -> m (DG f n C C, Fact C f)
284 cat :: forall e a x info info' info''.
285 (info' -> m (DG f n e a, info''))
286 -> (info -> m (DG f n a x, info'))
287 -> (info -> m (DG f n e x, info''))
288
289 graph GNil = \f -> return (dgnil, f)
290 graph (GUnit blk) = block blk
291 graph (GMany e bdy x) = (e `ebcat` bdy) `cat` exit x
292 where
293 ebcat :: MaybeO e (Block n O C) -> Body n -> Fact C f -> m (DG f n e C, Fact e f)
294 exit :: MaybeO x (Block n C O) -> Fact x f -> m (DG f n C x, Fact C f)
295 exit (JustO blk) = arbx block blk
296 exit NothingO = \fb -> return (dgnilC, fb)
297 ebcat entry bdy = c entries entry
298 where c :: MaybeC e [Label] -> MaybeO e (Block n O C)
299 -> Fact C f -> m (DG f n e C, Fact e f)
300 c NothingC (JustO entry) = block entry `cat` body (successors entry) bdy
301 c (JustC entries) NothingO = body entries bdy
302 c _ _ = error "bogus GADT pattern match failure"
303
304 -- Lift from nodes to blocks
305 block (BFirst n) = node n
306 block (BMiddle n) = node n
307 block (BLast n) = node n
308 block (BCat b1 b2) = block b1 `cat` block b2
309 block (BHead h n) = block h `cat` node n
310 block (BTail n t) = node n `cat` block t
311 block (BClosed h t)= block h `cat` block t
312
313 node n f
314 = do { bwdres <- brewrite pass n f >>= withFuel
315 ; case bwdres of
316 Nothing -> return (toDg entry_f (toBlock n), entry_f)
317 where entry_f = btransfer pass n f
318 Just (BwdRew g rw) ->
319 do { let pass' = pass { bp_rewrite = rw }
320 ; (g, f) <- arbGraph pass' (maybeEntry n) g f
321 ; return (g, bwdEntryFact (bp_lattice pass) n f)} }
322
323 -- | Compose fact transformers and concatenate the resulting
324 -- rewritten graphs.
325 {-# INLINE cat #-}
326 cat ft1 ft2 f = do { (g2,f2) <- ft2 f
327 ; (g1,f1) <- ft1 f2
328 ; return (g1 `dgCat` g2, f1) }
329
330 arbx :: forall thing x .
331 NonLocal thing
332 => (thing C x -> Fact x f -> m (DG f n C x, f))
333 -> (thing C x -> Fact x f -> m (DG f n C x, Fact C f))
334
335 arbx arb thing f = do { (rg, f) <- arb thing f
336 ; let fb = joinInFacts (bp_lattice pass) $
337 mkFactBase [(entryLabel thing, f)]
338 ; return (rg, fb) }
339 -- joinInFacts adds debugging information
340
341 -- Outgoing factbase is restricted to Labels *not* in
342 -- in the Body; the facts for Labels *in*
343 -- the Body are in the 'DG f n C C'
344 body entries blockmap init_fbase
345 = fixpoint False (bp_lattice pass) do_block blocks init_fbase
346 where
347 blocks = backwardBlockList entries blockmap
348 do_block b f = do (g, f) <- block b f
349 return (g, [(entryLabel b, f)])
350
351
352 backwardBlockList :: (LabelsPtr entries, NonLocal n) => entries -> Body n -> [Block n C C]
353 -- This produces a list of blocks in order suitable for backward analysis,
354 -- along with the list of Labels it may depend on for facts.
355 backwardBlockList entries body = reverse $ forwardBlockList entries body
356
357 {-
358
359 The forward and backward cases are not dual. In the forward case, the
360 entry points are known, and one simply traverses the body blocks from
361 those points. In the backward case, something is known about the exit
362 points, but this information is essentially useless, because we don't
363 actually have a dual graph (that is, one with edges reversed) to
364 compute with. (Even if we did have a dual graph, it would not avail
365 us---a backward analysis must include reachable blocks that don't
366 reach the exit, as in a procedure that loops forever and has side
367 effects.)
368
369 -}
370
371
372 -- | if the graph being analyzed is open at the exit, I don't
373 -- quite understand the implications of possible other exits
374 analyzeAndRewriteBwd
375 :: (FuelMonad m, NonLocal n, LabelsPtr entries)
376 => BwdPass m n f
377 -> MaybeC e entries -> Graph n e x -> Fact x f
378 -> m (Graph n e x, FactBase f, MaybeO e f)
379 analyzeAndRewriteBwd pass entries g f =
380 do (rg, fout) <- arbGraph pass (fmap targetLabels entries) g f
381 let (g', fb) = normalizeGraph rg
382 return (g', fb, distinguishedEntryFact g' fout)
383
384 distinguishedEntryFact :: forall n e x f . Graph n e x -> Fact e f -> MaybeO e f
385 distinguishedEntryFact g f = maybe g
386 where maybe :: Graph n e x -> MaybeO e f
387 maybe GNil = JustO f
388 maybe (GUnit {}) = JustO f
389 maybe (GMany e _ _) = case e of NothingO -> NothingO
390 JustO _ -> JustO f
391
392 -----------------------------------------------------------------------------
393 -- fixpoint: finding fixed points
394 -----------------------------------------------------------------------------
395
396 data TxFactBase n f
397 = TxFB { tfb_fbase :: FactBase f
398 , tfb_rg :: DG f n C C -- Transformed blocks
399 , tfb_cha :: ChangeFlag
400 , tfb_lbls :: LabelSet }
401 -- Note [TxFactBase change flag]
402 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
403 -- Set the tfb_cha flag iff
404 -- (a) the fact in tfb_fbase for or a block L changes
405 -- (b) L is in tfb_lbls.
406 -- The tfb_lbls are all Labels of the *original*
407 -- (not transformed) blocks
408
409 updateFact :: DataflowLattice f -> LabelSet -> (Label, f)
410 -> (ChangeFlag, FactBase f)
411 -> (ChangeFlag, FactBase f)
412 -- See Note [TxFactBase change flag]
413 updateFact lat lbls (lbl, new_fact) (cha, fbase)
414 | NoChange <- cha2 = (cha, fbase)
415 | lbl `setMember` lbls = (SomeChange, new_fbase)
416 | otherwise = (cha, new_fbase)
417 where
418 (cha2, res_fact) -- Note [Unreachable blocks]
419 = case lookupFact lbl fbase of
420 Nothing -> (SomeChange, new_fact_debug) -- Note [Unreachable blocks]
421 Just old_fact -> join old_fact
422 where join old_fact =
423 fact_join lat lbl
424 (OldFact old_fact) (NewFact new_fact)
425 (_, new_fact_debug) = join (fact_bot lat)
426 new_fbase = mapInsert lbl res_fact fbase
427
428 fixpoint :: forall m block n f. (FuelMonad m, NonLocal n, NonLocal (block n))
429 => Bool -- Going forwards?
430 -> DataflowLattice f
431 -> (block n C C -> FactBase f -> m (DG f n C C, [(Label, f)]))
432 -> [block n C C]
433 -> FactBase f
434 -> m (DG f n C C, FactBase f)
435 fixpoint is_fwd lat do_block blocks init_fbase
436 = do { fuel <- getFuel
437 ; tx_fb <- loop fuel init_fbase
438 ; return (tfb_rg tx_fb,
439 map (fst . fst) tagged_blocks `mapDeleteList` tfb_fbase tx_fb ) }
440 -- The successors of the Graph are the the Labels for which
441 -- we have facts, that are *not* in the blocks of the graph
442 where
443 tagged_blocks = map tag blocks
444 where tag b = ((entryLabel b, b), if is_fwd then [entryLabel b] else successors b)
445
446 tx_blocks :: [((Label, block n C C), [Label])] -- I do not understand this type
447 -> TxFactBase n f -> m (TxFactBase n f)
448 tx_blocks [] tx_fb = return tx_fb
449 tx_blocks (((lbl,blk), deps):bs) tx_fb = tx_block lbl blk deps tx_fb >>= tx_blocks bs
450 -- "deps" == Labels the block may _depend_ upon for facts
451
452 tx_block :: Label -> block n C C -> [Label]
453 -> TxFactBase n f -> m (TxFactBase n f)
454 tx_block lbl blk deps tx_fb@(TxFB { tfb_fbase = fbase, tfb_lbls = lbls
455 , tfb_rg = blks, tfb_cha = cha })
456 | is_fwd && not (lbl `mapMember` fbase)
457 = return tx_fb {tfb_lbls = lbls `setUnion` setFromList deps} -- Note [Unreachable blocks]
458 | otherwise
459 = do { (rg, out_facts) <- do_block blk fbase
460 ; let (cha',fbase')
461 = foldr (updateFact lat lbls) (cha,fbase) out_facts
462 lbls' = lbls `setUnion` setFromList deps
463 ; return (TxFB { tfb_lbls = lbls'
464 , tfb_rg = rg `dgCat` blks
465 , tfb_fbase = fbase', tfb_cha = cha' }) }
466
467 loop :: Fuel -> FactBase f -> m (TxFactBase n f)
468 loop fuel fbase
469 = do { let init_tx_fb = TxFB { tfb_fbase = fbase
470 , tfb_cha = NoChange
471 , tfb_rg = dgnilC
472 , tfb_lbls = setEmpty }
473 ; tx_fb <- tx_blocks tagged_blocks init_tx_fb
474 ; case tfb_cha tx_fb of
475 NoChange -> return tx_fb
476 SomeChange -> do { setFuel fuel
477 ; loop fuel (tfb_fbase tx_fb) } }
478
479 {- Note [Unreachable blocks]
480 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
481 A block that is not in the domain of tfb_fbase is "currently unreachable".
482 A currently-unreachable block is not even analyzed. Reason: consider
483 constant prop and this graph, with entry point L1:
484 L1: x:=3; goto L4
485 L2: x:=4; goto L4
486 L4: if x>3 goto L2 else goto L5
487 Here L2 is actually unreachable, but if we process it with bottom input fact,
488 we'll propagate (x=4) to L4, and nuke the otherwise-good rewriting of L4.
489
490 * If a currently-unreachable block is not analyzed, then its rewritten
491 graph will not be accumulated in tfb_rg. And that is good:
492 unreachable blocks simply do not appear in the output.
493
494 * Note that clients must be careful to provide a fact (even if bottom)
495 for each entry point. Otherwise useful blocks may be garbage collected.
496
497 * Note that updateFact must set the change-flag if a label goes from
498 not-in-fbase to in-fbase, even if its fact is bottom. In effect the
499 real fact lattice is
500 UNR
501 bottom
502 the points above bottom
503
504 * Even if the fact is going from UNR to bottom, we still call the
505 client's fact_join function because it might give the client
506 some useful debugging information.
507
508 * All of this only applies for *forward* fixpoints. For the backward
509 case we must treat every block as reachable; it might finish with a
510 'return', and therefore have no successors, for example.
511 -}
512
513 -----------------------------------------------------------------------------
514 -- DG: an internal data type for 'decorated graphs'
515 -- TOTALLY internal to Hoopl; each block is decorated with a fact
516 -----------------------------------------------------------------------------
517
518 type DG f n e x = Graph' (DBlock f) n e x
519 data DBlock f n e x = DBlock f (Block n e x) -- ^ block decorated with fact
520 instance NonLocal n => NonLocal (DBlock f n) where
521 entryLabel (DBlock _ b) = entryLabel b
522 successors (DBlock _ b) = successors b
523
524 --- constructors
525
526 dgnil :: DG f n O O
527 dgnilC :: DG f n C C
528 toDg :: NonLocal n => f -> Block n e x -> DG f n e x
529 dgCat :: NonLocal n => DG f n e a -> DG f n a x -> DG f n e x
530
531 ---- observers
532
533 type GraphWithFacts n f e x = (Graph n e x, FactBase f)
534 -- A Graph together with the facts for that graph
535 -- The domains of the two maps should be identical
536
537 normalizeGraph :: forall n f e x .
538 NonLocal n => DG f n e x -> GraphWithFacts n f e x
539
540 normalizeGraph g = (graphMapBlocks dropFact g, facts g)
541 where dropFact (DBlock _ b) = b
542 facts :: DG f n e x -> FactBase f
543 facts GNil = noFacts
544 facts (GUnit _) = noFacts
545 facts (GMany _ body exit) = bodyFacts body `mapUnion` exitFacts exit
546 exitFacts :: MaybeO x (DBlock f n C O) -> FactBase f
547 exitFacts NothingO = noFacts
548 exitFacts (JustO (DBlock f b)) = mkFactBase [(entryLabel b, f)]
549 bodyFacts :: Body' (DBlock f) n -> FactBase f
550 bodyFacts (Body body) = mapFold f noFacts body
551 where f (DBlock f b) fb = mapInsert (entryLabel b) f fb
552
553 --- implementation of the constructors (boring)
554
555 dgnil = GNil
556 dgnilC = GMany NothingO emptyBody NothingO
557
558 toDg f b@(BFirst {}) = gUnitCO (DBlock f b)
559 toDg f b@(BMiddle {}) = gUnitOO (DBlock f b)
560 toDg f b@(BLast {}) = gUnitOC (DBlock f b)
561 toDg f b@(BCat {}) = gUnitOO (DBlock f b)
562 toDg f b@(BHead {}) = gUnitCO (DBlock f b)
563 toDg f b@(BTail {}) = gUnitOC (DBlock f b)
564 toDg f b@(BClosed {}) = gUnitCC (DBlock f b)
565
566 dgCat = U.splice fzCat
567 where fzCat (DBlock f b1) (DBlock _ b2) = DBlock f (b1 `U.cat` b2)
568
569 ----------------------------------------------------------------
570 -- Utilities
571 ----------------------------------------------------------------
572
573 -- Lifting based on shape:
574 -- - from nodes to blocks
575 -- - from facts to fact-like things
576 -- Lowering back:
577 -- - from fact-like things to facts
578 -- Note that the latter two functions depend only on the entry shape.
579 class ShapeLifter e x where
580 toBlock :: n e x -> Block n e x
581 fwdEntryFact :: NonLocal n => n e x -> f -> Fact e f
582 bwdEntryFact :: NonLocal n => DataflowLattice f -> n e x -> Fact e f -> f
583 ftransfer :: FwdPass m n f -> n e x -> f -> Fact x f
584 btransfer :: BwdPass m n f -> n e x -> Fact x f -> f
585 frewrite :: FwdPass m n f -> n e x -> f -> m (Maybe (FwdRew m n f e x))
586 brewrite :: BwdPass m n f -> n e x -> Fact x f -> m (Maybe (BwdRew m n f e x))
587 maybeEntry :: NonLocal n => n e x -> Entries e
588
589 instance ShapeLifter C O where
590 toBlock = BFirst
591 fwdEntryFact n f = mkFactBase [(entryLabel n, f)]
592 bwdEntryFact lat n fb = getFact lat (entryLabel n) fb
593 ftransfer (FwdPass {fp_transfer = FwdTransfer3 (ft, _, _)}) n f = ft n f
594 btransfer (BwdPass {bp_transfer = BwdTransfer3 (bt, _, _)}) n f = bt n f
595 frewrite (FwdPass {fp_rewrite = FwdRewrite3 (fr, _, _)}) n f = fr n f
596 brewrite (BwdPass {bp_rewrite = BwdRewrite3 (br, _, _)}) n f = br n f
597 maybeEntry n = JustC [entryLabel n]
598
599 instance ShapeLifter O O where
600 toBlock = BMiddle
601 fwdEntryFact _ f = f
602 bwdEntryFact _ _ f = f
603 ftransfer (FwdPass {fp_transfer = FwdTransfer3 (_, ft, _)}) n f = ft n f
604 btransfer (BwdPass {bp_transfer = BwdTransfer3 (_, bt, _)}) n f = bt n f
605 frewrite (FwdPass {fp_rewrite = FwdRewrite3 (_, fr, _)}) n f = fr n f
606 brewrite (BwdPass {bp_rewrite = BwdRewrite3 (_, br, _)}) n f = br n f
607 maybeEntry _ = NothingC
608
609 instance ShapeLifter O C where
610 toBlock = BLast
611 fwdEntryFact _ f = f
612 bwdEntryFact _ _ f = f
613 ftransfer (FwdPass {fp_transfer = FwdTransfer3 (_, _, ft)}) n f = ft n f
614 btransfer (BwdPass {bp_transfer = BwdTransfer3 (_, _, bt)}) n f = bt n f
615 frewrite (FwdPass {fp_rewrite = FwdRewrite3 (_, _, fr)}) n f = fr n f
616 brewrite (BwdPass {bp_rewrite = BwdRewrite3 (_, _, br)}) n f = br n f
617 maybeEntry _ = NothingC
618
619 -- Fact lookup: the fact `orelse` bottom
620 getFact :: DataflowLattice f -> Label -> FactBase f -> f
621 getFact lat l fb = case lookupFact l fb of Just f -> f
622 Nothing -> fact_bot lat