[spec] Unbreak all_true again
diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index 76dc60d..5822150 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py
@@ -478,7 +478,7 @@ Instruction(2.0, r'\I8X16.\VABS', r'\hex{FD}~~\hex{60}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-iabs'), Instruction(2.0, r'\I8X16.\VNEG', r'\hex{FD}~~\hex{61}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-ineg'), Instruction(2.0, r'\I8X16.\VPOPCNT', r'\hex{FD}~~\hex{62}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-ipopcnt'), - Instruction(2.0, r'\I8X16.\VALLTRUE', r'\hex{FD}~~\hex{63}', r'[\V128] \to [\I32]', r'valid-vtestop', r'exec-vtestop', r'op-iall_true'), + Instruction(2.0, r'\I8X16.\VALLTRUE', r'\hex{FD}~~\hex{63}', r'[\V128] \to [\I32]', r'valid-vtestop', r'exec-vtestop'), Instruction(2.0, r'\I8X16.\VBITMASK', r'\hex{FD}~~\hex{64}', r'[\V128] \to [\I32]', r'valid-vbitmask', r'exec-vbitmask', r'op-ivbitmask'), Instruction(2.0, r'\I8X16.\VNARROW\K{\_i16x8\_s}', r'\hex{FD}~~\hex{65}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vnarrow', r'op-vnarrow'), Instruction(2.0, r'\I8X16.\VNARROW\K{\_i16x8\_u}', r'\hex{FD}~~\hex{66}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vnarrow', r'op-vnarrow'),
diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index a2886f8..ce0e42f 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst
@@ -583,16 +583,16 @@ \end{array} -.. _op-iall_true: +.. _op-inez: -:math:`\ialltrue_N(i)` -...................... +:math:`\inez_N(i)` +.................. * Return :math:`0` if :math:`i` is zero, :math:`1` otherwise. .. math:: \begin{array}{@{}lcll} - \ialltrue_N(i) &=& \tobool(i \neq 0) + \inez_N(i) &=& \tobool(i \neq 0) \end{array}
diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 7caefba..4af4c09 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def
@@ -1583,7 +1583,7 @@ .. |ictz| mathdef:: \xref{exec/numerics}{op-ictz}{\F{ictz}} .. |ipopcnt| mathdef:: \xref{exec/numerics}{op-ipopcnt}{\F{ipopcnt}} .. |ieqz| mathdef:: \xref{exec/numerics}{op-ieqz}{\F{ieqz}} -.. |ialltrue| mathdef:: \xref{exec/numerics}{op-iall_true}{\F{iall\_true}} +.. |inez| mathdef:: \xref{exec/numerics}{op-inez}{\F{inez}} .. |ieq| mathdef:: \xref{exec/numerics}{op-ieq}{\F{ieq}} .. |ine| mathdef:: \xref{exec/numerics}{op-ine}{\F{ine}} .. |ilt| mathdef:: \xref{exec/numerics}{op-ilt}{\F{ilt}}
diff --git a/specification/wasm-3.0/3.1-numerics.scalar.spectec b/specification/wasm-3.0/3.1-numerics.scalar.spectec index f277a74..832c219 100644 --- a/specification/wasm-3.0/3.1-numerics.scalar.spectec +++ b/specification/wasm-3.0/3.1-numerics.scalar.spectec
@@ -132,7 +132,7 @@ def $irelaxed_laneselect_(N, iN(N), iN(N), iN(N)) : iN(N)* def $ieqz_(N, iN(N)) : u32 -def $iall_true_(N, iN(N)) : u32 hint(show $iall__true_(%1,%2)) +def $inez_(N, iN(N)) : u32 def $ieq_(N, iN(N), iN(N)) : u32 def $ine_(N, iN(N), iN(N)) : u32 @@ -217,7 +217,7 @@ def $ieqz_(N, i_1) = $bool(i_1 = 0) -def $iall_true_(N, i_1) = $bool(i_1 =/= 0) +def $inez_(N, i_1) = $bool(i_1 =/= 0) def $ieq_(N, i_1, i_2) = $bool(i_1 = i_2)
diff --git a/specification/wasm-3.0/3.2-numerics.vector.spectec b/specification/wasm-3.0/3.2-numerics.vector.spectec index e476af0..c88b9da 100644 --- a/specification/wasm-3.0/3.2-numerics.vector.spectec +++ b/specification/wasm-3.0/3.2-numerics.vector.spectec
@@ -62,9 +62,6 @@ def $ivternopnd_(shape, def $f_(N, iN(N), iN(N), iN(N)) : iN(N)*, vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)* def $fvternop_(shape, def $f_(N, fN(N), fN(N), fN(N)) : fN(N)*, vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)* -def $ivtestop_(shape, def $f_(N, iN(N)) : u32, vec_(V128)) : u32 -def $fvtestop_(shape, def $f_(N, fN(N)) : u32, vec_(V128)) : u32 - def $ivrelop_(shape, def $f_(N, iN(N), iN(N)) : u32, vec_(V128), vec_(V128)) : vec_(V128) def $ivrelopsx_(shape, def $f_(N, sx, iN(N), iN(N)) : u32, sx, vec_(V128), vec_(V128)) : vec_(V128) def $fvrelop_(shape, def $f_(N, fN(N), fN(N)) : u32, vec_(V128), vec_(V128)) : vec_(V128) @@ -120,15 +117,6 @@ -- if c** = $setproduct_(lane_(Fnn), $f_($sizenn(Fnn), c_1, c_2, c_3)*) -def $ivtestop_(Jnn X M, def $f_, v_1) = $prod(c*) - -- if c_1* = $lanes_(Jnn X M, v_1) - -- if c* = $f_($lsizenn(Jnn), c_1)* - -def $fvtestop_(Fnn X M, def $f_, v_1) = $prod(c*) - -- if c_1* = $lanes_(Fnn X M, v_1) - -- if c* = $f_($sizenn(Fnn), c_1)* - - def $ivrelop_(Jnn X M, def $f_, v_1, v_2) = $inv_lanes_(Jnn X M, c*) -- if c_1* = $lanes_(Jnn X M, v_1) -- if c_2* = $lanes_(Jnn X M, v_2) @@ -187,8 +175,6 @@ hint(show %2#$_(%1,%3,%4)) def $vternop_(shape, vternop_(shape), vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)* hint(show %2#$_(%1,%3,%4,%5)) -def $vtestop_(shape, vtestop_(shape), vec_(V128)) : u32 - hint(show %2#$_(%1,%3)) def $vrelop_(shape, vrelop_(shape), vec_(V128), vec_(V128)) : vec_(V128) hint(show %2#$_(%1,%3,%4)) @@ -265,8 +251,6 @@ def $vternop_(Fnn X M, RELAXED_MADD, v_1, v_2, v_3) = $fvternop_(Fnn X M, $frelaxed_madd_, v_1, v_2, v_3) def $vternop_(Fnn X M, RELAXED_NMADD, v_1, v_2, v_3) = $fvternop_(Fnn X M, $frelaxed_nmadd_, v_1, v_2, v_3) -def $vtestop_(Jnn X M, ALL_TRUE, v) = $ivtestop_(Jnn X M, $iall_true_, v) - def $vrelop_(Jnn X M, EQ, v_1, v_2) = $ivrelop_(Jnn X M, $ieq_, v_1, v_2) def $vrelop_(Jnn X M, NE, v_1, v_2) = $ivrelop_(Jnn X M, $ine_, v_1, v_2) def $vrelop_(Jnn X M, LT sx, v_1, v_2) = $ivrelopsx_(Jnn X M, $ilt_, sx, v_1, v_2)
diff --git a/specification/wasm-3.0/4.3-execution.instructions.spectec b/specification/wasm-3.0/4.3-execution.instructions.spectec index 5c7a706..bde165a 100644 --- a/specification/wasm-3.0/4.3-execution.instructions.spectec +++ b/specification/wasm-3.0/4.3-execution.instructions.spectec
@@ -992,7 +992,7 @@ rule Step_pure/vvtestop: (VCONST V128 c_1) (VVTESTOP V128 ANY_TRUE) ~> (CONST I32 c) - -- if c = $ine_($vsize(V128), c_1, 0) + -- if c = $inez_($vsize(V128), c_1) rule Step_pure/vunop-val: @@ -1023,8 +1023,9 @@ rule Step_pure/vtestop: - (VCONST V128 c_1) (VTESTOP sh vtestop) ~> (CONST I32 i) - -- if i = $vtestop_(sh, vtestop, c_1) + (VCONST V128 c_1) (VTESTOP (Jnn X M) ALL_TRUE) ~> (CONST I32 c) + -- if i* = $lanes_(Jnn X M, c_1) + -- if c = $prod(($inez_($jsizenn(Jnn), i)*)) rule Step_pure/vrelop:
diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index 9847f49..9a2d1cc 100644 --- a/spectec/doc/example/output/NanoWasm.pdf +++ b/spectec/doc/example/output/NanoWasm.pdf Binary files differ
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index dbd1b24..59f6ed4 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md
@@ -4609,9 +4609,9 @@ def $ieqz_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 = 0))) ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec -def $iall_true_(N : N, iN : iN(N)) : u32 +def $inez_(N : N, iN : iN(N)) : u32 ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec - def $iall_true_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0))) + def $inez_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0))) ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec def $ieq_(N : N, iN : iN(N), iN : iN(N)) : u32 @@ -5037,20 +5037,6 @@ -- if (c*{c <- `c*`}*{`c*` <- `c**`} = $setproduct_(syntax lane_((Fnn : Fnn <: lanetype)), $f_($sizenn((Fnn : Fnn <: numtype)), c_1, c_2, c_3)*{c_1 <- `c_1*`, c_2 <- `c_2*`, c_3 <- `c_3*`})) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $ivtestop_(shape : shape, def $f_(N : N, iN : iN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $ivtestop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`})) - -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), v_1)) - -- if (c*{c <- `c*`} = $f_($lsizenn((Jnn : Jnn <: lanetype)), c_1)*{c_1 <- `c_1*`}) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $fvtestop_(shape : shape, def $f_(N : N, fN : fN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $fvtestop_{Fnn : Fnn, M : M, def $f_(N : N, fN : fN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`})) - -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), v_1)) - -- if (c*{c <- `c*`} = $f_($sizenn((Fnn : Fnn <: numtype)), c_1)*{c_1 <- `c_1*`}) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $ivrelop_(shape : shape, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $ivrelop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), `c*` : iN($lsizenn((Jnn : Jnn <: lanetype)))*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*, `c_2*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1, v_2) = $inv_lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c*{c <- `c*`}) @@ -5209,11 +5195,6 @@ def $vternop_{Fnn : Fnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), v_3 : vec_(V128_Vnn)}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), RELAXED_NMADD_vternop_, v_1, v_2, v_3) = $fvternop_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $frelaxed_nmadd_, v_1, v_2, v_3) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $vtestop_(shape : shape, vtestop_ : vtestop_(shape), vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $vtestop_{Jnn : Jnn, M : M, v : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_, v) = $ivtestop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $iall_true_, v) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $vrelop_(shape : shape, vrelop_ : vrelop_(shape), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $vrelop_{Jnn : Jnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), EQ_vrelop_, v_1, v_2) = $ivrelop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $ieq_, v_1, v_2) @@ -6221,7 +6202,7 @@ ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule vvtestop{c_1 : vec_(V128_Vnn), c : num_(I32_numtype)}: `%~>%`([VCONST_instr(V128_vectype, c_1) VVTESTOP_instr(V128_vectype, ANY_TRUE_vvtestop)], [CONST_instr(I32_numtype, c)]) - -- if (c = $ine_($vsize(V128_vectype), c_1, `%`_iN(0))) + -- if (c = $inez_($vsize(V128_vectype), c_1)) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule `vunop-val`{c_1 : vec_(V128_Vnn), sh : shape, vunop : vunop_(sh), c : vec_(V128_Vnn)}: @@ -6254,9 +6235,10 @@ -- if ($vternop_(sh, vternop, c_1, c_2, c_3) = []) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec - rule vtestop{c_1 : vec_(V128_Vnn), sh : shape, vtestop : vtestop_(sh), i : num_(I32_numtype)}: - `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(sh, vtestop)], [CONST_instr(I32_numtype, i)]) - -- if (i = $vtestop_(sh, vtestop, c_1)) + rule vtestop{c_1 : vec_(V128_Vnn), Jnn : Jnn, M : M, c : num_(I32_numtype), `i*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}: + `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_)], [CONST_instr(I32_numtype, c)]) + -- if (i*{i <- `i*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c_1)) + -- if (c!`%`_num_.0 = $prod($inez_($jsizenn(Jnn), i)!`%`_u32.0*{i <- `i*`})) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule vrelop{c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), sh : shape, vrelop : vrelop_(sh), c : vec_(V128_Vnn)}:
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 168b37b..d2141f7 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md
@@ -8110,7 +8110,7 @@ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{{\mathrm{iall\_true}}}_{N}(i_1) & = & \mathbb{B}(i_1 \neq 0) \\ +{{\mathrm{inez}}}_{N}(i_1) & = & \mathbb{B}(i_1 \neq 0) \\ \end{array} $$ @@ -8468,28 +8468,6 @@ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{{\mathrm{ivtestop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1) & = & {\Pi}\, {c^\ast} & \quad -\begin{array}[t]{@{}l@{}} -\mbox{if}~ {c_1^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1) \\ -{\land}~ {c^\ast} = {{{\mathrm{f}}}_{N}(c_1)^\ast} \\ -\end{array} \\ -\end{array} -$$ - -$$ -\begin{array}[t]{@{}lcl@{}l@{}} -{{\mathrm{fvtestop}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1) & = & {\Pi}\, {c^\ast} & \quad -\begin{array}[t]{@{}l@{}} -\mbox{if}~ {c_1^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}(v_1) \\ -{\land}~ {c^\ast} = {{{\mathrm{f}}}_{N}(c_1)^\ast} \\ -\end{array} \\ -\end{array} -$$ - -\vspace{1ex} - -$$ -\begin{array}[t]{@{}lcl@{}l@{}} {{\mathrm{ivrelop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1, v_2) & = & {{{{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}^{{-1}}}}{({c^\ast})} & \quad \begin{array}[t]{@{}l@{}} \mbox{if}~ {c_1^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1) \\ @@ -8657,12 +8635,6 @@ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{\mathsf{all\_true}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v)} & = & {{\mathrm{ivtestop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{iall}}_{{\mathit{true}}}, v) \\ -\end{array} -$$ - -$$ -\begin{array}[t]{@{}lcl@{}l@{}} {\mathsf{eq}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1, v_2)} & = & {{\mathrm{ivrelop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{ieq}}, v_1, v_2) \\ {\mathsf{ne}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1, v_2)} & = & {{\mathrm{ivrelop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{ine}}, v_1, v_2) \\ {{\mathsf{lt}}{\mathsf{\_}}{{\mathit{sx}}}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1, v_2)} & = & {{\mathrm{ivrelopsx}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{ilt}}, {\mathit{sx}}, v_1, v_2) \\ @@ -10747,7 +10719,7 @@ $$ \begin{array}[t]{@{}lrcl@{}l@{}} -{[\textsc{\scriptsize E{-}vvtestop}]} \quad & (\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)~(\mathsf{v{\scriptstyle 128}} {.} \mathsf{any\_true}) & \hookrightarrow & (\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c) & \quad \mbox{if}~ c = {{\mathrm{ine}}}_{{|\mathsf{v{\scriptstyle 128}}|}}(c_1, 0) \\ +{[\textsc{\scriptsize E{-}vvtestop}]} \quad & (\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)~(\mathsf{v{\scriptstyle 128}} {.} \mathsf{any\_true}) & \hookrightarrow & (\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c) & \quad \mbox{if}~ c = {{\mathrm{inez}}}_{{|\mathsf{v{\scriptstyle 128}}|}}(c_1) \\ \end{array} $$ @@ -10782,7 +10754,11 @@ $$ \begin{array}[t]{@{}lrcl@{}l@{}} -{[\textsc{\scriptsize E{-}vtestop}]} \quad & (\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)~({\mathit{sh}} {.} {\mathit{vtestop}}) & \hookrightarrow & (\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~i) & \quad \mbox{if}~ i = {{\mathit{vtestop}}}{{}_{{\mathit{sh}}}(c_1)} \\ +{[\textsc{\scriptsize E{-}vtestop}]} \quad & (\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)~({{\mathsf{i}}{N}}{\mathsf{x}}{M} {.} \mathsf{all\_true}) & \hookrightarrow & (\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c) & \quad +\begin{array}[t]{@{}l@{}} +\mbox{if}~ {i^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(c_1) \\ +{\land}~ c = {\Pi}\, ({{{\mathrm{inez}}}_{N}(i)^\ast}) \\ +\end{array} \\ \end{array} $$
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 411691d..167b1ba 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md
@@ -4599,9 +4599,9 @@ def $ieqz_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 = 0))) ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec -def $iall_true_(N : N, iN : iN(N)) : u32 +def $inez_(N : N, iN : iN(N)) : u32 ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec - def $iall_true_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0))) + def $inez_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0))) ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec def $ieq_(N : N, iN : iN(N), iN : iN(N)) : u32 @@ -5027,20 +5027,6 @@ -- if (c*{c <- `c*`}*{`c*` <- `c**`} = $setproduct_(syntax lane_((Fnn : Fnn <: lanetype)), $f_($sizenn((Fnn : Fnn <: numtype)), c_1, c_2, c_3)*{c_1 <- `c_1*`, c_2 <- `c_2*`, c_3 <- `c_3*`})) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $ivtestop_(shape : shape, def $f_(N : N, iN : iN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $ivtestop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`})) - -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), v_1)) - -- if (c*{c <- `c*`} = $f_($lsizenn((Jnn : Jnn <: lanetype)), c_1)*{c_1 <- `c_1*`}) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $fvtestop_(shape : shape, def $f_(N : N, fN : fN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $fvtestop_{Fnn : Fnn, M : M, def $f_(N : N, fN : fN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`})) - -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), v_1)) - -- if (c*{c <- `c*`} = $f_($sizenn((Fnn : Fnn <: numtype)), c_1)*{c_1 <- `c_1*`}) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $ivrelop_(shape : shape, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $ivrelop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), `c*` : iN($lsizenn((Jnn : Jnn <: lanetype)))*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*, `c_2*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1, v_2) = $inv_lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c*{c <- `c*`}) @@ -5199,11 +5185,6 @@ def $vternop_{Fnn : Fnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), v_3 : vec_(V128_Vnn)}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), RELAXED_NMADD_vternop_, v_1, v_2, v_3) = $fvternop_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $frelaxed_nmadd_, v_1, v_2, v_3) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $vtestop_(shape : shape, vtestop_ : vtestop_(shape), vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $vtestop_{Jnn : Jnn, M : M, v : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_, v) = $ivtestop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $iall_true_, v) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $vrelop_(shape : shape, vrelop_ : vrelop_(shape), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $vrelop_{Jnn : Jnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), EQ_vrelop_, v_1, v_2) = $ivrelop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $ieq_, v_1, v_2) @@ -6211,7 +6192,7 @@ ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule vvtestop{c_1 : vec_(V128_Vnn), c : num_(I32_numtype)}: `%~>%`([VCONST_instr(V128_vectype, c_1) VVTESTOP_instr(V128_vectype, ANY_TRUE_vvtestop)], [CONST_instr(I32_numtype, c)]) - -- if (c = $ine_($vsize(V128_vectype), c_1, `%`_iN(0))) + -- if (c = $inez_($vsize(V128_vectype), c_1)) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule `vunop-val`{c_1 : vec_(V128_Vnn), sh : shape, vunop : vunop_(sh), c : vec_(V128_Vnn)}: @@ -6244,9 +6225,10 @@ -- if ($vternop_(sh, vternop, c_1, c_2, c_3) = []) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec - rule vtestop{c_1 : vec_(V128_Vnn), sh : shape, vtestop : vtestop_(sh), i : num_(I32_numtype)}: - `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(sh, vtestop)], [CONST_instr(I32_numtype, i)]) - -- if (i = $vtestop_(sh, vtestop, c_1)) + rule vtestop{c_1 : vec_(V128_Vnn), Jnn : Jnn, M : M, c : num_(I32_numtype), `i*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}: + `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_)], [CONST_instr(I32_numtype, c)]) + -- if (i*{i <- `i*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c_1)) + -- if (c!`%`_num_.0 = $prod($inez_($jsizenn(Jnn), i)!`%`_u32.0*{i <- `i*`})) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule vrelop{c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), sh : shape, vrelop : vrelop_(sh), c : vec_(V128_Vnn)}: @@ -15948,9 +15930,9 @@ def $ieqz_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 = 0))) ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec -def $iall_true_(N : N, iN : iN(N)) : u32 +def $inez_(N : N, iN : iN(N)) : u32 ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec - def $iall_true_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0))) + def $inez_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0))) ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec def $ieq_(N : N, iN : iN(N), iN : iN(N)) : u32 @@ -16376,20 +16358,6 @@ -- if (c*{c <- `c*`}*{`c*` <- `c**`} = $setproduct_(syntax lane_((Fnn : Fnn <: lanetype)), $f_($sizenn((Fnn : Fnn <: numtype)), c_1, c_2, c_3)*{c_1 <- `c_1*`, c_2 <- `c_2*`, c_3 <- `c_3*`})) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $ivtestop_(shape : shape, def $f_(N : N, iN : iN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $ivtestop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`})) - -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), v_1)) - -- if (c*{c <- `c*`} = $f_($lsizenn((Jnn : Jnn <: lanetype)), c_1)*{c_1 <- `c_1*`}) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $fvtestop_(shape : shape, def $f_(N : N, fN : fN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $fvtestop_{Fnn : Fnn, M : M, def $f_(N : N, fN : fN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`})) - -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), v_1)) - -- if (c*{c <- `c*`} = $f_($sizenn((Fnn : Fnn <: numtype)), c_1)*{c_1 <- `c_1*`}) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $ivrelop_(shape : shape, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $ivrelop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), `c*` : iN($lsizenn((Jnn : Jnn <: lanetype)))*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*, `c_2*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1, v_2) = $inv_lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c*{c <- `c*`}) @@ -16548,11 +16516,6 @@ def $vternop_{Fnn : Fnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), v_3 : vec_(V128_Vnn)}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), RELAXED_NMADD_vternop_, v_1, v_2, v_3) = $fvternop_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $frelaxed_nmadd_, v_1, v_2, v_3) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $vtestop_(shape : shape, vtestop_ : vtestop_(shape), vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $vtestop_{Jnn : Jnn, M : M, v : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_, v) = $ivtestop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $iall_true_, v) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $vrelop_(shape : shape, vrelop_ : vrelop_(shape), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $vrelop_{Jnn : Jnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), EQ_vrelop_, v_1, v_2) = $ivrelop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $ieq_, v_1, v_2) @@ -17562,7 +17525,7 @@ ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule vvtestop{c_1 : vec_(V128_Vnn), c : num_(I32_numtype)}: `%~>%`([VCONST_instr(V128_vectype, c_1) VVTESTOP_instr(V128_vectype, ANY_TRUE_vvtestop)], [CONST_instr(I32_numtype, c)]) - -- if (c = $ine_($vsize(V128_vectype), c_1, `%`_iN(0))) + -- if (c = $inez_($vsize(V128_vectype), c_1)) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule `vunop-val`{c_1 : vec_(V128_Vnn), sh : shape, vunop : vunop_(sh), c : vec_(V128_Vnn)}: @@ -17595,9 +17558,10 @@ -- if ($vternop_(sh, vternop, c_1, c_2, c_3) = []) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec - rule vtestop{c_1 : vec_(V128_Vnn), sh : shape, vtestop : vtestop_(sh), i : num_(I32_numtype)}: - `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(sh, vtestop)], [CONST_instr(I32_numtype, i)]) - -- if (i = $vtestop_(sh, vtestop, c_1)) + rule vtestop{c_1 : vec_(V128_Vnn), Jnn : Jnn, M : M, c : num_(I32_numtype), `i*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}: + `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_)], [CONST_instr(I32_numtype, c)]) + -- if (i*{i <- `i*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c_1)) + -- if (c!`%`_num_.0 = $prod($inez_($jsizenn(Jnn), i)!`%`_u32.0*{i <- `i*`})) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule vrelop{c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), sh : shape, vrelop : vrelop_(sh), c : vec_(V128_Vnn)}: @@ -27423,9 +27387,9 @@ def $ieqz_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 = 0))) ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec -def $iall_true_(N : N, iN : iN(N)) : u32 +def $inez_(N : N, iN : iN(N)) : u32 ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec - def $iall_true_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0))) + def $inez_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0))) ;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec def $ieq_(N : N, iN : iN(N), iN : iN(N)) : u32 @@ -27851,20 +27815,6 @@ -- if (c*{c <- `c*`}*{`c*` <- `c**`} = $setproduct_(syntax lane_((Fnn : Fnn <: lanetype)), $f_($sizenn((Fnn : Fnn <: numtype)), c_1, c_2, c_3)*{c_1 <- `c_1*`, c_2 <- `c_2*`, c_3 <- `c_3*`})) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $ivtestop_(shape : shape, def $f_(N : N, iN : iN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $ivtestop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`})) - -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), v_1)) - -- if (c*{c <- `c*`} = $f_($lsizenn((Jnn : Jnn <: lanetype)), c_1)*{c_1 <- `c_1*`}) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $fvtestop_(shape : shape, def $f_(N : N, fN : fN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $fvtestop_{Fnn : Fnn, M : M, def $f_(N : N, fN : fN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`})) - -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), v_1)) - -- if (c*{c <- `c*`} = $f_($sizenn((Fnn : Fnn <: numtype)), c_1)*{c_1 <- `c_1*`}) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $ivrelop_(shape : shape, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $ivrelop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), `c*` : iN($lsizenn((Jnn : Jnn <: lanetype)))*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*, `c_2*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1, v_2) = $inv_lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c*{c <- `c*`}) @@ -28023,11 +27973,6 @@ def $vternop_{Fnn : Fnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), v_3 : vec_(V128_Vnn)}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), RELAXED_NMADD_vternop_, v_1, v_2, v_3) = $fvternop_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $frelaxed_nmadd_, v_1, v_2, v_3) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec -def $vtestop_(shape : shape, vtestop_ : vtestop_(shape), vec_ : vec_(V128_Vnn)) : u32 - ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec - def $vtestop_{Jnn : Jnn, M : M, v : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_, v) = $ivtestop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $iall_true_, v) - -;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $vrelop_(shape : shape, vrelop_ : vrelop_(shape), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec def $vrelop_{Jnn : Jnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), EQ_vrelop_, v_1, v_2) = $ivrelop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $ieq_, v_1, v_2) @@ -29052,7 +28997,7 @@ ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule vvtestop{c_1 : vec_(V128_Vnn), c : num_(I32_numtype)}: `%~>%`([VCONST_instr(V128_vectype, c_1) VVTESTOP_instr(V128_vectype, ANY_TRUE_vvtestop)], [CONST_instr(I32_numtype, c)]) - -- if (c = $ine_($vsize(V128_vectype), c_1, `%`_iN(0))) + -- if (c = $inez_($vsize(V128_vectype), c_1)) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule `vunop-val`{c_1 : vec_(V128_Vnn), sh : shape, vunop : vunop_(sh), c : vec_(V128_Vnn)}: @@ -29088,9 +29033,10 @@ -- if ($vternop_(sh, vternop, c_1, c_2, c_3) = []) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec - rule vtestop{c_1 : vec_(V128_Vnn), sh : shape, vtestop : vtestop_(sh), i : num_(I32_numtype)}: - `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(sh, vtestop)], [CONST_instr(I32_numtype, i)]) - -- if (i = $vtestop_(sh, vtestop, c_1)) + rule vtestop{c_1 : vec_(V128_Vnn), Jnn : Jnn, M : M, c : num_(I32_numtype), `i*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}: + `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_)], [CONST_instr(I32_numtype, c)]) + -- if (i*{i <- `i*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c_1)) + -- if (c!`%`_num_.0 = $prod($inez_($jsizenn(Jnn), i)!`%`_u32.0*{i <- `i*`})) ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule vrelop{c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), sh : shape, vrelop : vrelop_(sh), c : vec_(V128_Vnn)}:
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index adf3fc7..03a8738 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md
@@ -18740,7 +18740,7 @@ #. Pop the value :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)` from the stack. -#. Let :math:`c` be :math:`{{\mathrm{ine}}}_{{|\mathsf{v{\scriptstyle 128}}|}}(c_1, 0)`. +#. Let :math:`c` be :math:`{{\mathrm{inez}}}_{{|\mathsf{v{\scriptstyle 128}}|}}(c_1)`. #. Push the value :math:`(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c)` to the stack. @@ -18808,17 +18808,19 @@ #. Push the value :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c)` to the stack. -:math:`{\mathit{sh}} {.} {\mathit{vtestop}}` -............................................ +:math:`{{\mathsf{i}}{N}}{\mathsf{x}}{M} {.} \mathsf{all\_true}` +............................................................... 1. Assert: Due to validation, a value of vector type :math:`\mathsf{v{\scriptstyle 128}}` is on the top of the stack. #. Pop the value :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)` from the stack. -#. Let :math:`i` be :math:`{{\mathit{vtestop}}}{{}_{{\mathit{sh}}}(c_1)}`. +#. Let :math:`{i^\ast}` be :math:`{{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(c_1)`. -#. Push the value :math:`(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~i)` to the stack. +#. Let :math:`c` be :math:`{\Pi}\, {{{\mathrm{inez}}}_{N}(i)^\ast}`. + +#. Push the value :math:`(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c)` to the stack. :math:`{\mathit{sh}} {.} {\mathit{vrelop}}` @@ -23964,8 +23966,8 @@ 1. Return :math:`\mathbb{B}(i_1 = 0)`. -:math:`{{\mathrm{iall\_true}}}_{N}(i_1)` -........................................ +:math:`{{\mathrm{inez}}}_{N}(i_1)` +.................................. 1. Return :math:`\mathbb{B}(i_1 \neq 0)`. @@ -24613,40 +24615,6 @@ #. Return :math:`{{{{{\mathrm{lanes}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}^{{-1}}}}{({c^\ast})}^\ast}`. -:math:`{{\mathrm{ivtestop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1)` -................................................................................... - - -1. Let :math:`{c_1^\ast}` be :math:`{{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1)`. - -#. Let :math:`{c^\ast}` be :math:`\epsilon`. - -#. For each :math:`c_1` in :math:`{c_1^\ast}`, do: - - a. Let :math:`c` be :math:`{{\mathrm{f}}}_{N}(c_1)`. - - #. Append :math:`c` to :math:`{c^\ast}`. - -#. Return :math:`{\Pi}\, {c^\ast}`. - - -:math:`{{\mathrm{fvtestop}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1)` -................................................................................... - - -1. Let :math:`{c_1^\ast}` be :math:`{{\mathrm{lanes}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}(v_1)`. - -#. Let :math:`{c^\ast}` be :math:`\epsilon`. - -#. For each :math:`c_1` in :math:`{c_1^\ast}`, do: - - a. Let :math:`c` be :math:`{{\mathrm{f}}}_{N}(c_1)`. - - #. Append :math:`c` to :math:`{c^\ast}`. - -#. Return :math:`{\Pi}\, {c^\ast}`. - - :math:`{{\mathrm{ivrelop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1, v_2)` ....................................................................................... @@ -24989,13 +24957,6 @@ #. Return :math:`{{\mathrm{fvternop}}}_{{{\mathit{lanetype}}}{\mathsf{x}}{M}}({\mathrm{frelaxed}}_{{\mathit{nmadd}}}, v_1, v_2, v_3)`. -:math:`{\mathsf{all\_true}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v)}` -...................................................................... - - -1. Return :math:`{{\mathrm{ivtestop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{iall}}_{{\mathit{true}}}, v)`. - - :math:`{{\mathit{vrelop}}}{{}_{{{\mathit{lanetype}}}{\mathsf{x}}{M}}(v_1, v_2)}` ................................................................................ @@ -29296,7 +29257,7 @@ Step_pure/vvtestop V128 ANY_TRUE 1. Assert: Due to validation, a value of value type V128 is on the top of the stack. 2. Pop the value (V128.CONST c_1) from the stack. -3. Let c be $ine_($vsize(V128), c_1, 0). +3. Let c be $inez_($vsize(V128), c_1). 4. Push the value (I32.CONST c) to the stack. Step_pure/vunop sh vunop @@ -29329,11 +29290,12 @@ 8. Let c be an element of $vternop_(sh, vternop, c_1, c_2, c_3). 9. Push the value (V128.CONST c) to the stack. -Step_pure/vtestop sh vtestop +Step_pure/vtestop Jnn X M ALL_TRUE 1. Assert: Due to validation, a value of value type V128 is on the top of the stack. 2. Pop the value (V128.CONST c_1) from the stack. -3. Let i be $vtestop_(sh, vtestop, c_1). -4. Push the value (I32.CONST i) to the stack. +3. Let i* be $lanes_(Jnn X M, c_1). +4. Let c be $prod($inez_($jsizenn(Jnn), i)*). +5. Push the value (I32.CONST c) to the stack. Step_pure/vrelop sh vrelop 1. Assert: Due to validation, a value of value type V128 is on the top of the stack. @@ -31752,7 +31714,7 @@ ieqz_ N i_1 1. Return $bool((i_1 = 0)). -iall_true_ N i_1 +inez_ N i_1 1. Return $bool((i_1 =/= 0)). ieq_ N i_1 i_2 @@ -32062,22 +32024,6 @@ 4. Let c** be $setproduct_(`lane_((Fnn : Fnn <: lanetype)), $f_($sizenn(Fnn), c_1, c_2, c_3)*). 5. Return $inv_lanes_(Fnn X M, c*)*. -ivtestop_ Jnn X M $f_ v_1 -1. Let c_1* be $lanes_(Jnn X M, v_1). -2. Let c* be []. -3. For each c_1 in c_1*, do: - a. Let c be $f_($lsizenn(Jnn), c_1). - b. Append c to the c*. -4. Return $prod(c*). - -fvtestop_ Fnn X M $f_ v_1 -1. Let c_1* be $lanes_(Fnn X M, v_1). -2. Let c* be []. -3. For each c_1 in c_1*, do: - a. Let c be $f_($sizenn(Fnn), c_1). - b. Append c to the c*. -4. Return $prod(c*). - ivrelop_ Jnn X M $f_ v_1 v_2 1. Let c_1* be $lanes_(Jnn X M, v_1). 2. Let c_2* be $lanes_(Jnn X M, v_2). @@ -32242,9 +32188,6 @@ 4. Assert: Due to validation, (vternop_ = RELAXED_NMADD). 5. Return $fvternop_(lanetype X M, $frelaxed_nmadd_, v_1, v_2, v_3). -vtestop_ Jnn X M ALL_TRUE v -1. Return $ivtestop_(Jnn X M, $iall_true_, v). - vrelop_ lanetype X M vrelop_ v_1 v_2 1. If lanetype is Jnn, then: a. If (vrelop_ = EQ), then:
diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 617e983..bfcc596 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md
@@ -1625,7 +1625,6 @@ warning: definition `fvbinop_` was never spliced warning: definition `fvrelop_` was never spliced warning: definition `fvternop_` was never spliced -warning: definition `fvtestop_` was never spliced warning: definition `fvunop_` was never spliced warning: definition `fzero` was never spliced warning: definition `global` was never spliced @@ -1641,7 +1640,6 @@ warning: definition `iabs_` was never spliced warning: definition `iadd_` was never spliced warning: definition `iadd_sat_` was never spliced -warning: definition `iall_true_` was never spliced warning: definition `iand_` was never spliced warning: definition `iandnot_` was never spliced warning: definition `iavgr_` was never spliced @@ -1665,6 +1663,7 @@ warning: definition `imul_` was never spliced warning: definition `ine_` was never spliced warning: definition `ineg_` was never spliced +warning: definition `inez_` was never spliced warning: definition `inot_` was never spliced warning: definition `inst_globaltype` was never spliced warning: definition `inst_memtype` was never spliced @@ -1724,7 +1723,6 @@ warning: definition `ivshufflop_` was never spliced warning: definition `ivswizzlop_` was never spliced warning: definition `ivternopnd_` was never spliced -warning: definition `ivtestop_` was never spliced warning: definition `ivunop_` was never spliced warning: definition `ixor_` was never spliced warning: definition `jsize` was never spliced @@ -1862,7 +1860,6 @@ warning: definition `vsizenn` was never spliced warning: definition `vswizzlop_` was never spliced warning: definition `vternop_` was never spliced -warning: definition `vtestop_` was never spliced warning: definition `vunop_` was never spliced warning: definition `vunpack` was never spliced warning: definition `vvbinop_` was never spliced @@ -2472,7 +2469,6 @@ warning: definition prose `fvbinop_` was never spliced warning: definition prose `fvrelop_` was never spliced warning: definition prose `fvternop_` was never spliced -warning: definition prose `fvtestop_` was never spliced warning: definition prose `fvunop_` was never spliced warning: definition prose `fzero` was never spliced warning: definition prose `global` was never spliced @@ -2488,7 +2484,6 @@ warning: definition prose `iabs_` was never spliced warning: definition prose `iadd_` was never spliced warning: definition prose `iadd_sat_` was never spliced -warning: definition prose `iall_true_` was never spliced warning: definition prose `idiv_` was never spliced warning: definition prose `ieq_` was never spliced warning: definition prose `ieqz_` was never spliced @@ -2503,6 +2498,7 @@ warning: definition prose `imul_` was never spliced warning: definition prose `ine_` was never spliced warning: definition prose `ineg_` was never spliced +warning: definition prose `inez_` was never spliced warning: definition prose `inst_globaltype` was never spliced warning: definition prose `inst_memtype` was never spliced warning: definition prose `inst_reftype` was never spliced @@ -2539,7 +2535,6 @@ warning: definition prose `ivshufflop_` was never spliced warning: definition prose `ivswizzlop_` was never spliced warning: definition prose `ivternopnd_` was never spliced -warning: definition prose `ivtestop_` was never spliced warning: definition prose `ivunop_` was never spliced warning: definition prose `jsize` was never spliced warning: definition prose `jsizenn` was never spliced @@ -2666,7 +2661,6 @@ warning: definition prose `vsizenn` was never spliced warning: definition prose `vswizzlop_` was never spliced warning: definition prose `vternop_` was never spliced -warning: definition prose `vtestop_` was never spliced warning: definition prose `vunop_` was never spliced warning: definition prose `vunpack` was never spliced warning: definition prose `vvbinop_` was never spliced