From dd3c8d4ba35b0831b98442c5e13adc665a3206bd Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 13 Jun 2024 17:26:47 +0200 Subject: [PATCH] Tweak layout --- document/core/binary/modules.rst | 55 ----------------------- document/core/util/macros.def | 4 +- spectec/spec/wasm-3.0/2-syntax-aux.watsup | 10 ++--- spectec/spec/wasm-3.0/A-binary.watsup | 34 ++++++++------ spectec/src/backend-latex/render.ml | 8 +++- spectec/test-frontend/TEST.md | 4 +- spectec/test-latex/TEST.md | 39 +++++++++------- spectec/test-middlend/TEST.md | 20 ++++----- 8 files changed, 69 insertions(+), 105 deletions(-) diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index eeef8a886d..093d3f3b0d 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -383,61 +383,6 @@ Furthermore, it must be present if any :ref:`data index ` occurs $${grammar: {Bmagic Bversion Bmodule}} -.. math:: - \begin{array}{llcllll} - \production{magic} & \Bmagic &::=& - \hex{00}~\hex{61}~\hex{73}~\hex{6D} \\ - \production{version} & \Bversion &::=& - \hex{01}~\hex{00}~\hex{00}~\hex{00} \\ - \production{module} & \Bmodule &::=& - \Bmagic \\ &&& - \Bversion \\ &&& - \Bcustomsec^\ast \\ &&& - \rectype^\ast{:\,}\Btypesec \\ &&& - \Bcustomsec^\ast \\ &&& - \import^\ast{:\,}\Bimportsec \\ &&& - \Bcustomsec^\ast \\ &&& - \typeidx^n{:\,}\Bfuncsec \\ &&& - \Bcustomsec^\ast \\ &&& - \table^\ast{:\,}\Btablesec \\ &&& - \Bcustomsec^\ast \\ &&& - \mem^\ast{:\,}\Bmemsec \\ &&& - \Bcustomsec^\ast \\ &&& - \global^\ast{:\,}\Bglobalsec \\ &&& - \Bcustomsec^\ast \\ &&& - \export^\ast{:\,}\Bexportsec \\ &&& - \Bcustomsec^\ast \\ &&& - \start^?{:\,}\Bstartsec \\ &&& - \Bcustomsec^\ast \\ &&& - \elem^\ast{:\,}\Belemsec \\ &&& - \Bcustomsec^\ast \\ &&& - m^?{:\,}\Bdatacntsec \\ &&& - \Bcustomsec^\ast \\ &&& - \X{code}^n{:\,}\Bcodesec \\ &&& - \Bcustomsec^\ast \\ &&& - \data^m{:\,}\Bdatasec \\ &&& - \Bcustomsec^\ast - \quad\Rightarrow\quad \{~ - \begin{array}[t]{@{}l@{}} - \MTYPES~\rectype^\ast, \\ - \MFUNCS~\func^n, \\ - \MTABLES~\table^\ast, \\ - \MMEMS~\mem^\ast, \\ - \MGLOBALS~\global^\ast, \\ - \MELEMS~\elem^\ast, \\ - \MDATAS~\data^m, \\ - \MSTART~\start^?, \\ - \MIMPORTS~\import^\ast, \\ - \MEXPORTS~\export^\ast ~\} \\ - \end{array} \\ &&& - (\iff m^? \neq \epsilon \vee \freedataidx(\X{code}^n) = \emptyset) \\ - \end{array} - -where for each :math:`t_i^\ast, e_i` in :math:`\X{code}^n`, - -.. math:: - \func^n[i] = \{ \FTYPE~\typeidx^n[i], \FLOCALS~t_i^\ast, \FBODY~e_i \} \\ - .. note:: The version of the WebAssembly binary format may increase in the future if backward-incompatible changes have to be made to the format. diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 497b0eaea0..864b3a94bf 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -1331,7 +1331,7 @@ .. |TIREFS| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\K{elem}} .. |MITYPE| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{type}} -.. |MIBYTES| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{data}} +.. |MIBYTES| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{bytes}} .. |GITYPE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{type}} .. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}} @@ -1340,7 +1340,7 @@ .. |EIREFS| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{elem}} .. |DITYPE| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{data}} -.. |DIBYTES| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{data}} +.. |DIBYTES| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{bytes}} .. |EINAME| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{name}} .. |EIVALUE| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{value}} diff --git a/spectec/spec/wasm-3.0/2-syntax-aux.watsup b/spectec/spec/wasm-3.0/2-syntax-aux.watsup index 99f3778540..80dca15d6b 100644 --- a/spectec/spec/wasm-3.0/2-syntax-aux.watsup +++ b/spectec/spec/wasm-3.0/2-syntax-aux.watsup @@ -17,22 +17,22 @@ def $setminus1(x, y_1 y*) = $setminus1(x, y*) -- otherwise ;; Free indices -def $dataidx_instr(instr) : dataidx* hint(show $dataidx(%)) +def $dataidx_instr(instr) : dataidx* hint(show $dataidx(%)) hint(macro "freedataidx") def $dataidx_instr(MEMORY.INIT x y) = y def $dataidx_instr(DATA.DROP x) = x def $dataidx_instr(in) = eps -def $dataidx_instrs(instr*) : dataidx* hint(show $dataidx(%)) +def $dataidx_instrs(instr*) : dataidx* hint(show $dataidx(%)) hint(macro "freedataidx") def $dataidx_instrs(eps) = eps def $dataidx_instrs(instr instr'*) = $dataidx_instr(instr) $dataidx_instrs(instr'*) -def $dataidx_expr(expr) : dataidx* hint(show $dataidx(%)) +def $dataidx_expr(expr) : dataidx* hint(show $dataidx(%)) hint(macro "freedataidx") def $dataidx_expr(in*) = $dataidx_instrs(in*) -def $dataidx_func(func) : dataidx* hint(show $dataidx(%)) +def $dataidx_func(func) : dataidx* hint(show $dataidx(%)) hint(macro "freedataidx") def $dataidx_func(FUNC x loc* e) = $dataidx_expr(e) -def $dataidx_funcs(func*) : dataidx* hint(show $dataidx(%)) +def $dataidx_funcs(func*) : dataidx* hint(show $dataidx(%)) hint(macro "freedataidx") def $dataidx_funcs(eps) = eps def $dataidx_funcs(func func'*) = $dataidx_func(func) $dataidx_funcs(func'*) diff --git a/spectec/spec/wasm-3.0/A-binary.watsup b/spectec/spec/wasm-3.0/A-binary.watsup index e6de9385d5..24b0739097 100644 --- a/spectec/spec/wasm-3.0/A-binary.watsup +++ b/spectec/spec/wasm-3.0/A-binary.watsup @@ -1067,6 +1067,7 @@ grammar Bexportsec : export* hint(desc "export section") = ;; Start section +;; TODO: should return start? grammar Bstart : start* = | x:Bfuncidx => (START x) @@ -1132,6 +1133,7 @@ grammar Bdatasec : data* hint(desc "data section") = ;; Data count section +;; TODO: should return u32? grammar Bdatacnt : u32* hint(desc "data count") = | n:Bu32 => n @@ -1141,61 +1143,65 @@ grammar Bdatacntsec : u32* hint(desc "data count section") = ;; Modules +;; TODO: avoid double empty lines grammar Bmagic : () = 0x00 0x61 0x73 0x6D => () grammar Bversion : () = 0x01 0x00 0x00 0x00 => () grammar Bmodule : module = | Bmagic Bversion - Bcustomsec* - type*:Btypesec Bcustomsec* + type*:Btypesec - import*:Bimportsec Bcustomsec* + import*:Bimportsec - typeidx^n:Bfuncsec Bcustomsec* + typeidx^n:Bfuncsec - table*:Btablesec Bcustomsec* + table*:Btablesec - mem*:Bmemsec Bcustomsec* + mem*:Bmemsec - global*:Bglobalsec Bcustomsec* + global*:Bglobalsec - export*:Bexportsec Bcustomsec* + export*:Bexportsec - start*:Bstartsec Bcustomsec* + start*:Bstartsec - elem*:Belemsec Bcustomsec* + elem*:Belemsec - m'*:Bdatacntsec Bcustomsec* + m'*:Bdatacntsec ;; TODO: should be m'? - (local*, expr)^n:Bcodesec Bcustomsec* + (local*, expr)^n:Bcodesec + Bcustomsec* data^m:Bdatasec + + Bcustomsec* => MODULE type* import* func^n global* table* mem* elem* data^m start* export* - -- if m'* = eps \/ $dataidx_funcs(func^n) = eps + ---- + -- if m'* =/= eps \/ $dataidx_funcs(func^n) = eps -- if m = $sum(m'*) - -- if (func = FUNC typeidx local* expr)^n + -- (if func = FUNC typeidx local* expr)^n diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml index 53d45d73e2..bfb69f8b4a 100644 --- a/spectec/src/backend-latex/render.ml +++ b/spectec/src/backend-latex/render.ml @@ -1237,7 +1237,7 @@ and render_sym env g = | UnparenG ({it = ParenG g1; _} | g1) -> render_sym env g1 and render_syms sep env gs = - altern_map_nl sep " \\\\ &&&\\quad " (render_sym env) gs + altern_map_nl sep " \\\\ &&& " (render_sym env) gs and render_prod arrow env prod = let (g, e, prems) = prod.it in @@ -1245,7 +1245,11 @@ and render_prod arrow env prod = | (TupE [] | ParenE ({it = SeqE []; _}, _)), [] -> render_sym env g | _ -> render_sym env g ^ " " ^ arrow ^ " " ^ - render_conditions env (render_exp env e) "&&&&&" prems + if g.at.right.line = e.at.left.line then + render_conditions env (render_exp env e) "&&&&&" prems + else + render_conditions env ("\\\\\n &&& \\multicolumn{3}{@{}l@{}}{\\qquad " ^ + render_exp env e ^ " }") "&&&&&" prems and render_gram arrow env gram = let (dots1, prods, dots2) = gram.it in diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 2436ac3b00..55021fb5d6 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -1314,7 +1314,7 @@ def $dataidx_instr(instr : instr) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:25.1-25.63 +;; 2-syntax-aux.watsup:25.1-25.89 def $dataidx_instrs(instr*) : dataidx* ;; 2-syntax-aux.watsup:26.1-26.31 def $dataidx_instrs([]) = [] @@ -1335,7 +1335,7 @@ def $dataidx_func(func : func) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:35.1-35.61 +;; 2-syntax-aux.watsup:35.1-35.87 def $dataidx_funcs(func*) : dataidx* ;; 2-syntax-aux.watsup:36.1-36.30 def $dataidx_funcs([]) = [] diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 17f59d0317..9958b9a62c 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -8330,7 +8330,7 @@ $$ \mathtt{0x02}~~{\mathit{bt}}{:}{\mathtt{blocktype}}~~{({\mathit{in}}{:}{\mathtt{instr}})^\ast}~~\mathtt{0x0B} &\quad\Rightarrow&\quad \mathsf{block}~{\mathit{bt}}~{{\mathit{in}}^\ast} \\ &&|& \mathtt{0x03}~~{\mathit{bt}}{:}{\mathtt{blocktype}}~~{({\mathit{in}}{:}{\mathtt{instr}})^\ast}~~\mathtt{0x0B} &\quad\Rightarrow&\quad \mathsf{loop}~{\mathit{bt}}~{{\mathit{in}}^\ast} \\ &&|& \mathtt{0x04}~~{\mathit{bt}}{:}{\mathtt{blocktype}}~~{({\mathit{in}}{:}{\mathtt{instr}})^\ast}~~\mathtt{0x0B} &\quad\Rightarrow&\quad \mathsf{if}~{\mathit{bt}}~{{\mathit{in}}^\ast}~\mathsf{else}~\epsilon \\ &&|& -\mathtt{0x04}~~{\mathit{bt}}{:}{\mathtt{blocktype}}~~{({\mathit{in}}_1{:}{\mathtt{instr}})^\ast} \\ &&&\quad \mathtt{0x05}~~{({\mathit{in}}_2{:}{\mathtt{instr}})^\ast}~~\mathtt{0x0B} &\quad\Rightarrow&\quad \mathsf{if}~{\mathit{bt}}~{{\mathit{in}}_1^\ast}~\mathsf{else}~{{\mathit{in}}_2^\ast} \\ &&|& +\mathtt{0x04}~~{\mathit{bt}}{:}{\mathtt{blocktype}}~~{({\mathit{in}}_1{:}{\mathtt{instr}})^\ast} \\ &&& \mathtt{0x05}~~{({\mathit{in}}_2{:}{\mathtt{instr}})^\ast}~~\mathtt{0x0B} &\quad\Rightarrow&\quad \mathsf{if}~{\mathit{bt}}~{{\mathit{in}}_1^\ast}~\mathsf{else}~{{\mathit{in}}_2^\ast} \\ &&|& \mathtt{0x0C}~~l{:}{\mathtt{labelidx}} &\quad\Rightarrow&\quad \mathsf{br}~l \\ &&|& \mathtt{0x0D}~~l{:}{\mathtt{labelidx}} &\quad\Rightarrow&\quad \mathsf{br\_if}~l \\ &&|& \mathtt{0x0E}~~{l^\ast}{:}{\mathtt{list}}({\mathtt{labelidx}})~~l_n{:}{\mathtt{labelidx}} &\quad\Rightarrow&\quad \mathsf{br\_table}~{l^\ast}~l_n \\ &&|& @@ -8389,8 +8389,8 @@ $$ \mathtt{0xFB}~~21{:}{\mathtt{u32}}~~{\mathit{ht}}{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{ref{.}test}~(\mathsf{ref}~\mathsf{null}~{\mathit{ht}}) \\ &&|& \mathtt{0xFB}~~22{:}{\mathtt{u32}}~~{\mathit{ht}}{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{ref{.}cast}~(\mathsf{ref}~{\mathit{ht}}) \\ &&|& \mathtt{0xFB}~~23{:}{\mathtt{u32}}~~{\mathit{ht}}{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{ref{.}cast}~(\mathsf{ref}~\mathsf{null}~{\mathit{ht}}) \\ &&|& -\mathtt{0xFB}~~24{:}{\mathtt{u32}}~~({\mathsf{null}}{{{}_{1}^?}}, {\mathsf{null}}{{{}_{2}^?}}){:}{\mathtt{castop}} \\ &&&\quad l{:}{\mathtt{labelidx}}~~{\mathit{ht}}_1{:}{\mathtt{heaptype}}~~{\mathit{ht}}_2{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{br\_on\_cast}~l~(\mathsf{ref}~{\mathsf{null}}{{{}_{1}^?}}~{\mathit{ht}}_1)~(\mathsf{ref}~{\mathsf{null}}{{{}_{2}^?}}~{\mathit{ht}}_2) \\ &&|& -\mathtt{0xFB}~~25{:}{\mathtt{u32}}~~({\mathsf{null}}{{{}_{1}^?}}, {\mathsf{null}}{{{}_{2}^?}}){:}{\mathtt{castop}} \\ &&&\quad l{:}{\mathtt{labelidx}}~~{\mathit{ht}}_1{:}{\mathtt{heaptype}}~~{\mathit{ht}}_2{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{br\_on\_cast\_fail}~l~(\mathsf{ref}~{\mathsf{null}}{{{}_{1}^?}}~{\mathit{ht}}_1)~(\mathsf{ref}~{\mathsf{null}}{{{}_{2}^?}}~{\mathit{ht}}_2) \\ &&|& +\mathtt{0xFB}~~24{:}{\mathtt{u32}}~~({\mathsf{null}}{{{}_{1}^?}}, {\mathsf{null}}{{{}_{2}^?}}){:}{\mathtt{castop}} \\ &&& l{:}{\mathtt{labelidx}}~~{\mathit{ht}}_1{:}{\mathtt{heaptype}}~~{\mathit{ht}}_2{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{br\_on\_cast}~l~(\mathsf{ref}~{\mathsf{null}}{{{}_{1}^?}}~{\mathit{ht}}_1)~(\mathsf{ref}~{\mathsf{null}}{{{}_{2}^?}}~{\mathit{ht}}_2) \\ &&|& +\mathtt{0xFB}~~25{:}{\mathtt{u32}}~~({\mathsf{null}}{{{}_{1}^?}}, {\mathsf{null}}{{{}_{2}^?}}){:}{\mathtt{castop}} \\ &&& l{:}{\mathtt{labelidx}}~~{\mathit{ht}}_1{:}{\mathtt{heaptype}}~~{\mathit{ht}}_2{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{br\_on\_cast\_fail}~l~(\mathsf{ref}~{\mathsf{null}}{{{}_{1}^?}}~{\mathit{ht}}_1)~(\mathsf{ref}~{\mathsf{null}}{{{}_{2}^?}}~{\mathit{ht}}_2) \\ &&|& \mathtt{0xFB}~~26{:}{\mathtt{u32}} &\quad\Rightarrow&\quad \mathsf{any{.}convert\_extern} \\ &&|& \mathtt{0xFB}~~27{:}{\mathtt{u32}} &\quad\Rightarrow&\quad \mathsf{extern{.}convert\_any} \\ &&|& \mathtt{0xFB}~~28{:}{\mathtt{u32}} &\quad\Rightarrow&\quad \mathsf{ref{.}i{\scriptstyle 31}} \\ &&|& @@ -9003,14 +9003,22 @@ $$ $$ \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}} & {\mathtt{elemkind}} &::=& \mathtt{0x00} &\quad\Rightarrow&\quad \mathsf{ref}~\mathsf{null}~\mathsf{func} \\ -& {\mathtt{elem}} &::=& 0{:}{\mathtt{u32}}~~e_o{:}{\mathtt{expr}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{func})~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~0~e_o) \\ &&|& -1{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~\mathsf{passive} \\ &&|& -2{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~e{:}{\mathtt{expr}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~x~e) \\ &&|& -3{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~\mathsf{declare} \\ &&|& -4{:}{\mathtt{u32}}~~e_{\mathsf{o}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~0~e_{\mathsf{o}}) \\ &&|& -5{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{reftype}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{e^\ast}~\mathsf{passive} \\ &&|& -6{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~e_{\mathsf{o}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~x~e_{\mathsf{o}}) \\ &&|& -7{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{reftype}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{e^\ast}~\mathsf{declare} \\ +& {\mathtt{elem}} &::=& 0{:}{\mathtt{u32}}~~e_o{:}{\mathtt{expr}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \\ + &&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~(\mathsf{ref}~\mathsf{func})~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~0~e_o) } \\ &&|& +1{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \\ + &&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~\mathsf{passive} } \\ &&|& +2{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~e{:}{\mathtt{expr}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \\ + &&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~x~e) } \\ &&|& +3{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \\ + &&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~\mathsf{declare} } \\ &&|& +4{:}{\mathtt{u32}}~~e_{\mathsf{o}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \\ + &&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~0~e_{\mathsf{o}}) } \\ &&|& +5{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{reftype}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \\ + &&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~{\mathit{rt}}~{e^\ast}~\mathsf{passive} } \\ &&|& +6{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~e_{\mathsf{o}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \\ + &&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~x~e_{\mathsf{o}}) } \\ &&|& +7{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{reftype}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \\ + &&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~{\mathit{rt}}~{e^\ast}~\mathsf{declare} } \\ & {\mathtt{elemsec}} &::=& {{\mathit{elem}}^\ast}{:}{{\mathtt{section}}}_{9}({\mathtt{list}}({\mathtt{elem}})) &\quad\Rightarrow&\quad {{\mathit{elem}}^\ast} \\ \end{array} $$ @@ -9060,10 +9068,11 @@ $$ \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}} & {\mathtt{magic}} &::=& \mathtt{0x00}~~\mathtt{0x61}~~\mathtt{0x73}~~\mathtt{0x6D} \\ & {\mathtt{version}} &::=& \mathtt{0x01}~~\mathtt{0x00}~~\mathtt{0x00}~~\mathtt{0x00} \\ -& {\mathtt{module}} &::=& {\mathtt{magic}}~~{\mathtt{version}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{type}}^\ast}{:}{\mathtt{typesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{import}}^\ast}{:}{\mathtt{importsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{typeidx}}^{n}}{:}{\mathtt{funcsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{table}}^\ast}{:}{\mathtt{tablesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{mem}}^\ast}{:}{\mathtt{memsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{global}}^\ast}{:}{\mathtt{globalsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{export}}^\ast}{:}{\mathtt{exportsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{start}}^\ast}{:}{\mathtt{startsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{elem}}^\ast}{:}{\mathtt{elemsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{m'}^\ast}{:}{\mathtt{datacntsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {({{\mathit{local}}^\ast}, {\mathit{expr}})^{n}}{:}{\mathtt{codesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{data}}^{m}}{:}{\mathtt{datasec}}~~{{\mathtt{customsec}}^\ast} &\quad\Rightarrow&\quad \mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^{n}}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^{m}}~{{\mathit{start}}^\ast}~{{\mathit{export}}^\ast} - &\qquad \mbox{if}~{{m'}^\ast} = \epsilon \lor {\mathrm{dataidx}}({{\mathit{func}}^{n}}) = \epsilon \\ - &&&&&&\qquad {\land}~m = {\mathrm{sum}}({{m'}^\ast}) \\ - &&&&&&\qquad {\land}~(({\mathit{func}} = \mathsf{func}~{\mathit{typeidx}}~{{\mathit{local}}^\ast}~{\mathit{expr}}))^{n} \\ +& {\mathtt{module}} &::=& {\mathtt{magic}}~~{\mathtt{version}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{type}}^\ast}{:}{\mathtt{typesec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{import}}^\ast}{:}{\mathtt{importsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{typeidx}}^{n}}{:}{\mathtt{funcsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{table}}^\ast}{:}{\mathtt{tablesec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{mem}}^\ast}{:}{\mathtt{memsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{global}}^\ast}{:}{\mathtt{globalsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{export}}^\ast}{:}{\mathtt{exportsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{start}}^\ast}{:}{\mathtt{startsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{elem}}^\ast}{:}{\mathtt{elemsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{m'}^\ast}{:}{\mathtt{datacntsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{({{\mathit{local}}^\ast}, {\mathit{expr}})^{n}}{:}{\mathtt{codesec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{data}}^{m}}{:}{\mathtt{datasec}} \\ &&& {{\mathtt{customsec}}^\ast} &\quad\Rightarrow&\quad \\ + &&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^{n}}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^{m}}~{{\mathit{start}}^\ast}~{{\mathit{export}}^\ast} } \\ + &&&&& \multicolumn{2}{l@{}}{\quad \mbox{if}~{{m'}^\ast} \neq \epsilon \lor {\mathrm{dataidx}}({{\mathit{func}}^{n}}) = \epsilon} \\ + &&&&& \multicolumn{2}{l@{}}{\quad {\land}~m = {\mathrm{sum}}({{m'}^\ast})} \\ + &&&&& \multicolumn{2}{l@{}}{\quad {\land}~({\mathit{func}} = \mathsf{func}~{\mathit{typeidx}}~{{\mathit{local}}^\ast}~{\mathit{expr}})^{n}} \\ \end{array} $$ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 58a63f1a94..5d3f4f6b69 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -1304,7 +1304,7 @@ def $dataidx_instr(instr : instr) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:25.1-25.63 +;; 2-syntax-aux.watsup:25.1-25.89 def $dataidx_instrs(instr*) : dataidx* ;; 2-syntax-aux.watsup:26.1-26.31 def $dataidx_instrs([]) = [] @@ -1325,7 +1325,7 @@ def $dataidx_func(func : func) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:35.1-35.61 +;; 2-syntax-aux.watsup:35.1-35.87 def $dataidx_funcs(func*) : dataidx* ;; 2-syntax-aux.watsup:36.1-36.30 def $dataidx_funcs([]) = [] @@ -7160,7 +7160,7 @@ def $dataidx_instr(instr : instr) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:25.1-25.63 +;; 2-syntax-aux.watsup:25.1-25.89 def $dataidx_instrs(instr*) : dataidx* ;; 2-syntax-aux.watsup:26.1-26.31 def $dataidx_instrs([]) = [] @@ -7181,7 +7181,7 @@ def $dataidx_func(func : func) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:35.1-35.61 +;; 2-syntax-aux.watsup:35.1-35.87 def $dataidx_funcs(func*) : dataidx* ;; 2-syntax-aux.watsup:36.1-36.30 def $dataidx_funcs([]) = [] @@ -13021,7 +13021,7 @@ def $dataidx_instr(instr : instr) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:25.1-25.63 +;; 2-syntax-aux.watsup:25.1-25.89 def $dataidx_instrs(instr*) : dataidx* ;; 2-syntax-aux.watsup:26.1-26.31 def $dataidx_instrs([]) = [] @@ -13042,7 +13042,7 @@ def $dataidx_func(func : func) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:35.1-35.61 +;; 2-syntax-aux.watsup:35.1-35.87 def $dataidx_funcs(func*) : dataidx* ;; 2-syntax-aux.watsup:36.1-36.30 def $dataidx_funcs([]) = [] @@ -18882,7 +18882,7 @@ def $dataidx_instr(instr : instr) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:25.1-25.63 +;; 2-syntax-aux.watsup:25.1-25.89 def $dataidx_instrs(instr*) : dataidx* ;; 2-syntax-aux.watsup:26.1-26.31 def $dataidx_instrs([]) = [] @@ -18903,7 +18903,7 @@ def $dataidx_func(func : func) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:35.1-35.61 +;; 2-syntax-aux.watsup:35.1-35.87 def $dataidx_funcs(func*) : dataidx* ;; 2-syntax-aux.watsup:36.1-36.30 def $dataidx_funcs([]) = [] @@ -24909,7 +24909,7 @@ def $dataidx_instr(instr : instr) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:25.1-25.63 +;; 2-syntax-aux.watsup:25.1-25.89 def $dataidx_instrs(instr*) : dataidx* ;; 2-syntax-aux.watsup:26.1-26.31 def $dataidx_instrs([]) = [] @@ -24930,7 +24930,7 @@ def $dataidx_func(func : func) : dataidx* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:35.1-35.61 +;; 2-syntax-aux.watsup:35.1-35.87 def $dataidx_funcs(func*) : dataidx* ;; 2-syntax-aux.watsup:36.1-36.30 def $dataidx_funcs([]) = []