From 8227387bb7a5fa3ce461b12f71dfc4f218d23169 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Thu, 10 Oct 2024 13:57:55 +0100 Subject: [PATCH] docs: Try to not repeat ourselves in the spec for CFGs (#1565) I had to refer to this recently to check that a CFG must have at least two blocks, and found it was...very repetitive and not that easy to follow. Hoping this is a bit better.... --- specification/hugr.md | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 370aba99c..1c34760c6 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -390,26 +390,24 @@ and evaluating it. The `Sum` produced controls iteration of the loop: ##### Control Flow Graphs When Conditional and `TailLoop` are not sufficient, the HUGR allows -arbitrarily-complex (even irreducible) control flow via an explicit CFG, -expressed using `ControlFlow` edges between `BasicBlock`-nodes that are -children of a CFG-node. `BasicBlock`-nodes only exist as children of CFG-nodes. +arbitrarily-complex (even irreducible) control flow via an explicit `CFG` node: +a dataflow node defined by a child control sibling graph. This sibling +graph contains `BasicBlock` nodes (and [scoped definitions](#scoped-definitions)), +with the `BasicBock` nodes connected by `ControlFlow` edges (not dataflow). +`BasicBlock`-nodes only exist as children of `CFG`-nodes. There are two kinds of `BasicBlock`: `DFB` (dataflow block) and `Exit`. +Each `DFB` node is parent to a dataflow sibling graph. `Exit` blocks +have only incoming control-flow edges, and no children. -`DFB` nodes are CFG basic blocks. Edges between them are -control-flow (as opposed to dataflow), and express traditional -control-flow concepts of branch/merge. Each `DFB` node is -parent to a dataflow sibling graph. `Exit` blocks have only incoming control-flow edges, and no children. - -A `CFG` node is a dataflow node which is defined by a child control -sibling graph. The children are all `BasicBlock`s or [scoped definitions](#scoped-definitions). -The first child is the entry block and must be a `DFB`, with inputs the same as the CFG-node; the second child is an +The first child of the `CFG` is the entry block and must be a `DFB`, +with inputs the same as the CFG-node; the second child is an `Exit` node, whose inputs match the outputs of the CFG-node. The remaining children are either `DFB`s or [scoped definitions](#scoped-definitions). -The first output of the graph contained in a `BasicBlock` has type -`Sum(#t0,...#t(n-1))`, where the node has `n` successors, and the -remaining outputs are a row `#x`. `#ti` with `#x` appended matches the +The first output of the graph contained in a `DFB` has type +`Sum(\#t(0),...,#t(n-1))`, where the node has `n` successors, and the +remaining outputs are a row `#x`. `#t(i)` with `#x` appended matches the inputs of successor `i`. Some normalizations are possible: