|
|
|
@ -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.
|
|
|
|
@ -266,8 +272,29 @@ the thing we apply it to. We then create a new node on the heap
|
|
|
|
|
that is an `NApp` node, with its two children being the nodes we popped off.
|
|
|
|
|
Finally, we push it onto the stack.
|
|
|
|
|
|
|
|
|
|
Let's try use these instructions to get a feel for it.
|
|
|
|
|
{{< todo >}}Add an example, probably without notation.{{< /todo >}}
|
|
|
|
|
Let's try use these instructions to get a feel for it. In
|
|
|
|
|
order to conserve space, let's use \\(\\text{G}\\) for PushGlobal,
|
|
|
|
|
\\(\\text{I}\\) for PushInt, and \\(\\text{A}\\) for PushApp.
|
|
|
|
|
Let's say we want to construct a graph for `double 326`. We'll
|
|
|
|
|
use the instructions \\(\\text{I} \; 326\\), \\(\\text{G} \; \\text{double}\\),
|
|
|
|
|
and \\(\\text{A}\\). Let's watch these instructions play out:
|
|
|
|
|
$$
|
|
|
|
|
\\begin{align}
|
|
|
|
|
[\\text{I} \; 326, \\text{G} \; \text{double}, \\text{A}] & \\quad s \\quad & d \\quad & h \\quad & m[\\text{double} : a\_d] \\\\\\
|
|
|
|
|
[\\text{G} \; \text{double}, \\text{A}] & \\quad a\_1 : s \\quad & d \\quad & h[a\_1 : \\text{NInt} \; 326] \\quad & m[\\text{double} : a\_d] \\\\\\
|
|
|
|
|
[\\text{A}] & \\quad a\_d, a\_1 : s \\quad & d \\quad & h[a\_1 : \\text{NInt} \; 326] \\quad & m[\\text{double} : a\_d] \\\\\\
|
|
|
|
|
[] & \\quad a\_2 : s \\quad & d \\quad & h[\\substack{\\begin{aligned}a\_1 & : \\text{NInt} \; 326 \\\\ a\_2 & : \\text{NApp} \; a\_d \; a\_1 \\end{aligned}}] \\quad & m[\\text{double} : a\_d] \\\\\\
|
|
|
|
|
\\end{align}
|
|
|
|
|
$$
|
|
|
|
|
How did we come up with these instructions? We'll answer this question with
|
|
|
|
|
more generality later, but let's take a look at this particular expression
|
|
|
|
|
right now. We know it's an application, so we'll be using MkApp eventually.
|
|
|
|
|
We also know that MkApp expects two values on top of the stack from
|
|
|
|
|
which to make an application. The node on top has to be the function, and the next
|
|
|
|
|
node is the value to be passed into that function. Since a stack is first-in-last-out,
|
|
|
|
|
for the function (`double`, in our case) to be on top, we need
|
|
|
|
|
to push it last. Thus, we push `double` first, then 326. Finally,
|
|
|
|
|
we call MkApp now that the stack is in the right state.
|
|
|
|
|
|
|
|
|
|
Having defined instructions to __build__ graphs, it's now time
|
|
|
|
|
to move on to instructions to __reduce__ graphs - after all,
|
|
|
|
@ -284,10 +311,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 +335,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 +360,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 +375,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 +413,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 +429,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 +455,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 +478,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 +500,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 +524,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 -
|
|
|
|
@ -562,6 +587,9 @@ We can allocate an indirection on the stack, and call Update on it when
|
|
|
|
|
we've constructed a node. While we're constructing the tree, we can
|
|
|
|
|
refer to the indirection when a self-reference is required.
|
|
|
|
|
|
|
|
|
|
That's it for the instructions. Next up, we have to convert our expression
|
|
|
|
|
trees into such instructions. However, this has already gotten pretty long,
|
|
|
|
|
so we'll do it in the next post.
|
|
|
|
|
That's it for the instructions. Knowing them, however, doesn't
|
|
|
|
|
tell us what to do with our `ast` structs. We'll need to define
|
|
|
|
|
rules to translate trees into these instructions, and I've already
|
|
|
|
|
alluded to this when we went over `double 326`.
|
|
|
|
|
However, this has already gotten pretty long,
|
|
|
|
|
so we'll do it in the next post: (link me!)
|
|
|
|
|