Refactor extops

document/core/util/macros.def

@@ -476,6 +476,8 @@
 
 .. |S| mathdef:: \xref{syntax/instructions}{syntax-sx}{\K{s}}
 .. |U| mathdef:: \xref{syntax/instructions}{syntax-sx}{\K{u}}
+.. |VS| mathdef:: \xref{syntax/instructions}{syntax-sx}{\K{s}}
+.. |VU| mathdef:: \xref{syntax/instructions}{syntax-sx}{\K{u}}
 
 .. |OFFSET| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{offset}}
 .. |ALIGN| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{align}}

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

@@ -330,11 +330,11 @@ syntax vshiftop_(Jnn X N) = SHL | SHR sx
 
 syntax vextunop_(ishape)
 syntax vextunop_(Jnn X N) =
-  | EXTADD_PAIRWISE  -- if `16 <= $sizemm(Jnn) <= `32
+  | EXTADD_PAIRWISE sx -- if `16 <= $sizemm(Jnn) <= `32
 syntax vextbinop_(ishape)
 syntax vextbinop_(Jnn X N) =
-  | EXTMUL half      hint(show EXTMUL#_#%)
-  | DOT              -- if $sizemm(Jnn) = `32
+  | EXTMUL sx half     hint(show EXTMUL#_#%)
+  | DOT S              -- if $sizemm(Jnn) = `32
 
 
 ;; Memory operators
@@ -418,13 +418,12 @@ syntax instr/vec hint(desc "vector instruction") = ...
   | VEXTRACT_LANE shape sx? laneidx     hint(show %.EXTRACT_LANE_#% %)
     -- if $lanetype(shape) = numtype <=> sx? = eps
   | VREPLACE_LANE shape laneidx         hint(show %.REPLACE_LANE %)
-  | VEXTUNOP ishape_1 ishape_2 vextunop_(ishape_1) sx
+  | VEXTUNOP ishape_1 ishape_2 vextunop_(ishape_1)
     hint(show %1.%3#_#%2#_#%4)
     -- if $($lsize($lanetype(ishape_1)) = 2*$lsize($lanetype(ishape_2)))
-  | VEXTBINOP ishape_1 ishape_2 vextbinop_(ishape_1) sx
+  | VEXTBINOP ishape_1 ishape_2 vextbinop_(ishape_1)
     hint(show %1.%3#_#%2#_#%4)
     -- if $($lsize($lanetype(ishape_1)) = 2*$lsize($lanetype(ishape_2)))
-    ;; TODO: /\ (vextbinop =/= DOT \/ sx = S)
   | VNARROW ishape_1 ishape_2 sx        hint(show %.NARROW#_#%#_#%)
     -- if $($lsize($lanetype(ishape_2)) = 2*$lsize($lanetype(ishape_1)) <= 32)
   | VCVTOP shape shape vcvtop half? sx? zero?

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

@@ -413,24 +413,24 @@ def $vcvtop(F64 X N_1, F32 X N_2, DEMOTE, sx?, f64) = f32
 def $vcvtop(F32 X N_1, F64 X N_2, PROMOTE, sx?, f32) = f64
     -- if f64 = $promote(32, 64, f32)
 
-def $vextunop(ishape_1, ishape_2, vextunop_(ishape_1), sx, vec_(V128)) : vec_(V128)
+def $vextunop(ishape_1, ishape_2, vextunop_(ishape_1), vec_(V128)) : vec_(V128)
     hint(show %3#$_((%1,%2))^(%5)#((%6)))
-def $vextbinop(ishape_1, ishape_2, vextbinop_(ishape_1), sx, vec_(V128), vec_(V128)) : vec_(V128)
+def $vextbinop(ishape_1, ishape_2, vextbinop_(ishape_1), vec_(V128), vec_(V128)) : vec_(V128)
     hint(show %3#$_((%1,%2))^(%5)#((%6,%7)))
 
-def $vextunop(Inn_1 X N_1, Inn_2 X N_2, EXTADD_PAIRWISE, sx, c_1) = c
+def $vextunop(Inn_1 X N_1, Inn_2 X N_2, EXTADD_PAIRWISE sx, c_1) = c
   -- var cj_1 : iN($lsize(Inn_1))
   -- var cj_2 : iN($lsize(Inn_1))
   -- if ci* = $lanes_(Inn_2 X N_2, c_1)
   -- if $concat_(iN($lsize(Inn_1)), (cj_1 cj_2)*) = $ext($lsize(Inn_2), $lsize(Inn_1), sx, ci)*
   -- if c = $invlanes_(Inn_1 X N_1, $iadd($lsize(Inn_1), cj_1, cj_2)*)
 
-def $vextbinop(Inn_1 X N_1, Inn_2 X N_2, EXTMUL hf, sx, c_1, c_2) = c
+def $vextbinop(Inn_1 X N_1, Inn_2 X N_2, EXTMUL sx hf, c_1, c_2) = c
   -- if ci_1* = $lanes_(Inn_2 X N_2, c_1)[$halfop(hf, 0, N_1) : N_1]
   -- if ci_2* = $lanes_(Inn_2 X N_2, c_2)[$halfop(hf, 0, N_1) : N_1]
   -- if c = $invlanes_(Inn_1 X N_1, $imul($lsize(Inn_1), $ext($lsize(Inn_2), $lsize(Inn_1), sx, ci_1), $ext($lsize(Inn_2), $lsize(Inn_1), sx, ci_2))*)
 
-def $vextbinop(Inn_1 X N_1, Inn_2 X N_2, DOT, sx, c_1, c_2) = c
+def $vextbinop(Inn_1 X N_1, Inn_2 X N_2, DOT S, c_1, c_2) = c
   -- var cj_1 : iN($lsize(Inn_1))
   -- var cj_2 : iN($lsize(Inn_1))
   -- if ci_1* = $lanes_(Inn_2 X N_2, c_1)

spectec/spec/wasm-2.0/6-typing.watsup

@@ -344,10 +344,10 @@ rule Instr_ok/vreplace_lane:
   -- if i < $dim(sh)
 
 rule Instr_ok/vextunop:
-  C |- VEXTUNOP sh_1 sh_2 vextunop sx : V128 -> V128
+  C |- VEXTUNOP sh_1 sh_2 vextunop : V128 -> V128
 
 rule Instr_ok/vextbinop:
-  C |- VEXTBINOP sh_1 sh_2 vextbinop sx : V128 V128 -> V128
+  C |- VEXTBINOP sh_1 sh_2 vextbinop : V128 V128 -> V128
 
 rule Instr_ok/vnarrow:
   C |- VNARROW sh_1 sh_2 sx : V128 V128 -> V128

spectec/spec/wasm-2.0/8-reduction.watsup

@@ -328,13 +328,13 @@ rule Step_pure/vreplace_lane:
 
 
 rule Step_pure/vextunop:
-  (VCONST V128 c_1) (VEXTUNOP sh_1 sh_2 vextunop sx) ~> (VCONST V128 c)
-  -- if $vextunop(sh_1, sh_2, vextunop, sx, c_1) = c
+  (VCONST V128 c_1) (VEXTUNOP sh_1 sh_2 vextunop) ~> (VCONST V128 c)
+  -- if $vextunop(sh_1, sh_2, vextunop, c_1) = c
 
 
 rule Step_pure/vextbinop:
-  (VCONST V128 c_1) (VCONST V128 c_2) (VEXTBINOP sh_1 sh_2 vextbinop sx) ~> (VCONST V128 c)
-  -- if $vextbinop(sh_1, sh_2, vextbinop, sx, c_1, c_2) = c
+  (VCONST V128 c_1) (VCONST V128 c_2) (VEXTBINOP sh_1 sh_2 vextbinop) ~> (VCONST V128 c)
+  -- if $vextbinop(sh_1, sh_2, vextbinop, c_1, c_2) = c
 
 
 rule Step_pure/vnarrow:

spectec/spec/wasm-2.0/A-binary.watsup

@@ -616,8 +616,8 @@ grammar Binstr/vector-v-i8x16 : instr = ...
   | ...
 
 grammar Binstr/vector-v-i16x8 : instr = ...
-  | 0xFD 124:Bu32 => VEXTUNOP (I16 X 8) (I8 X 16) EXTADD_PAIRWISE S
-  | 0xFD 125:Bu32 => VEXTUNOP (I16 X 8) (I8 X 16) EXTADD_PAIRWISE U
+  | 0xFD 124:Bu32 => VEXTUNOP (I16 X 8) (I8 X 16) (EXTADD_PAIRWISE S)
+  | 0xFD 125:Bu32 => VEXTUNOP (I16 X 8) (I8 X 16) (EXTADD_PAIRWISE U)
   | 0xFD 128:Bu32 => VUNOP (I16 X 8) ABS
   | 0xFD 129:Bu32 => VUNOP (I16 X 8) NEG
   | 0xFD 130:Bu32 => VBINOP (I16 X 8) Q15MULR_SAT_S
@@ -644,15 +644,15 @@ grammar Binstr/vector-v-i16x8 : instr = ...
   | 0xFD 152:Bu32 => VBINOP (I16 X 8) (MAX S)
   | 0xFD 153:Bu32 => VBINOP (I16 X 8) (MAX U)
   | 0xFD 155:Bu32 => VBINOP (I16 X 8) AVGR_U
-  | 0xFD 156:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL LOW) S
-  | 0xFD 157:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL HIGH) S
-  | 0xFD 158:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL LOW) U
-  | 0xFD 159:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL HIGH) U
+  | 0xFD 156:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL S LOW)
+  | 0xFD 157:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL S HIGH)
+  | 0xFD 158:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL U LOW)
+  | 0xFD 159:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL U HIGH)
   | ...
 
 grammar Binstr/vector-v-i32x4 : instr = ...
