Add dump to other rules in compiler posts

content/blog/05_compiler_execution.md

@@ -140,7 +140,7 @@ for a [G-machine](https://link.springer.com/chapter/10.1007/3-540-15975-4_50),
 an abstract architecture which we will use to reduce our graphs. The G-machine
 is stack-based - all operations push and pop items from a stack. The machine
 will also have a "dump", which is a stack of stacks; this will help with
-separating function calls.
+separating evaluation of various graphs.
 
 We will follow the same notation as Simon Peyton Jones in
 [his book](https://www.microsoft.com/en-us/research/wp-content/uploads/1992/01/student.pdf)
@@ -152,7 +152,13 @@ an instruction x and ends with instructions \\(i\\)". A stack machine
 obviously needs to have a stack - we will call it \\(s\\), and will
 adopt a similar notation to the instruction queue: \\(a\_1, a\_2, a\_3 : s\\)
 will mean "a stack with the top values \\(a\_1\\), \\(a\_2\\), and \\(a\_3\\),
-and remaining instructions \\(s\\)".
+and remaining instructions \\(s\\)". Finally, as we said, our stack
+machine has a dump, which we will write as \\(d\\). On this dump,
+we will push not only the current stack, but also the current
+instructions that we are executing, so we may resume execution
+later. We will write \\(\\langle i, s \\rangle : d\\) to mean
+"a dump with instructions \\(i\\) and stack \\(s\\) on top,
+followed by instructions and stacks in \\(d\\)".
 
 There's one more thing the G-machine will have that we've not yet discussed at all,
 and it's needed because of the following quip earlier in the post:
@@ -199,10 +205,10 @@ First up is __PushInt__:
 
 {{< gmachine "PushInt" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{PushInt} \; n : i \quad s \quad h \quad m \)
+    \( \text{PushInt} \; n : i \quad s \quad d \quad h \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( i \quad a : s \quad h[a : \text{NInt} \; n] \quad m \)
+    \( i \quad a : s \quad d \quad h[a : \text{NInt} \; n] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Push an integer \(n\) onto the stack.
@@ -217,10 +223,10 @@ __PushGlobal__:
 
 {{< gmachine "PushGlobal" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{PushGlobal} \; f : i \quad s \quad h \quad m[f : a] \)
+    \( \text{PushGlobal} \; f : i \quad s \quad d \quad h \quad m[f : a] \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( i \quad a : s \quad h \quad m[f : a] \)
+    \( i \quad a : s \quad d \quad h \quad m[f : a] \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Push a global function \(f\) onto the stack.
@@ -233,10 +239,10 @@ __Push__:
 
 {{< gmachine "Push" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{Push} \; n : i \quad a_0, a_1, ..., a_n : s \quad h \quad m \)
+    \( \text{Push} \; n : i \quad a_0, a_1, ..., a_n : s \quad d \quad h \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( i \quad a_n, a_0, a_1, ..., a_n : s \quad h \quad m \)
+    \( i \quad a_n, a_0, a_1, ..., a_n : s \quad d \quad h \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Push a value at offset \(n\) from the top of the stack onto the stack.
@@ -251,10 +257,10 @@ define an instruction to combine two nodes into an application:
 
 {{< gmachine "MkApp" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{MkApp} : i \quad a_0, a_1 : s \quad h \quad m \)
+    \( \text{MkApp} : i \quad a_0, a_1 : s \quad d \quad h \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( i \quad a : s \quad h[ a : \text{NApp} \; a_0 \; a_1] \quad m \)
+    \( i \quad a : s \quad d \quad h[ a : \text{NApp} \; a_0 \; a_1] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Apply a function at the top of the stack to a value after it.
@@ -284,10 +290,10 @@ that __isn't__ an application. Let's write this rule as follows:
 
 {{< gmachine "Unwind-App" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{Unwind} : i \quad a : s \quad h[a : \text{NApp} \; a_0 \; a_1] \quad m \)
+    \( \text{Unwind} : i \quad a : s \quad d \quad h[a : \text{NApp} \; a_0 \; a_1] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( \text{Unwind} : i \quad a_0, a : s \quad h[ a : \text{NApp} \; a_0 \; a_1] \quad m \)
+    \( \text{Unwind} : i \quad a_0, a : s \quad d \quad h[ a : \text{NApp} \; a_0 \; a_1] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Unwind an application by pushing its left node.
@@ -308,10 +314,10 @@ code for the global function:
 
 {{< gmachine "Unwind-Global" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{Unwind} : i \quad a, a_0, a_1, ..., a_n : s \quad h[\substack{a : \text{NGlobal} \; n \; c \\ a_k : \text{NApp} \; a_{k-1} \; a_k'}] \quad m \)
+    \( \text{Unwind} : i \quad a, a_0, a_1, ..., a_n : s \quad d \quad h[\substack{a : \text{NGlobal} \; n \; c \\ a_k : \text{NApp} \; a_{k-1} \; a_k'}] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( c \quad a_0', a_1', ..., a_n', a_n : s \quad h[\substack{a : \text{NGlobal} \; n \; c \\ a_k : \text{NApp} \; a_{k-1} \; a_k'}] \quad m \)
+    \( c \quad a_0', a_1', ..., a_n', a_n : s \quad d \quad h[\substack{a : \text{NGlobal} \; n \; c \\ a_k : \text{NApp} \; a_{k-1} \; a_k'}] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Call a global function.
@@ -333,10 +339,10 @@ We simply replace `NInd` with the node it points to, and resume Unwind:
 
 {{< gmachine "Unwind-Ind" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{Unwind} : i \quad a : s \quad h[a : \text{NInd} \; a' ] \quad m \)
+    \( \text{Unwind} : i \quad a : s \quad d \quad h[a : \text{NInd} \; a' ] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( \text{Unwind} : i \quad a' : s \quad h[a : \text{NInd} \; a' ] \quad m \)
+    \( \text{Unwind} : i \quad a' : s \quad d \quad h[a : \text{NInd} \; a' ] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Replace indirection node with its target.
@@ -348,10 +354,10 @@ haven't yet an instruction to perform these actions. Let's do so now:
 
 {{< gmachine "Update" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{Update} \; n : i \quad a,a_0,a_1,...a_n : s \quad h \quad m \)
+    \( \text{Update} \; n : i \quad a,a_0,a_1,...a_n : s \quad d \quad h \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( i \quad a_0,a_1,...,a_n : s \quad h[a_n : \text{NInd} \; a ] \quad m \)
+    \( i \quad a_0,a_1,...,a_n : s \quad d \quad h[a_n : \text{NInd} \; a ] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Transform node at offset into an indirection.
@@ -386,10 +392,10 @@ allocated array:
 
 {{< gmachine "Pack" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{Pack} \; t \; n : i \quad a_1,a_2,...a_n : s \quad h \quad m \)
+    \( \text{Pack} \; t \; n : i \quad a_1,a_2,...a_n : s \quad d \quad h \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( i \quad a : s \quad h[a : \text{NData} \; t \; [a_1, a_2, ..., a_n] ] \quad m \)
+    \( i \quad a : s \quad d \quad h[a : \text{NData} \; t \; [a_1, a_2, ..., a_n] ] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Pack \(n\) nodes from the stack into a node with tag \(t\).
@@ -402,10 +408,10 @@ array onto the stack:
 
 {{< gmachine "Split" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{Split} : i \quad a : s \quad h[a : \text{NData} \; t \; [a_1, a_2, ..., a_n] ] \quad m \)
+    \( \text{Split} : i \quad a : s \quad d \quad h[a : \text{NData} \; t \; [a_1, a_2, ..., a_n] ] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( i \quad a_1, a_2, ...,a_n : s \quad h[a : \text{NData} \; t \; [a_1, a_2, ..., a_n] ] \quad m \)
+    \( i \quad a_1, a_2, ...,a_n : s \quad d \quad h[a : \text{NData} \; t \; [a_1, a_2, ..., a_n] ] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Unpack a data node on top of the stack.
@@ -428,10 +434,10 @@ Let's define the rule for it:
 
 {{< gmachine "Jump" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{Jump} [..., t \rightarrow i_t, ...] : i \quad a : s \quad h[a : \text{NData} \; t \; as ] \quad m \)
+    \( \text{Jump} [..., t \rightarrow i_t, ...] : i \quad a : s \quad d \quad h[a : \text{NData} \; t \; as ] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( i_t, i \quad a : s \quad h[a : \text{NData} \; t \; as ] \quad m \)
+    \( i_t, i \quad a : s \quad d \quad h[a : \text{NData} \; t \; as ] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Execute instructions corresponding to a tag.
@@ -451,10 +457,10 @@ rid of the next \\(n\\) addresses:
 
 {{< gmachine "Slide" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{Slide} \; n : i \quad a_0, a_1, ..., a_n : s \quad h \quad m \)
+    \( \text{Slide} \; n : i \quad a_0, a_1, ..., a_n : s \quad d \quad h \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( i \quad a_0 : s \quad h \quad m \)
+    \( i \quad a_0 : s \quad d \quad h \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Remove \(n\) addresses after the top from the stack.
@@ -473,10 +479,10 @@ them, called __BinOp__:
 
 {{< gmachine "BinOp" >}}
     {{< gmachine_inner "Before">}}
-    \( \text{BinOp} \; \text{op} : i \quad a_0, a_1 : s \quad h[\substack{a_0 : \text{NInt} \; n \\ a_1 : \text{NInt} \; m}] \quad m \)
+    \( \text{BinOp} \; \text{op} : i \quad a_0, a_1 : s \quad d \quad h[\substack{a_0 : \text{NInt} \; n \\ a_1 : \text{NInt} \; m}] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "After" >}}
-    \( i \quad a : s \quad h[\substack{a_0 : \text{NInt} \; n \\ a_1 : \text{NInt} \; m \\ a : \text{NInt} \; (\text{op} \; n \; m)}] \quad m \)
+    \( i \quad a : s \quad d \quad h[\substack{a_0 : \text{NInt} \; n \\ a_1 : \text{NInt} \; m \\ a : \text{NInt} \; (\text{op} \; n \; m)}] \quad m \)
     {{< /gmachine_inner >}}
     {{< gmachine_inner "Description" >}}
     Apply a binary operator on integers.
@@ -497,8 +503,6 @@ reducing a graph, to say, "we need this value now".
 We call this instruction __Eval__. This is where
 the dump finally comes in!
 
-{{< todo >}}Actually show the dump in the previous evaluasion rules.{{< /todo >}}
-
 When we execute Eval, another graph becomes our "focus", and we switch
 to a new stack. We obviously want to return from this once we've finished
 evaluating what we "focused" on, so we must store the program state somewhere -