Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix submodule links in SPA part 6 which got out of sync with the code

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2026-05-19 17:05:43 -07:00
parent 487681df16
commit 8795003ce7
2 changed files with 6 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
content/blog/06_spa_agda_cfg/index.md
View File

@@ -130,7 +130,7 @@ by one, leading to another `suc n` in the final type. This makes sense because i
Here's my definition of `Graph`s written using `Fin`:
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 24 39 >}}
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 23 38 >}}
I explicitly used a `size` field, which determines how many nodes are in the
graph, and serves as the upper bound for the edge indices. From there, an
@@ -176,7 +176,7 @@ we will connect each of the outputs of one to each of the inputs of the other.
This is defined by the operation `g₁ ↦ g₂`, which sequences two graphs `g₁` and `g₂`:
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 72 83 >}}
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 71 82 >}}
The definition starts out pretty innocuous, but gets a bit complicated by the
end. The sum of the numbers of nodes in the two operands becomes the new graph
@@ -238,7 +238,7 @@ operation when combining the sub-CFGs of the "if" and "else" branches of an
`if`/`else`, which both follow the condition, and both proceed to the code after
the conditional.
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 59 70 >}}
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 58 69 >}}
Everything here is just concatenation; we pool together the nodes, edges,
inputs, and outputs, and the main source of complexity is the re-indexing.
@@ -250,12 +250,12 @@ from the graph for `while` loops I showed above; the reason for that is that
I currently don't include the conditional expressions in my CFG. This is a
limitation that I will address in future work.
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 85 95 >}}
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 84 94 >}}
Given these thee operations, I construct Control Flow Graphs as follows, where
`singleton` creates a new CFG node with the given list of simple statements:
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 122 126 >}}
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 121 125 >}}
Throughout this, I've been liberal to include empty CFG nodes as was convenient.
This is a departure from the formal definition I gave above, but it makes