@@ -1844,31 +1844,31 @@ Most other vector instructions are defined in terms of numeric operators that ar
1844
1844
1845
1845
1. Assert: due to :ref: `validation <valid-vec-replace_lane >`, :math: `x < \dim (\shape )`.
1846
1846
1847
- 2. Let :math: `t_ 1 ` be the type :math: `\unpacked (\shape )`.
1847
+ 2. Let :math: `t_ 2 ` be the type :math: `\unpacked (\shape )`.
1848
1848
1849
1849
3. Assert: due to :ref: `validation <valid-vec-replace_lane >`, a value of :ref: `value type <syntax-valtype >` :math: `t_1 ` is on the top of the stack.
1850
1850
1851
- 4. Pop the value :math: `t_ 1 .\CONST ~c_ 1 ` from the stack.
1851
+ 4. Pop the value :math: `t_ 2 .\CONST ~c_ 2 ` from the stack.
1852
1852
1853
1853
5. Assert: due to :ref: `validation <valid-vec-replace_lane >`, a value of :ref: `value type <syntax-valtype >` |V128 | is on the top of the stack.
1854
1854
1855
- 6. Pop the value :math: `\V128 .\VCONST ~c_ 2 ` from the stack.
1855
+ 6. Pop the value :math: `\V128 .\VCONST ~c_ 1 ` from the stack.
1856
1856
1857
- 7. Let :math: `i^\ast ` be the result of computing :math: `\lanes _{\shape }(c_ 2 )`.
1857
+ 7. Let :math: `i^\ast ` be the result of computing :math: `\lanes _{\shape }(c_ 1 )`.
1858
1858
1859
- 8. Let :math: `c` be the result of computing :math: `\lanes ^{-1 }_{\shape }(i^\ast \with [x] = c_ 1 )`.
1859
+ 8. Let :math: `c` be the result of computing :math: `\lanes ^{-1 }_{\shape }(i^\ast \with [x] = c_ 2 )`.
1860
1860
1861
1861
9. Push :math: `\V128 .\VCONST ~c` on the stack.
1862
1862
1863
1863
.. math ::
1864
1864
\begin {array}{l}
1865
1865
\begin {array}{lcl@{\qquad }l}
1866
- (t_ 1 \ K {.}\CONST ~c_1 )~(\V 128 \ K {.}\VCONST ~c_2 )~(\shape\K {.}\REPLACELANE ~x) &\stepto & (\V128 \K {.}\VCONST ~c)
1866
+ (\V 128 \ K {.}\VCONST ~c_1 )~(t_ 2 \ K {.}\CONST ~c_2 )~(\shape\K {.}\REPLACELANE ~x) &\stepto & (\V128 \K {.}\VCONST ~c)
1867
1867
\end {array}
1868
1868
\\ \qquad
1869
1869
\begin {array}[t]{@{}r@{~}l@{}}
1870
- (\iff & i^\ast = \lanes _{\shape }(c_ 2 ) \\
1871
- \wedge & c = \lanes ^{-1 }_{\shape }(i^\ast \with [x] = c_ 1 ))
1870
+ (\iff & i^\ast = \lanes _{\shape }(c_ 1 ) \\
1871
+ \wedge & c = \lanes ^{-1 }_{\shape }(i^\ast \with [x] = c_ 2 ))
1872
1872
\end {array}
1873
1873
\end {array}
1874
1874
@@ -2168,8 +2168,8 @@ where:
2168
2168
\end {array}
2169
2169
2170
2170
2171
- :math: `t_2 \K {x}N\K {.}\vcvtop\K {\_ }t_1 \K {x}M\K {\_ }\sx\K {\_zero}`
2172
- ...............................................................
2171
+ :math: `t_2 \K {x}N\K {.}\vcvtop\K {\_ }t_1 \K {x}M\K {\_ }\sx ^? \K {\_zero}`
2172
+ .................................................................
2173
2173
2174
2174
1. Assert: due to :ref: `syntax <syntax-instr-vec >`, :math: `N = 2 \cdot M`.
2175
2175
@@ -2179,7 +2179,7 @@ where:
2179
2179
2180
2180
4. Let :math: `i^\ast ` be the result of computing :math: `\lanes _{t_1 \K {x}M}(c_1 )`.
2181
2181
2182
- 5. Let :math: `j^\ast ` be the result of computing :math: `\vcvtop ^{\sx }_{|t_1 |,|t_2 |}(i^\ast )`.
2182
+ 5. Let :math: `j^\ast ` be the result of computing :math: `\vcvtop ^{\sx ^? }_{|t_1 |,|t_2 |}(i^\ast )`.
2183
2183
2184
2184
6. Let :math: `k^\ast ` be the concatenation of the two sequences :math: `j^\ast ` and :math: `0 ^M`.
2185
2185
@@ -2190,11 +2190,11 @@ where:
2190
2190
.. math ::
2191
2191
\begin {array}{l}
2192
2192
\begin {array}{lcl@{\qquad }l}
2193
- (\V128 \K {.}\VCONST ~c_1 )~t_2 \K {x}N\K {.}\vcvtop\K {\_ }t_1 \K {x}M\K {\_ }\sx\K {\_zero} &\stepto & (\V128 \K {.}\VCONST ~c) \\
2193
+ (\V128 \K {.}\VCONST ~c_1 )~t_2 \K {x}N\K {.}\vcvtop\K {\_ }t_1 \K {x}M\K {\_ }\sx ^? \K {\_zero} &\stepto & (\V128 \K {.}\VCONST ~c) \\
2194
2194
\end {array}
2195
2195
\\ \qquad
2196
2196
\begin {array}[t]{@{}r@{~}l@{}}
2197
- (\iff & c = \lanes ^{-1 }_{t_2 \K {x}N}(\vcvtop ^{\sx }_{|t_1 |,|t_2 |}(\lanes _{t_1 \K {x}M}(c_1 ))~0 ^M))
2197
+ (\iff & c = \lanes ^{-1 }_{t_2 \K {x}N}(\vcvtop ^{\sx ^? }_{|t_1 |,|t_2 |}(\lanes _{t_1 \K {x}M}(c_1 ))~0 ^M))
2198
2198
\end {array}
2199
2199
\end {array}
2200
2200
@@ -2273,7 +2273,7 @@ where:
2273
2273
2274
2274
10. Let :math: `k_2 ^\ast ` be the result of computing :math: `\extend ^{\sx }_{|t_1 |,|t_2 |}(j_2 ^\ast )`.
2275
2275
2276
- 11. Let :math: `k^\ast ` be the result of computing :math: `\imul _{t_2 \K {x}N }(k_1 ^\ast , k_2 ^\ast )`.
2276
+ 11. Let :math: `k^\ast ` be the result of computing :math: `\imul _{| t_2 | }(k_1 ^\ast , k_2 ^\ast )`.
2277
2277
2278
2278
12. Let :math: `c` be the result of computing :math: `\lanes ^{-1 }_{t_2 \K {x}N}(k^\ast )`.
2279
2279
@@ -2287,7 +2287,7 @@ where:
2287
2287
\begin {array}[t]{@{}r@{~}l@{}}
2288
2288
(\iff & i^\ast = \lanes _{t_1 \K {x}M}(c_1 )[\half (0 , N) \slice N] \\
2289
2289
\wedge & j^\ast = \lanes _{t_1 \K {x}M}(c_2 )[\half (0 , N) \slice N] \\
2290
- \wedge & c = \lanes ^{-1 }_{t_2 \K {x}N}(\imul _{t_2 \K {x}N }(\extend ^{\sx }_{|t_1 |,|t_2 |}(i^\ast ), \extend ^{\sx }_{|t_1 |,|t_2 |}(j^\ast ))))
2290
+ \wedge & c = \lanes ^{-1 }_{t_2 \K {x}N}(\imul _{| t_2 | }(\extend ^{\sx }_{|t_1 |,|t_2 |}(i^\ast ), \extend ^{\sx }_{|t_1 |,|t_2 |}(j^\ast ))))
2291
2291
\end {array}
2292
2292
2293
2293
where:
@@ -2314,7 +2314,7 @@ where:
2314
2314
2315
2315
5. Let :math: `(j_1 ~j_2 )^\ast ` be the result of computing :math: `\extend ^{\sx }_{|t_1 |,|t_2 |}(i^\ast )`.
2316
2316
2317
- 6. Let :math: `k^\ast ` be the result of computing :math: `\iadd _{N }(j_1 , j_2 )^\ast `.
2317
+ 6. Let :math: `k^\ast ` be the result of computing :math: `\iadd _{|t_ 2 | }(j_1 , j_2 )^\ast `.
2318
2318
2319
2319
7. Let :math: `c` be the result of computing :math: `\lanes ^{-1 }_{t_2 \K {x}N}(k^\ast )`.
2320
2320
@@ -2328,7 +2328,7 @@ where:
2328
2328
\\ \qquad
2329
2329
\begin {array}[t]{@{}r@{~}l@{}}
2330
2330
(\iff & (i_1 ~i_2 )^\ast = \extend ^{\sx }_{|t_1 |,|t_2 |}(\lanes _{t_1 \K {x}M}(c_1 )) \\
2331
- \wedge & j^\ast = \iadd _{N }(i_1 , i_2 )^\ast \\
2331
+ \wedge & j^\ast = \iadd _{|t_ 2 | }(i_1 , i_2 )^\ast \\
2332
2332
\wedge & c = \lanes ^{-1 }_{t_2 \K {x}N}(j^\ast ))
2333
2333
\end {array}
2334
2334
\end {array}
0 commit comments