-  | 0xFD 126:Bu32 => VEXTUNOP (I32 X 4) (I16 X 8) EXTADD_PAIRWISE S
-  | 0xFD 127:Bu32 => VEXTUNOP (I32 X 4) (I16 X 8) EXTADD_PAIRWISE U
+  | 0xFD 126:Bu32 => VEXTUNOP (I32 X 4) (I16 X 8) (EXTADD_PAIRWISE S)
+  | 0xFD 127:Bu32 => VEXTUNOP (I32 X 4) (I16 X 8) (EXTADD_PAIRWISE U)
   | 0xFD 160:Bu32 => VUNOP (I32 X 4) ABS
   | 0xFD 161:Bu32 => VUNOP (I32 X 4) NEG
   | 0xFD 163:Bu32 => VTESTOP (I32 X 4) ALL_TRUE
@@ -671,11 +671,11 @@ grammar Binstr/vector-v-i32x4 : instr = ...
   | 0xFD 183:Bu32 => VBINOP (I32 X 4) (MIN U)
   | 0xFD 184:Bu32 => VBINOP (I32 X 4) (MAX S)
   | 0xFD 185:Bu32 => VBINOP (I32 X 4) (MAX U)
-  | 0xFD 186:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) DOT S
-  | 0xFD 188:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL LOW) S
-  | 0xFD 189:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL HIGH) S
-  | 0xFD 190:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL LOW) U
-  | 0xFD 191:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL HIGH) U
+  | 0xFD 186:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (DOT S)
+  | 0xFD 188:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL S LOW)
+  | 0xFD 189:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL S HIGH)
+  | 0xFD 190:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL U LOW)
+  | 0xFD 191:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL U HIGH)
   | ...
 
 grammar Binstr/vector-v-i64x2 : instr = ...
