Cross-references for syntax names

Wasm-DSL · Apr 29, 2024 · ea05b84 · ea05b84
1 parent 3daa1db
commit ea05b84
Show file tree

Hide file tree

Showing 66 changed files with 8,788 additions and 8,887 deletions.
diff --git a/document/core/Makefile b/document/core/Makefile
@@ -104,7 +104,7 @@ $(SPLICEDIR)/_splice: $(SPLICEDIR) $(RSTFILES) $(SPECTECFILES)
 	@echo Modified $?
 	@echo ${if ${filter %.$(SPECTECEXT), $?}, $(RSTFILES), ${filter %.rst, $?}} >$@
 	@echo Splicing `cat $@`
-	@$(SPECTEC) $(SPECTECPAT) --splice-sphinx -p `cat $@` -o $(SPLICEDIR)
+	@$(SPECTEC) $(SPECTECPAT) --splice-sphinx --latex-macros -p `cat $@` -o $(SPLICEDIR)
 
 #$(RSTFILES:%=$(SPLICEDIR)/%): $(SPLICEDIR)/%: % $(SPECTECFILES)
 #	$(SPECTEC) $(SPECTECFILES) --splice-sphinx -p $< -o $@

diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst
@@ -50,8 +50,8 @@ Similarly, :ref:`defined types <syntax-deftype>` :code:`def_type` can be represe
 
 .. code-block:: pseudo
 
-   type packed_type = I8 | I16
-   type field_type = Field(val : val_type | packed_type, mut : bool)
+   type pack_type = I8 | I16
+   type field_type = Field(val : val_type | pack_type, mut : bool)
 
    type struct_type = Struct(fields : list(field_type))
    type array_type = Array(fields : field_type)

diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py
diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst
@@ -18,7 +18,7 @@ Construct                                        Judgement
 :ref:`Heap type <valid-heaptype>`                :math:`C \vdashheaptype \heaptype \ok`
 :ref:`Reference type <valid-reftype>`            :math:`C \vdashreftype \reftype \ok`
 :ref:`Value type <valid-valtype>`                :math:`C \vdashvaltype \valtype \ok`
-:ref:`Packed type <valid-packedtype>`            :math:`C \vdashpackedtype \packedtype \ok`
+:ref:`Packed type <valid-packtype>`              :math:`C \vdashpacktype \packtype \ok`
 :ref:`Storage type <valid-storagetype>`          :math:`C \vdashstoragetype \storagetype \ok`
 :ref:`Field type <valid-fieldtype>`              :math:`C \vdashfieldtype \fieldtype \ok`
 :ref:`Result type <valid-resulttype>`            :math:`C \vdashresulttype \resulttype \ok`
@@ -77,7 +77,7 @@ Construct                                        Judgement
 ===============================================  ===============================================================================
 :ref:`Value <valid-val>`                         :math:`S \vdashval \val : \valtype`
 :ref:`Result <valid-result>`                     :math:`S \vdashresult \result : \resulttype`
-:ref:`Packed value <valid-packedval>`            :math:`S \vdashpackedval \packedval : \packedtype`
+:ref:`Packed value <valid-packval>`              :math:`S \vdashpackval \packval : \packtype`
 :ref:`Field value <valid-fieldval>`              :math:`S \vdashfieldval \fieldval : \storagetype`
 :ref:`External value <valid-externval>`          :math:`S \vdashexternval \externval : \externtype`
 :ref:`Function instance <valid-funcinst>`        :math:`S \vdashfuncinst \funcinst : \functype`
@@ -119,7 +119,7 @@ Construct                                        Judgement
 :ref:`Heap type <match-heaptype>`                :math:`C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2`
 :ref:`Reference type <match-reftype>`            :math:`C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2`
 :ref:`Value type <match-valtype>`                :math:`C \vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2`
