diff --git a/content/blog/05_compiler_execution.md b/content/blog/05_compiler_execution.md index 5ba5d94..5b4bc1d 100644 --- a/content/blog/05_compiler_execution.md +++ b/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 -