ControlFlow.CFG.Simple

(source)

This module contains a representation of a control-flow graph that aims to
enforce the correctness of jumps between vertices of graphs, i.e., blocks
of code.
The graph model permits graphs to be incomplete and facilitates easy
composition of such graphs when they are compatible.

*This model is a simplified version of the model in `ControlFlow.CFG`,
which also allows for incomplete vertices.*

A graph is incomplete when vertices need to be added to it in order for it
to be a valid function body.
For example a graph that contains only the following pseudo-code block:
```
L0: x = call func ()
    jump L1
```
is incomplete because the code block ends with a jump to the block `L1` but
`L1` is not in the graph.

In this model, graphs can be incomplete at the beginning or at the end
(or both). In other words, graphs can be completed only by prepending or
appending vertices to them.

Reexports

import public ControlFlow.Edge

Definitions

Neighbors : Type -> Type

  Neighbors of a vertex

Visibility: public export

Vertex : Type -> Type

  A constructor of verteices of a directed graph
  @ a    the type of vertex identifiers
  @ v    the identifier              of the vertex
  @ ins  the inputs  (in-neighbors)  of the vertex
  @ outs the outputs (out-neighbors) of the vertex

Visibility: public export

Edges : Type -> Type

  Input or output edges of an incomplete graph
  @ a the type of vertex identifiers

Visibility: public export

data CFG : Vertex a -> Edges a -> Edges a -> Type

  A potentially incomplete control flow graph.
  @ ins    edges from "to be defined" vertices to vertices in the graph
  @ outs   edges from vertices in the graph to "to be defined" vertices
  @ vertex constructor of vertex types.

Totality: total
Visibility: public export
Constructors:

Empty : CFG vertex edges edges

  An empty graph

SingleVertex : vertex v vins vouts -> CFG vertex (vins ~~> v) (v ~>> vouts)

  A singleton graph - a graph containing a single vertex

Cycle : CFG vertex (ins ++ loopOuts) (loopIns ++ outs) -> CFG vertex loopIns loopOuts -> CFG vertex ins outs

  A graph that represents a while loop
  @ node the graph in which the while condition is computed
  @ loop the body of the loop

Series : CFG vertex ins edges -> CFG vertex edges outs -> CFG vertex ins outs

  A sequential connection of two graphs
  The output vertices of one (`pre`) are being connected to the input
  vertices of the other (`post`)
  @ pre  the predecessor of `post`
  @ post the successor   of `pre`

Parallel : CFG vertex ins outs -> CFG vertex ins' outs' -> CFG vertex (ins ++ ins') (outs ++ outs')

  A parallel connection of graphs
  Two graphs are combined into one without any connections beetween them
  The result has the inputs and outputs of both
  @ left  the left sub-graph
  @ right the right sub-graph

IFlip : CFG vertex (ins ++ ins') outs -> CFG vertex (ins' ++ ins) outs

  Used to flip the inputs of a graph to make it connectable with another

OFlip : CFG vertex ins (outs ++ outs') -> CFG vertex ins (outs' ++ outs)

  Used to flip the outputs of a graph to make it connectable with another

(|-|) : CFG vertex ins outs -> CFG vertex ins' outs' -> CFG vertex (ins ++ ins') (outs ++ outs')

  Alias for `Parallel`

Visibility: public export
Fixity Declarations:
infixr operator, level 4
infixr operator, level 4

(*->) : CFG vertex ins edges -> CFG vertex edges outs -> CFG vertex ins outs

  Alias for `Series`

Visibility: public export
Fixity Declarations:
infixr operator, level 5
infixr operator, level 5

prepend : vertex v vins vouts -> CFG vertex (v ~>> vouts) gouts -> CFG vertex (vins ~~> v) gouts

Visibility: public export

append : CFG vertex gins (vins ~~> v) -> vertex v vins vouts -> CFG vertex gins (v ~>> vouts)

Visibility: public export

lbranch : CFG vertex ins (ls ++ rs) -> CFG vertex ls ls' -> CFG vertex ins (ls' ++ rs)

  A partial sequential connection of two graphs
  The left outputs of the predecessor are connected with all inputs of
  the successor
  @ node   the           predecessor of `branch`
  @ branch the (partial) successor   of `node`
  @ ls     the left  outputs of `node` / the inputs of `branch`
  @ rs     the right outputs of `node`

Visibility: public export

rbranch : CFG vertex ins (ls ++ rs) -> CFG vertex rs rs' -> CFG vertex ins (ls ++ rs')

  A partial sequential connection of two graphs
  The right outputs of the predecessor are connected with all inputs of
  the successor
  @ node   the           predecessor of `branch`
  @ branch the (partial) successor   of `node`
  @ ls     the left  outputs of `node`
  @ rs     the right outputs of `node` / the inputs of `branch`

Visibility: public export

lmerge : CFG vertex ls ls' -> CFG vertex (ls' ++ rs) outs -> CFG vertex (ls ++ rs) outs

  A partial sequential connection of two graphs
  All outputs of the predecessor are connected with the left inputs of
  the successor
  @ branch the           predecessor of `node`
  @ node   the (partial) successor   of `branch`
  @ ls'    the left  inputs of `node` / the outputs of `branch`
  @ rs     the right inputs of `node`

Visibility: public export

rmerge : CFG vertex rs rs' -> CFG vertex (ls ++ rs') outs -> CFG vertex (ls ++ rs) outs

  A partial sequential connection of two graphs
  All outputs of the predecessor are connected with the right inputs of
  the successor
  @ branch the           predecessor of `node`
  @ node   the (partial) successor   of `branch`
  @ ls     the left  inputs of `node`
  @ rs'    the right inputs of `node` / the outputs of `branch`

Visibility: public export

initGraph : vertex v ins outs -> CFG vertex (ins ~~> v) (v ~>> outs)

Visibility: export

vmap : (vertex v vins vouts -> vertex' v vins vouts) -> CFG vertex ins outs -> CFG vertex' ins outs

  Apply a function to all vertices in a grpaph

Visibility: export