From 8564ff3eac8440e0a34ab81dad0a1fd656275a36 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Wed, 19 Jul 2023 14:59:45 -0700 Subject: [PATCH] Make metavariables used in execution spec more consistent Many of the new GC instructions used metavariables like `\typeidx` and `\dataidx` in their prose, but `x` and `y` in their formalisms. To make the prose and formalisms more consistent, and for consistency with the metavariables used for other pre-existing instructions, use the `x` and `y` metavariables everywhere. --- document/core/exec/instructions.rst | 124 ++++++++++++++-------------- 1 file changed, 62 insertions(+), 62 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ec347147f..21261ac4e 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -424,14 +424,14 @@ Reference Instructions .. _exec-struct.new: -:math:`\STRUCTNEW~\typeidx` -........................... +:math:`\STRUCTNEW~x` +.................... .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is a :ref:`structure type `. @@ -471,14 +471,14 @@ Reference Instructions .. _exec-struct.new_default: -:math:`\STRUCTNEWDEFAULT~\typeidx` -.................................. +:math:`\STRUCTNEWDEFAULT~x` +........................... .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is a :ref:`structure type `. @@ -494,7 +494,7 @@ Reference Instructions c. Push the :ref:`value ` :math:`\default_{t_i}` to the stack. -7. Execute the instruction :math:`(\STRUCTNEW~\typeidx)`. +7. Execute the instruction :math:`(\STRUCTNEW~x)`. .. math:: \begin{array}{lcl@{\qquad}l} @@ -521,14 +521,14 @@ Reference Instructions .. _exec-struct.get: .. _exec-struct.get_sx: -:math:`\STRUCTGET\K{\_}\sx^?~\typeidx~i` -........................................ +:math:`\STRUCTGET\K{\_}\sx^?~x~i` +................................. .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is a :ref:`structure type ` with at least :math:`i + 1` fields. @@ -570,14 +570,14 @@ Reference Instructions .. _exec-struct.set: -:math:`\STRUCTSET~\typeidx~i` -............................. +:math:`\STRUCTSET~x~i` +...................... .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is a :ref:`structure type ` with at least :math:`i + 1` fields. @@ -621,14 +621,14 @@ Reference Instructions .. _exec-array.new: -:math:`\ARRAYNEW~\typeidx` -.......................... +:math:`\ARRAYNEW~x` +................... .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is an :ref:`array type `. @@ -644,7 +644,7 @@ Reference Instructions 9. Push the value :math:`\val` to the stack :math:`n` times. -10. Execute the instruction :math:`(\ARRAYNEWFIXED~\typeidx~n)`. +10. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. .. math:: \begin{array}{lcl@{\qquad}l} @@ -666,14 +666,14 @@ Reference Instructions .. _exec-array.new_default: -:math:`\ARRAYNEWDEFAULT~\typeidx` -.................................. +:math:`\ARRAYNEWDEFAULT~x` +.......................... .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is an :ref:`array type `. @@ -689,7 +689,7 @@ Reference Instructions 9. Push the :ref:`value ` :math:`\default_t` to the stack :math:`n` times. -10. Execute the instruction :math:`(\ARRAYNEWFIXED~\typeidx~n)`. +10. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. .. math:: \begin{array}{lcl@{\qquad}l} @@ -715,14 +715,14 @@ Reference Instructions .. _exec-array.new_fixed: -:math:`\ARRAYNEWFIXED~\typeidx~n` -................................. +:math:`\ARRAYNEWFIXED~x~n` +.......................... .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is a :ref:`array type `. @@ -760,23 +760,23 @@ Reference Instructions .. _exec-array.new_data: -:math:`\ARRAYNEWDATA~\typeidx~\dataidx` -....................................... +:math:`\ARRAYNEWDATA~x~y` +......................... .. todo:: extend type size convention to field types .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is an :ref:`array type `. 4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type ` :math:`\deftype`. (todo: unroll) -5. Assert: due to :ref:`validation `, the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[\dataidx]` exists. +5. Assert: due to :ref:`validation `, the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]` exists. -6. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[\dataidx]`. +6. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. 7. Assert: due to :ref:`validation `, the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]` exists. @@ -806,7 +806,7 @@ Reference Instructions b. Push the value :math:`(t.\CONST~c_i)` to the stack. -18. Execute the instruction :math:`(\ARRAYNEWFIXED~\typeidx~n)`. +18. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. .. math:: ~\\[-1ex] @@ -830,22 +830,22 @@ Reference Instructions .. _exec-array.new_elem: -:math:`\ARRAYNEWELEM~\typeidx~\elemidx` -....................................... +:math:`\ARRAYNEWELEM~x~y` +......................... .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is an :ref:`array type `. 4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type ` :math:`\deftype`. (todo: unroll) -5. Assert: due to :ref:`validation `, the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[\elemidx]` exists. +5. Assert: due to :ref:`validation `, the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]` exists. -6. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[\elemidx]`. +6. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. 7. Assert: due to :ref:`validation `, the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]` exists. @@ -865,7 +865,7 @@ Reference Instructions 14. Push the references :math:`\reff^\ast` to the stack. -15. Execute the instruction :math:`(\ARRAYNEWFIXED~\typeidx~n)`. +15. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. .. math:: ~\\[-1ex] @@ -885,14 +885,14 @@ Reference Instructions .. _exec-array.get: .. _exec-array.get_sx: -:math:`\ARRAYGET\K{\_}\sx^?~\typeidx` -..................................... +:math:`\ARRAYGET\K{\_}\sx^?~x` +.............................. .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is an :ref:`array type `. @@ -942,14 +942,14 @@ Reference Instructions .. _exec-array.set: -:math:`\ARRAYSET~\typeidx` -.......................... +:math:`\ARRAYSET~x` +................... .. todo:: unroll type -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. -2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[\typeidx]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 3. Assert: due to :ref:`validation `, :math:`\deftype` is an :ref:`array type `. @@ -959,7 +959,7 @@ Reference Instructions 6. Pop the value :math:`\val` from the stack. -7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. 8. Pop the value :math:`(\I32.\CONST~i)` from the stack. @@ -1029,8 +1029,8 @@ Reference Instructions .. _exec-array.fill: -:math:`\ARRAYFILL~\typeidx` -........................... +:math:`\ARRAYFILL~x` +.................... .. todo:: Prose @@ -1063,8 +1063,8 @@ Reference Instructions .. _exec-array.copy: -:math:`\ARRAYCOPY~\typeidx~\typeidx` -.................................... +:math:`\ARRAYCOPY~x~y` +...................... .. todo:: Prose @@ -1115,8 +1115,8 @@ Reference Instructions .. _exec-array.init_data: -:math:`\ARRAYINITDATA~\typeidx~\dataidx` -........................................ +:math:`\ARRAYINITDATA~x~y` +.......................... .. todo:: Prose @@ -1156,8 +1156,8 @@ Reference Instructions .. _exec-array.init_elem: -:math:`\ARRAYINITELEM~\typeidx~\elemidx` -........................................ +:math:`\ARRAYINITELEM~x~y` +.......................... .. todo:: Prose