Update doc

document/core/exec/modules.rst

@@ -394,10 +394,10 @@ where:
    \moduleinst &=& \{~
      \begin{array}[t]{@{}l@{}}
      \MITYPES~\deftype^\ast, \\
-     \MIFUNCS~\evfuncs(\externval_{\F{im}}^\ast)~\funcaddr^\ast, \\
-     \MITABLES~\evtables(\externval_{\F{im}}^\ast)~\tableaddr^\ast, \\
-     \MIMEMS~\evmems(\externval_{\F{im}}^\ast)~\memaddr^\ast, \\
-     \MIGLOBALS~\evglobals(\externval_{\F{im}}^\ast)~\globaladdr^\ast, \\
+     \MIFUNCS~\funcsxv(\externval_{\F{im}}^\ast)~\funcaddr^\ast, \\
+     \MITABLES~\tablesxv(\externval_{\F{im}}^\ast)~\tableaddr^\ast, \\
+     \MIMEMS~\memsxv(\externval_{\F{im}}^\ast)~\memaddr^\ast, \\
+     \MIGLOBALS~\globalsxv(\externval_{\F{im}}^\ast)~\globaladdr^\ast, \\
      \MIELEMS~\elemaddr^\ast, \\
      \MIDATAS~\dataaddr^\ast, \\
      \MIEXPORTS~\exportinst^\ast ~\}
