Skip to content
This repository has been archived by the owner on Nov 3, 2021. It is now read-only.

Commit

Permalink
[spec] Documentation of text format (#18)
Browse files Browse the repository at this point in the history
  • Loading branch information
binji committed May 31, 2018
1 parent 506907b commit 008e552
Show file tree
Hide file tree
Showing 4 changed files with 52 additions and 6 deletions.
2 changes: 2 additions & 0 deletions document/core/text/conventions.rst
Expand Up @@ -122,6 +122,8 @@ It is convenient to define identifier contexts as :ref:`records <notation-record
& \ITABLES & (\Tid^?)^\ast, \\
& \IMEMS & (\Tid^?)^\ast, \\
& \IGLOBALS & (\Tid^?)^\ast, \\
& \IELEM & (\Tid^?)^\ast, \\
& \IDATA & (\Tid^?)^\ast, \\
& \ILOCALS & (\Tid^?)^\ast, \\
& \ILABELS & (\Tid^?)^\ast, \\
& \ITYPEDEFS & \functype^\ast ~\} \\
Expand Down
26 changes: 25 additions & 1 deletion document/core/text/instructions.rst
Expand Up @@ -175,6 +175,10 @@ Memory Instructions
.. _text-storen:
.. _text-memory.size:
.. _text-memory.grow:
.. _text-memory.init:
.. _text-memory.drop:
.. _text-memory.copy:
.. _text-memory.fill:

The offset and alignment immediates to memory instructions are optional.
The offset defaults to :math:`\T{0}`, the alignment to the storage size of the respective memory access, which is its *natural alignment*.
Expand Down Expand Up @@ -215,7 +219,27 @@ Lexically, an |Toffset| or |Talign| phrase is considered a single :ref:`keyword
\text{i64.store16}~~m{:}\Tmemarg_2 &\Rightarrow& \I64.\STORE\K{16}~m \\ &&|&
\text{i64.store32}~~m{:}\Tmemarg_4 &\Rightarrow& \I64.\STORE\K{32}~m \\ &&|&
\text{memory.size} &\Rightarrow& \MEMORYSIZE \\ &&|&
\text{memory.grow} &\Rightarrow& \MEMORYGROW \\
\text{memory.grow} &\Rightarrow& \MEMORYGROW \\ &&|&
\text{memory.init}~~x{:}\Tdataidx_I &\Rightarrow& \MEMORYINIT~x \\ &&|&
\text{memory.drop}~~x{:}\Tdataidx_I &\Rightarrow& \MEMORYDROP~x \\ &&|&
\text{memory.copy} &\Rightarrow& \MEMORYCOPY \\ &&|&
\text{memory.fill} &\Rightarrow& \MEMORYFILL \\
\end{array}
Table Instructions
~~~~~~~~~~~~~~~~~~

.. _text-table.init:
.. _text-table.drop:
.. _text-table.copy:

.. math::
\begin{array}{llcllll}
\production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|&
\text{table.init}~~x{:}\Telemidx_I &\Rightarrow& \TABLEINIT~x \\ &&|&
\text{table.drop}~~x{:}\Telemidx_I &\Rightarrow& \TABLEDROP~x \\ &&|&
\text{table.copy} &\Rightarrow& \TABLECOPY \\
\end{array}
Expand Down
26 changes: 21 additions & 5 deletions document/core/text/modules.rst
Expand Up @@ -2,12 +2,14 @@ Modules
-------


.. index:: index, type index, function index, table index, memory index, global index, local index, label index
.. index:: index, type index, function index, table index, memory index, global index, element index, data index, local index, label index
pair: text format; type index
pair: text format; function index
pair: text format; table index
pair: text format; memory index
pair: text format; global index
pair: text format; element index
pair: text format; data index
pair: text format; local index
pair: text format; label index
.. _text-typeidx:
Expand Down Expand Up @@ -42,6 +44,12 @@ Such identifiers are looked up in the suitable space of the :ref:`identifier con
\production{global index} & \Tglobalidx_I &::=&
x{:}\Tu32 &\Rightarrow& x \\&&|&
v{:}\Tid &\Rightarrow& x & (\iff I.\IGLOBALS[x] = v) \\
\production{element index} & \Telemidx_I &::=&
x{:}\Tu32 &\Rightarrow& x \\&&|&
v{:}\Tid &\Rightarrow& x & (\iff I.\IELEM[x] = v) \\
\production{data index} & \Tdataidx_I &::=&
x{:}\Tu32 &\Rightarrow& x \\&&|&
v{:}\Tid &\Rightarrow& x & (\iff I.\IDATA[x] = v) \\
\production{local index} & \Tlocalidx_I &::=&
x{:}\Tu32 &\Rightarrow& x \\&&|&
v{:}\Tid &\Rightarrow& x & (\iff I.\ILOCALS[x] = v) \\
Expand Down Expand Up @@ -475,8 +483,10 @@ Element segments allow for an optional :ref:`table index <text-tableidx>` to ide
.. math::
\begin{array}{llclll}
\production{element segment} & \Telem_I &::=&
\text{(}~\text{elem}~~x{:}\Ttableidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad
\Rightarrow\quad \{ \ETABLE~x, \EOFFSET~e, \EINIT~y^\ast \} \\
\text{(}~\text{elem}~~\Tid^?~~x{:}\Ttableidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad
\Rightarrow\quad \{ \ETABLE~x, \EOFFSET~e, \EINIT~y^\ast \} \\ &&|&
\text{(}~\text{elem}~~\Tid^?~~\text{passive}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad
\Rightarrow\quad \{ \EINIT~y^\ast \} \\
\end{array}
.. note::
Expand Down Expand Up @@ -525,8 +535,10 @@ The data is written as a :ref:`string <text-string>`, which may be split up into
.. math::
\begin{array}{llclll}
\production{data segment} & \Tdata_I &::=&
\text{(}~\text{data}~~x{:}\Tmemidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~b^\ast{:}\Tdatastring~\text{)} \\ &&& \qquad
\Rightarrow\quad \{ \DMEM~x', \DOFFSET~e, \DINIT~b^\ast \} \\[1ex]
\text{(}~\text{data}~~\Tid^?~~x{:}\Tmemidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~b^\ast{:}\Tdatastring~\text{)} \\ &&& \qquad
\Rightarrow\quad \{ \DMEM~x', \DOFFSET~e, \DINIT~b^\ast \} \\ &&|&
\text{(}~\text{data}~~\Tid^?~~\text{passive}~~b^\ast{:}\Tdatastring~\text{)} \\ &&& \qquad
\Rightarrow\quad \{ \DINIT~b^\ast \} \\
\production{data string} & \Tdatastring &::=&
(b^\ast{:}\Tstring)^\ast \quad\Rightarrow\quad \concat((b^\ast)^\ast) \\
\end{array}
Expand Down Expand Up @@ -631,6 +643,10 @@ The definition of the initial :ref:`identifier context <text-context>` :math:`I`
\{\IMEMS~(\Tid^?)\} \\
\F{idc}(\text{(}~\text{global}~\Tid^?~\dots~\text{)}) &=&
\{\IGLOBALS~(\Tid^?)\} \\
\F{idc}(\text{(}~\text{elem}~\Tid^?~\dots~\text{)}) &=&
\{\IELEM~(\Tid^?)\} \\
\F{idc}(\text{(}~\text{data}~\Tid^?~\dots~\text{)}) &=&
\{\IDATA~(\Tid^?)\} \\
\F{idc}(\text{(}~\text{import}~\dots~\text{(}~\text{func}~\Tid^?~\dots~\text{)}~\text{)}) &=&
\{\IFUNCS~(\Tid^?)\} \\
\F{idc}(\text{(}~\text{import}~\dots~\text{(}~\text{table}~\Tid^?~\dots~\text{)}~\text{)}) &=&
Expand Down
4 changes: 4 additions & 0 deletions document/core/util/macros.def
Expand Up @@ -639,6 +639,8 @@
.. |Ttableidx| mathdef:: \xref{text/modules}{text-tableidx}{\T{tableidx}}
.. |Tmemidx| mathdef:: \xref{text/modules}{text-memidx}{\T{memidx}}
.. |Tglobalidx| mathdef:: \xref{text/modules}{text-globalidx}{\T{globalidx}}
.. |Telemidx| mathdef:: \xref{text/modules}{text-elemidx}{\T{elemidx}}
.. |Tdataidx| mathdef:: \xref{text/modules}{text-dataidx}{\T{dataidx}}
.. |Tlocalidx| mathdef:: \xref{text/modules}{text-localidx}{\T{localidx}}
.. |Tlabelidx| mathdef:: \xref{text/modules}{text-labelidx}{\T{labelidx}}

Expand Down Expand Up @@ -701,6 +703,8 @@
.. |ITABLES| mathdef:: \xref{text/conventions}{text-context}{\K{tables}}
.. |IMEMS| mathdef:: \xref{text/conventions}{text-context}{\K{mems}}
.. |IGLOBALS| mathdef:: \xref{text/conventions}{text-context}{\K{globals}}
.. |IELEM| mathdef:: \xref{text/conventions}{text-context}{\K{elem}}
.. |IDATA| mathdef:: \xref{text/conventions}{text-context}{\K{data}}
.. |ILOCALS| mathdef:: \xref{text/conventions}{text-context}{\K{locals}}
.. |ILABELS| mathdef:: \xref{text/conventions}{text-context}{\K{labels}}

Expand Down

0 comments on commit 008e552

Please sign in to comment.