@@ -693,10 +693,10 @@ grammar Binstr/vector-v-i64x2 : instr = ...
   | 0xFD 206:Bu32 => VBINOP (I64 X 2) ADD
   | 0xFD 209:Bu32 => VBINOP (I64 X 2) SUB
   | 0xFD 213:Bu32 => VBINOP (I64 X 2) MUL
-  | 0xFD 220:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL LOW) S
-  | 0xFD 221:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL HIGH) S
-  | 0xFD 222:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL LOW) U
-  | 0xFD 223:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL HIGH) U
+  | 0xFD 220:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL S LOW)
+  | 0xFD 221:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL S HIGH)
+  | 0xFD 222:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL U LOW)
+  | 0xFD 223:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL U HIGH)
   | ...
 
 grammar Binstr/vector-v-f32x4 : instr = ...

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

@@ -408,8 +408,8 @@ syntax vbinop_(Jnn X M) =
   | ADD_SAT sx hint(show ADD_SAT#_#%)      -- if $lsizenn(Jnn) <= `16
   | SUB_SAT sx hint(show SUB_SAT#_#%)      -- if $lsizenn(Jnn) <= `16
   | MUL                                    -- if $lsizenn(Jnn) >= `16
-  | AVGR_U                                 -- if $lsizenn(Jnn) <= `16
-  | Q15MULR_SAT_S                          -- if $lsizenn(Jnn) = `16
+  | AVGR_U                                 -- if $lsizenn(Jnn) <= `16  ;; TODO(2, rossberg): AVGR U
+  | Q15MULR_SAT_S                          -- if $lsizenn(Jnn) = `16   ;; TODO(2, rossberg): Q15MULR_SAT S
   | MIN sx hint(show MIN#_#%)              -- if $lsizenn(Jnn) <= `32
   | MAX sx hint(show MAX#_#%)              -- if $lsizenn(Jnn) <= `32
 syntax vbinop_(Fnn X M) = ADD | SUB | MUL | DIV | MIN | MAX | PMIN | PMAX
@@ -449,12 +449,15 @@ syntax vshiftop_(Jnn X M) = SHL | SHR sx hint(show SHR#_#%)
 
 syntax vextunop_(ishape_1, ishape_2) hint(show vextunop_((%,%))) hint(macro "%" "V%")
 syntax vextunop_(Jnn_1 X M_1, Jnn_2 X M_2) =
-  | EXTADD_PAIRWISE  -- if 16 <= $(2 * $lsizenn1(Jnn_1)) = $lsizenn2(Jnn_2) <= `32
+  | EXTADD_PAIRWISE sx hint(show EXTADD_PAIRWISE#_#%)
+    -- if 16 <= $(2 * $lsizenn1(Jnn_1)) = $lsizenn2(Jnn_2) <= `32
 
 syntax vextbinop_(ishape_1, ishape_2) hint(show vextbinop_((%,%))) hint(macro "%" "V%")
 syntax vextbinop_(Jnn_1 X M_1, Jnn_2 X M_2) =
-  | EXTMUL half_(Jnn_1 X M_1, Jnn_2 X M_2) hint(show EXTMUL#_#%) -- if $(2 * $lsizenn1(Jnn_1)) = $lsizenn2(Jnn_2) >= `16
-  | DOT                                                          -- if $(2 * $lsizenn1(Jnn_1)) = $lsizenn2(Jnn_2) = `32
+  | EXTMUL sx half_(Jnn_1 X M_1, Jnn_2 X M_2) hint(show EXTMUL#_#%#_#%)
+    -- if $(2 * $lsizenn1(Jnn_1)) = $lsizenn2(Jnn_2) >= `16
+  | DOT S hint(show DOT#_#%)
+    -- if $(2 * $lsizenn1(Jnn_1)) = $lsizenn2(Jnn_2) = `32
 
 
 ;; Memory operators
@@ -543,13 +546,10 @@ syntax instr/vec hint(desc "vector instruction") = ...
   | VSHUFFLE ishape laneidx*            hint(show ##%.SHUFFLE %) hint(macro "VSHUFFLE")
     -- if ishape = I8 X `16 /\ |laneidx*| = `16
     ;; TODO(3, rossberg): enable ^16 in type
-  | VEXTUNOP ishape_1 ishape_2 vextunop_(ishape_2, ishape_1) sx
-    hint(show ##%1.##%3#_# ##%2#_#%4)
-    -- if $($lsize($lanetype(ishape_1)) = 2*$lsize($lanetype(ishape_2)))
-  | VEXTBINOP ishape_1 ishape_2 vextbinop_(ishape_2, ishape_1) sx
-    hint(show ##%1.##%3#_# ##%2#_#%4)
-    -- if $($lsize($lanetype(ishape_1)) = 2*$lsize($lanetype(ishape_2)))
-    ;; TODO(1, rossberg): /\ (vextbinop =/= DOT \/ sx = S)
+  | VEXTUNOP ishape_1 ishape_2 vextunop_(ishape_2, ishape_1)
+    hint(show ##%1.##%3#_# ##%2)
+  | VEXTBINOP ishape_1 ishape_2 vextbinop_(ishape_2, ishape_1)
+    hint(show ##%1.##%3#_# ##%2)
   | VNARROW ishape_1 ishape_2 sx        hint(show ##%.NARROW#_# ##%#_#%) hint(macro "VNARROW")
     -- if $($lsize($lanetype(ishape_2)) = 2*$lsize($lanetype(ishape_1)) <= `32)
   | VCVTOP shape_1 shape_2 vcvtop_(shape_2, shape_1) half_(shape_2, shape_1)? sx? zero_(shape_2, shape_1)?

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

@@ -373,9 +373,9 @@ def $free_instr(VSHIFTOP ishape vshiftop) = $free_shape(ishape)
 def $free_instr(VBITMASK ishape) = $free_shape(ishape)
 def $free_instr(VSWIZZLE ishape) = $free_shape(ishape)
 def $free_instr(VSHUFFLE ishape laneidx*) = $free_shape(ishape)
-def $free_instr(VEXTUNOP ishape_1 ishape_2 vextunop sx) =
+def $free_instr(VEXTUNOP ishape_1 ishape_2 vextunop) =
   $free_shape(ishape_1) ++ $free_shape(ishape_2)
-def $free_instr(VEXTBINOP ishape_1 ishape_2 vextbinop sx) =
+def $free_instr(VEXTBINOP ishape_1 ishape_2 vextbinop) =
   $free_shape(ishape_1) ++ $free_shape(ishape_2)
 def $free_instr(VNARROW ishape_1 ishape_2 sx) =
   $free_shape(ishape_1) ++ $free_shape(ishape_2)

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

@@ -19,7 +19,7 @@ def $invsigned(N, i) = j        -- if $signed(N, j) = i
 
 ;; TODO(3, all): implement numerics internally
 
-;; TODO(2, rossberg): show as function ids, not var ids
+;; TODO(2, rossberg): show as function ids, not var ids (similarly below)
 def $unop(numtype, unop_(numtype), num_(numtype)) : num_(numtype)*
     hint(show %2#$_(%1)#((%3)))
 def $binop(numtype, binop_(numtype), num_(numtype), num_(numtype)) : num_(numtype)*
@@ -430,24 +430,24 @@ def $vcvtop(F64 X N_1, F32 X N_2, DEMOTE, sx?, f64) = f32
 def $vcvtop(F32 X N_1, F64 X N_2, PROMOTE, sx?, f32) = f64
     -- if f64 = $promote(32, 64, f32)
 
-def $vextunop(ishape_1, ishape_2, vextunop_(ishape_1, ishape_2), sx, vec_(V128)) : vec_(V128)
-    hint(show %3#$_((%1,%2))^(%5)#((%6)))
-def $vextbinop(ishape_1, ishape_2, vextbinop_(ishape_1, ishape_2), sx, vec_(V128), vec_(V128)) : vec_(V128)
-    hint(show %3#$_((%1,%2))^(%5)#((%6,%7)))
+def $vextunop(ishape_1, ishape_2, vextunop_(ishape_1, ishape_2), vec_(V128)) : vec_(V128)
+    hint(show %3#$_((%1,%2),%4))
+def $vextbinop(ishape_1, ishape_2, vextbinop_(ishape_1, ishape_2), vec_(V128), vec_(V128)) : vec_(V128)
+    hint(show %3#$_((%1,%2),%4,%5))
 
-def $vextunop(Jnn_1 X N_1, Jnn_2 X N_2, EXTADD_PAIRWISE, sx, c_1) = c
+def $vextunop(Jnn_1 X N_1, Jnn_2 X N_2, EXTADD_PAIRWISE sx, c_1) = c
   -- var cj_1 : iN($lsize(Jnn_2))
   -- var cj_2 : iN($lsize(Jnn_2))
   -- if ci* = $lanes_(Jnn_1 X N_1, c_1)
   -- if $concat_(iN($lsize(Jnn_2)), (cj_1 cj_2)*) = $ext($lsize(Jnn_1), $lsize(Jnn_2), sx, ci)*
   -- if c = $invlanes_(Jnn_2 X N_2, $iadd($lsize(Jnn_2), cj_1, cj_2)*)
 
-def $vextbinop(Jnn_1 X N_1, Jnn_2 X N_2, EXTMUL half, sx, c_1, c_2) = c
+def $vextbinop(Jnn_1 X N_1, Jnn_2 X N_2, EXTMUL sx half, c_1, c_2) = c
   -- if ci_1* = $lanes_(Jnn_1 X N_1, c_1)[$half(Jnn_1 X N_1, Jnn_2 X N_2, half, 0, N_2) : N_2]
   -- if ci_2* = $lanes_(Jnn_1 X N_1, c_2)[$half(Jnn_1 X N_1, Jnn_2 X N_2, half, 0, N_2) : N_2]
   -- if c = $invlanes_(Jnn_2 X N_2, $imul($lsize(Jnn_2), $ext($lsize(Jnn_1), $lsize(Jnn_2), sx, ci_1), $ext($lsize(Jnn_1), $lsize(Jnn_2), sx, ci_2))*)
 
-def $vextbinop(Jnn_1 X N_1, Jnn_2 X N_2, DOT, sx, c_1, c_2) = c
+def $vextbinop(Jnn_1 X N_1, Jnn_2 X N_2, DOT S, c_1, c_2) = c
   -- var cj_1 : iN($lsize(Jnn_2))
   -- var cj_2 : iN($lsize(Jnn_2))
   -- if ci_1* = $lanes_(Jnn_1 X N_1, c_1)

spectec/spec/wasm-3.0/6-typing.watsup

@@ -916,10 +916,10 @@ rule Instr_ok/vreplace_lane:
   -- if i < $dim(sh)
 
 rule Instr_ok/vextunop:
-  C |- VEXTUNOP sh_1 sh_2 vextunop sx : V128 -> V128
+  C |- VEXTUNOP sh_1 sh_2 vextunop : V128 -> V128
 
 rule Instr_ok/vextbinop:
-  C |- VEXTBINOP sh_1 sh_2 vextbinop sx : V128 V128 -> V128
+  C |- VEXTBINOP sh_1 sh_2 vextbinop : V128 V128 -> V128
 
 rule Instr_ok/vnarrow:
   C |- VNARROW sh_1 sh_2 sx : V128 V128 -> V128

spectec/spec/wasm-3.0/8-reduction.watsup

@@ -693,13 +693,13 @@ rule Step_pure/vreplace_lane:
 
 
 rule Step_pure/vextunop:
-  (VCONST V128 c_1) (VEXTUNOP sh_2 sh_1 vextunop sx) ~> (VCONST V128 c)
-  -- if $vextunop(sh_1, sh_2, vextunop, sx, c_1) = c
+  (VCONST V128 c_1) (VEXTUNOP sh_2 sh_1 vextunop) ~> (VCONST V128 c)
+  -- if $vextunop(sh_1, sh_2, vextunop, c_1) = c
 
 
 rule Step_pure/vextbinop:
-  (VCONST V128 c_1) (VCONST V128 c_2) (VEXTBINOP sh_2 sh_1 vextbinop sx) ~> (VCONST V128 c)
-  -- if $vextbinop(sh_1, sh_2, vextbinop, sx, c_1, c_2) = c
+  (VCONST V128 c_1) (VCONST V128 c_2) (VEXTBINOP sh_2 sh_1 vextbinop) ~> (VCONST V128 c)
+  -- if $vextbinop(sh_1, sh_2, vextbinop, c_1, c_2) = c
 
 
 rule Step_pure/vnarrow:

spectec/spec/wasm-3.0/A-binary.watsup

@@ -760,8 +760,8 @@ grammar Binstr/vec-bin-i8x16 : instr = ...
   | ...
 
 grammar Binstr/vec-extun-i16x8 : instr = ...
-  | 0xFD 124:Bu32 => VEXTUNOP (I16 X `8) (I8 X `16) EXTADD_PAIRWISE S
-  | 0xFD 125:Bu32 => VEXTUNOP (I16 X `8) (I8 X `16) EXTADD_PAIRWISE U
+  | 0xFD 124:Bu32 => VEXTUNOP (I16 X `8) (I8 X `16) (EXTADD_PAIRWISE S)
+  | 0xFD 125:Bu32 => VEXTUNOP (I16 X `8) (I8 X `16) (EXTADD_PAIRWISE U)
   | ...
 
 grammar Binstr/vec-un-i16x8 : instr = ...
@@ -815,15 +815,15 @@ grammar Binstr/vec-bin-i16x8 : instr = ...
   | ...
 
 grammar Binstr/vec-extbin-i16x8 : instr = ...
-  | 0xFD 156:Bu32 => VEXTBINOP (I16 X `8) (I8 X `16) (EXTMUL LOW) S
-  | 0xFD 157:Bu32 => VEXTBINOP (I16 X `8) (I8 X `16) (EXTMUL HIGH) S
-  | 0xFD 158:Bu32 => VEXTBINOP (I16 X `8) (I8 X `16) (EXTMUL LOW) U
-  | 0xFD 159:Bu32 => VEXTBINOP (I16 X `8) (I8 X `16) (EXTMUL HIGH) U
+  | 0xFD 156:Bu32 => VEXTBINOP (I16 X `8) (I8 X `16) (EXTMUL S LOW)
+  | 0xFD 157:Bu32 => VEXTBINOP (I16 X `8) (I8 X `16) (EXTMUL S HIGH)
+  | 0xFD 158:Bu32 => VEXTBINOP (I16 X `8) (I8 X `16) (EXTMUL U LOW)
+  | 0xFD 159:Bu32 => VEXTBINOP (I16 X `8) (I8 X `16) (EXTMUL U HIGH)
   | ...
 
 grammar Binstr/vec-extun-i32x4 : instr = ...
-  | 0xFD 126:Bu32 => VEXTUNOP (I32 X `4) (I16 X `8) EXTADD_PAIRWISE S
-  | 0xFD 127:Bu32 => VEXTUNOP (I32 X `4) (I16 X `8) EXTADD_PAIRWISE U
+  | 0xFD 126:Bu32 => VEXTUNOP (I32 X `4) (I16 X `8) (EXTADD_PAIRWISE S)
+  | 0xFD 127:Bu32 => VEXTUNOP (I32 X `4) (I16 X `8) (EXTADD_PAIRWISE U)
   | ...
 
 grammar Binstr/vec-un-i32x4 : instr = ...
@@ -863,11 +863,11 @@ grammar Binstr/vec-bin-i32x4 : instr = ...
   | ...
 
 grammar Binstr/vec-extbin-i32x4 : instr = ...
-  | 0xFD 186:Bu32 => VEXTBINOP (I32 X `4) (I16 X `8) DOT S
-  | 0xFD 188:Bu32 => VEXTBINOP (I32 X `4) (I16 X `8) (EXTMUL LOW) S
-  | 0xFD 189:Bu32 => VEXTBINOP (I32 X `4) (I16 X `8) (EXTMUL HIGH) S
-  | 0xFD 190:Bu32 => VEXTBINOP (I32 X `4) (I16 X `8) (EXTMUL LOW) U
-  | 0xFD 191:Bu32 => VEXTBINOP (I32 X `4) (I16 X `8) (EXTMUL HIGH) U
+  | 0xFD 186:Bu32 => VEXTBINOP (I32 X `4) (I16 X `8) (DOT S)
+  | 0xFD 188:Bu32 => VEXTBINOP (I32 X `4) (I16 X `8) (EXTMUL S LOW)
+  | 0xFD 189:Bu32 => VEXTBINOP (I32 X `4) (I16 X `8) (EXTMUL S HIGH)
+  | 0xFD 190:Bu32 => VEXTBINOP (I32 X `4) (I16 X `8) (EXTMUL U LOW)
+  | 0xFD 191:Bu32 => VEXTBINOP (I32 X `4) (I16 X `8) (EXTMUL U HIGH)
   | ...
 
 grammar Binstr/vec-un-i64x2 : instr = ...
@@ -912,10 +912,10 @@ grammar Binstr/vec-rel-i64x2 : instr = ...
   | ...
 
 grammar Binstr/vec-extbin-i64x2 : instr = ...
-  | 0xFD 220:Bu32 => VEXTBINOP (I64 X `2) (I32 X `4) (EXTMUL LOW) S
-  | 0xFD 221:Bu32 => VEXTBINOP (I64 X `2) (I32 X `4) (EXTMUL HIGH) S
-  | 0xFD 222:Bu32 => VEXTBINOP (I64 X `2) (I32 X `4) (EXTMUL LOW) U
-  | 0xFD 223:Bu32 => VEXTBINOP (I64 X `2) (I32 X `4) (EXTMUL HIGH) U
+  | 0xFD 220:Bu32 => VEXTBINOP (I64 X `2) (I32 X `4) (EXTMUL S LOW)
+  | 0xFD 221:Bu32 => VEXTBINOP (I64 X `2) (I32 X `4) (EXTMUL S HIGH)
+  | 0xFD 222:Bu32 => VEXTBINOP (I64 X `2) (I32 X `4) (EXTMUL U LOW)
+  | 0xFD 223:Bu32 => VEXTBINOP (I64 X `2) (I32 X `4) (EXTMUL U HIGH)
   | ...
 
 grammar Binstr/vec-un-f32x4 : instr = ...