@@ -419,14 +419,14 @@ where:
      \allocdata^\ast(S_5, \data.\DINIT^\ast) \\
    \exportinst^\ast &=&
      \{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast \\[1ex]
-   \evfuncs(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast
-     \qquad~ (\where x^\ast = \edfuncs(\export^\ast)) \\
-   \evtables(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MITABLES[x])^\ast
-     \qquad (\where x^\ast = \edtables(\export^\ast)) \\
-   \evmems(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIMEMS[x])^\ast
-     \qquad (\where x^\ast = \edmems(\export^\ast)) \\
-   \evglobals(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIGLOBALS[x])^\ast
-     \qquad\!\!\! (\where x^\ast = \edglobals(\export^\ast)) \\
+   \funcsxv(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast
+     \qquad~ (\where x^\ast = \funcsed(\export^\ast)) \\
+   \tablesxv(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MITABLES[x])^\ast
+     \qquad (\where x^\ast = \tablesed(\export^\ast)) \\
+   \memsxv(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIMEMS[x])^\ast
+     \qquad (\where x^\ast = \memsed(\export^\ast)) \\
+   \globalsxv(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIGLOBALS[x])^\ast
+     \qquad\!\!\! (\where x^\ast = \globalsed(\export^\ast)) \\
    \end{array}
 
 .. scratch

document/core/exec/numerics.rst

@@ -165,6 +165,8 @@ where :math:`M = \signif(N)` and :math:`E = \expon(N)`.
 
 .. index:: numeric vector, shape, lane
 .. _aux-lanes:
+.. _aux-packnum:
+.. _aux-unpacknum:
 .. _syntax-i128:
 
 Vectors
@@ -190,6 +192,8 @@ provided that :math:`N = |t|\cdot M`.
 
 This function is a bijection on |IN|, hence it is invertible.
 
+.. todo:: pack/unpacknum
+
 
 .. index:: byte, little endian, memory
 .. _aux-littleendian:

document/core/exec/runtime.rst

@@ -454,13 +454,13 @@ Conventions
 The following auxiliary notation is defined for sequences of external values.
 It filters out entries of a specific kind in an order-preserving fashion:
 
-* :math:`\evfuncs(\externval^\ast) = [\funcaddr ~|~ (\EVFUNC~\funcaddr) \in \externval^\ast]`
+* :math:`\funcsxv(\externval^\ast) = [\funcaddr ~|~ (\EVFUNC~\funcaddr) \in \externval^\ast]`
 
-* :math:`\evtables(\externval^\ast) = [\tableaddr ~|~ (\EVTABLE~\tableaddr) \in \externval^\ast]`
+* :math:`\tablesxv(\externval^\ast) = [\tableaddr ~|~ (\EVTABLE~\tableaddr) \in \externval^\ast]`
 
-* :math:`\evmems(\externval^\ast) = [\memaddr ~|~ (\EVMEM~\memaddr) \in \externval^\ast]`
+* :math:`\memsxv(\externval^\ast) = [\memaddr ~|~ (\EVMEM~\memaddr) \in \externval^\ast]`
 
-* :math:`\evglobals(\externval^\ast) = [\globaladdr ~|~ (\EVGLOBAL~\globaladdr) \in \externval^\ast]`
+* :math:`\globalsxv(\externval^\ast) = [\globaladdr ~|~ (\EVGLOBAL~\globaladdr) \in \externval^\ast]`
 
 
 .. index:: ! structure instance, ! array instance, structure type, array type, defined type, ! field value, ! packed value

document/core/syntax/modules.rst

@@ -362,13 +362,13 @@ Conventions
 
 The following auxiliary notation is defined for sequences of exports, filtering out indices of a specific kind in an order-preserving fashion:
 
-* :math:`\edfuncs(\export^\ast) = [\funcidx ~|~ \EDFUNC~\funcidx \in (\export.\EDESC)^\ast]`
+* :math:`\funcsed(\export^\ast) = [\funcidx ~|~ \EDFUNC~\funcidx \in (\export.\EDESC)^\ast]`
 
-* :math:`\edtables(\export^\ast) = [\tableidx ~|~ \EDTABLE~\tableidx \in (\export.\EDESC)^\ast]`
+* :math:`\tablesed(\export^\ast) = [\tableidx ~|~ \EDTABLE~\tableidx \in (\export.\EDESC)^\ast]`
 
-* :math:`\edmems(\export^\ast) = [\memidx ~|~ \EDMEM~\memidx \in (\export.\EDESC)^\ast]`
+* :math:`\memsed(\export^\ast) = [\memidx ~|~ \EDMEM~\memidx \in (\export.\EDESC)^\ast]`
 
-* :math:`\edglobals(\export^\ast) = [\globalidx ~|~ \EDGLOBAL~\globalidx \in (\export.\EDESC)^\ast]`
+* :math:`\globalsed(\export^\ast) = [\globalidx ~|~ \EDGLOBAL~\globalidx \in (\export.\EDESC)^\ast]`
 
 
 .. index:: ! import, name, function type, table type, memory type, global type, index, index space, type index, function index, table index, memory index, global index, function, table, memory, global, instantiation

document/core/util/macros.def

@@ -218,12 +218,12 @@
 .. |NOFUNC| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{nofunc}}
 .. |NOEXTERN| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{noextern}}
 
-.. |I8X16| mathdef:: \xref{syntax/types}{syntax-shape}{\K{i8x16}}
-.. |I16X8| mathdef:: \xref{syntax/types}{syntax-shape}{\K{i16x8}}
-.. |I32X4| mathdef:: \xref{syntax/types}{syntax-shape}{\K{i32x4}}
-.. |I64X2| mathdef:: \xref{syntax/types}{syntax-shape}{\K{i64x2}}
-.. |F32X4| mathdef:: \xref{syntax/types}{syntax-shape}{\K{f32x4}}
-.. |F64X2| mathdef:: \xref{syntax/types}{syntax-shape}{\K{f64x2}}
+.. |I8X16| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{i8x16}}
+.. |I16X8| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{i16x8}}
+.. |I32X4| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{i32x4}}
+.. |I64X2| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{i64x2}}
+.. |F32X4| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{f32x4}}
+.. |F64X2| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{f64x2}}
 
 .. |REC| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{rec}}
 
@@ -299,10 +299,10 @@
 
 .. |unpack| mathdef:: \xref{syntax/types}{aux-unpack}{\F{unpack}}
 
-.. |etfuncs| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}}
-.. |ettables| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}}
-.. |etmems| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{mems}}
-.. |etglobals| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{globals}}
+.. |funcsxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}}
+.. |tablesxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}}
+.. |memsxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{mems}}
+.. |globalsxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{globals}}
 
 
 .. Indices, non-terminals
