diff --git a/specification/wasm-3.0/2.4-validation.modules.spectec b/specification/wasm-3.0/2.4-validation.modules.spectec index 2f758642a7..51fcc8d0e3 100644 --- a/specification/wasm-3.0/2.4-validation.modules.spectec +++ b/specification/wasm-3.0/2.4-validation.modules.spectec @@ -138,10 +138,10 @@ relation Types_ok: context |- type* : deftype* hint(name "T-types") hin relation Globals_ok: context |- global* : globaltype* hint(name "T-globals") hint(macro "%globals") ;; HACK for notation -syntax nonfuncs = global* mem* table* elem* start? export* +syntax nonfuncs = global* mem* table* elem* export* def $funcidx_nonfuncs(nonfuncs) : funcidx* hint(show $funcidx(%)) hint(macro "freefuncidx") -def $funcidx_nonfuncs(global* mem* table* elem* start? export*) = - $funcidx_module(MODULE eps eps eps global* mem* table* eps eps elem* start? export*) +def $funcidx_nonfuncs(global* mem* table* elem* export*) = + $funcidx_module(MODULE eps eps eps global* mem* table* eps eps elem* eps export*) rule Module_ok: |- MODULE type* import* tag* global* mem* table* func* data* elem* start? export* : $clos_moduletype(C, xt_I* -> xt_E*) @@ -163,7 +163,7 @@ rule Module_ok: -- if C = C' ++ {TAGS jt_I* jt*, GLOBALS gt*, MEMS mt_I* mt*, TABLES tt_I* tt*, DATAS ok*, ELEMS rt*} ---- -- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS dt_I* dt*, REFS x*} - -- if x* = $funcidx_nonfuncs(global* mem* table* elem* start? export*) + -- if x* = $funcidx_nonfuncs(global* mem* table* elem* export*) ---- -- if jt_I* = $tagsxt(xt_I*) -- if gt_I* = $globalsxt(xt_I*) diff --git a/specification/wasm-latest/2.4-validation.modules.spectec b/specification/wasm-latest/2.4-validation.modules.spectec index 2f758642a7..51fcc8d0e3 100644 --- a/specification/wasm-latest/2.4-validation.modules.spectec +++ b/specification/wasm-latest/2.4-validation.modules.spectec @@ -138,10 +138,10 @@ relation Types_ok: context |- type* : deftype* hint(name "T-types") hin relation Globals_ok: context |- global* : globaltype* hint(name "T-globals") hint(macro "%globals") ;; HACK for notation -syntax nonfuncs = global* mem* table* elem* start? export* +syntax nonfuncs = global* mem* table* elem* export* def $funcidx_nonfuncs(nonfuncs) : funcidx* hint(show $funcidx(%)) hint(macro "freefuncidx") -def $funcidx_nonfuncs(global* mem* table* elem* start? export*) = - $funcidx_module(MODULE eps eps eps global* mem* table* eps eps elem* start? export*) +def $funcidx_nonfuncs(global* mem* table* elem* export*) = + $funcidx_module(MODULE eps eps eps global* mem* table* eps eps elem* eps export*) rule Module_ok: |- MODULE type* import* tag* global* mem* table* func* data* elem* start? export* : $clos_moduletype(C, xt_I* -> xt_E*) @@ -163,7 +163,7 @@ rule Module_ok: -- if C = C' ++ {TAGS jt_I* jt*, GLOBALS gt*, MEMS mt_I* mt*, TABLES tt_I* tt*, DATAS ok*, ELEMS rt*} ---- -- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS dt_I* dt*, REFS x*} - -- if x* = $funcidx_nonfuncs(global* mem* table* elem* start? export*) + -- if x* = $funcidx_nonfuncs(global* mem* table* elem* export*) ---- -- if jt_I* = $tagsxt(xt_I*) -- if gt_I* = $globalsxt(xt_I*) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index b07cb41377..55e860ccc4 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -4770,12 +4770,12 @@ relation Types_ok: `%|-%:%`(context, type*, deftype*) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec syntax nonfuncs = - | `%%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*) + | `%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec def $funcidx_nonfuncs(nonfuncs : nonfuncs) : funcidx* ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec - def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*}(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), start?{start <- `start?`}, `%`_list(export*{export <- `export*`},))) + def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*}(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), ?(), `%`_list(export*{export <- `export*`},))) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec relation Module_ok: `|-%:%`(module, moduletype) @@ -4796,7 +4796,7 @@ relation Module_ok: `|-%:%`(module, moduletype) -- if $disjoint_(syntax name, nm*{nm <- `nm*`}) -- if (C = C' +++ {TYPES [], TAGS jt_I*{jt_I <- `jt_I*`} ++ jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt_I*{mt_I <- `mt_I*`} ++ mt*{mt <- `mt*`}, TABLES tt_I*{tt_I <- `tt_I*`} ++ tt*{tt <- `tt*`}, FUNCS [], DATAS ok*{ok <- `ok*`}, ELEMS rt*{rt <- `rt*`}, LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []}) -- if (C' = {TYPES dt'*{dt' <- `dt'*`}, TAGS [], GLOBALS gt_I*{gt_I <- `gt_I*`}, MEMS [], TABLES [], FUNCS dt_I*{dt_I <- `dt_I*`} ++ dt*{dt <- `dt*`}, DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS x*{x <- `x*`}, RECS []}) - -- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`}))) + -- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`}))) -- if (jt_I*{jt_I <- `jt_I*`} = $tagsxt(xt_I*{xt_I <- `xt_I*`})) -- if (gt_I*{gt_I <- `gt_I*`} = $globalsxt(xt_I*{xt_I <- `xt_I*`})) -- if (mt_I*{mt_I <- `mt_I*`} = $memsxt(xt_I*{xt_I <- `xt_I*`})) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index be5440eb04..335cd42374 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -7904,16 +7904,16 @@ $\boxed{{\mathit{context}} \vdash {{\mathit{global}}^\ast} : {{\mathit{globaltyp $$ \begin{array}[t]{@{}lrrl@{}l@{}} -& {\mathit{nonfuncs}} & ::= & {{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast} \\ +& {\mathit{nonfuncs}} & ::= & {{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{export}}^\ast} \\ \end{array} $$ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast}) & = & & \\ +{\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{export}}^\ast}) & = & & \\ \multicolumn{4}{@{}l@{}}{\quad \begin{array}[t]{@{}l@{}} -{\mathrm{funcidx}}(\mathsf{module}~\epsilon~\epsilon~\epsilon~{{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~\epsilon~\epsilon~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast}) \\ +{\mathrm{funcidx}}(\mathsf{module}~\epsilon~\epsilon~\epsilon~{{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~\epsilon~\epsilon~{{\mathit{elem}}^\ast}~\epsilon~{{\mathit{export}}^\ast}) \\ \end{array} } \\ \end{array} @@ -7951,7 +7951,7 @@ C = {C'} \oplus \{ \mathsf{tags}~{{\mathit{jt}}_{\mathsf{i}}^\ast}~{{\mathit{jt} \\ {C'} = \{ \mathsf{types}~{{\mathit{dt}'}^\ast},\;\allowbreak \mathsf{globals}~{{\mathit{gt}}_{\mathsf{i}}^\ast},\;\allowbreak \mathsf{funcs}~{{\mathit{dt}}_{\mathsf{i}}^\ast}~{{\mathit{dt}}^\ast},\;\allowbreak \mathsf{refs}~{x^\ast} \} \qquad -{x^\ast} = {\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast}) +{x^\ast} = {\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{export}}^\ast}) \\ {{\mathit{jt}}_{\mathsf{i}}^\ast} = {\mathrm{tags}}({{\mathit{xt}}_{\mathsf{i}}^\ast}) \qquad diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 44af5b8ccf..c1096068df 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -4293,12 +4293,12 @@ relation Types_ok: `%|-%:%`(context, type*, deftype*) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec syntax nonfuncs = - | `%%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*) + | `%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec def $funcidx_nonfuncs(nonfuncs : nonfuncs) : funcidx* ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec - def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*}(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), start?{start <- `start?`}, `%`_list(export*{export <- `export*`},))) + def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*}(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), ?(), `%`_list(export*{export <- `export*`},))) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec relation Module_ok: `|-%:%`(module, moduletype) @@ -4319,7 +4319,7 @@ relation Module_ok: `|-%:%`(module, moduletype) -- if $disjoint_(syntax name, nm*{nm <- `nm*`}) -- if (C = C' +++ {TYPES [], TAGS jt_I*{jt_I <- `jt_I*`} ++ jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt_I*{mt_I <- `mt_I*`} ++ mt*{mt <- `mt*`}, TABLES tt_I*{tt_I <- `tt_I*`} ++ tt*{tt <- `tt*`}, FUNCS [], DATAS ok*{ok <- `ok*`}, ELEMS rt*{rt <- `rt*`}, LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []}) -- if (C' = {TYPES dt'*{dt' <- `dt'*`}, TAGS [], GLOBALS gt_I*{gt_I <- `gt_I*`}, MEMS [], TABLES [], FUNCS dt_I*{dt_I <- `dt_I*`} ++ dt*{dt <- `dt*`}, DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS x*{x <- `x*`}, RECS []}) - -- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`}))) + -- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`}))) -- if (jt_I*{jt_I <- `jt_I*`} = $tagsxt(xt_I*{xt_I <- `xt_I*`})) -- if (gt_I*{gt_I <- `gt_I*`} = $globalsxt(xt_I*{xt_I <- `xt_I*`})) -- if (mt_I*{mt_I <- `mt_I*`} = $memsxt(xt_I*{xt_I <- `xt_I*`})) @@ -16167,12 +16167,12 @@ relation Types_ok: `%|-%:%`(context, type*, deftype*) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec syntax nonfuncs = - | `%%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*) + | `%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec def $funcidx_nonfuncs(nonfuncs : nonfuncs) : funcidx* ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec - def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*}(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), start?{start <- `start?`}, `%`_list(export*{export <- `export*`},))) + def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*}(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), ?(), `%`_list(export*{export <- `export*`},))) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec relation Module_ok: `|-%:%`(module, moduletype) @@ -16193,7 +16193,7 @@ relation Module_ok: `|-%:%`(module, moduletype) -- if $disjoint_(syntax name, nm*{nm <- `nm*`}) -- if (C = C' +++ {TYPES [], TAGS jt_I*{jt_I <- `jt_I*`} ++ jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt_I*{mt_I <- `mt_I*`} ++ mt*{mt <- `mt*`}, TABLES tt_I*{tt_I <- `tt_I*`} ++ tt*{tt <- `tt*`}, FUNCS [], DATAS ok*{ok <- `ok*`}, ELEMS rt*{rt <- `rt*`}, LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []}) -- if (C' = {TYPES dt'*{dt' <- `dt'*`}, TAGS [], GLOBALS gt_I*{gt_I <- `gt_I*`}, MEMS [], TABLES [], FUNCS dt_I*{dt_I <- `dt_I*`} ++ dt*{dt <- `dt*`}, DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS x*{x <- `x*`}, RECS []}) - -- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`}))) + -- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`}))) -- if (jt_I*{jt_I <- `jt_I*`} = $tagsxt(xt_I*{xt_I <- `xt_I*`})) -- if (gt_I*{gt_I <- `gt_I*`} = $globalsxt(xt_I*{xt_I <- `xt_I*`})) -- if (mt_I*{mt_I <- `mt_I*`} = $memsxt(xt_I*{xt_I <- `xt_I*`})) @@ -28161,12 +28161,12 @@ relation Types_ok: `%|-%:%`(context, type*, deftype*) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec syntax nonfuncs = - | `%%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*) + | `%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec def $funcidx_nonfuncs(nonfuncs : nonfuncs) : funcidx* ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec - def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*}(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), start?{start <- `start?`}, `%`_list(export*{export <- `export*`},))) + def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*}(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), ?(), `%`_list(export*{export <- `export*`},))) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec relation Module_ok: `|-%:%`(module, moduletype) @@ -28196,7 +28196,7 @@ relation Module_ok: `|-%:%`(module, moduletype) -- if $disjoint_(syntax name, nm*{nm <- `nm*`}) -- if (C = C' +++ {TYPES [], TAGS jt_I*{jt_I <- `jt_I*`} ++ jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt_I*{mt_I <- `mt_I*`} ++ mt*{mt <- `mt*`}, TABLES tt_I*{tt_I <- `tt_I*`} ++ tt*{tt <- `tt*`}, FUNCS [], DATAS ok*{ok <- `ok*`}, ELEMS rt*{rt <- `rt*`}, LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []}) -- if (C' = {TYPES dt'*{dt' <- `dt'*`}, TAGS [], GLOBALS gt_I*{gt_I <- `gt_I*`}, MEMS [], TABLES [], FUNCS dt_I*{dt_I <- `dt_I*`} ++ dt*{dt <- `dt*`}, DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS x*{x <- `x*`}, RECS []}) - -- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`}))) + -- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`}))) -- if (jt_I*{jt_I <- `jt_I*`} = $tagsxt(xt_I*{xt_I <- `xt_I*`})) -- if (gt_I*{gt_I <- `gt_I*`} = $globalsxt(xt_I*{xt_I <- `xt_I*`})) -- if (mt_I*{mt_I <- `mt_I*`} = $memsxt(xt_I*{xt_I <- `xt_I*`})) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 6d1894b49b..67a6205cbe 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -17389,7 +17389,7 @@ The module :math:`(\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\as * The context :math:`{C'}` is of the form :math:`\{ \mathsf{types}~{{\mathit{dt}'}^\ast},\;\allowbreak \mathsf{globals}~{{\mathit{gt}}_{\mathsf{i}}^\ast},\;\allowbreak \mathsf{funcs}~{{\mathit{dt}}_{\mathsf{i}}^\ast}~{{\mathit{dt}}^\ast},\;\allowbreak \mathsf{return}~\epsilon,\;\allowbreak \mathsf{refs}~{x^\ast} \}`. - * The function index sequence :math:`{x^\ast}` is of the form :math:`{\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast})`. + * The function index sequence :math:`{x^\ast}` is of the form :math:`{\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{export}}^\ast})`. * The tag type sequence :math:`{{\mathit{jt}}_{\mathsf{i}}^\ast}` is of the form :math:`{\mathrm{tags}}({{\mathit{xt}}_{\mathsf{i}}^\ast})`. @@ -24589,11 +24589,11 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i 1. Return :math:`{\mathit{zt}} \neq {\mathrm{unpack}}({\mathit{zt}})`. -:math:`{\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast})` -....................................................................................................................................................................... +:math:`{\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{export}}^\ast})` +.................................................................................................................................................. -1. Return :math:`{\mathrm{funcidx}}(\mathsf{module}~{{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast})`. +1. Return :math:`{\mathrm{funcidx}}(\mathsf{module}~{{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{export}}^\ast})`. :math:`{{\mathrm{relaxed}}(i)}{{}[ X_1, X_2 ]}` @@ -29557,7 +29557,7 @@ Module_ok - $disjoint_(`name, nm*) is true. - the context C is C' with .TAGS appended by jt_I* :: jt* and .GLOBALS appended by gt* and .MEMS appended by mt_I* :: mt* and .TABLES appended by tt_I* :: tt* and .DATAS appended by ok* and .ELEMS appended by rt*. - the context C' is { TYPES: dt'*; GLOBALS: gt_I*; FUNCS: dt_I* :: dt*; RETURN: ?(); REFS: x* }. - - the function index sequence x* is $funcidx_nonfuncs((global* mem* table* elem* start? export*)). + - the function index sequence x* is $funcidx_nonfuncs((global* mem* table* elem* export*)). - the tag type sequence jt_I* is $tagsxt(xt_I*). - the global type sequence gt_I* is $globalsxt(xt_I*). - the memory type sequence mt_I* is $memsxt(xt_I*). @@ -32992,8 +32992,8 @@ default_ valtype is_packtype zt 1. Return (zt =/= $unpack(zt)). -funcidx_nonfuncs (global* mem* table* elem* start? export*) -1. Return $funcidx_module((MODULE [] [] [] global* mem* table* [] [] elem* start? export*)). +funcidx_nonfuncs (global* mem* table* elem* export*) +1. Return $funcidx_module((MODULE [] [] [] global* mem* table* [] [] elem* ?() export*)). relaxed2 i `X X_1 X_2 1. If $ND(), then: