[spec] Fix rendering of Expand

Author: rossberg

document/core/valid/conventions.rst

@@ -167,7 +167,6 @@ In addition, the following auxiliary relation denotes the *expansion* of a :ref:
 $${rule: Expand {Expand_use/*}}
 
 $${relation-ignore: Expand Expand_use}
-$${definition-ignore: expanddt}
 
 
 .. index:: ! instruction type, value type, result type, instruction, local, local index

specification/wasm-3.0/1.2-syntax.types.spectec

@@ -459,7 +459,6 @@ def $rollrt(typeidx, rectype) : rectype  hint(show $roll_(%, %))   hint(macro "r
 def $unrollrt(rectype) : rectype         hint(show $unroll(%))     hint(macro "unrollrt")
 def $rolldt(typeidx, rectype) : deftype* hint(show $roll_(%)*#((%))) hint(macro "rolldt")
 def $unrolldt(deftype) : subtype         hint(show $unroll(%))     hint(macro "unrolldt")
-def $expanddt(deftype) : comptype        hint(show $expand(%))     hint(macro "expanddt")
 
 def $rollrt(x, rectype) = REC ($subst_subtype(subtype, ((_IDX $(x + i)))^(i<n), (REC i)^(i<n)))^n
   -- if rectype = REC subtype^n
@@ -469,8 +468,6 @@ def $unrollrt(rectype) = REC ($subst_subtype(subtype, (REC i)^(i<n), (_DEF recty
 def $rolldt(x, rectype) = (_DEF (REC subtype^n) i)^(i<n)  -- if $rollrt(x, rectype) = REC subtype^n
 def $unrolldt(_DEF rectype i) = subtype*[i]               -- if $unrollrt(rectype) = REC subtype*
 
-def $expanddt(deftype) = comptype                         -- if $unrolldt(deftype) = SUB final? typeuse* comptype
-
 
 ;; Free indices
 

specification/wasm-3.0/2.1-validation.types.spectec

@@ -72,11 +72,10 @@ rule Instrtype_ok:
 
 relation Expand: deftype ~~ comptype hint(macro "%expanddt") hint(tabular)
   hint(prose "The :ref:`expansion <aux-expand-deftype>` of %1 is %2")  ;; TODO(3, ?): avoid hardcoding reST
-
 relation Expand_use: typeuse ~~_context comptype  hint(macro "%expandyy") hint(tabular)
   hint(prose "The :ref:`expansion <aux-expand-typeuse>` of %2 is %3")  ;; TODO(3, ?): avoid hardcoding reST
 
-rule Expand: deftype ~~ comptype   -- if $expanddt(deftype) = comptype
+rule Expand: deftype ~~ comptype   -- if $unrolldt(deftype) = SUB final? typeuse* comptype
 
 rule Expand_use/deftype: deftype ~~_C comptype       -- Expand: deftype ~~ comptype
 rule Expand_use/typeidx: _IDX typeidx ~~_C comptype  -- Expand: C.TYPES[typeidx] ~~ comptype

specification/wasm-latest/1.2-syntax.types.spectec

@@ -459,7 +459,6 @@ def $rollrt(typeidx, rectype) : rectype  hint(show $roll_(%, %))   hint(macro "r
 def $unrollrt(rectype) : rectype         hint(show $unroll(%))     hint(macro "unrollrt")
 def $rolldt(typeidx, rectype) : deftype* hint(show $roll_(%)*#((%))) hint(macro "rolldt")
 def $unrolldt(deftype) : subtype         hint(show $unroll(%))     hint(macro "unrolldt")
-def $expanddt(deftype) : comptype        hint(show $expand(%))     hint(macro "expanddt")
 
 def $rollrt(x, rectype) = REC ($subst_subtype(subtype, ((_IDX $(x + i)))^(i<n), (REC i)^(i<n)))^n
   -- if rectype = REC subtype^n
@@ -469,8 +468,6 @@ def $unrollrt(rectype) = REC ($subst_subtype(subtype, (REC i)^(i<n), (_DEF recty
 def $rolldt(x, rectype) = (_DEF (REC subtype^n) i)^(i<n)  -- if $rollrt(x, rectype) = REC subtype^n
 def $unrolldt(_DEF rectype i) = subtype*[i]               -- if $unrollrt(rectype) = REC subtype*
 
-def $expanddt(deftype) = comptype                         -- if $unrolldt(deftype) = SUB final? typeuse* comptype
-
 
 ;; Free indices
 

specification/wasm-latest/2.1-validation.types.spectec

@@ -72,11 +72,10 @@ rule Instrtype_ok:
 
 relation Expand: deftype ~~ comptype hint(macro "%expanddt") hint(tabular)
   hint(prose "The :ref:`expansion <aux-expand-deftype>` of %1 is %2")  ;; TODO(3, ?): avoid hardcoding reST
-
 relation Expand_use: typeuse ~~_context comptype  hint(macro "%expandyy") hint(tabular)
   hint(prose "The :ref:`expansion <aux-expand-typeuse>` of %2 is %3")  ;; TODO(3, ?): avoid hardcoding reST
 
-rule Expand: deftype ~~ comptype   -- if $expanddt(deftype) = comptype
+rule Expand: deftype ~~ comptype   -- if $unrolldt(deftype) = SUB final? typeuse* comptype
 
 rule Expand_use/deftype: deftype ~~_C comptype       -- Expand: deftype ~~ comptype
 rule Expand_use/typeidx: _IDX typeidx ~~_C comptype  -- Expand: C.TYPES[typeidx] ~~ comptype

spectec/test-frontend/TEST.md

@@ -3440,12 +3440,6 @@ $$
 \end{array}
 $$
 
-$$
-\begin{array}[t]{@{}lcl@{}l@{}}
-{\mathrm{expand}}({\mathit{deftype}}) & = & {\mathit{comptype}} & \quad \mbox{if}~ {\mathrm{unroll}}({\mathit{deftype}}) = \mathsf{sub}~{\mathsf{final}^?}~{{\mathit{typeuse}}^\ast}~{\mathit{comptype}} \\
-\end{array}
-$$
-
 \vspace{1ex}
 
 \vspace{1ex}
@@ -4764,7 +4758,7 @@ $\boxed{{\mathit{typeuse}} \approx_{{\mathit{context}}} {\mathit{comptype}}}$
 
 $$
 \begin{array}[t]{@{}lrcl@{}l@{}}
-{[\textsc{\scriptsize Expand}]} \quad & {\mathit{deftype}} & \approx & {\mathit{comptype}} & \quad \mbox{if}~ {\mathrm{expand}}({\mathit{deftype}}) = {\mathit{comptype}} \\
+{[\textsc{\scriptsize Expand}]} \quad & {\mathit{deftype}} & \approx & {\mathit{comptype}} & \quad \mbox{if}~ {\mathrm{unroll}}({\mathit{deftype}}) = \mathsf{sub}~{\mathsf{final}^?}~{{\mathit{typeuse}}^\ast}~{\mathit{comptype}} \\
 \end{array}
 $$