document a few strs
This commit is contained in:
@@ -1,8 +1,26 @@
|
|||||||
The *Spineless Tagless G-Machine*
|
The *Spineless Tagless G-Machine*
|
||||||
=================================
|
=================================
|
||||||
|
|
||||||
WIP. Here's a typeset state transition rule describing the action of
|
WIP. This will hopefully be expanded into a thorough explanation of the state
|
||||||
dereferencing indirections when passed as function arguments.
|
machine.
|
||||||
|
|
||||||
|
Evaluation is complete when a single \texttt{NNum} remains on the stack and the
|
||||||
|
dump is empty.
|
||||||
|
|
||||||
|
.. math::
|
||||||
|
\transrule
|
||||||
|
{ a : \nillist
|
||||||
|
& \nillist
|
||||||
|
& h
|
||||||
|
\begin{bmatrix}
|
||||||
|
a : \mathtt{NNum} \; n
|
||||||
|
\end{bmatrix}
|
||||||
|
& g
|
||||||
|
}
|
||||||
|
{ \mathtt{HALT}
|
||||||
|
}
|
||||||
|
|
||||||
|
Dereference an indirection passed as an argument to a function.
|
||||||
|
|
||||||
.. math::
|
.. math::
|
||||||
\transrule
|
\transrule
|
||||||
@@ -10,7 +28,78 @@ dereferencing indirections when passed as function arguments.
|
|||||||
\begin{bmatrix}
|
\begin{bmatrix}
|
||||||
a : \mathtt{NAp} \; a_1 \; a_2 \\
|
a : \mathtt{NAp} \; a_1 \; a_2 \\
|
||||||
a_2 : \mathtt{NInd} \; a_3
|
a_2 : \mathtt{NInd} \; a_3
|
||||||
\end{bmatrix} & f}
|
\end{bmatrix} & g}
|
||||||
{a : s & d & h[a : \mathtt{NAp} \; a_1 \; a_3] & f}
|
{a : s & d & h[a : \mathtt{NAp} \; a_1 \; a_3] & g}
|
||||||
:label: rule1
|
|
||||||
|
Dereference an indirection on top of the stack.
|
||||||
|
|
||||||
|
.. math::
|
||||||
|
\transrule
|
||||||
|
{p : s & d & h
|
||||||
|
\begin{bmatrix}
|
||||||
|
p : \mathtt{NInd} \; a
|
||||||
|
\end{bmatrix} & g}
|
||||||
|
{a : s & d & h & g}
|
||||||
|
|
||||||
|
Perform a unary operation :math:`o(n)` with internal :code:`Prim` constructor
|
||||||
|
:code:`O` on an argument in normal form.
|
||||||
|
|
||||||
|
.. math::
|
||||||
|
\transrule
|
||||||
|
{ f : a : s
|
||||||
|
& d
|
||||||
|
& h
|
||||||
|
\begin{bmatrix}
|
||||||
|
f : \mathtt{NPrim} \; \mathtt{O} \\
|
||||||
|
a : \mathtt{NAp} \; f \; x \\
|
||||||
|
x : \mathtt{NNum} \; n
|
||||||
|
\end{bmatrix}
|
||||||
|
& g
|
||||||
|
}
|
||||||
|
{ a : s
|
||||||
|
& d
|
||||||
|
& h
|
||||||
|
\begin{bmatrix}
|
||||||
|
a : \mathtt{NNum} \; (o(n))
|
||||||
|
\end{bmatrix}
|
||||||
|
& g
|
||||||
|
}
|
||||||
|
|
||||||
|
Perform a unary operation :math:`o(n)` with internal :code:`Prim` constructor
|
||||||
|
:code:`O` on an unevaluated argument.
|
||||||
|
|
||||||
|
.. math::
|
||||||
|
\transrule
|
||||||
|
{ f : a : \nillist
|
||||||
|
& d
|
||||||
|
& h
|
||||||
|
\begin{bmatrix}
|
||||||
|
f : \mathtt{NPrim} \; \mathtt{O} \\
|
||||||
|
a : \mathtt{NAp} \; f \; x
|
||||||
|
\end{bmatrix}
|
||||||
|
& g
|
||||||
|
}
|
||||||
|
{ b : \nillist
|
||||||
|
& (f : a : \nillist) : d
|
||||||
|
& h
|
||||||
|
& g
|
||||||
|
}
|
||||||
|
|
||||||
|
Restore the stack when a sub-computation has completed.
|
||||||
|
|
||||||
|
.. math::
|
||||||
|
\transrule
|
||||||
|
{ a : \nillist
|
||||||
|
& s : d
|
||||||
|
& h
|
||||||
|
\begin{bmatrix}
|
||||||
|
a : \mathtt{NNum} \; n
|
||||||
|
\end{bmatrix}
|
||||||
|
& g
|
||||||
|
}
|
||||||
|
{ s
|
||||||
|
& d
|
||||||
|
& h
|
||||||
|
& g
|
||||||
|
}
|
||||||
|
|
||||||
|
|||||||
@@ -38,7 +38,10 @@ imgmath_latex_preamble = r'''
|
|||||||
\implies & #2 \\
|
\implies & #2 \\
|
||||||
\hline
|
\hline
|
||||||
\end{tblr} }
|
\end{tblr} }
|
||||||
|
|
||||||
|
\newcommand{\nillist}{[\,]}
|
||||||
'''
|
'''
|
||||||
|
|
||||||
imgmath_image_format = 'svg'
|
imgmath_image_format = 'svg'
|
||||||
imgmath_font_size = 14
|
imgmath_font_size = 14
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user