Used at the type level to indicate an open structure with a unique, unnamed control-flow edge flowing in or out. Fallthrough and concatenation are permitted at an open point.

Used at the type level to indicate a closed structure which supports control transfer only through the use of named labels---no fallthrough is permitted. The number of control-flow edges is unconstrained.

A sequence of nodes. May be any of four shapes (OO, OC, CO, CC). Open at the entry means single entry, mutatis mutandis for exit. A closedclosed block is a basic/ block and can't be extended further. Clients should avoid manipulating blocks and should stick to either nodes or graphs.

A (possibly empty) collection of closed/closed blocks

A control-flow graph, which may take any of four shapes (OO, OC, CO, CC). A graph open at the entry has a single, distinguished, anonymous entry point; if a graph is closed at the entry, its entry point(s) are supplied by a context.

Maybe type indexed by open/closed

Maybe type indexed by closed/open

Dynamic shape value

Either type indexed by closed/open using type families

Gives access to the anchor points for nonlocal edges as well as the edges themselves

Maps over all nodes in a graph.

The type of abstract graphs. Offers extra smart constructors that may consume fresh labels during construction.

Take an abstract AGraph and make a concrete (if monadic) Graph.

Take a graph and make it abstract.

Concatenate two graphs; control flows from left to right.

Splice together two graphs at a closed point; nothing is known about control flow.

Conveniently concatenate a sequence of open/open graphs using <*>.

Extend an existing AGraph with extra basic blocks out of line. No control flow is implied. Simon PJ should give example use case.

An empty graph that is open at entry and exit. It is the left and right identity of <*>.

An empty graph that is closed at entry and exit. It is the left and right identity of |*><*|.

Create a graph from a first node

Create a graph from a middle node

Conveniently concatenate a sequence of middle nodes to form an open/open graph.

Create a graph from a last node

Create a graph that branches to a label

Create a graph that defines a label

Create a graph containing only an entry sequence

Create a graph containing only an exit sequence

For some graph-construction operations and some optimizations, Hoopl must be able to create control-flow edges using a given node type n.

A utility function so that a transfer function for a first node can be given just a fact; we handle the lookup. This function is planned to be made obsolete by changes in the dataflow interface.

This utility function handles a common case in which a transfer function produces a single fact out of a last node, which is then distributed over the outgoing edges.

This utility function handles a common case in which a transfer function for a last node takes the incoming fact unchanged and simply distributes that fact over the outgoing edges.

This utility function handles a common case in which a backward transfer function takes the incoming fact unchanged and tags it with the node's label.

List of (unlabelled) facts from the successors of a last node

Join a list of facts.

It's common to represent dataflow facts as a map from variables to some fact about the locations. For these maps, the join operation on the map can be expressed in terms of the join on each element of the codomain:

Fold a function over every node in a graph. The fold function must be polymorphic in the shape of the nodes.

Fold a function over every node in a block, forward or backward. The fold function must be polymorphic in the shape of the nodes.

A fold function that relies on the IndexedCO type function. Note that the type parameter e is available to the functions that are applied to the middle and last nodes.

Convert a block to a list of nodes. The entry and exit node is or is not present depending on the shape of the block.

The blockToNodeList function cannot be currently expressed using foldBlockNodesB, because it returns IndexedCO e a b, which means two different types depending on the shape of the block entry. But blockToNodeList returns one of four possible types, depending on the shape of the block entry *and* exit.

Convert a list of nodes to a block. The entry and exit node must or must not be present depending on the shape of the block.

Forward dataflow analysis and rewriting for the special case of a Body. A set of entry points must be supplied; blocks not reachable from the set are thrown away.

Backward dataflow analysis and rewriting for the special case of a Body. A set of entry points must be supplied; blocks not reachable from the set are thrown away.

Forward dataflow analysis and rewriting for the special case of a graph open at the entry. This special case relieves the client from having to specify a type signature for NothingO, which beginners might find confusing and experts might find annoying.

