diff --git a/docs/src/commentary/gm.rst b/docs/src/commentary/gm.rst index fe867b9..1682a58 100644 --- a/docs/src/commentary/gm.rst +++ b/docs/src/commentary/gm.rst @@ -58,287 +58,7 @@ sequence of instructions* which instantiate the expression at execution. Trees and Vines, in Theory ************************** -WIP. 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$} - } +WIP. ************************** Evaluation: Slurping Vines diff --git a/docs/src/commentary/ti.rst b/docs/src/commentary/ti.rst new file mode 100644 index 0000000..ee192fd --- /dev/null +++ b/docs/src/commentary/ti.rst @@ -0,0 +1,6 @@ +The *Template Instantiation Machine* +==================================== + +WIP. This will hopefully be expanded into a thorough walkthrough of the state +machine. + diff --git a/docs/src/conf.py b/docs/src/conf.py index 9d5374d..8bb359c 100644 --- a/docs/src/conf.py +++ b/docs/src/conf.py @@ -6,7 +6,7 @@ # -- Project information ----------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information -project = 'rlp' +project = "rl'" copyright = '2023, madeleine sydney ślaga' author = 'madeleine sydney slaga' @@ -15,7 +15,7 @@ author = 'madeleine sydney slaga' extensions = ['sphinx.ext.imgmath'] -templates_path = ['_templates'] +# templates_path = ['_templates'] exclude_patterns = [] # 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 html_theme = 'alabaster' -html_static_path = ['_static'] +# html_static_path = ['_static'] # -- Options for LaTeX image math -------------------------------------------- imgmath_latex_preamble = r''' diff --git a/docs/src/index.rst b/docs/src/index.rst index 707ee37..bf4caa1 100644 --- a/docs/src/index.rst +++ b/docs/src/index.rst @@ -17,3 +17,10 @@ Contents commentary/* +.. toctree:: + :maxdepth: 1 + :caption: References + :glob: + + references/* + diff --git a/docs/src/references/gm-state-transition-rules.rst b/docs/src/references/gm-state-transition-rules.rst new file mode 100644 index 0000000..53485c1 --- /dev/null +++ b/docs/src/references/gm-state-transition-rules.rst @@ -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$} + } + diff --git a/docs/src/commentary/tim.rst b/docs/src/references/ti-state-transitions.rst similarity index 97% rename from docs/src/commentary/tim.rst rename to docs/src/references/ti-state-transitions.rst index 4dd05cd..590a165 100644 --- a/docs/src/commentary/tim.rst +++ b/docs/src/references/ti-state-transitions.rst @@ -1,8 +1,6 @@ -The *Template Instantiation Machine* -==================================== - -WIP. This will hopefully be expanded into a thorough walkthrough of the state -machine. +========================= +TI State Transition Rules +========================= Evaluation is complete when a single :code:`NNum` remains on the stack and the dump is empty.