@@ -651,42 +651,49 @@ Table Instructions
651
651
652
652
11. Pop the value :math: `\I32 .\CONST ~i` from the stack.
653
653
654
- 12. If :math: `n` is :math: `0 `, then:
654
+ 12. If :math: `i + n` is larger than the length of :math: `\X {tab}. \TIELEM `, then:
655
655
656
- a. If :math: `i` is larger than the length of :math: ` \X {tab}. \TIELEM `, then:
656
+ a. Trap.
657
657
658
- i. Trap.
658
+ 12. If :math: `n` is :math: ` 0 `, then:
659
659
660
- 12. Else:
660
+ a. Return.
661
661
662
- a . Push the value :math: `\I32 .CONST~i` to the stack.
662
+ 13 . Push the value :math: `\I32 .CONST~i` to the stack.
663
663
664
- b . Push the value :math: `\val ` to the stack.
664
+ 14 . Push the value :math: `\val ` to the stack.
665
665
666
- c . Execute the instruction :math: `\TABLESET ~x`.
666
+ 15 . Execute the instruction :math: `\TABLESET ~x`.
667
667
668
- d . Push the value :math: `\I32 .CONST~(i+1 )` to the stack.
668
+ 16 . Push the value :math: `\I32 .CONST~(i+1 )` to the stack.
669
669
670
- e . Push the value :math: `\val ` to the stack.
670
+ 17 . Push the value :math: `\val ` to the stack.
671
671
672
- f . Push the value :math: `\I32 .CONST~(n-1 )` to the stack.
672
+ 18 . Push the value :math: `\I32 .CONST~(n-1 )` to the stack.
673
673
674
- c . Execute the instruction :math: `\TABLEFILL ~x`.
674
+ 19 . Execute the instruction :math: `\TABLEFILL ~x`.
675
675
676
676
.. math ::
677
677
\begin {array}{l}
678
- \begin {array}{lcl@{\qquad }l}
679
- S; F; (\I32 .\CONST ~i)~\val ~(\I32 .\CONST ~(n+1 ))~(\TABLEFILL ~x) &\stepto & S'; F; (\I32 .\CONST ~i)~\val ~(\TABLESET ~x)~(\I32 .\CONST ~(i+1 ))~\val ~(\I32 .\CONST ~n)~(\TABLEFILL ~x)
680
- \end {array} \\
681
- \begin {array}{lcl@{\qquad }l}
682
- S; F; (\I32 .\CONST ~i)~\val ~(\I32 .\CONST ~0 )~(\TABLEFILL ~x) &\stepto & S'; F; \epsilon
683
- \end {array}
684
- \\ \qquad
685
- (\iff i \leq |\STABLES [F.\AMODULE .\MITABLES [x]]|) \\
686
- \begin {array}{lcl@{\qquad }l}
687
- S; F; (\I32 .\CONST ~i)~\val ~(\I32 .\CONST ~0 )~(\TABLEFILL ~x) &\stepto & S; F; \TRAP
688
- \end {array}
689
- \\ \qquad
678
+ S; F; (\I32 .\CONST ~i)~\val ~(\I32 .\CONST ~n)~(\TABLEFILL ~x)
679
+ \quad\stepto\quad S; F; \TRAP
680
+ \\ \qquad
681
+ \begin {array}[t]{@{}r@{~}l@{}}
682
+ (\iff & i + n > |S.\STABLES [F.\AMODULE .\MITABLES [x]].\TIELEM |) \\
683
+ \end {array}
684
+ \\[ 1 ex]
685
+ S; F; (\I32 .\CONST ~i)~\val ~(\I32 .\CONST ~0 )~(\TABLEFILL ~x)
686
+ \quad\stepto\quad S; F; \epsilon
687
+ \\ \qquad
688
+ (\otherwise )
689
+ \\[ 1 ex]
690
+ S; F; (\I32 .\CONST ~i)~\val ~(\I32 .\CONST ~n+1 )~(\TABLEFILL ~x)
691
+ \quad\stepto\quad S; F;
692
+ \begin {array}[t]{@{}l@{}}
693
+ (\I32 .\CONST ~i)~\val ~(\TABLESET ~x) \\
694
+ (\I32 .\CONST ~i+1 )~\val ~(\I32 .\CONST ~n)~(\TABLEFILL ~x) \\
695
+ \end {array}
696
+ \\ \qquad
690
697
(\otherwise ) \\
691
698
\end {array}
692
699
0 commit comments