-:ref:`Packed type <match-packedtype>`            :math:`C \vdashpackedtypematch \packedtype_1 \matchespackedtype \packedtype_2`
+:ref:`Packed type <match-packtype>`              :math:`C \vdashpacktypematch \packtype_1 \matchespacktype \packtype_2`
 :ref:`Storage type <match-storagetype>`          :math:`C \vdashstoragetypematch \storagetype_1 \matchesstoragetype \storagetype_2`
 :ref:`Field type <match-fieldtype>`              :math:`C \vdashfieldtypematch \fieldtype_1 \matchesfieldtype \fieldtype_2`
 :ref:`Result type <match-resulttype>`            :math:`C \vdashresulttypematch \resulttype_1 \matchesresulttype \resulttype_2`

diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst
@@ -14,8 +14,8 @@ Category                                  Constructor
 :ref:`Number type <syntax-numtype>`       |F64|                                               :math:`\hex{7C}` (-4 as |Bs7|)
 :ref:`Vector type <syntax-vectype>`       |V128|                                              :math:`\hex{7B}` (-5 as |Bs7|)
 (reserved)                                                                                    :math:`\hex{7A}` .. :math:`\hex{79}`
-:ref:`Packed type <syntax-packedtype>`    |I8|                                                :math:`\hex{78}` (-8 as |Bs7|)
-:ref:`Packed type <syntax-packedtype>`    |I16|                                               :math:`\hex{77}` (-9 as |Bs7|)
+:ref:`Packed type <syntax-packtype>`      |I8|                                                :math:`\hex{78}` (-8 as |Bs7|)
+:ref:`Packed type <syntax-packtype>`      |I16|                                               :math:`\hex{77}` (-9 as |Bs7|)
 (reserved)                                                                                    :math:`\hex{78}` .. :math:`\hex{74}`
 :ref:`Heap type <syntax-heaptype>`        |NOFUNC|                                            :math:`\hex{73}` (-13 as |Bs7|)
 :ref:`Heap type <syntax-heaptype>`        |NOEXTERN|                                          :math:`\hex{72}` (-14 as |Bs7|)

diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst
@@ -639,7 +639,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 
 .. index:: field value, field type, validation, store, packed value, packed type
 .. _valid-fieldval:
-.. _valid-packedval:
+.. _valid-packval:
 
 :ref:`Field Values <syntax-fieldval>` :math:`\fieldval`
 .......................................................
@@ -650,16 +650,16 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 
   - Then the field value is valid with :ref:`value type <syntax-valtype>` :math:`t`.
 
-* Else, :math:`\fieldval` is a :ref:`packed value <syntax-packedval>` :math:`\packedval`:
+* Else, :math:`\fieldval` is a :ref:`packed value <syntax-packval>` :math:`\packval`:
 
-  - Let :math:`\packedtype.\PACK~i` be the field value :math:`\fieldval`.
+  - Let :math:`\packtype.\PACK~i` be the field value :math:`\fieldval`.
 
-  - Then the field value is valid with :ref:`packed type <syntax-packedtype>` :math:`\packedtype`.
+  - Then the field value is valid with :ref:`packed type <syntax-packtype>` :math:`\packtype`.
 
 .. math::
    \frac{
    }{
-     S \vdashpackedval \X{pt}.\PACK~i : \X{pt}
+     S \vdashpackval \X{pt}.\PACK~i : \X{pt}
    }
 
 

diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst
@@ -161,7 +161,7 @@ Function Types
 .. _binary-arraytype:
 .. _binary-fieldtype:
 .. _binary-storagetype:
-.. _binary-packedtype:
+.. _binary-packtype:
 
 Aggregate Types
 ~~~~~~~~~~~~~~~
@@ -182,9 +182,9 @@ Aggregate Types
    \production{storage type} & \Bstoragetype &::=&
      t{:}\Bvaltype
        &\Rightarrow& t \\ &&|&
-     t{:}\Bpackedtype
+     t{:}\Bpacktype
        &\Rightarrow& t \\
-   \production{packed type} & \Bpackedtype &::=&
+   \production{packed type} & \Bpacktype &::=&
      \hex{78}
        &\Rightarrow& \I8 \\ &&|&
      \hex{77}