@@ -424,10 +424,10 @@
 
 .. Modules, meta functions
 
-.. |edfuncs| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{funcs}}
-.. |edtables| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{tables}}
-.. |edmems| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{mems}}
-.. |edglobals| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{globals}}
+.. |funcsed| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{funcs}}
+.. |tablesed| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{tables}}
+.. |memsed| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{mems}}
+.. |globalsed| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{globals}}
 
 
 .. Instructions, terminals
@@ -1286,10 +1286,10 @@
 
 .. Instances, meta functions
 
-.. |evfuncs| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{funcs}}
-.. |evtables| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{tables}}
-.. |evmems| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{mems}}
-.. |evglobals| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{globals}}
+.. |funcsxv| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{funcs}}
+.. |tablesxv| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{tables}}
+.. |memsxv| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{mems}}
+.. |globalsxv| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{globals}}
 
 
 .. Store, terminals
@@ -1356,6 +1356,9 @@
 
 .. |default| mathdef:: \xref{exec/runtime}{default-val}{\F{default}}
 
+.. |packnum| mathdef:: \xref{exec/numerics}{aux-packnum}{\F{pack}}
+.. |unpacknum| mathdef:: \xref{exec/numerics}{aux-unpacknum}{\F{unpack}}
+
 
 .. Fields, meta-functions
 

document/core/valid/modules.rst

@@ -681,16 +681,16 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
 
   * :math:`C.\CTYPES` is :math:`C_0.\CTYPES`,
 
-  * :math:`C.\CFUNCS` is :math:`\etfuncs(\X{it}^\ast)` concatenated with :math:`\X{dt}^\ast`,
+  * :math:`C.\CFUNCS` is :math:`\funcsxt(\X{it}^\ast)` concatenated with :math:`\X{dt}^\ast`,
     with the import's :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast` and the internal :ref:`defined types <syntax-deftype>` :math:`\X{dt}^\ast` as determined below,
 
-  * :math:`C.\CTABLES` is :math:`\ettables(\X{it}^\ast)` concatenated with :math:`\X{tt}^\ast`,
+  * :math:`C.\CTABLES` is :math:`\tablesxt(\X{it}^\ast)` concatenated with :math:`\X{tt}^\ast`,
     with the import's :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast` and the internal :ref:`table types <syntax-tabletype>` :math:`\X{tt}^\ast` as determined below,
 
-  * :math:`C.\CMEMS` is :math:`\etmems(\X{it}^\ast)` concatenated with :math:`\X{mt}^\ast`,
+  * :math:`C.\CMEMS` is :math:`\memsxt(\X{it}^\ast)` concatenated with :math:`\X{mt}^\ast`,
     with the import's :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast` and the internal :ref:`memory types <syntax-memtype>` :math:`\X{mt}^\ast` as determined below,
 
-  * :math:`C.\CGLOBALS` is :math:`\etglobals(\X{it}^\ast)` concatenated with :math:`\X{gt}^\ast`,
+  * :math:`C.\CGLOBALS` is :math:`\globalsxt(\X{it}^\ast)` concatenated with :math:`\X{gt}^\ast`,
     with the import's :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast` and the internal :ref:`global types <syntax-globaltype>` :math:`\X{gt}^\ast` as determined below,
 
   * :math:`C.\CELEMS` is :math:`{\X{rt}}^\ast` as determined below,
@@ -707,7 +707,7 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
 
 * Let :math:`C'` be the :ref:`context <context>` where:
 
-  * :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\X{it}^\ast)`,
+  * :math:`C'.\CGLOBALS` is the sequence :math:`\globalsxt(\X{it}^\ast)`,
 
   * :math:`C'.\CTYPES` is the same as :math:`C.\CTYPES`,
 
@@ -792,13 +792,13 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
      \quad
      (C \vdashexport \export : \X{et})^\ast
      \\
