From 20a5418f378e0c73217fab2b698fbe03c7aec046 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 26 Jun 2023 14:43:21 +0200 Subject: [PATCH 1/2] Extend indices --- document/core/appendix/index-instructions.py | 35 +++++++++++- document/core/appendix/index-rules.rst | 20 ++++++- document/core/appendix/index-types.rst | 59 ++++++++++++-------- 3 files changed, 87 insertions(+), 27 deletions(-) diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index 00cb5800d..16b1287b1 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -282,7 +282,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\FUNCREF]', r'valid-ref.func', r'exec-ref.func'), Instruction(r'\REFASNONNULL', r'\hex{D3}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'), Instruction(r'\BRONNULL~l', r'\hex{D4}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'), - Instruction(None, r'\hex{D5}'), + Instruction(r'\REFEQ', r'\hex{D5}', r'[\EQREF~\EQREF] \to [\I32]', r'valid-ref.eq', r'exec-ref.eq'), Instruction(r'\BRONNONNULL~l', r'\hex{D6}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]', r'valid-br_on_non_null', r'exec-br_on_non_null'), Instruction(None, r'\hex{D7}'), Instruction(None, r'\hex{D8}'), @@ -320,7 +320,37 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(None, r'\hex{F8}'), Instruction(None, r'\hex{F9}'), Instruction(None, r'\hex{FA}'), - Instruction(None, r'\hex{FB}'), + Instruction(r'\STRUCTNEW~x', r'\hex{FB}~\hex{01}', r'[t^\ast] \to [(\REF~x)]', r'valid-struct.new', r'exec-struct.new'), + Instruction(r'\STRUCTNEWDEFAULT~x', r'\hex{FB}~\hex{02}', r'[] \to [(\REF~x)]', r'valid-struct.new_default', r'exec-struct.new_default'), + Instruction(r'\STRUCTGET~x~i', r'\hex{FB}~\hex{03}', r'[(\REF~\NULL~x)] \to [t]', r'valid-struct.get', r'exec-struct.get'), + Instruction(r'\STRUCTGETS~x~i', r'\hex{FB}~\hex{04}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'), + Instruction(r'\STRUCTGETU~x~i', r'\hex{FB}~\hex{05}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'), + Instruction(r'\STRUCTSET~x~i', r'\hex{FB}~\hex{06}', r'[(\REF~\NULL~x)~t] \to []', r'valid-struct.set', r'exec-struct.set'), + Instruction(r'\ARRAYFILL~x', r'\hex{FB}~\hex{0F}', r'[(\REF~\NULL~x)~\I32~t~\I32] \to []', r'valid-array.fill', r'exec-array.fill'), + Instruction(r'\ARRAYNEW~x', r'\hex{FB}~\hex{11}', r'[t] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'), + Instruction(r'\ARRAYNEWDEFAULT~x', r'\hex{FB}~\hex{12}', r'[] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'), + Instruction(r'\ARRAYGET~x', r'\hex{FB}~\hex{13}', r'[(\REF~\NULL~x)~\I32] \to [t]', r'valid-array.get', r'exec-array.get'), + Instruction(r'\ARRAYGETS~x', r'\hex{FB}~\hex{14}', r'[(\REF~\NULL~x)~\I32] \to [\I32]', r'valid-array.get', r'exec-array.get'), + Instruction(r'\ARRAYGETU~x', r'\hex{FB}~\hex{15}', r'[(\REF~\NULL~x)~\I32] \to [\I32]', r'valid-array.get', r'exec-array.get'), + Instruction(r'\ARRAYSET~x', r'\hex{FB}~\hex{16}', r'[(\REF~\NULL~x)~\I32~t] \to []', r'valid-array.set', r'exec-array.set'), + Instruction(r'\ARRAYLEN', r'\hex{FB}~\hex{17}', r'[\ARRAYREF] \to []', r'valid-array.len', r'exec-array.len'), + Instruction(r'\ARRAYCOPY~x~y', r'\hex{FB}~\hex{18}', r'[(\REF~\NULL~x)~\I32~(\REF~\NULL~y)~\I32~\I32] \to []', r'valid-array.copy', r'exec-array.copy'), + Instruction(r'\ARRAYNEWFIXED~x~n', r'\hex{FB}~\hex{19}', r'[t^n] \to [(\REF~x)]', r'valid-array.new_fixed', r'exec-array.new_fixed'), + Instruction(r'\ARRAYNEWDATA~x~y', r'\hex{FB}~\hex{1B}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_data', r'exec-array.new_data'), + Instruction(r'\ARRAYNEWELEM~x~y', r'\hex{FB}~\hex{1C}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_elem', r'exec-array.new_elem'), + Instruction(r'\I31NEW', r'\hex{FB}~\hex{20}', r'[\I32] \to [\I31REF]', r'valid-i31.new', r'exec-i31.new'), + Instruction(r'\I31GETS', r'\hex{FB}~\hex{21}', r'[\I31REF] \to [\I32]', r'valid-i31.get_s', r'exec-i31.get_s'), + Instruction(r'\I31GETU', r'\hex{FB}~\hex{22}', r'[\I31REF] \to [\I32]', r'valid-i31.get_s', r'exec-i31.get_s'), + Instruction(r'\REFTEST~(\REF~t)', r'\hex{FB}~\hex{40}', r'[(REF~t\')] \to [\I32]', r'valid-ref.test', r'exec-ref.test'), + Instruction(r'\REFCAST~(\REF~t)', r'\hex{FB}~\hex{41}', r'[(\REF~t\')] \to [(\REF~t)]', r'valid-ref.test', r'exec-ref.test'), + Instruction(r'\REFTEST~(\REF~\NULL~t)', r'\hex{FB}~\hex{48}', r'[(REF~\NULL~t\')] \to [\I32]', r'valid-ref.test', r'exec-ref.test'), + Instruction(r'\REFCAST~(\REF~\NULL~t)', r'\hex{FB}~\hex{49}', r'[(\REF~\NULL~t\')] \to [(\REF~\NULL~t)]', r'valid-ref.cast', r'exec-ref.cast'), + Instruction(r'\BRONCAST~t_1~t_2', r'\hex{FB}~\hex{4E}', r'[t_1] \to [t_1\typediff t_2]', r'valid-br_on_cast', r'exec-br_on_cast'), + Instruction(r'\BRONCASTFAIL~t_1~t_2', r'\hex{FB}~\hex{4F}', r'[t_1] \to [t_2]', r'valid-br_on_cast_fail', r'exec-br_on_cast_fail'), + Instruction(r'\ARRAYINITDATA~x~y', r'\hex{FB}~\hex{54}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_data', r'exec-array.init_data'), + Instruction(r'\ARRAYINITELEM~x~y', r'\hex{FB}~\hex{55}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_elem', r'exec-array.init_elem'), + Instruction(r'\EXTERNINTERNALIZE', r'\hex{FB}~\hex{70}', r'[\EXTERNREF] \to [\ANYREF]', r'valid-extern.internalize', r'exec-extern.internalize'), + Instruction(r'\EXTERNEXTERNALIZE', r'\hex{FB}~\hex{71}', r'[\ANYREF] \to [\EXTERNREF]', r'valid-extern.externalize', r'exec-extern.externalize'), Instruction(r'\I32.\TRUNC\K{\_sat\_}\F32\K{\_s}', r'\hex{FC}~\hex{00}', r'[\F32] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat_s'), Instruction(r'\I32.\TRUNC\K{\_sat\_}\F32\K{\_u}', r'\hex{FC}~\hex{01}', r'[\F32] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat_u'), Instruction(r'\I32.\TRUNC\K{\_sat\_}\F64\K{\_s}', r'\hex{FC}~\hex{02}', r'[\F64] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat_s'), @@ -578,6 +608,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat ] + def ColumnWidth(n): return max([len(instr[n]) for instr in INSTRUCTIONS]) diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index 64f91a514..90f1e56fe 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -19,7 +19,15 @@ Construct Judgement :ref:`Heap type ` :math:`C \vdashheaptype \heaptype \ok` :ref:`Reference type ` :math:`C \vdashreftype \reftype \ok` :ref:`Value type ` :math:`C \vdashvaltype \valtype \ok` +:ref:`Packed type ` :math:`C \vdashpackedtype \packedtype \ok` +:ref:`Storage type ` :math:`C \vdashstoragetype \storagetype \ok` +:ref:`Field type ` :math:`C \vdashfieldtype \fieldtype \ok` :ref:`Function type ` :math:`C \vdashfunctype \functype \ok` +:ref:`Structure type ` :math:`C \vdashstructtype \structtype \ok` +:ref:`Array type ` :math:`C \vdasharraytype \arraytype \ok` +:ref:`Compound type ` :math:`C \vdashcomptype \comptype \ok` +:ref:`Sub type ` :math:`C \vdashsubtype \subtype \ok` +:ref:`Recursive type ` :math:`C \vdashrectype \rectype \ok` :ref:`Block type ` :math:`C \vdashblocktype \blocktype : \instrtype` :ref:`Instruction type ` :math:`C \vdashinstrtype \instrtype \ok` :ref:`Table type ` :math:`C \vdashtabletype \tabletype \ok` @@ -97,22 +105,28 @@ Construct Judgement Matching ~~~~~~~~ -=============================================== =============================================================================== +=============================================== ================================================================================== Construct Judgement -=============================================== =============================================================================== +=============================================== ================================================================================== :ref:`Number type ` :math:`C \vdashnumtypematch \numtype_1 \matchesnumtype \numtype_2` :ref:`Heap type ` :math:`C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2` :ref:`Reference type ` :math:`C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2` :ref:`Value type ` :math:`C \vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2` +:ref:`Packed type ` :math:`C \vdashpackedtypematch \packedtype_1 \matchespackedtype \packedtype_2` +:ref:`Storage type ` :math:`C \vdashstoragetypematch \storagetype_1 \matchesstoragetype \storagetype_2` +:ref:`Field type ` :math:`C \vdashfieldtypematch \fieldtype_1 \matchesfieldtype \fieldtype_2` :ref:`Result type ` :math:`C \vdashresulttypematch \resulttype_1 \matchesresulttype \resulttype_2` :ref:`Instruction type ` :math:`C \vdashinstrtypematch \instrtype_1 \matchesinstrtype \instrtype_2` :ref:`Function type ` :math:`C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2` +:ref:`Structure type ` :math:`C \vdashstructtypematch \structtype_1 \matchesstructtype \structtype_2` +:ref:`Array type ` :math:`C \vdasharraytypematch \arraytype_1 \matchesarraytype \arraytype_2` +:ref:`Compound type ` :math:`C \vdashcomptypematch \comptype_1 \matchescomptype \comptype_2` :ref:`Table type ` :math:`C \vdashtabletypematch \tabletype_1 \matchestabletype \tabletype_2` :ref:`Memory type ` :math:`C \vdashmemtypematch \memtype_1 \matchesmemtype \memtype_2` :ref:`Global type ` :math:`C \vdashglobaltypematch \globaltype_1 \matchesglobaltype \globaltype_2` :ref:`External type ` :math:`C \vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2` :ref:`Limits ` :math:`C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2` -=============================================== =============================================================================== +=============================================== ================================================================================== Store Extension diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index 9db74d3b3..b4da9888d 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -4,26 +4,41 @@ Index of Types -------------- -======================================== =========================================== =============================================================================== +======================================== ================================================== =============================================================== Category Constructor Binary Opcode -======================================== =========================================== =============================================================================== -:ref:`Type index ` :math:`x` (positive number as |Bs32| or |Bu32|) -:ref:`Number type ` |I32| :math:`\hex{7F}` (-1 as |Bs7|) -:ref:`Number type ` |I64| :math:`\hex{7E}` (-2 as |Bs7|) -:ref:`Number type ` |F32| :math:`\hex{7D}` (-3 as |Bs7|) -:ref:`Number type ` |F64| :math:`\hex{7C}` (-4 as |Bs7|) -:ref:`Vector type ` |V128| :math:`\hex{7B}` (-5 as |Bs7|) -(reserved) :math:`\hex{7A}` .. :math:`\hex{71}` -:ref:`Heap type ` |FUNC| :math:`\hex{70}` (-16 as |Bs7|) -:ref:`Heap type ` |EXTERN| :math:`\hex{6F}` (-17 as |Bs7|) -(reserved) :math:`\hex{6E}` .. :math:`\hex{6D}` -:ref:`Reference type ` |REF| |NULL| :math:`\hex{6C}` (-20 as |Bs7|) -:ref:`Reference type ` |REF| :math:`\hex{6B}` (-21 as |Bs7|) -(reserved) :math:`\hex{6A}` .. :math:`\hex{61}` -:ref:`Function type ` :math:`[\valtype^\ast] \toF[\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|) -(reserved) :math:`\hex{5F}` .. :math:`\hex{41}` -:ref:`Result type ` :math:`[\epsilon]` :math:`\hex{40}` (-64 as |Bs7|) -:ref:`Table type ` :math:`\limits~\reftype` (none) -:ref:`Memory type ` :math:`\limits` (none) -:ref:`Global type ` :math:`\mut~\valtype` (none) -======================================== =========================================== =============================================================================== +======================================== ================================================== =============================================================== +:ref:`Type index ` :math:`x` (positive number as |Bs32| or |Bu32|) +:ref:`Number type ` |I32| :math:`\hex{7F}` (-1 as |Bs7|) +:ref:`Number type ` |I64| :math:`\hex{7E}` (-2 as |Bs7|) +:ref:`Number type ` |F32| :math:`\hex{7D}` (-3 as |Bs7|) +:ref:`Number type ` |F64| :math:`\hex{7C}` (-4 as |Bs7|) +:ref:`Vector type ` |V128| :math:`\hex{7B}` (-5 as |Bs7|) +:ref:`Packed type ` |I8| :math:`\hex{7A}` (-6 as |Bs7|) +:ref:`Packed type ` |I16| :math:`\hex{79}` (-7 as |Bs7|) +(reserved) :math:`\hex{78}` .. :math:`\hex{71}` +:ref:`Heap type ` |FUNC| :math:`\hex{70}` (-16 as |Bs7|) +:ref:`Heap type ` |EXTERN| :math:`\hex{6F}` (-17 as |Bs7|) +:ref:`Heap type ` |ANY| :math:`\hex{6E}` (-18 as |Bs7|) +:ref:`Heap type ` |EQT| :math:`\hex{6D}` (-19 as |Bs7|) +:ref:`Reference type ` |REF| |NULL| :math:`\hex{6C}` (-20 as |Bs7|) +:ref:`Reference type ` |REF| :math:`\hex{6B}` (-21 as |Bs7|) +:ref:`Heap type ` |I31| :math:`\hex{6A}` (-22 as |Bs7|) +:ref:`Heap type ` |NOFUNC| :math:`\hex{69}` (-23 as |Bs7|) +:ref:`Heap type ` |NOEXTERN| :math:`\hex{68}` (-24 as |Bs7|) +:ref:`Heap type ` |STRUCT| :math:`\hex{67}` (-25 as |Bs7|) +:ref:`Heap type ` |ARRAY| :math:`\hex{66}` (-26 as |Bs7|) +:ref:`Heap type ` |NONE| :math:`\hex{65}` (-27 as |Bs7|) +(reserved) :math:`\hex{64}` .. :math:`\hex{61}` +:ref:`Compound type ` :math:`\TFUNC~[\valtype^\ast] \toF[\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|) +:ref:`Compound type ` :math:`\TSTRUCT~\fieldtype^\ast` :math:`\hex{5F}` (-33 as |Bs7|) +:ref:`Compound type ` :math:`\TARRAY~\fieldtype` :math:`\hex{5E}` (-34 as |Bs7|) +(reserved) :math:`\hex{5D}` .. :math:`\hex{51}` +:ref:`Sub type ` :math:`\TSUB~\typedx^\ast~\comptype` :math:`\hex{50}` (-48 as |Bs7|) +:ref:`Recursive type ` :math:`\TREC~\subtype^\ast` :math:`\hex{4F}` (-49 as |Bs7|) +:ref:`Sub type ` :math:`\TSUB~\FINAL~\typedx^\ast~\comptype` :math:`\hex{4E}` (-50 as |Bs7|) +(reserved) :math:`\hex{4D}` .. :math:`\hex{41}` +:ref:`Result type ` :math:`[\epsilon]` :math:`\hex{40}` (-64 as |Bs7|) +:ref:`Table type ` :math:`\limits~\reftype` (none) +:ref:`Memory type ` :math:`\limits` (none) +:ref:`Global type ` :math:`\mut~\valtype` (none) +======================================== ================================================== =============================================================== From 024656713bba155240a2f98707c491a1689a0dab Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sun, 23 Jul 2023 19:12:28 +0200 Subject: [PATCH 2/2] Fix typos; add missing rules --- document/core/appendix/index-instructions.py | 14 +++++------ document/core/appendix/index-rules.rst | 26 +++++++++++++++----- document/core/appendix/index-types.rst | 4 +-- document/core/appendix/index.rst | 11 +++------ document/core/util/macros.def | 3 +++ document/core/valid/matching.rst | 6 ++--- 6 files changed, 38 insertions(+), 26 deletions(-) diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index 81791f56a..8d33768ab 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -339,13 +339,13 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\ARRAYNEWDATA~x~y', r'\hex{FB}~\hex{1B}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_data', r'exec-array.new_data'), Instruction(r'\ARRAYNEWELEM~x~y', r'\hex{FB}~\hex{1C}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_elem', r'exec-array.new_elem'), Instruction(r'\I31NEW', r'\hex{FB}~\hex{20}', r'[\I32] \to [\I31REF]', r'valid-i31.new', r'exec-i31.new'), - Instruction(r'\I31GETS', r'\hex{FB}~\hex{21}', r'[\I31REF] \to [\I32]', r'valid-i31.get_s', r'exec-i31.get_s'), - Instruction(r'\I31GETU', r'\hex{FB}~\hex{22}', r'[\I31REF] \to [\I32]', r'valid-i31.get_s', r'exec-i31.get_s'), - Instruction(r'\REFTEST~(\REF~t)', r'\hex{FB}~\hex{40}', r'[(REF~t\')] \to [\I32]', r'valid-ref.test', r'exec-ref.test'), - Instruction(r'\REFCAST~(\REF~t)', r'\hex{FB}~\hex{41}', r'[(\REF~t\')] \to [(\REF~t)]', r'valid-ref.test', r'exec-ref.test'), - Instruction(r'\REFTEST~(\REF~\NULL~t)', r'\hex{FB}~\hex{48}', r'[(REF~\NULL~t\')] \to [\I32]', r'valid-ref.test', r'exec-ref.test'), - Instruction(r'\REFCAST~(\REF~\NULL~t)', r'\hex{FB}~\hex{49}', r'[(\REF~\NULL~t\')] \to [(\REF~\NULL~t)]', r'valid-ref.cast', r'exec-ref.cast'), - Instruction(r'\BRONCAST~t_1~t_2', r'\hex{FB}~\hex{4E}', r'[t_1] \to [t_1\typediff t_2]', r'valid-br_on_cast', r'exec-br_on_cast'), + Instruction(r'\I31GETS', r'\hex{FB}~\hex{21}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'), + Instruction(r'\I31GETU', r'\hex{FB}~\hex{22}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'), + Instruction(r'\REFTEST~(\REF~t)', r'\hex{FB}~\hex{40}', r"[(\REF~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'), + Instruction(r'\REFCAST~(\REF~t)', r'\hex{FB}~\hex{41}', r"[(\REF~t')] \to [(\REF~t)]", r'valid-ref.test', r'exec-ref.test'), + Instruction(r'\REFTEST~(\REF~\NULL~t)', r'\hex{FB}~\hex{48}', r"[(REF~\NULL~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'), + Instruction(r'\REFCAST~(\REF~\NULL~t)', r'\hex{FB}~\hex{49}', r"[(\REF~\NULL~t')] \to [(\REF~\NULL~t)]", r'valid-ref.cast', r'exec-ref.cast'), + Instruction(r'\BRONCAST~t_1~t_2', r'\hex{FB}~\hex{4E}', r'[t_1] \to [t_1\reftypediff t_2]', r'valid-br_on_cast', r'exec-br_on_cast'), Instruction(r'\BRONCASTFAIL~t_1~t_2', r'\hex{FB}~\hex{4F}', r'[t_1] \to [t_2]', r'valid-br_on_cast_fail', r'exec-br_on_cast_fail'), Instruction(r'\ARRAYINITDATA~x~y', r'\hex{FB}~\hex{54}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_data', r'exec-array.init_data'), Instruction(r'\ARRAYINITELEM~x~y', r'\hex{FB}~\hex{55}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_elem', r'exec-array.init_elem'), diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index 90f1e56fe..0c5f40216 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -4,16 +4,15 @@ Index of Semantic Rules ----------------------- -.. index:: validation +.. index:: validation, type .. _index-valid: -Typing of Static Constructs -~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Well-formedness of Types +~~~~~~~~~~~~~~~~~~~~~~~~ =============================================== =============================================================================== Construct Judgement =============================================== =============================================================================== -:ref:`Limits ` :math:`C \vdashlimits \limits : k` :ref:`Numeric type ` :math:`C \vdashnumtype \numtype \ok` :ref:`Vector type ` :math:`C \vdashvectype \vectype \ok` :ref:`Heap type ` :math:`C \vdashheaptype \heaptype \ok` @@ -22,18 +21,30 @@ Construct Judgement :ref:`Packed type ` :math:`C \vdashpackedtype \packedtype \ok` :ref:`Storage type ` :math:`C \vdashstoragetype \storagetype \ok` :ref:`Field type ` :math:`C \vdashfieldtype \fieldtype \ok` +:ref:`Result type ` :math:`C \vdashresulttype \resulttype \ok` +:ref:`Instruction type ` :math:`C \vdashinstrtype \instrtype \ok` :ref:`Function type ` :math:`C \vdashfunctype \functype \ok` :ref:`Structure type ` :math:`C \vdashstructtype \structtype \ok` :ref:`Array type ` :math:`C \vdasharraytype \arraytype \ok` :ref:`Compound type ` :math:`C \vdashcomptype \comptype \ok` :ref:`Sub type ` :math:`C \vdashsubtype \subtype \ok` :ref:`Recursive type ` :math:`C \vdashrectype \rectype \ok` +:ref:`Defined type ` :math:`C \vdashdeftype \deftype \ok` :ref:`Block type ` :math:`C \vdashblocktype \blocktype : \instrtype` -:ref:`Instruction type ` :math:`C \vdashinstrtype \instrtype \ok` :ref:`Table type ` :math:`C \vdashtabletype \tabletype \ok` :ref:`Memory type ` :math:`C \vdashmemtype \memtype \ok` :ref:`Global type ` :math:`C \vdashglobaltype \globaltype \ok` :ref:`External type ` :math:`C \vdashexterntype \externtype \ok` +:ref:`Type definitions ` :math:`C \vdashtypes \type^\ast \ok` +=============================================== =============================================================================== + + +Typing of Static Constructs +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +=============================================== =============================================================================== +Construct Judgement +=============================================== =============================================================================== :ref:`Instruction ` :math:`S;C \vdashinstr \instr : \functype` :ref:`Instruction sequence ` :math:`S;C \vdashinstrseq \instr^\ast : \functype` :ref:`Expression ` :math:`C \vdashexpr \expr : \resulttype` @@ -41,6 +52,7 @@ Construct Judgement :ref:`Local ` :math:`C \vdashlocal \local : \localtype` :ref:`Table ` :math:`C \vdashtable \table : \tabletype` :ref:`Memory ` :math:`C \vdashmem \mem : \memtype` +:ref:`Limits ` :math:`C \vdashlimits \limits : k` :ref:`Global ` :math:`C \vdashglobal \global : \globaltype` :ref:`Element segment ` :math:`C \vdashelem \elem : \reftype` :ref:`Element mode ` :math:`C \vdashelemmode \elemmode : \reftype` @@ -109,6 +121,7 @@ Matching Construct Judgement =============================================== ================================================================================== :ref:`Number type ` :math:`C \vdashnumtypematch \numtype_1 \matchesnumtype \numtype_2` +:ref:`Vector type ` :math:`C \vdashvectypematch \vectype_1 \matchesvectype \vectype_2` :ref:`Heap type ` :math:`C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2` :ref:`Reference type ` :math:`C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2` :ref:`Value type ` :math:`C \vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2` @@ -121,6 +134,7 @@ Construct Judgement :ref:`Structure type ` :math:`C \vdashstructtypematch \structtype_1 \matchesstructtype \structtype_2` :ref:`Array type ` :math:`C \vdasharraytypematch \arraytype_1 \matchesarraytype \arraytype_2` :ref:`Compound type ` :math:`C \vdashcomptypematch \comptype_1 \matchescomptype \comptype_2` +:ref:`Defined type ` :math:`C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2` :ref:`Table type ` :math:`C \vdashtabletypematch \tabletype_1 \matchestabletype \tabletype_2` :ref:`Memory type ` :math:`C \vdashmemtypematch \memtype_1 \matchesmemtype \memtype_2` :ref:`Global type ` :math:`C \vdashglobaltypematch \globaltype_1 \matchesglobaltype \globaltype_2` @@ -139,7 +153,7 @@ Construct Judgement :ref:`Table instance ` :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2` :ref:`Memory instance ` :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2` :ref:`Global instance ` :math:`\vdashglobalinstextends \globalinst_1 \extendsto \globalinst_2` -:ref:`Element instance ` :math:`\vdasheleminstextends \eleminst_1 \extendsto \eleminst_2` +:ref:`Element instance ` :math:`\vdasheleminstextends \eleminst_1 \extendsto \eleminst_2` :ref:`Data instance ` :math:`\vdashdatainstextends \datainst_1 \extendsto \datainst_2` :ref:`Store ` :math:`\vdashstoreextends \store_1 \extendsto \store_2` =============================================== =============================================================================== diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index b4da9888d..2e6282113 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -33,9 +33,9 @@ Category Constructor :ref:`Compound type ` :math:`\TSTRUCT~\fieldtype^\ast` :math:`\hex{5F}` (-33 as |Bs7|) :ref:`Compound type ` :math:`\TARRAY~\fieldtype` :math:`\hex{5E}` (-34 as |Bs7|) (reserved) :math:`\hex{5D}` .. :math:`\hex{51}` -:ref:`Sub type ` :math:`\TSUB~\typedx^\ast~\comptype` :math:`\hex{50}` (-48 as |Bs7|) +:ref:`Sub type ` :math:`\TSUB~\typeidx^\ast~\comptype` :math:`\hex{50}` (-48 as |Bs7|) :ref:`Recursive type ` :math:`\TREC~\subtype^\ast` :math:`\hex{4F}` (-49 as |Bs7|) -:ref:`Sub type ` :math:`\TSUB~\FINAL~\typedx^\ast~\comptype` :math:`\hex{4E}` (-50 as |Bs7|) +:ref:`Sub type ` :math:`\TSUB~\TFINAL~\typeidx^\ast~\comptype` :math:`\hex{4E}` (-50 as |Bs7|) (reserved) :math:`\hex{4D}` .. :math:`\hex{41}` :ref:`Result type ` :math:`[\epsilon]` :math:`\hex{40}` (-64 as |Bs7|) :ref:`Table type ` :math:`\limits~\reftype` (none) diff --git a/document/core/appendix/index.rst b/document/core/appendix/index.rst index 448dbcb2f..9054e64e3 100644 --- a/document/core/appendix/index.rst +++ b/document/core/appendix/index.rst @@ -13,11 +13,6 @@ Appendix custom changes -.. only:: singlehtml - - .. toctree:: - - index-types - index-instructions - index-rules - + index-types + index-instructions + index-rules diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 59aed667f..1833fdc98 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -1006,6 +1006,7 @@ .. |matches| mathdef:: \leq .. |matchesnumtype| mathdef:: \xref{valid/matching}{match-numtype}{\leq} +.. |matchesvectype| mathdef:: \xref{valid/matching}{match-vectype}{\leq} .. |matchesheaptype| mathdef:: \xref{valid/matching}{match-heaptype}{\leq} .. |matchesreftype| mathdef:: \xref{valid/matching}{match-reftype}{\leq} .. |matchesvaltype| mathdef:: \xref{valid/matching}{match-valtype}{\leq} @@ -1058,6 +1059,8 @@ .. |vdashlimits| mathdef:: \xref{valid/types}{valid-limits}{\vdash} .. |vdashblocktype| mathdef:: \xref{valid/types}{valid-blocktype}{\vdash} .. |vdashfunctype| mathdef:: \xref{valid/types}{valid-functype}{\vdash} +.. |vdashstructtype| mathdef:: \xref{valid/types}{valid-structtype}{\vdash} +.. |vdasharraytype| mathdef:: \xref{valid/types}{valid-arraytype}{\vdash} .. |vdashcomptype| mathdef:: \xref{valid/types}{valid-comptype}{\vdash} .. |vdashfieldtype| mathdef:: \xref{valid/types}{valid-fieldtype}{\vdash} .. |vdashpackedtype| mathdef:: \xref{valid/types}{valid-packedtype}{\vdash} diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index 760ebeb4f..349e92db2 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -22,12 +22,12 @@ A :ref:`number type ` :math:`\numtype_1` matches a :ref:`number ~\\[-1ex] \frac{ }{ - C \vdashnumtypematch \numtype \matchesvaltype \numtype + C \vdashnumtypematch \numtype \matchesnumtype \numtype } .. index:: vector type -.. _match-vectortype: +.. _match-vectype: Vector Types ~~~~~~~~~~~~ @@ -40,7 +40,7 @@ A :ref:`vector type ` :math:`\vectype_1` matches a :ref:`vector ~\\[-1ex] \frac{ }{ - C \vdashvectypematch \vectype \matchesvaltype \vectype + C \vdashvectypematch \vectype \matchesvectype \vectype }