Math for valid modules

Wasm-DSL · May 28, 2024 · 262d517 · 262d517
1 parent 0bf9adb
commit 262d517
Show file tree

Hide file tree

Showing 11 changed files with 403 additions and 619 deletions.
diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst
@@ -96,13 +96,16 @@ Conventions
 
 .. index:: ! type definition, type index, function type, aggregate type
    pair: abstract syntax; type definition
+.. _syntax-type:
 .. _syntax-typedef:
 
 Types
 ~~~~~
 
-The ${:type} section of a module defines a list of :ref:`recursive types <syntax-rectype>`, each of consisting of a list of :ref:`sub types <syntax-subtype>` referenced by individual :ref:`type indices <syntax-typeidx>`.
-All :ref:`function <syntax-functype>` or :ref:`aggregate <syntax-aggrtype>` types used in a module must be defined in this component.
+The ${:type} section of a module defines a list of :ref:`recursive types <syntax-rectype>`, each consisting of a list of :ref:`sub types <syntax-subtype>` referenced by individual :ref:`type indices <syntax-typeidx>`.
+All :ref:`function <syntax-functype>` or :ref:`aggregate <syntax-aggrtype>` types used in a module must be defined in this section.
+
+$${syntax: type}
 
 
 .. index:: ! function, ! local, function index, local index, type index, value type, expression, import

diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst
@@ -1,6 +1,5 @@
 .. index:: ! type, validation, instantiation, execution
    pair: abstract syntax; type
-.. _syntax-type:
 
 Types
 -----

diff --git a/document/core/util/macros.def b/document/core/util/macros.def
@@ -184,6 +184,7 @@
 
 .. |toF| mathdef:: \xref{syntax/types}{syntax-functype}{\rightarrow}
 .. |to| mathdef:: \mathrel{\xref{valid/conventions}{syntax-instrtype}{\rightarrow}}
+.. |toM| mathdef:: \mathrel{\xref{valid/modules}{syntax-moduletype}{\rightarrow}}
 
 .. |BOTH| mathdef:: \xref{valid/conventions}{syntax-heaptype-ext}{\K{bot}}
 .. |BOT| mathdef:: \xref{valid/conventions}{syntax-valtype-ext}{\K{bot}}
@@ -297,6 +298,7 @@
 .. |instrtype| mathdef:: \xref{valid/conventions}{syntax-instrtype}{\X{instrtype}}
 .. |localtype| mathdef:: \xref{valid/conventions}{syntax-localtype}{\X{localtype}}
 .. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}}
+.. |moduletype| mathdef:: \xref{syntax/types}{syntax-moduletype}{\X{moduletype}}
 
 
 .. Types, meta functions
@@ -367,8 +369,9 @@
 .. |MELEMS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{elems}}
 .. |MSTART| mathdef:: \xref{syntax/modules}{syntax-module}{\K{start}}
 
+.. |TYPE| mathdef:: \xref{syntax/modules}{syntax-type}{\K{type}}
 .. |FUNC| mathdef:: \xref{syntax/modules}{syntax-func}{\K{func}}
-.. |LOCAL| mathdef:: \xref{syntax/modules}{syntax-func}{\K{local}}
+.. |LOCAL| mathdef:: \xref{syntax/modules}{syntax-local}{\K{local}}
 .. |FTYPE| mathdef:: \xref{syntax/modules}{syntax-func}{\K{type}}
 .. |FLOCALS| mathdef:: \xref{syntax/modules}{syntax-func}{\K{locals}}
 .. |FBODY| mathdef:: \xref{syntax/modules}{syntax-func}{\K{body}}
@@ -1214,6 +1217,9 @@
 .. |CONSTexprconst| mathdef:: \xref{valid/instructions}{valid-const}{\K{const}}
 .. |CONSTexprokconst| mathdef:: \xref{valid/instructions}{valid-const}{\K{const}}
 
+.. |vdashexternidx| mathdef:: \xref{valid/modules}{valid-exxternidx}{\vdash}
+
+.. |vdashtype| mathdef:: \xref{valid/modules}{valid-type}{\vdash}
 .. |vdashtypes| mathdef:: \xref{valid/modules}{valid-types}{\vdash}
 .. |vdashfunc| mathdef:: \xref{valid/modules}{valid-func}{\vdash}
 .. |vdashlocal| mathdef:: \xref{valid/modules}{valid-local}{\vdash}