Backward dataflow analysis and rewriting for the special case of a graph open at the entry. This special case relieves the client from having to specify a type signature for NothingO, which beginners might find confusing and experts might find annoying.

A value that can be used for the entry point of a graph open at the entry.

Obeys the following law: for all m do { s <- checkpoint; m; restart s } == return ()

A transfer function might want to use the logging flag to control debugging, as in for example, it updates just one element in a big finite map. We don't want Hoopl to show the whole fact, and only the transfer function knows exactly what changed.

mkFactBase creates a FactBase from a list of (Label, fact) pairs. If the same label appears more than once, the relevant facts are joined.

Functions passed to mkFRewrite should not be aware of the fuel supply. The result returned by mkFRewrite respects fuel.

Functions passed to mkFRewrite3 should not be aware of the fuel supply. The result returned by mkFRewrite3 respects fuel.

Functions passed to mkBRewrite should not be aware of the fuel supply. The result returned by mkBRewrite respects fuel.

Functions passed to mkBRewrite3 should not be aware of the fuel supply. The result returned by mkBRewrite3 respects fuel.

if the graph being analyzed is open at the entry, there must be no other entry point, or all goes horribly wrong...

if the graph being analyzed is open at the exit, I don't quite understand the implications of possible other exits

Adds top, bottom, or both to help form a lattice

The type parameters t and b are used to say whether top and bottom elements have been added. The analogy with Block is nearly exact:

• A Block is closed at the entry if and only if it has a first node; a Pointed is closed at the top if and only if it has a top element.
• A Block is closed at the exit if and only if it has a last node; a Pointed is closed at the bottom if and only if it has a bottom element.

We thus have four possible types, of which three are interesting:

Pointed C C a

Type a extended with both top and bottom elements.

Pointed C O a

Type a extended with a top element only. (Presumably a comes equipped with a bottom element of its own.)

Pointed O C a

Type a extended with a bottom element only.

Pointed O O a

Isomorphic to a, and therefore not interesting.

The advantage of all this GADT-ishness is that the constructors Bot, Top, and PElem can all be used polymorphically.

A 'Pointed t b' type is an instance of Functor and Show.

Given a join function and a name, creates a semi lattice by adding a bottom element, and possibly a top element also. A specialized version of addPoints'.

A more general case for creating a new lattice

Given a join function and a name, creates a semi lattice by adding a top element but no bottom element. Caller must supply the bottom element.

A more general case for creating a new lattice

Type a with a top element adjoined

Type a with a bottom element adjoined

Type a with top and bottom elements adjoined

Find out how much fuel remains after a computation. Can be subtracted from initial fuel to get total consumption.

Function graphMapBlocks enables a change of representation of blocks, nodes, or both. It lifts a polymorphic block transform into a polymorphic graph transform. When the block representation stabilizes, a similar function should be provided for blocks.

Function blockMapNodes enables a change of nodes in a block.

Traversal: postorder_dfs returns a list of blocks reachable from the entry of enterable graph. The entry and exit are *not* included. The list has the following property:

Say a back reference exists if one of a block's control-flow successors precedes it in the output list

Then there are as few back references as possible

The output is suitable for use in a forward dataflow problem. For a backward problem, simply reverse the list. (postorder_dfs is sufficiently tricky to implement that one doesn't want to try and maintain both forward and backward versions.)

Debugging combinators: Each combinator takes a dataflow pass and produces a dataflow pass that can output debugging messages. You provide the function, we call it with the applicable message.

The most common use case is probably to:

1. import Debug.Trace
2. pass trace as the 1st argument to the debug combinator
3. pass 'const true' as the 2nd argument to the debug combinator

There are two kinds of debugging messages for a join, depending on whether the join is higher in the lattice than the old fact: 1. If the join is higher, we show: + JoinL: f1 join f2 = f' where: + indicates a change L is the label where the join takes place f1 is the old fact at the label f2 is the new fact we are joining to f1 f' is the result of the join 2. _ JoinL: f2 <= f1 where: _ indicates no change L is the label where the join takes place f1 is the old fact at the label (which remains unchanged) f2 is the new fact we joined with f1