module type WeiMaoZouChenInput = sig
.. end
type
graph
type
node
type
tenv
val init : graph ->
tenv * node
build a new env from a graph,
and also return the entry point of the graph which has to be unique.
val fold_succ : (tenv ->
node -> tenv) ->
tenv ->
node -> tenv
apply the function on the node successors
val eq_nodes : node -> node -> bool
val set_pos : tenv ->
node -> int -> tenv
store the position for the node and also the fact that the node has
been seen
val reset_pos : tenv ->
node -> tenv
reset the position (set the position to 0), but should keep the
information that the node has been seen already.
val get_pos : tenv -> node -> int
get the previously stored position of the node or 0 if nothing has been
stored
val get_pos_if_traversed : tenv ->
node -> int option
get the previously stored position of the node if any, or None
if set_pos
hasn't been called already for this node.
: tenv ->
node ->
node -> tenv
set_iloop_header env b h
store h as the innermost loop header for b.
Beware that this function can be called several times for the same b
with different values of h during the computation. Only the last one
will give the correct information.
: tenv ->
node -> node option
get the node innermost loop header if any
: tenv ->
node -> tenv
store the node as a loop header.
val add_irreducible : tenv ->
node -> tenv
store the node as an irreducible loop header.
val add_reentry_edge : tenv ->
node ->
node -> tenv
store the edge between the two nodes (n1, n2) as a reentry edge.
n2 is the reentry point which means that it is in a loop,
but it is not the loop header, and n1 is not in the loop.