msyds/rlp
1
0
Fork 0
Code Issues 4 Pull Requests Actions Packages Projects Releases 2 Wiki Activity

docs

Browse Source
This commit is contained in:
crumbtoo
2023-12-01 15:16:54 -07:00
parent 9570b1935a
commit f2da7938d5
6 changed files with 306 additions and 289 deletions
Download Patch File Download Diff File Expand all files Collapse all files

282
docs/src/commentary/gm.rst
View File

@@ -58,287 +58,7 @@ sequence of instructions* which instantiate the expression at execution.
Trees and Vines, in Theory Trees and Vines, in Theory
************************** **************************
WIP. state transition rules WIP.
Core Transition Rules
---------------------
1. Lookup a global by name and push its value onto the stack
.. math::
\gmrule
{ \mathtt{PushGlobal} \; f : i
& s
& h
& m
\begin{bmatrix}
f : a
\end{bmatrix}
}
{ i
& a : s
& h
& m
}
2. Allocate an int node on the heap, and push the address of the newly created
node onto the stack
.. math::
\gmrule
{ \mathtt{PushInt} \; n : i
& s
& h
& m
}
{ i
& a : s
& h
\begin{bmatrix}
a : \mathtt{NNum} \; n
\end{bmatrix}
& m
}
3. Allocate an application node on the heap, applying the top of the stack to
the address directly below it. The address of the application node is pushed
onto the stack.
.. math::
\gmrule
{ \mathtt{MkAp} : i
& f : x : s
& h
& m
}
{ i
& a : s
& h
\begin{bmatrix}
a : \mathtt{NAp} \; f \; x
\end{bmatrix}
& m
}
4. Push a function's argument onto the stack
.. math::
\gmrule
{ \mathtt{Push} \; n : i
& a_0 : \ldots : a_n : s
& h
& m
}
{ i
& a_n : a_0 : \ldots : a_n : s
& h
& m
}
5. Tidy up the stack after instantiating a supercombinator
.. math::
\gmrule
{ \mathtt{Slide} \; n : i
& a_0 : \ldots : a_n : s
& h
& m
}
{ i
& a_0 : s
& h
& m
}
6. If a number is on top of the stack, :code:`Unwind` leaves the machine in a
halt state
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
& h
\begin{bmatrix}
a : \mathtt{NNum} \; n
\end{bmatrix}
& m
}
{ \nillist
& a : s
& h
& m
}
7. If an application is on top of the stack, :code:`Unwind` continues unwinding
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
& h
\begin{bmatrix}
a : \mathtt{NAp} \; f \; x
\end{bmatrix}
& m
}
{ \mathtt{Unwind} : \nillist
& f : a : s
& h
& m
}
8. When a supercombinator is on top of the stack (and the correct number of
arguments have been provided), :code:`Unwind` sets up the stack and jumps to
the supercombinator's code (:math:`\beta`-reduction)
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a_0 : \ldots : a_n : s
& h
\begin{bmatrix}
a_0 : \mathtt{NGlobal} \; n \; c \\
a_1 : \mathtt{NAp} \; a_0 \; e_1 \\
\vdots \\
a_n : \mathtt{NAp} \; a_{n-1} \; e_n \\
\end{bmatrix}
& m
}
{ c
& e_1 : \ldots : e_n : a_n : s
& h
& m
}
9. Pop the stack, and update the nth node to point to the popped address
.. math::
\gmrule
{ \mathtt{Update} \; n : i
& e : f : a_1 : \ldots : a_n : s
& h
\begin{bmatrix}
a_1 : \mathtt{NAp} \; f \; e \\
\vdots \\
a_n : \mathtt{NAp} \; a_{n-1} \; e_n
\end{bmatrix}
& m
}
{ i
& f : a_1 : \ldots : a_n : s
& h
\begin{bmatrix}
a_n : \mathtt{NInd} \; e
\end{bmatrix}
& m
}
10. Pop the stack.
.. math::
\gmrule
{ \mathtt{Pop} \; n : i
& a_1 : \ldots : a_n : s
& h
& m
}
{ i
& s
& h
& m
}
11. Follow indirections while unwinding
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
& h
\begin{bmatrix}
a : \mathtt{NInd} \; a'
\end{bmatrix}
& m
}
{ \mathtt{Unwind} : \nillist
& a' : s
& h
& m
}
12. Allocate uninitialised heap space
.. math::
\gmrule
{ \mathtt{Alloc} \; n : i
& s
& h
& m
}
{ i
& a_1 : \ldots : a_n : s
& h
\begin{bmatrix}
a_1 : \mathtt{NUninitialised} \\
\vdots \\
a_n : \mathtt{NUninitialised} \\
\end{bmatrix}
& m
}
Extension Rules
---------------
1. A sneaky trick to enable sharing of :code:`NNum` nodes. We note that the
global environment is a mapping of :code:`Name` objects (i.e. identifiers) to
heap addresses. Strings of digits are not considered valid identifiers! We
abuse this by modifying Core Rule 2 to update the global environment with the
new node's address. Consider how this rule might impact garbage collection
(remember that the environment is intended for *globals*).
.. math::
\gmrule
{ \mathtt{PushInt} \; n : i
& s
& h
& m
}
{ i
& a : s
& h
\begin{bmatrix}
a : \mathtt{NNum} \; n
\end{bmatrix}
& m
\begin{bmatrix}
n' : a
\end{bmatrix}
\\
\SetCell[c=5]{c}
\text{where $n'$ is the base-10 string rep. of $n$}
}
2. In order for Extension Rule 1. to be effective, we are also required to take
action when a number already exists in the environment:
.. math::
\transrule
{ \mathtt{PushInt} \; n : i
& s
& h
& m
\begin{bmatrix}
n' : a
\end{bmatrix}
}
{ i
& a : s
& h
& m
\\
\SetCell[c=5]{c}
\text{where $n'$ is the base-10 string rep. of $n$}
}
************************** **************************
Evaluation: Slurping Vines Evaluation: Slurping Vines

6
docs/src/commentary/ti.rst Normal file
View File

@@ -0,0 +1,6 @@
The *Template Instantiation Machine*
====================================
WIP. This will hopefully be expanded into a thorough walkthrough of the state
machine.

6
docs/src/conf.py
View File

@@ -6,7 +6,7 @@
# -- Project information ----------------------------------------------------- # -- Project information -----------------------------------------------------
# https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information # https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information
project = 'rlp' project = "rl'"
copyright = '2023, madeleine sydney ślaga' copyright = '2023, madeleine sydney ślaga'
author = 'madeleine sydney slaga' author = 'madeleine sydney slaga'
@@ -15,7 +15,7 @@ author = 'madeleine sydney slaga'
extensions = ['sphinx.ext.imgmath'] extensions = ['sphinx.ext.imgmath']
templates_path = ['_templates'] # templates_path = ['_templates']
exclude_patterns = [] exclude_patterns = []
# for the haskell girlies # for the haskell girlies
@@ -26,7 +26,7 @@ add_function_parentheses = False
# https://www.sphinx-doc.org/en/master/usage/configuration.html#options-for-html-output # https://www.sphinx-doc.org/en/master/usage/configuration.html#options-for-html-output
html_theme = 'alabaster' html_theme = 'alabaster'
html_static_path = ['_static'] # html_static_path = ['_static']
# -- Options for LaTeX image math -------------------------------------------- # -- Options for LaTeX image math --------------------------------------------
imgmath_latex_preamble = r''' imgmath_latex_preamble = r'''

7
docs/src/index.rst
View File

@@ -17,3 +17,10 @@ Contents
commentary/* commentary/*
.. toctree::
:maxdepth: 1
:caption: References
:glob:
references/*

286
docs/src/references/gm-state-transition-rules.rst Normal file
View File

@@ -0,0 +1,286 @@
================================
G-Machine State Transition Rules
================================
*********************
Core Transition Rules
*********************
1. Lookup a global by name and push its value onto the stack
.. math::
\gmrule
{ \mathtt{PushGlobal} \; f : i
& s
& h
& m
\begin{bmatrix}
f : a
\end{bmatrix}
}
{ i
& a : s
& h
& m
}
2. Allocate an int node on the heap, and push the address of the newly created
node onto the stack
.. math::
\gmrule
{ \mathtt{PushInt} \; n : i
& s
& h
& m
}
{ i
& a : s
& h
\begin{bmatrix}
a : \mathtt{NNum} \; n
\end{bmatrix}
& m
}
3. Allocate an application node on the heap, applying the top of the stack to
the address directly below it. The address of the application node is pushed
onto the stack.
.. math::
\gmrule
{ \mathtt{MkAp} : i
& f : x : s
& h
& m
}
{ i
& a : s
& h
\begin{bmatrix}
a : \mathtt{NAp} \; f \; x
\end{bmatrix}
& m
}
4. Push a function's argument onto the stack
.. math::
\gmrule
{ \mathtt{Push} \; n : i
& a_0 : \ldots : a_n : s
& h
& m
}
{ i
& a_n : a_0 : \ldots : a_n : s
& h
& m
}
5. Tidy up the stack after instantiating a supercombinator
.. math::
\gmrule
{ \mathtt{Slide} \; n : i
& a_0 : \ldots : a_n : s
& h
& m
}
{ i
& a_0 : s
& h
& m
}
6. If a number is on top of the stack, :code:`Unwind` leaves the machine in a
halt state
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
& h
\begin{bmatrix}
a : \mathtt{NNum} \; n
\end{bmatrix}
& m
}
{ \nillist
& a : s
& h
& m
}
7. If an application is on top of the stack, :code:`Unwind` continues unwinding
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
& h
\begin{bmatrix}
a : \mathtt{NAp} \; f \; x
\end{bmatrix}
& m
}
{ \mathtt{Unwind} : \nillist
& f : a : s
& h
& m
}
8. When a supercombinator is on top of the stack (and the correct number of
arguments have been provided), :code:`Unwind` sets up the stack and jumps to
the supercombinator's code (:math:`\beta`-reduction)
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a_0 : \ldots : a_n : s
& h
\begin{bmatrix}
a_0 : \mathtt{NGlobal} \; n \; c \\
a_1 : \mathtt{NAp} \; a_0 \; e_1 \\
\vdots \\
a_n : \mathtt{NAp} \; a_{n-1} \; e_n \\
\end{bmatrix}
& m
}
{ c
& e_1 : \ldots : e_n : a_n : s
& h
& m
}
9. Pop the stack, and update the nth node to point to the popped address
.. math::
\gmrule
{ \mathtt{Update} \; n : i
& e : f : a_1 : \ldots : a_n : s
& h
\begin{bmatrix}
a_1 : \mathtt{NAp} \; f \; e \\
\vdots \\
a_n : \mathtt{NAp} \; a_{n-1} \; e_n
\end{bmatrix}
& m
}
{ i
& f : a_1 : \ldots : a_n : s
& h
\begin{bmatrix}
a_n : \mathtt{NInd} \; e
\end{bmatrix}
& m
}
10. Pop the stack.
.. math::
\gmrule
{ \mathtt{Pop} \; n : i
& a_1 : \ldots : a_n : s
& h
& m
}
{ i
& s
& h
& m
}
11. Follow indirections while unwinding
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
& h
\begin{bmatrix}
a : \mathtt{NInd} \; a'
\end{bmatrix}
& m
}
{ \mathtt{Unwind} : \nillist
& a' : s
& h
& m
}
12. Allocate uninitialised heap space
.. math::
\gmrule
{ \mathtt{Alloc} \; n : i
& s
& h
& m
}
{ i
& a_1 : \ldots : a_n : s
& h
\begin{bmatrix}
a_1 : \mathtt{NUninitialised} \\
\vdots \\
a_n : \mathtt{NUninitialised} \\
\end{bmatrix}
& m
}
***************
Extension Rules
***************
1. A sneaky trick to enable sharing of :code:`NNum` nodes. We note that the
global environment is a mapping of :code:`Name` objects (i.e. identifiers) to
heap addresses. Strings of digits are not considered valid identifiers! We
abuse this by modifying Core Rule 2 to update the global environment with the
new node's address. Consider how this rule might impact garbage collection
(remember that the environment is intended for *globals*).
.. math::
\gmrule
{ \mathtt{PushInt} \; n : i
& s
& h
& m
}
{ i
& a : s
& h
\begin{bmatrix}
a : \mathtt{NNum} \; n
\end{bmatrix}
& m
\begin{bmatrix}
n' : a
\end{bmatrix}
\\
\SetCell[c=5]{c}
\text{where $n'$ is the base-10 string rep. of $n$}
}
2. In order for Extension Rule 1. to be effective, we are also required to take
action when a number already exists in the environment:
.. math::
\transrule
{ \mathtt{PushInt} \; n : i
& s
& h
& m
\begin{bmatrix}
n' : a
\end{bmatrix}
}
{ i
& a : s
& h
& m
\\
\SetCell[c=5]{c}
\text{where $n'$ is the base-10 string rep. of $n$}
}

8
docs/src/commentary/tim.rst → docs/src/references/ti-state-transitions.rst
View File

@@ -1,8 +1,6 @@
The *Template Instantiation Machine* =========================
==================================== TI State Transition Rules
=========================
WIP. This will hopefully be expanded into a thorough walkthrough of the state
machine.
Evaluation is complete when a single :code:`NNum` remains on the stack and the Evaluation is complete when a single :code:`NNum` remains on the stack and the
dump is empty. dump is empty.