Skip to content

Commit cbef362

Browse files
zilinczilinc
authored
[spec] Fix typo (#2143)
1 parent f9c743a commit cbef362

6 files changed

Lines changed: 13 additions & 13 deletions

File tree

‎specification/wasm-3.0/2.1-validation.types.spectec‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
159159
def $unrollht(C, REC i) = C.RECS[i]
160160

161161
rule Subtype_ok2:
162-
C |- SUB FINAL? typeuse* compttype : OK x i
162+
C |- SUB FINAL? typeuse* comptype : OK x i
163163
-- if |typeuse*| <= 1
164164
-- (if $before(typeuse, x, i))*
165165
-- (if $unrollht(C, typeuse) = SUB typeuse'* comptype')*

‎specification/wasm-latest/2.1-validation.types.spectec‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
159159
def $unrollht(C, REC i) = C.RECS[i]
160160

161161
rule Subtype_ok2:
162-
C |- SUB FINAL? typeuse* compttype : OK x i
162+
C |- SUB FINAL? typeuse* comptype : OK x i
163163
-- if |typeuse*| <= 1
164164
-- (if $before(typeuse, x, i))*
165165
-- (if $unrollht(C, typeuse) = SUB typeuse'* comptype')*

‎spectec/test-frontend/TEST.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2912,8 +2912,8 @@ relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx)
29122912
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:90.1-90.126
29132913
relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat)
29142914
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:161.1-168.49
2915-
rule _{C : context, `typeuse*` : typeuse*, compttype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**, comptype : comptype}:
2916-
`%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, compttype), OK_oktypeidxnat(x, i))
2915+
rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
2916+
`%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypeidxnat(x, i))
29172917
-- if (|typeuse*{typeuse <- `typeuse*`}| <= 1)
29182918
-- (if $before(typeuse, x, i))*{typeuse <- `typeuse*`}
29192919
-- (if ($unrollht(C, (typeuse : typeuse <: heaptype)) = SUB_subtype(?(), typeuse'*{typeuse' <- `typeuse'*`}, comptype')))*{comptype' <- `comptype'*`, typeuse <- `typeuse*`, `typeuse'*` <- `typeuse'**`}

‎spectec/test-latex/TEST.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4943,7 +4943,7 @@ C \vdash {\mathit{comptype}} : \mathsf{ok}
49434943
(C \vdash {\mathit{comptype}} \leq {\mathit{comptype}'})^\ast
49444944
\end{array}
49454945
}{
4946-
C \vdash \mathsf{sub}~{\mathsf{final}^?}~{{\mathit{typeuse}}^\ast}~{\mathit{compttype}} : {\mathsf{ok}}{(x, i)}
4946+
C \vdash \mathsf{sub}~{\mathsf{final}^?}~{{\mathit{typeuse}}^\ast}~{\mathit{comptype}} : {\mathsf{ok}}{(x, i)}
49474947
} \, {[\textsc{\scriptsize K{-}sub2}]}
49484948
\qquad
49494949
\end{array}

‎spectec/test-middlend/TEST.md‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2902,8 +2902,8 @@ relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx)
29022902
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:90.1-90.126
29032903
relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat)
29042904
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:161.1-168.49
2905-
rule _{C : context, `typeuse*` : typeuse*, compttype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**, comptype : comptype}:
2906-
`%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, compttype), OK_oktypeidxnat(x, i))
2905+
rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
2906+
`%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypeidxnat(x, i))
29072907
-- if (|typeuse*{typeuse <- `typeuse*`}| <= 1)
29082908
-- (if $before(typeuse, x, i))*{typeuse <- `typeuse*`}
29092909
-- (if ($unrollht(C, (typeuse : typeuse <: heaptype)) = SUB_subtype(?(), typeuse'*{typeuse' <- `typeuse'*`}, comptype')))*{comptype' <- `comptype'*`, typeuse <- `typeuse*`, `typeuse'*` <- `typeuse'**`}
@@ -14321,8 +14321,8 @@ relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx)
1432114321
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:90.1-90.126
1432214322
relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat)
1432314323
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:161.1-168.49
14324-
rule _{C : context, `typeuse*` : typeuse*, compttype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**, comptype : comptype}:
14325-
`%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, compttype), OK_oktypeidxnat(x, i))
14324+
rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
14325+
`%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypeidxnat(x, i))
1432614326
-- if (|typeuse*{typeuse <- `typeuse*`}| <= 1)
1432714327
-- (if $before(typeuse, x, i))*{typeuse <- `typeuse*`}
1432814328
-- (if ($unrollht(C, (typeuse : typeuse <: heaptype)) = SUB_subtype(?(), typeuse'*{typeuse' <- `typeuse'*`}, comptype')))*{comptype' <- `comptype'*`, typeuse <- `typeuse*`, `typeuse'*` <- `typeuse'**`}
@@ -25747,8 +25747,8 @@ relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx)
2574725747
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:90.1-90.126
2574825748
relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat)
2574925749
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:161.1-168.49
25750-
rule _{C : context, `typeuse*` : typeuse*, compttype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**, comptype : comptype}:
25751-
`%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, compttype), OK_oktypeidxnat(x, i))
25750+
rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
25751+
`%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypeidxnat(x, i))
2575225752
-- if (|typeuse*{typeuse <- `typeuse*`}| <= 1)
2575325753
-- (if $before(typeuse, x, i))*{typeuse <- `typeuse*`}
2575425754
-- if (|`comptype'*`| = |`typeuse*`|)

‎spectec/test-prose/TEST.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14089,7 +14089,7 @@ The recursive type :math:`(\mathsf{rec}~{\mathit{subtype}}_1~{{\mathit{subtype}}
1408914089

1409014090

1409114091

14092-
The sub type :math:`(\mathsf{sub}~{\mathsf{final}^?}~{{\mathit{typeuse}}^\ast}~{\mathit{compttype}})` is :ref:`valid <valid-val>` for :math:`({\mathsf{ok}}{(x, i)})` if:
14092+
The sub type :math:`(\mathsf{sub}~{\mathsf{final}^?}~{{\mathit{typeuse}}^\ast}~{\mathit{comptype}})` is :ref:`valid <valid-val>` for :math:`({\mathsf{ok}}{(x, i)})` if:
1409314093

1409414094

1409514095
* The length of :math:`{{\mathit{typeuse}}^\ast}` is less than or equal to :math:`1`.
@@ -27042,7 +27042,7 @@ Rectype_ok/cons
2704227042
- the recursive type (REC subtype*) is valid for the type index (OK (x + 1)).
2704327043

2704427044
Subtype_ok2
27045-
- the sub type (SUB FINAL? typeuse* compttype) is valid for (OK x i) if:
27045+
- the sub type (SUB FINAL? typeuse* comptype) is valid for (OK x i) if:
2704627046
- |typeuse*| is less than or equal to 1.
2704727047
- For all typeuse in typeuse*:
2704827048
- $before(typeuse, x, i) is true.

0 commit comments

Comments
 (0)