
   0 | ||| This module contains a representation of a control-flow graph that aims to
   1 | ||| enforce the correctness of jumps between vertices of graphs, i.e., blocks
   2 | ||| of code.
   3 | ||| The graph model permits graphs to be incomplete and facilitates easy
   4 | ||| composition of such graphs when they are compatible.
   5 | |||
   6 | ||| *This model is a simplified version of the model in `ControlFlow.CFG`,
   7 | ||| which also allows for incomplete vertices.*
   8 | |||
   9 | ||| A graph is incomplete when vertices need to be added to it in order for it
  10 | ||| to be a valid function body.
  11 | ||| For example a graph that contains only the following pseudo-code block:
  12 | ||| ```
  13 | ||| L0: x = call func ()
  14 | |||     jump L1
  15 | ||| ```
  16 | ||| is incomplete because the code block ends with a jump to the block `L1` but
  17 | ||| `L1` is not in the graph.
  18 | |||
  19 | ||| In this model, graphs can be incomplete at the beginning or at the end
  20 | ||| (or both). In other words, graphs can be completed only by prepending or
  21 | ||| appending vertices to them.
  22 | 
  23 | module ControlFlow.CFG.Simple
  24 | 
  25 | import public ControlFlow.Edge
  26 | 
  27 | ||| Neighbors of a vertex
  28 | public export
  29 | Neighbors : Type -> Type
  30 | Neighbors a = List a
  31 | 
  32 | ||| A constructor of verteices of a directed graph
  33 | ||| @ a    the type of vertex identifiers
  34 | ||| @ v    the identifier              of the vertex
  35 | ||| @ ins  the inputs  (in-neighbors)  of the vertex
  36 | ||| @ outs the outputs (out-neighbors) of the vertex
  37 | public export
  38 | Vertex : Type -> Type
  39 | Vertex a = (v : a) -> (ins : Neighbors a) -> (outs : Neighbors a) -> Type
  40 | 
  41 | ||| Input or output edges of an incomplete graph
  42 | ||| @ a the type of vertex identifiers
  43 | public export
  44 | Edges : Type -> Type
  45 | Edges a = List (Edge a)
  46 | 
  47 | ||| A potentially incomplete control flow graph.
  48 | ||| @ ins    edges from "to be defined" vertices to vertices in the graph
  49 | ||| @ outs   edges from vertices in the graph to "to be defined" vertices
  50 | ||| @ vertex constructor of vertex types.
  51 | public export
  52 | data CFG : (vertex : Vertex a) -> (ins : Edges a) -> (outs : Edges a) -> Type where
  53 | 
  54 |   ||| An empty graph
  55 |   Empty : CFG vertex edges edges
  56 | 
  57 |   ||| A singleton graph - a graph containing a single vertex
  58 |   SingleVertex
  59 |      : {0 vertex : Vertex a}
  60 |     -> {vins, vouts : Neighbors a}
  61 |     -> vertex v vins vouts
  62 |     -> CFG vertex (vins ~~> v) (v ~>> vouts)
  63 | 
  64 |   ||| A graph that represents a while loop
  65 |   ||| @ node the graph in which the while condition is computed
  66 |   ||| @ loop the body of the loop
  67 |   Cycle
  68 |      : {ins, outs, loopIns, loopOuts : Edges a}
  69 |     -> (node : CFG vertex (ins ++ loopOuts) (loopIns ++ outs))
  70 |     -> (loop : CFG vertex loopIns loopOuts)
  71 |     -> CFG vertex ins outs
  72 | 
  73 |   ||| A sequential connection of two graphs
  74 |   ||| The output vertices of one (`pre`) are being connected to the input
  75 |   ||| vertices of the other (`post`)
  76 |   ||| @ pre  the predecessor of `post`
  77 |   ||| @ post the successor   of `pre`
  78 |   Series
  79 |      : (pre  : CFG vertex ins edges)
  80 |     -> (post : CFG vertex edges outs)
  81 |     -> CFG vertex ins outs
  82 | 
  83 |   ||| A parallel connection of graphs
  84 |   ||| Two graphs are combined into one without any connections beetween them
  85 |   ||| The result has the inputs and outputs of both
  86 |   ||| @ left  the left sub-graph
  87 |   ||| @ right the right sub-graph
  88 |   Parallel
  89 |      : (left  : CFG vertex ins  outs)
  90 |     -> (right : CFG vertex ins' outs')
  91 |     -> CFG vertex (ins ++ ins') (outs ++ outs')
  92 | 
  93 |   -- TODO: consider removing these constructors
  94 |   ||| Used to flip the inputs of a graph to make it connectable with another
  95 |   IFlip
  96 |      : {ins, ins' : Edges a}
  97 |     -> CFG vertex (ins ++ ins') outs
  98 |     -> CFG vertex (ins' ++ ins) outs
  99 | 
 100 |   ||| Used to flip the outputs of a graph to make it connectable with another
 101 |   OFlip
 102 |      : {outs, outs' : List (Edge a)}
 103 |     -> CFG vertex ins (outs ++ outs')
 104 |     -> CFG vertex ins (outs' ++ outs)
 105 | 
 106 | export infixr 4 |-|
 107 | ||| Alias for `Parallel`
 108 | public export
 109 | (|-|)
 110 |    : CFG vertex ins           outs
 111 |   -> CFG vertex ins'          outs'
 112 |   -> CFG vertex (ins ++ ins') (outs ++ outs')
 113 | (|-|) = Parallel
 114 | 
 115 | export infixr 5 *->
 116 | ||| Alias for `Series`
 117 | public export
 118 | (*->)
 119 |    : CFG vertex ins edges
 120 |   -> CFG vertex edges outs
 121 |   -> CFG vertex ins outs
 122 | (*->) = Series
 123 | 
 124 | 
 125 | public export
 126 | prepend
 127 |    : {0 vertex : Vertex a}
 128 |   -> {vins, vouts : Neighbors a}
 129 |   -> vertex v vins vouts
 130 |   -> CFG vertex (v ~>> vouts) gouts
 131 |   -> CFG vertex (vins ~~> v) gouts
 132 | prepend v g = (SingleVertex v) *-> g
 133 | 
 134 | public export
 135 | append
 136 |    : {vins, vouts : Neighbors a}
 137 | 
 138 |   -> CFG vertex gins (vins ~~> v)
 139 |   -> vertex v vins vouts
 140 |   -> CFG vertex gins (v ~>> vouts)
 141 | append g v = g *-> (SingleVertex v)
 142 | 
 143 | branch
 144 |    : {0 vertex : Vertex a}
 145 |   -> {vins : Neighbors a}
 146 |   -> {w, w' : a}
 147 | 
 148 |   -> (pre   : vertex v vins [w, w'])
 149 |   -> (left  : CFG vertex [v ~> w]  louts)
 150 |   -> (right : CFG vertex [v ~> w'] routs)
 151 |   -> CFG vertex (vins ~~> v) (louts ++ routs)
 152 | branch pre left right = pre `prepend` (left |-| right)
 153 | 
 154 | fullBranch
 155 |    : {0 vertex : Vertex a}
 156 |   -> {vins, vouts : Neighbors a}
 157 |   -> {w, w', u, u' : a}
 158 | 
 159 |   -> (pre   : vertex v vins [w, w'])
 160 |   -> (left  : CFG vertex [v ~> w]  [u  ~> t])
 161 |   -> (right : CFG vertex [v ~> w'] [u' ~> t])
 162 |   -> (post  : vertex t [u, u'] vouts)
 163 |   -> CFG vertex (vins ~~> v) (t ~>> vouts)
 164 | fullBranch pre left right post = (branch pre left right) `append` post
 165 | 
 166 | ||| A partial sequential connection of two graphs
 167 | ||| The left outputs of the predecessor are connected with all inputs of
 168 | ||| the successor
 169 | ||| @ node   the           predecessor of `branch`
 170 | ||| @ branch the (partial) successor   of `node`
 171 | ||| @ ls     the left  outputs of `node` / the inputs of `branch`
 172 | ||| @ rs     the right outputs of `node`
 173 | public export
 174 | lbranch
 175 |    : {ls, rs : List (Edge a)}
 176 |   -> (node   : CFG vertex ins (ls ++ rs))
 177 |   -> (branch : CFG vertex ls ls')
 178 |   ->           CFG vertex ins (ls' ++ rs)
 179 | lbranch node branch = node *-> (branch |-| Empty)
 180 | 
 181 | ||| A partial sequential connection of two graphs
 182 | ||| The right outputs of the predecessor are connected with all inputs of
 183 | ||| the successor
 184 | ||| @ node   the           predecessor of `branch`
 185 | ||| @ branch the (partial) successor   of `node`
 186 | ||| @ ls     the left  outputs of `node`
 187 | ||| @ rs     the right outputs of `node` / the inputs of `branch`
 188 | public export
 189 | rbranch
 190 |    : {ls, rs : List (Edge a)}
 191 |   -> (node   : CFG vertex ins (ls ++ rs))
 192 |   -> (branch : CFG vertex rs rs')
 193 |   ->           CFG vertex ins (ls ++ rs')
 194 | rbranch node branch = node *-> (Empty |-| branch)
 195 | 
 196 | ||| A partial sequential connection of two graphs
 197 | ||| All outputs of the predecessor are connected with the left inputs of
 198 | ||| the successor
 199 | ||| @ branch the           predecessor of `node`
 200 | ||| @ node   the (partial) successor   of `branch`
 201 | ||| @ ls'    the left  inputs of `node` / the outputs of `branch`
 202 | ||| @ rs     the right inputs of `node`
 203 | public export
 204 | lmerge
 205 |    : {ls, rs : Edges a}
 206 |   -> (branch : CFG vertex ls ls')
 207 |   -> (node   : CFG vertex (ls' ++ rs) outs)
 208 |   ->           CFG vertex (ls  ++ rs) outs
 209 | lmerge branch node = (branch |-| Empty) *-> node
 210 | 
 211 | ||| A partial sequential connection of two graphs
 212 | ||| All outputs of the predecessor are connected with the right inputs of
 213 | ||| the successor
 214 | ||| @ branch the           predecessor of `node`
 215 | ||| @ node   the (partial) successor   of `branch`
 216 | ||| @ ls     the left  inputs of `node`
 217 | ||| @ rs'    the right inputs of `node` / the outputs of `branch`
 218 | public export
 219 | rmerge
 220 |    : {ls, rs : Edges a}
 221 |   -> (branch : CFG vertex rs rs')
 222 |   -> (node   : CFG vertex (ls ++ rs') outs)
 223 |   ->           CFG vertex (ls ++ rs)  outs
 224 | rmerge branch node = (Empty |-| branch) *-> node
 225 | 
 226 | export
 227 | initGraph
 228 |    : {0 vertex : Vertex a}
 229 |   -> {ins, outs : Neighbors a}
 230 |   -> vertex v ins outs
 231 |   -> CFG vertex (ins ~~> v) (v ~>> outs)
 232 | initGraph v = SingleVertex v
 233 | 
 234 | ||| Apply a function to all vertices in a grpaph
 235 | export
 236 | vmap
 237 |    : {0 a : Type}
 238 |   -> {0 vertex, vertex' : Vertex a}
 239 |   -> {0 ins, outs : Edges a}
 240 |   -> ( {0 v : a}
 241 |     -> {vins, vouts : Neighbors a}
 242 |     -> vertex v vins vouts
 243 |     -> vertex' v vins vouts
 244 |      )
 245 |   -> CFG vertex ins outs
 246 |   -> CFG vertex' ins outs
 247 | 
 248 | vmap f Empty              = Empty
 249 | vmap f (SingleVertex v)   = SingleVertex (f v)
 250 | vmap f (Cycle node loop)  = Cycle (vmap f node) (vmap f loop)
 251 | vmap f (Series g g')      = Series (vmap f g) (vmap f g')
 252 | vmap f (Parallel g g')    = Parallel (vmap f g) (vmap f g')
 253 | vmap f (IFlip g)          = IFlip (vmap f g)
 254 | vmap f (OFlip g)          = OFlip (vmap f g)
 255 |