-     \X{idt}^\ast = \etfuncs(\X{it}^\ast)
+     \X{idt}^\ast = \funcsxt(\X{it}^\ast)
      \qquad
-     \X{itt}^\ast = \ettables(\X{it}^\ast)
+     \X{itt}^\ast = \tablesxt(\X{it}^\ast)
      \qquad
-     \X{imt}^\ast = \etmems(\X{it}^\ast)
+     \X{imt}^\ast = \memsxt(\X{it}^\ast)
      \qquad
-     \X{igt}^\ast = \etglobals(\X{it}^\ast)
+     \X{igt}^\ast = \globalsxt(\X{it}^\ast)
      \\
      x^\ast = \freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon)
      \\

spectec/spec/wasm-3.0/1-syntax.watsup

@@ -15,11 +15,11 @@ syntax list(syntax X) = X*  -- if |X*| < $(2^32)
 syntax bit hint(desc "bit") = 0 | 1
 syntax byte hint(desc "byte") = 0x00 | ... | 0xFF
 
-syntax uN(N) hint(desc "unsigned integer") hint(show u#%) =
+syntax uN(N) hint(desc "unsigned integer") hint(show u#%) hint(macro "uN") =
   0 | ... | 2^N-1
-syntax sN(N) hint(desc "signed integer") hint(show s#%) =
+syntax sN(N) hint(desc "signed integer") hint(show s#%) hint(macro "sN") =
   -2^(N-1) | ... | -1 | 0 | +1 | ... | 2^(N-1)-1
-syntax iN(N) hint(desc "integer") hint(show i#%) =
+syntax iN(N) hint(desc "integer") hint(show i#%) hint(macro "iN") =
   uN(N)
 
 syntax u8 = uN(8)
@@ -49,7 +49,7 @@ def $M(N) = $signif(N)
 def $E(N) : nat hint(show `E) hint(macro none)
 def $E(N) = $expon(N)
 
-syntax fN(N) hint(desc "floating-point number") hint(show f#%) =
+syntax fN(N) hint(desc "floating-point number") hint(show f#%) hint(macro "fN") =
   | POS fNmag(N)  hint(show $(+%)) \
   | NEG fNmag(N)  hint(show $(-%))
 
@@ -74,7 +74,7 @@ def $canon_(N) = $(2^($signif(N)-1))
 
 ;; Vectors
 
-syntax vN(N) hint(desc "vector") hint(show v#%) =
+syntax vN(N) hint(desc "vector") hint(show v#%) hint(macro "vN") =
   iN(N)
 
 

spectec/spec/wasm-3.0/2-syntax-aux.watsup

@@ -231,11 +231,11 @@ def $subst_all_deftypes(dt_1 dt*, tu*) = $subst_all_deftype(dt_1, tu*) $subst_al
 
 ;; Rolling and Unrolling
 
-def $rollrt(typeidx, rectype) : rectype  hint(show $roll_(%, %))
-def $unrollrt(rectype) : rectype         hint(show $unroll(%))
-def $rolldt(typeidx, rectype) : deftype* hint(show $roll_(%, %))
-def $unrolldt(deftype) : subtype         hint(show $unroll(%))
-def $expanddt(deftype) : comptype        hint(show $expand(%))
+def $rollrt(typeidx, rectype) : rectype  hint(show $roll_(%, %)) hint(macro "rollrt")
+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")
 
 ;; TODO: in general, multi-dimensional use of dimensioned vars is ambiguous;
 ;; for example, x** with dimension x* could be x1 x2 x1 x2 of x1 x1 x2 x2.
@@ -256,10 +256,10 @@ rule Expand: dt ~~ ct                          -- if $expanddt(dt) = ct
 ;; Projections
 
 ;; TODO: use built-in notation
-def $funcsxt(externtype*) : deftype*       hint(show $funcs(%))   hint(macro "%xt")
-def $globalsxt(externtype*) : globaltype*  hint(show $globals(%)) hint(macro "%xt")
-def $tablesxt(externtype*) : tabletype*    hint(show $tables(%))  hint(macro "%xt")
-def $memsxt(externtype*) : memtype*        hint(show $mems(%))    hint(macro "%xt")
+def $funcsxt(externtype*) : deftype*       hint(show $funcs(%))   hint(macro "funcsxt")
+def $globalsxt(externtype*) : globaltype*  hint(show $globals(%)) hint(macro "globalsxt")
+def $tablesxt(externtype*) : tabletype*    hint(show $tables(%))  hint(macro "tablesxt")
+def $memsxt(externtype*) : memtype*        hint(show $mems(%))    hint(macro "memsxt")
 
 def $funcsxt(eps) = eps
 def $funcsxt((FUNC dt) xt*) = dt $funcsxt(xt*)

spectec/spec/wasm-3.0/3-numerics.watsup

@@ -180,12 +180,12 @@ def $cvtop(Fnn, Inn, REINTERPRET, sx?, fN) = $reinterpret(Fnn, Inn, fN) -- if $s
 ;; Packed numbers
 
 def $lpacknum(lanetype, num_($lunpack(lanetype))) : lane_(lanetype)
-    hint(show $pack_(%,%))
+    hint(show $pack_(%,%)) hint(macro "packnum")
 def $lpacknum(numtype, c) = c
 def $lpacknum(packtype, c) = $wrap($size($lunpack(packtype)), $psize(packtype), c)
 
 def $lunpacknum(lanetype, lane_(lanetype)) : num_($lunpack(lanetype))
-    hint(show $unpack_(%,%))
+    hint(show $unpack_(%,%)) hint(macro "unpacknum")
 def $lunpacknum(numtype, c) = c
 def $lunpacknum(packtype, c) = $ext($psize(packtype), $size($lunpack(packtype)), U, c)
 

spectec/spec/wasm-3.0/5-runtime-aux.watsup

@@ -4,7 +4,7 @@
 
 ;; Instantiation
 
-def $inst_reftype(moduleinst, reftype) : reftype  hint(show $inst_(%,%))
+def $inst_reftype(moduleinst, reftype) : reftype  hint(show $inst_(%,%)) hint(macro "insttype")
 
 def $inst_reftype(mm, rt) = $subst_all_reftype(rt, dt*)
   -- if dt* = mm.TYPES
@@ -29,8 +29,8 @@ def $default_(REF eps ht) = eps
 
 ;; Packed fields
 
-def $packfield(storagetype, val) : fieldval         hint(show $pack_(%,%))
-def $unpackfield(storagetype, sx?, fieldval) : val  hint(show $unpack_(%)^(%)#((%)))
+def $packfield(storagetype, val) : fieldval         hint(show $pack_(%,%)) hint(macro "packfield")
+def $unpackfield(storagetype, sx?, fieldval) : val  hint(show $unpack_(%)^(%)#((%))) hint(macro "unpackfield")
 
 def $packfield(t, val) = val
 def $packfield(pt, CONST I32 i) = PACK pt $wrap(32, $psize(pt), i)
@@ -41,10 +41,10 @@ def $unpackfield(pt, sx, PACK pt i) = CONST I32 $ext($psize(pt), 32, sx, i)
 
 ;; Projections
 
-def $funcsxv(externval*) : funcaddr*     hint(show $funcs(%))
-def $globalsxv(externval*) : globaladdr* hint(show $globals(%))
-def $tablesxv(externval*) : tableaddr*   hint(show $tables(%))
-def $memsxv(externval*) : memaddr*       hint(show $mems(%))
+def $funcsxv(externval*) : funcaddr*     hint(show $funcs(%))   hint(macro "funcsxv")
+def $globalsxv(externval*) : globaladdr* hint(show $globals(%)) hint(macro "globalssxv")
+def $tablesxv(externval*) : tableaddr*   hint(show $tables(%))  hint(macro "tablessxv")
+def $memsxv(externval*) : memaddr*       hint(show $mems(%))    hint(macro "memsxv")
 
 def $funcsxv(eps) = eps
 def $funcsxv((FUNC fa) xv*) = fa $funcsxv(xv*)