@@ -8708,14 +8708,21 @@ grammar Btypesec : type*
87088708 prod{`ty*` : type*} ty*{ty <- `ty*`}:Bsection_(1, syntax type, grammar Blist(syntax type, grammar Btype)) => ty*{ty <- `ty*`}
87098709
87108710;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
8711- grammar Bimport : import
8711+ grammar Bimport : (name, externtype)
87128712 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
8713- prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {nm_2:Bname} {xt:Bexterntype}} => IMPORT_import(nm_1, nm_2, xt)
8713+ prod{nm_2 : name, xt : externtype} {{nm_2:Bname} {xt:Bexterntype}} => (nm_2, xt)
8714+
8715+ ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
8716+ grammar Bimports : import*
8717+ ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
8718+ prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {(nm_2, xt):Bimport}} => [IMPORT_import(nm_1, nm_2, xt)]
8719+ ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
8720+ prod{nm_1 : name, `nm_2*` : name*, `xt*` : externtype*} {{0x01} {0xFF} {nm_1:Bname} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimport)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
87148721
87158722;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
87168723grammar Bimportsec : import*
87178724 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
8718- prod{`im*` : import*} im*{im <- `im*`}:Bsection_(2, syntax import, grammar Blist(syntax import, grammar Bimport )) => im*{im <- `im*`}
8725+ prod{`im** ` : import** } im*{im <- `im*`}*{`im*` <- `im**`} :Bsection_(2, syntax import* , grammar Blist(syntax import* , grammar Bimports )) => $concat_(syntax import, im*{im <- `im*`}*{`im*` <- `im**`})
87198726
87208727;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
87218728grammar Bfuncsec : typeidx*
@@ -10863,6 +10870,9 @@ grammar Tstart_(I : I) : (start, idctxt)
1086310870 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1086410871 prod{x : idx} {{"("} {"start"} {x:Tfuncidx_(I)} {")"}} => (START_start(x), {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []})
1086510872
10873+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
10874+ grammar Timports_(I : I) : (import*, idctxt)
10875+
1086610876;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1086710877grammar Timport_(I : I) : (import, idctxt)
1086810878 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
@@ -10963,153 +10973,153 @@ syntax decl =
1096310973;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1096410974rec {
1096510975
10966- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:258 .1-258 .76
10976+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261 .1-261 .76
1096710977def $typesd(decl*) : type*
10968- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270 .1-270 .23
10978+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273 .1-273 .23
1096910979 def $typesd([]) = []
10970- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271 .1-271 .48
10980+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274 .1-274 .48
1097110981 def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`})
10972- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:272 .1-272 .57
10982+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275 .1-275 .57
1097310983 def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`})
1097410984 -- otherwise
1097510985}
1097610986
1097710987;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1097810988rec {
1097910989
10980- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:259 .1-259 .78
10990+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262 .1-262 .78
1098110991def $importsd(decl*) : import*
10982- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274 .1-274 .25
10992+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:277 .1-277 .25
1098310993 def $importsd([]) = []
10984- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275 .1-275 .56
10994+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278 .1-278 .56
1098510995 def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`})
10986- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:276 .1-276 .61
10996+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279 .1-279 .61
1098710997 def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`})
1098810998 -- otherwise
1098910999}
1099011000
1099111001;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1099211002rec {
1099311003
10994- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:260 .1-260 .75
11004+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263 .1-263 .75
1099511005def $tagsd(decl*) : tag*
10996- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278 .1-278 .22
11006+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:281 .1-281 .22
1099711007 def $tagsd([]) = []
10998- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279 .1-279 .44
11008+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282 .1-282 .44
1099911009 def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`})
11000- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:280 .1-280 .55
11010+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283 .1-283 .55
1100111011 def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`})
1100211012 -- otherwise
1100311013}
1100411014
1100511015;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1100611016rec {
1100711017
11008- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261 .1-261 .78
11018+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264 .1-264 .78
1100911019def $globalsd(decl*) : global*
11010- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282 .1-282 .25
11020+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:285 .1-285 .25
1101111021 def $globalsd([]) = []
11012- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283 .1-283 .56
11022+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286 .1-286 .56
1101311023 def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`})
11014- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:284 .1-284 .61
11024+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287 .1-287 .61
1101511025 def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`})
1101611026 -- otherwise
1101711027}
1101811028
1101911029;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1102011030rec {
1102111031
11022- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262 .1-262 .75
11032+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265 .1-265 .75
1102311033def $memsd(decl*) : mem*
11024- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286 .1-286 .22
11034+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:289 .1-289 .22
1102511035 def $memsd([]) = []
11026- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287 .1-287 .44
11036+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290 .1-290 .44
1102711037 def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`})
11028- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:288 .1-288 .55
11038+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291 .1-291 .55
1102911039 def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`})
1103011040 -- otherwise
1103111041}
1103211042
1103311043;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1103411044rec {
1103511045
11036- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263 .1-263 .77
11046+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266 .1-266 .77
1103711047def $tablesd(decl*) : table*
11038- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290 .1-290 .24
11048+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:293 .1-293 .24
1103911049 def $tablesd([]) = []
11040- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291 .1-291 .52
11050+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294 .1-294 .52
1104111051 def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`})
11042- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:292 .1-292 .59
11052+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295 .1-295 .59
1104311053 def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`})
1104411054 -- otherwise
1104511055}
1104611056
1104711057;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1104811058rec {
1104911059
11050- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264 .1-264 .76
11060+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267 .1-267 .76
1105111061def $funcsd(decl*) : func*
11052- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294 .1-294 .23
11062+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:297 .1-297 .23
1105311063 def $funcsd([]) = []
11054- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295 .1-295 .48
11064+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298 .1-298 .48
1105511065 def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`})
11056- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:296 .1-296 .57
11066+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299 .1-299 .57
1105711067 def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`})
1105811068 -- otherwise
1105911069}
1106011070
1106111071;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1106211072rec {
1106311073
11064- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265 .1-265 .76
11074+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268 .1-268 .76
1106511075def $datasd(decl*) : data*
11066- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298 .1-298 .23
11076+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:301 .1-301 .23
1106711077 def $datasd([]) = []
11068- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299 .1-299 .48
11078+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302 .1-302 .48
1106911079 def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`})
11070- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:300 .1-300 .57
11080+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303 .1-303 .57
1107111081 def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`})
1107211082 -- otherwise
1107311083}
1107411084
1107511085;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1107611086rec {
1107711087
11078- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266 .1-266 .76
11088+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269 .1-269 .76
1107911089def $elemsd(decl*) : elem*
11080- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302 .1-302 .23
11090+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:305 .1-305 .23
1108111091 def $elemsd([]) = []
11082- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303 .1-303 .48
11092+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306 .1-306 .48
1108311093 def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`})
11084- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:304 .1-304 .57
11094+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307 .1-307 .57
1108511095 def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`})
1108611096 -- otherwise
1108711097}
1108811098
1108911099;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1109011100rec {
1109111101
11092- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267 .1-267 .77
11102+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270 .1-270 .77
1109311103def $startsd(decl*) : start*
11094- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306 .1-306 .24
11104+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:309 .1-309 .24
1109511105 def $startsd([]) = []
11096- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307 .1-307 .52
11106+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310 .1-310 .52
1109711107 def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
11098- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:308 .1-308 .59
11108+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311 .1-311 .59
1109911109 def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
1110011110 -- otherwise
1110111111}
1110211112
1110311113;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
1110411114rec {
1110511115
11106- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268 .1-268 .78
11116+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271 .1-271 .78
1110711117def $exportsd(decl*) : export*
11108- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310 .1-310 .25
11118+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:313 .1-313 .25
1110911119 def $exportsd([]) = []
11110- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311 .1-311 .56
11120+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314 .1-314 .56
1111111121 def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`})
11112- ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:312 .1-312 .61
11122+ ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315 .1-315 .61
1111311123 def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`})
1111411124 -- otherwise
1111511125}
0 commit comments