From 692b6e649b5df1156d6c25af1e3ae418b2ad4a4e Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 12 Sep 2024 09:39:00 +0200 Subject: [PATCH 1/3] Fix closing of types; fix rendering of nul --- spectec/spec/wasm-3.0/2-syntax-aux.watsup | 6 + spectec/spec/wasm-3.0/6-typing.watsup | 6 +- spectec/spec/wasm-3.0/9-module.watsup | 12 +- spectec/test-frontend/TEST.md | 239 +++--- spectec/test-latex/TEST.md | 36 +- spectec/test-middlend/TEST.md | 956 ++++++++++++---------- spectec/test-prose/TEST.md | 76 +- spectec/test-splice/TEST.md | 8 +- 8 files changed, 748 insertions(+), 591 deletions(-) diff --git a/spectec/spec/wasm-3.0/2-syntax-aux.watsup b/spectec/spec/wasm-3.0/2-syntax-aux.watsup index 7d33db4c1c..dead0cd665 100644 --- a/spectec/spec/wasm-3.0/2-syntax-aux.watsup +++ b/spectec/spec/wasm-3.0/2-syntax-aux.watsup @@ -611,11 +611,17 @@ def $subst_moduletype(xt_1* -> xt_2*, tv*, tu*) = $subst_externtype(xt_1, tv*, t def $subst_all_valtype(valtype, heaptype*) : valtype hint(show %#`[:=%]) hint(macro "%subst") def $subst_all_reftype(reftype, heaptype*) : reftype hint(show %#`[:=%]) hint(macro "%subst") def $subst_all_deftype(deftype, heaptype*) : deftype hint(show %#`[:=%]) hint(macro "%subst") +def $subst_all_globaltype(globaltype, heaptype*) : globaltype hint(show %#`[:=%]) hint(macro "%subst") +def $subst_all_tabletype(tabletype, heaptype*) : tabletype hint(show %#`[:=%]) hint(macro "%subst") +def $subst_all_memtype(memtype, heaptype*) : memtype hint(show %#`[:=%]) hint(macro "%subst") def $subst_all_moduletype(moduletype, heaptype*) : moduletype hint(show %#`[:=%]) hint(macro "%subst") def $subst_all_valtype(t, tu^n) = $subst_valtype(t, (_IDX i)^(i (REF nul EXTERN) + C |- EXTERN.CONVERT_ANY : (REF nul1 ANY) -> (REF nul2 EXTERN) + -- if nul1 = nul2 rule Instr_ok/any.convert_extern: - C |- ANY.CONVERT_EXTERN : (REF nul EXTERN) -> (REF nul ANY) + C |- ANY.CONVERT_EXTERN : (REF nul1 EXTERN) -> (REF nul2 ANY) + -- if nul1 = nul2 ;; Vector instructions diff --git a/spectec/spec/wasm-3.0/9-module.watsup b/spectec/spec/wasm-3.0/9-module.watsup index a72ffa9b91..da7e945483 100644 --- a/spectec/spec/wasm-3.0/9-module.watsup +++ b/spectec/spec/wasm-3.0/9-module.watsup @@ -57,9 +57,9 @@ def $allocmems(s, memtype memtype'*) = (s_2, ma ma'*) -- if (s_2, ma'*) = $allocmems(s_1, memtype'*) def $alloctag(store, tagtype) : (store, tagaddr) -def $alloctag(s, at) = (s ++ {TAGS taginst}, |s.TAGS|) +def $alloctag(s, tagtype) = (s ++ {TAGS taginst}, |s.TAGS|) ---- ---- - -- if taginst = { TYPE at } + -- if taginst = { TYPE tagtype } def $alloctags(store, tagtype*) : (store, tagaddr*) hint(show $alloctag*#((%,%))) def $alloctags(s, eps) = (s, eps) @@ -129,11 +129,11 @@ def $allocmodule(s, module, externaddr*, val_G*, ref_T*, (ref_E*)*) = (s_7, modu -- if da* = ($(|s.DATAS|+i_D))^(i_D<|data*|) -- if dt* = $alloctypes(type*) -- if (s_1, fa*) = $allocfuncs(s, dt*[x]*, (FUNC x local* expr_F)*, moduleinst^(|func*|)) - -- if (s_2, ga*) = $allocglobals(s_1, globaltype*, val_G*) - -- if (s_3, ta*) = $alloctables(s_2, tabletype*, ref_T*) - -- if (s_4, ma*) = $allocmems(s_3, memtype*) + -- if (s_2, ga*) = $allocglobals(s_1, $subst_all_globaltype(globaltype, dt*)*, val_G*) + -- if (s_3, ta*) = $alloctables(s_2, $subst_all_tabletype(tabletype, dt*)*, ref_T*) + -- if (s_4, ma*) = $allocmems(s_3, $subst_all_memtype(memtype, dt*)*) -- if (s_5, aa*) = $alloctags(s_4, dt*[y]*) - -- if (s_6, ea*) = $allocelems(s_5, elemtype*, (ref_E*)*) + -- if (s_6, ea*) = $allocelems(s_5, $subst_all_reftype(elemtype, dt*)*, (ref_E*)*) -- if (s_7, da*) = $allocdatas(s_6, OK^(|data*|), (byte*)*) ;; TODO(2, rossberg): use moduleinst here and remove hack above -- if xi* = $allocexports({FUNCS fa_I* fa*, GLOBALS ga_I* ga*, TABLES ta_I* ta*, MEMS ma_I* ma*, TAGS aa_I* aa*}, export*) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 1f95f5a671..110b985a80 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -2270,6 +2270,21 @@ def $subst_all_deftype(deftype : deftype, heaptype*) : deftype ;; 2-syntax-aux.watsup def $subst_all_deftype{dt : deftype, `tu*` : typeuse*, n : n, `i*` : nat*}(dt, (tu : typeuse <: heaptype)^n{tu <- `tu*`}) = $subst_deftype(dt, _IDX_typevar(`%`_typeidx(i))^(i_%%`_instrtype(`%`_resulttype([REF_valtype(nul, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(nul, EXTERN_heaptype)]))) + ;; 6-typing.watsup:916.1-918.20 + rule extern.convert_any{C : context, nul1 : nul1, nul2 : nul2}: + `%|-%:%`(C, EXTERN.CONVERT_ANY_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul1, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(nul2, EXTERN_heaptype)]))) + -- if (nul1 = nul2) - ;; 6-typing.watsup:919.1-920.62 - rule any.convert_extern{C : context, nul : nul}: - `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(nul, ANY_heaptype)]))) + ;; 6-typing.watsup:920.1-922.20 + rule any.convert_extern{C : context, nul1 : nul1, nul2 : nul2}: + `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul1, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(nul2, ANY_heaptype)]))) + -- if (nul1 = nul2) - ;; 6-typing.watsup:925.1-926.35 + ;; 6-typing.watsup:927.1-928.35 rule vconst{C : context, c : vec_(V128_Vnn)}: `%|-%:%`(C, VCONST_instr(V128_vectype, c), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:928.1-929.41 + ;; 6-typing.watsup:930.1-931.41 rule vvunop{C : context, vvunop : vvunop}: `%|-%:%`(C, VVUNOP_instr(V128_vectype, vvunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:931.1-932.48 + ;; 6-typing.watsup:933.1-934.48 rule vvbinop{C : context, vvbinop : vvbinop}: `%|-%:%`(C, VVBINOP_instr(V128_vectype, vvbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:934.1-935.55 + ;; 6-typing.watsup:936.1-937.55 rule vvternop{C : context, vvternop : vvternop}: `%|-%:%`(C, VVTERNOP_instr(V128_vectype, vvternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:937.1-938.44 + ;; 6-typing.watsup:939.1-940.44 rule vvtestop{C : context, vvtestop : vvtestop}: `%|-%:%`(C, VVTESTOP_instr(V128_vectype, vvtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:940.1-941.37 + ;; 6-typing.watsup:942.1-943.37 rule vunop{C : context, sh : shape, vunop : vunop_(sh)}: `%|-%:%`(C, VUNOP_instr(sh, vunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:943.1-944.44 + ;; 6-typing.watsup:945.1-946.44 rule vbinop{C : context, sh : shape, vbinop : vbinop_(sh)}: `%|-%:%`(C, VBINOP_instr(sh, vbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:946.1-947.40 + ;; 6-typing.watsup:948.1-949.40 rule vtestop{C : context, sh : shape, vtestop : vtestop_(sh)}: `%|-%:%`(C, VTESTOP_instr(sh, vtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:949.1-950.44 + ;; 6-typing.watsup:951.1-952.44 rule vrelop{C : context, sh : shape, vrelop : vrelop_(sh)}: `%|-%:%`(C, VRELOP_instr(sh, vrelop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:952.1-953.47 + ;; 6-typing.watsup:954.1-955.47 rule vshiftop{C : context, sh : ishape, vshiftop : vshiftop_(sh)}: `%|-%:%`(C, VSHIFTOP_instr(sh, vshiftop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype I32_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:955.1-956.33 + ;; 6-typing.watsup:957.1-958.33 rule vbitmask{C : context, sh : ishape}: `%|-%:%`(C, VBITMASK_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:958.1-959.39 + ;; 6-typing.watsup:960.1-961.39 rule vswizzle{C : context, sh : ishape}: `%|-%:%`(C, VSWIZZLE_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:961.1-963.29 + ;; 6-typing.watsup:963.1-965.29 rule vshuffle{C : context, sh : ishape, `i*` : nat*}: `%|-%:%`(C, VSHUFFLE_instr(sh, `%`_laneidx(i)*{i <- `i*`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- (if (i < (2 * $dim((sh : ishape <: shape))!`%`_dim.0)))*{i <- `i*`} - ;; 6-typing.watsup:965.1-966.44 + ;; 6-typing.watsup:967.1-968.44 rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:968.1-970.21 + ;; 6-typing.watsup:970.1-972.21 rule vextract_lane{C : context, sh : shape, `sx?` : sx?, i : nat}: `%|-%:%`(C, VEXTRACT_LANE_instr(sh, sx?{sx <- `sx?`}, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([($unpackshape(sh) : numtype <: valtype)]))) -- if (i < $dim(sh)!`%`_dim.0) - ;; 6-typing.watsup:972.1-974.21 + ;; 6-typing.watsup:974.1-976.21 rule vreplace_lane{C : context, sh : shape, i : nat}: `%|-%:%`(C, VREPLACE_LANE_instr(sh, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([V128_valtype ($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (i < $dim(sh)!`%`_dim.0) - ;; 6-typing.watsup:976.1-977.50 + ;; 6-typing.watsup:978.1-979.50 rule vextunop{C : context, sh_1 : ishape, sh_2 : ishape, vextunop : vextunop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTUNOP_instr(sh_1, sh_2, vextunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:979.1-980.57 + ;; 6-typing.watsup:981.1-982.57 rule vextbinop{C : context, sh_1 : ishape, sh_2 : ishape, vextbinop : vextbinop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTBINOP_instr(sh_1, sh_2, vextbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:982.1-983.48 + ;; 6-typing.watsup:984.1-985.48 rule vnarrow{C : context, sh_1 : ishape, sh_2 : ishape, sx : sx}: `%|-%:%`(C, VNARROW_instr(sh_1, sh_2, sx), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:985.1-986.58 + ;; 6-typing.watsup:987.1-988.58 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop__(sh_2, sh_1), `half?` : half__(sh_2, sh_1)?, `zero?` : zero__(sh_2, sh_1)?}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop, half?{half <- `half?`}, zero?{zero <- `zero?`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:991.1-993.28 + ;; 6-typing.watsup:993.1-995.28 rule local.get{C : context, x : idx, t : valtype}: `%|-%:%`(C, LOCAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(SET_init, t)) - ;; 6-typing.watsup:995.1-997.29 + ;; 6-typing.watsup:997.1-999.29 rule local.set{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; 6-typing.watsup:999.1-1001.29 + ;; 6-typing.watsup:1001.1-1003.29 rule local.tee{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.TEE_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; 6-typing.watsup:1006.1-1008.29 + ;; 6-typing.watsup:1008.1-1010.29 rule global.get{C : context, x : idx, t : valtype, mut : mut}: `%|-%:%`(C, GLOBAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(mut, t)) - ;; 6-typing.watsup:1010.1-1012.29 + ;; 6-typing.watsup:1012.1-1014.29 rule global.set{C : context, x : idx, t : valtype}: `%|-%:%`(C, GLOBAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [], `%`_resulttype([]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(`MUT%?`_mut(?(())), t)) - ;; 6-typing.watsup:1017.1-1019.29 + ;; 6-typing.watsup:1019.1-1021.29 rule table.get{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(rt : reftype <: valtype)]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1021.1-1023.29 + ;; 6-typing.watsup:1023.1-1025.29 rule table.set{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (rt : reftype <: valtype)]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1025.1-1027.29 + ;; 6-typing.watsup:1027.1-1029.29 rule table.size{C : context, x : idx, lim : limits, rt : reftype}: `%|-%:%`(C, TABLE.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([I32_valtype]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1029.1-1031.29 + ;; 6-typing.watsup:1031.1-1033.29 rule table.grow{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) I32_valtype]), [], `%`_resulttype([I32_valtype]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1033.1-1035.29 + ;; 6-typing.watsup:1035.1-1037.29 rule table.fill{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (rt : reftype <: valtype) I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1037.1-1041.36 + ;; 6-typing.watsup:1039.1-1043.36 rule table.copy{C : context, x_1 : idx, x_2 : idx, lim_1 : limits, rt_1 : reftype, lim_2 : limits, rt_2 : reftype}: `%|-%:%`(C, TABLE.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x_1!`%`_idx.0] = `%%`_tabletype(lim_1, rt_1)) -- if (C.TABLES_context[x_2!`%`_idx.0] = `%%`_tabletype(lim_2, rt_2)) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; 6-typing.watsup:1043.1-1047.36 + ;; 6-typing.watsup:1045.1-1049.36 rule table.init{C : context, x : idx, y : idx, lim : limits, rt_1 : reftype, rt_2 : reftype}: `%|-%:%`(C, TABLE.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt_1)) -- if (C.ELEMS_context[y!`%`_idx.0] = rt_2) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; 6-typing.watsup:1049.1-1051.24 + ;; 6-typing.watsup:1051.1-1053.24 rule elem.drop{C : context, x : idx, rt : reftype}: `%|-%:%`(C, ELEM.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.ELEMS_context[x!`%`_idx.0] = rt) - ;; 6-typing.watsup:1056.1-1058.23 + ;; 6-typing.watsup:1058.1-1060.23 rule memory.size{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([I32_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1060.1-1062.23 + ;; 6-typing.watsup:1062.1-1064.23 rule memory.grow{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([I32_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1064.1-1066.23 + ;; 6-typing.watsup:1066.1-1068.23 rule memory.fill{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1068.1-1071.27 + ;; 6-typing.watsup:1070.1-1073.27 rule memory.copy{C : context, x_1 : idx, x_2 : idx, mt_1 : memtype, mt_2 : memtype}: `%|-%:%`(C, MEMORY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x_1!`%`_idx.0] = mt_1) -- if (C.MEMS_context[x_2!`%`_idx.0] = mt_2) - ;; 6-typing.watsup:1073.1-1076.24 + ;; 6-typing.watsup:1075.1-1078.24 rule memory.init{C : context, x : idx, y : idx, mt : memtype}: `%|-%:%`(C, MEMORY.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; 6-typing.watsup:1078.1-1080.24 + ;; 6-typing.watsup:1080.1-1082.24 rule data.drop{C : context, x : idx}: `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) - ;; 6-typing.watsup:1091.1-1094.43 + ;; 6-typing.watsup:1093.1-1096.43 rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8)) - ;; 6-typing.watsup:1096.1-1099.35 + ;; 6-typing.watsup:1098.1-1101.35 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8)) - ;; 6-typing.watsup:1110.1-1113.43 + ;; 6-typing.watsup:1112.1-1115.43 rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8)) - ;; 6-typing.watsup:1115.1-1118.35 + ;; 6-typing.watsup:1117.1-1120.35 rule `store-pack`{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8)) - ;; 6-typing.watsup:1120.1-1123.46 + ;; 6-typing.watsup:1122.1-1125.46 rule `vload-val`{C : context, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8)) - ;; 6-typing.watsup:1125.1-1128.39 + ;; 6-typing.watsup:1127.1-1130.39 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N)) - ;; 6-typing.watsup:1130.1-1133.35 + ;; 6-typing.watsup:1132.1-1135.35 rule `vload-splat`{C : context, N : N, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) - ;; 6-typing.watsup:1135.1-1138.35 + ;; 6-typing.watsup:1137.1-1140.35 rule `vload-zero`{C : context, N : N, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) - ;; 6-typing.watsup:1140.1-1144.21 + ;; 6-typing.watsup:1142.1-1146.21 rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}: `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) -- if (i < (128 / N)) - ;; 6-typing.watsup:1146.1-1149.46 + ;; 6-typing.watsup:1148.1-1151.46 rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8)) - ;; 6-typing.watsup:1151.1-1155.21 + ;; 6-typing.watsup:1153.1-1157.21 rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}: `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) @@ -5084,13 +5101,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1356.1-1356.100 +;; 6-typing.watsup:1358.1-1358.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1400.1-1401.17 + ;; 6-typing.watsup:1402.1-1403.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1403.1-1406.54 + ;; 6-typing.watsup:1405.1-1408.54 rule cons{C : context, global_1 : global, `global*` : global*, gt_1 : globaltype, `gt*` : globaltype*}: `%|-%:%`(C, [global_1] ++ global*{global <- `global*`}, [gt_1] ++ gt*{gt <- `gt*`}) -- Global_ok: `%|-%:%`(C, global_1, gt_1) @@ -5100,13 +5117,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1355.1-1355.98 +;; 6-typing.watsup:1357.1-1357.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1392.1-1393.17 + ;; 6-typing.watsup:1394.1-1395.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1395.1-1398.49 + ;; 6-typing.watsup:1397.1-1400.49 rule cons{C : context, type_1 : type, `type*` : type*, `dt_1*` : deftype*, `dt*` : deftype*}: `%|-%:%`(C, [type_1] ++ type*{type <- `type*`}, dt_1*{dt_1 <- `dt_1*`} ++ dt*{dt <- `dt*`}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 <- `dt_1*`}) @@ -6474,8 +6491,8 @@ def $allocmems(store : store, memtype*) : (store, memaddr*) ;; 9-module.watsup def $alloctag(store : store, tagtype : tagtype) : (store, tagaddr) ;; 9-module.watsup - def $alloctag{s : store, at : tagtype, taginst : taginst}(s, at) = (s +++ {FUNCS [], GLOBALS [], TABLES [], MEMS [], TAGS [taginst], ELEMS [], DATAS [], STRUCTS [], ARRAYS [], EXNS []}, |s.TAGS_store|) - -- if (taginst = {TYPE at}) + def $alloctag{s : store, tagtype : tagtype, taginst : taginst}(s, tagtype) = (s +++ {FUNCS [], GLOBALS [], TABLES [], MEMS [], TAGS [taginst], ELEMS [], DATAS [], STRUCTS [], ARRAYS [], EXNS []}, |s.TAGS_store|) + -- if (taginst = {TYPE tagtype}) ;; 9-module.watsup rec { @@ -6572,11 +6589,11 @@ def $allocmodule(store : store, module : module, externaddr*, val*, ref*, ref**) -- if (da*{da <- `da*`} = (|s.DATAS_store| + i_D)^(i_D<|data*{data <- `data*`}|){i_D <- `i_D*`}) -- if (dt*{dt <- `dt*`} = $alloctypes(type*{type <- `type*`})) -- if ((s_1, fa*{fa <- `fa*`}) = $allocfuncs(s, dt*{dt <- `dt*`}[x!`%`_idx.0]*{x <- `x*`}, FUNC_funccode(x, local*{local <- `local*`}, expr_F)*{expr_F <- `expr_F*`, `local*` <- `local**`, x <- `x*`}, moduleinst^|func*{func <- `func*`}|{})) - -- if ((s_2, ga*{ga <- `ga*`}) = $allocglobals(s_1, globaltype*{globaltype <- `globaltype*`}, val_G*{val_G <- `val_G*`})) - -- if ((s_3, ta*{ta <- `ta*`}) = $alloctables(s_2, tabletype*{tabletype <- `tabletype*`}, ref_T*{ref_T <- `ref_T*`})) - -- if ((s_4, ma*{ma <- `ma*`}) = $allocmems(s_3, memtype*{memtype <- `memtype*`})) + -- if ((s_2, ga*{ga <- `ga*`}) = $allocglobals(s_1, $subst_all_globaltype(globaltype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{globaltype <- `globaltype*`}, val_G*{val_G <- `val_G*`})) + -- if ((s_3, ta*{ta <- `ta*`}) = $alloctables(s_2, $subst_all_tabletype(tabletype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{tabletype <- `tabletype*`}, ref_T*{ref_T <- `ref_T*`})) + -- if ((s_4, ma*{ma <- `ma*`}) = $allocmems(s_3, $subst_all_memtype(memtype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{memtype <- `memtype*`})) -- if ((s_5, aa*{aa <- `aa*`}) = $alloctags(s_4, dt*{dt <- `dt*`}[y!`%`_idx.0]*{y <- `y*`})) - -- if ((s_6, ea*{ea <- `ea*`}) = $allocelems(s_5, elemtype*{elemtype <- `elemtype*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) + -- if ((s_6, ea*{ea <- `ea*`}) = $allocelems(s_5, $subst_all_reftype(elemtype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{elemtype <- `elemtype*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) -- if ((s_7, da*{da <- `da*`}) = $allocdatas(s_6, OK_datatype^|data*{data <- `data*`}|{}, byte*{byte <- `byte*`}*{`byte*` <- `byte**`})) -- if (xi*{xi <- `xi*`} = $allocexports({TYPES [], FUNCS fa_I*{fa_I <- `fa_I*`} ++ fa*{fa <- `fa*`}, GLOBALS ga_I*{ga_I <- `ga_I*`} ++ ga*{ga <- `ga*`}, TABLES ta_I*{ta_I <- `ta_I*`} ++ ta*{ta <- `ta*`}, MEMS ma_I*{ma_I <- `ma_I*`} ++ ma*{ma <- `ma*`}, TAGS aa_I*{aa_I <- `aa_I*`} ++ aa*{aa <- `aa*`}, ELEMS [], DATAS [], EXPORTS []}, export*{export <- `export*`})) -- if (moduleinst = {TYPES dt*{dt <- `dt*`}, FUNCS fa_I*{fa_I <- `fa_I*`} ++ fa*{fa <- `fa*`}, GLOBALS ga_I*{ga_I <- `ga_I*`} ++ ga*{ga <- `ga*`}, TABLES ta_I*{ta_I <- `ta_I*`} ++ ta*{ta <- `ta*`}, MEMS ma_I*{ma_I <- `ma_I*`} ++ ma*{ma <- `ma*`}, TAGS aa_I*{aa_I <- `aa_I*`} ++ aa*{aa <- `aa*`}, ELEMS ea*{ea <- `ea*`}, DATAS da*{da <- `da*`}, EXPORTS xi*{xi <- `xi*`}}) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 88d8b1917f..27cb1b7775 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -3302,6 +3302,24 @@ $$ \end{array} $$ +$$ +\begin{array}{@{}lcl@{}l@{}} +{{\mathit{gt}}}{{}[ {:=}\, {{\mathit{tu}}^{n}} ]} &=& {{\mathit{gt}}}{{}[ {i^{i_%%`_instrtype(`%`_resulttype([REF_valtype(nul, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(nul, EXTERN_heaptype)]))) + ;; 6-typing.watsup:916.1-918.20 + rule extern.convert_any{C : context, nul1 : nul1, nul2 : nul2}: + `%|-%:%`(C, EXTERN.CONVERT_ANY_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul1, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(nul2, EXTERN_heaptype)]))) + -- if (nul1 = nul2) - ;; 6-typing.watsup:919.1-920.62 - rule any.convert_extern{C : context, nul : nul}: - `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(nul, ANY_heaptype)]))) + ;; 6-typing.watsup:920.1-922.20 + rule any.convert_extern{C : context, nul1 : nul1, nul2 : nul2}: + `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul1, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(nul2, ANY_heaptype)]))) + -- if (nul1 = nul2) - ;; 6-typing.watsup:925.1-926.35 + ;; 6-typing.watsup:927.1-928.35 rule vconst{C : context, c : vec_(V128_Vnn)}: `%|-%:%`(C, VCONST_instr(V128_vectype, c), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:928.1-929.41 + ;; 6-typing.watsup:930.1-931.41 rule vvunop{C : context, vvunop : vvunop}: `%|-%:%`(C, VVUNOP_instr(V128_vectype, vvunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:931.1-932.48 + ;; 6-typing.watsup:933.1-934.48 rule vvbinop{C : context, vvbinop : vvbinop}: `%|-%:%`(C, VVBINOP_instr(V128_vectype, vvbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:934.1-935.55 + ;; 6-typing.watsup:936.1-937.55 rule vvternop{C : context, vvternop : vvternop}: `%|-%:%`(C, VVTERNOP_instr(V128_vectype, vvternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:937.1-938.44 + ;; 6-typing.watsup:939.1-940.44 rule vvtestop{C : context, vvtestop : vvtestop}: `%|-%:%`(C, VVTESTOP_instr(V128_vectype, vvtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:940.1-941.37 + ;; 6-typing.watsup:942.1-943.37 rule vunop{C : context, sh : shape, vunop : vunop_(sh)}: `%|-%:%`(C, VUNOP_instr(sh, vunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:943.1-944.44 + ;; 6-typing.watsup:945.1-946.44 rule vbinop{C : context, sh : shape, vbinop : vbinop_(sh)}: `%|-%:%`(C, VBINOP_instr(sh, vbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:946.1-947.40 + ;; 6-typing.watsup:948.1-949.40 rule vtestop{C : context, sh : shape, vtestop : vtestop_(sh)}: `%|-%:%`(C, VTESTOP_instr(sh, vtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:949.1-950.44 + ;; 6-typing.watsup:951.1-952.44 rule vrelop{C : context, sh : shape, vrelop : vrelop_(sh)}: `%|-%:%`(C, VRELOP_instr(sh, vrelop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:952.1-953.47 + ;; 6-typing.watsup:954.1-955.47 rule vshiftop{C : context, sh : ishape, vshiftop : vshiftop_(sh)}: `%|-%:%`(C, VSHIFTOP_instr(sh, vshiftop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype I32_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:955.1-956.33 + ;; 6-typing.watsup:957.1-958.33 rule vbitmask{C : context, sh : ishape}: `%|-%:%`(C, VBITMASK_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:958.1-959.39 + ;; 6-typing.watsup:960.1-961.39 rule vswizzle{C : context, sh : ishape}: `%|-%:%`(C, VSWIZZLE_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:961.1-963.29 + ;; 6-typing.watsup:963.1-965.29 rule vshuffle{C : context, sh : ishape, `i*` : nat*}: `%|-%:%`(C, VSHUFFLE_instr(sh, `%`_laneidx(i)*{i <- `i*`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- (if (i < (2 * $dim((sh : ishape <: shape))!`%`_dim.0)))*{i <- `i*`} - ;; 6-typing.watsup:965.1-966.44 + ;; 6-typing.watsup:967.1-968.44 rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:968.1-970.21 + ;; 6-typing.watsup:970.1-972.21 rule vextract_lane{C : context, sh : shape, `sx?` : sx?, i : nat}: `%|-%:%`(C, VEXTRACT_LANE_instr(sh, sx?{sx <- `sx?`}, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([($unpackshape(sh) : numtype <: valtype)]))) -- if (i < $dim(sh)!`%`_dim.0) - ;; 6-typing.watsup:972.1-974.21 + ;; 6-typing.watsup:974.1-976.21 rule vreplace_lane{C : context, sh : shape, i : nat}: `%|-%:%`(C, VREPLACE_LANE_instr(sh, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([V128_valtype ($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (i < $dim(sh)!`%`_dim.0) - ;; 6-typing.watsup:976.1-977.50 + ;; 6-typing.watsup:978.1-979.50 rule vextunop{C : context, sh_1 : ishape, sh_2 : ishape, vextunop : vextunop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTUNOP_instr(sh_1, sh_2, vextunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:979.1-980.57 + ;; 6-typing.watsup:981.1-982.57 rule vextbinop{C : context, sh_1 : ishape, sh_2 : ishape, vextbinop : vextbinop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTBINOP_instr(sh_1, sh_2, vextbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:982.1-983.48 + ;; 6-typing.watsup:984.1-985.48 rule vnarrow{C : context, sh_1 : ishape, sh_2 : ishape, sx : sx}: `%|-%:%`(C, VNARROW_instr(sh_1, sh_2, sx), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:985.1-986.58 + ;; 6-typing.watsup:987.1-988.58 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop__(sh_2, sh_1), `half?` : half__(sh_2, sh_1)?, `zero?` : zero__(sh_2, sh_1)?}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop, half?{half <- `half?`}, zero?{zero <- `zero?`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:991.1-993.28 + ;; 6-typing.watsup:993.1-995.28 rule local.get{C : context, x : idx, t : valtype}: `%|-%:%`(C, LOCAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(SET_init, t)) - ;; 6-typing.watsup:995.1-997.29 + ;; 6-typing.watsup:997.1-999.29 rule local.set{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; 6-typing.watsup:999.1-1001.29 + ;; 6-typing.watsup:1001.1-1003.29 rule local.tee{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.TEE_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; 6-typing.watsup:1006.1-1008.29 + ;; 6-typing.watsup:1008.1-1010.29 rule global.get{C : context, x : idx, t : valtype, mut : mut}: `%|-%:%`(C, GLOBAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(mut, t)) - ;; 6-typing.watsup:1010.1-1012.29 + ;; 6-typing.watsup:1012.1-1014.29 rule global.set{C : context, x : idx, t : valtype}: `%|-%:%`(C, GLOBAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [], `%`_resulttype([]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(`MUT%?`_mut(?(())), t)) - ;; 6-typing.watsup:1017.1-1019.29 + ;; 6-typing.watsup:1019.1-1021.29 rule table.get{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(rt : reftype <: valtype)]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1021.1-1023.29 + ;; 6-typing.watsup:1023.1-1025.29 rule table.set{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (rt : reftype <: valtype)]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1025.1-1027.29 + ;; 6-typing.watsup:1027.1-1029.29 rule table.size{C : context, x : idx, lim : limits, rt : reftype}: `%|-%:%`(C, TABLE.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([I32_valtype]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1029.1-1031.29 + ;; 6-typing.watsup:1031.1-1033.29 rule table.grow{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) I32_valtype]), [], `%`_resulttype([I32_valtype]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1033.1-1035.29 + ;; 6-typing.watsup:1035.1-1037.29 rule table.fill{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (rt : reftype <: valtype) I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1037.1-1041.36 + ;; 6-typing.watsup:1039.1-1043.36 rule table.copy{C : context, x_1 : idx, x_2 : idx, lim_1 : limits, rt_1 : reftype, lim_2 : limits, rt_2 : reftype}: `%|-%:%`(C, TABLE.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x_1!`%`_idx.0] = `%%`_tabletype(lim_1, rt_1)) -- if (C.TABLES_context[x_2!`%`_idx.0] = `%%`_tabletype(lim_2, rt_2)) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; 6-typing.watsup:1043.1-1047.36 + ;; 6-typing.watsup:1045.1-1049.36 rule table.init{C : context, x : idx, y : idx, lim : limits, rt_1 : reftype, rt_2 : reftype}: `%|-%:%`(C, TABLE.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt_1)) -- if (C.ELEMS_context[y!`%`_idx.0] = rt_2) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; 6-typing.watsup:1049.1-1051.24 + ;; 6-typing.watsup:1051.1-1053.24 rule elem.drop{C : context, x : idx, rt : reftype}: `%|-%:%`(C, ELEM.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.ELEMS_context[x!`%`_idx.0] = rt) - ;; 6-typing.watsup:1056.1-1058.23 + ;; 6-typing.watsup:1058.1-1060.23 rule memory.size{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([I32_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1060.1-1062.23 + ;; 6-typing.watsup:1062.1-1064.23 rule memory.grow{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([I32_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1064.1-1066.23 + ;; 6-typing.watsup:1066.1-1068.23 rule memory.fill{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1068.1-1071.27 + ;; 6-typing.watsup:1070.1-1073.27 rule memory.copy{C : context, x_1 : idx, x_2 : idx, mt_1 : memtype, mt_2 : memtype}: `%|-%:%`(C, MEMORY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x_1!`%`_idx.0] = mt_1) -- if (C.MEMS_context[x_2!`%`_idx.0] = mt_2) - ;; 6-typing.watsup:1073.1-1076.24 + ;; 6-typing.watsup:1075.1-1078.24 rule memory.init{C : context, x : idx, y : idx, mt : memtype}: `%|-%:%`(C, MEMORY.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; 6-typing.watsup:1078.1-1080.24 + ;; 6-typing.watsup:1080.1-1082.24 rule data.drop{C : context, x : idx}: `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) - ;; 6-typing.watsup:1091.1-1094.43 + ;; 6-typing.watsup:1093.1-1096.43 rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8)) - ;; 6-typing.watsup:1096.1-1099.35 + ;; 6-typing.watsup:1098.1-1101.35 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8)) - ;; 6-typing.watsup:1110.1-1113.43 + ;; 6-typing.watsup:1112.1-1115.43 rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8)) - ;; 6-typing.watsup:1115.1-1118.35 + ;; 6-typing.watsup:1117.1-1120.35 rule `store-pack`{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8)) - ;; 6-typing.watsup:1120.1-1123.46 + ;; 6-typing.watsup:1122.1-1125.46 rule `vload-val`{C : context, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8)) - ;; 6-typing.watsup:1125.1-1128.39 + ;; 6-typing.watsup:1127.1-1130.39 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N)) - ;; 6-typing.watsup:1130.1-1133.35 + ;; 6-typing.watsup:1132.1-1135.35 rule `vload-splat`{C : context, N : N, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) - ;; 6-typing.watsup:1135.1-1138.35 + ;; 6-typing.watsup:1137.1-1140.35 rule `vload-zero`{C : context, N : N, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) - ;; 6-typing.watsup:1140.1-1144.21 + ;; 6-typing.watsup:1142.1-1146.21 rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}: `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) -- if (i < (128 / N)) - ;; 6-typing.watsup:1146.1-1149.46 + ;; 6-typing.watsup:1148.1-1151.46 rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8)) - ;; 6-typing.watsup:1151.1-1155.21 + ;; 6-typing.watsup:1153.1-1157.21 rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}: `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) @@ -5074,13 +5091,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1356.1-1356.100 +;; 6-typing.watsup:1358.1-1358.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1400.1-1401.17 + ;; 6-typing.watsup:1402.1-1403.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1403.1-1406.54 + ;; 6-typing.watsup:1405.1-1408.54 rule cons{C : context, global_1 : global, `global*` : global*, gt_1 : globaltype, `gt*` : globaltype*}: `%|-%:%`(C, [global_1] ++ global*{global <- `global*`}, [gt_1] ++ gt*{gt <- `gt*`}) -- Global_ok: `%|-%:%`(C, global_1, gt_1) @@ -5090,13 +5107,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1355.1-1355.98 +;; 6-typing.watsup:1357.1-1357.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1392.1-1393.17 + ;; 6-typing.watsup:1394.1-1395.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1395.1-1398.49 + ;; 6-typing.watsup:1397.1-1400.49 rule cons{C : context, type_1 : type, `type*` : type*, `dt_1*` : deftype*, `dt*` : deftype*}: `%|-%:%`(C, [type_1] ++ type*{type <- `type*`}, dt_1*{dt_1 <- `dt_1*`} ++ dt*{dt <- `dt*`}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 <- `dt_1*`}) @@ -6464,8 +6481,8 @@ def $allocmems(store : store, memtype*) : (store, memaddr*) ;; 9-module.watsup def $alloctag(store : store, tagtype : tagtype) : (store, tagaddr) ;; 9-module.watsup - def $alloctag{s : store, at : tagtype, taginst : taginst}(s, at) = (s +++ {FUNCS [], GLOBALS [], TABLES [], MEMS [], TAGS [taginst], ELEMS [], DATAS [], STRUCTS [], ARRAYS [], EXNS []}, |s.TAGS_store|) - -- if (taginst = {TYPE at}) + def $alloctag{s : store, tagtype : tagtype, taginst : taginst}(s, tagtype) = (s +++ {FUNCS [], GLOBALS [], TABLES [], MEMS [], TAGS [taginst], ELEMS [], DATAS [], STRUCTS [], ARRAYS [], EXNS []}, |s.TAGS_store|) + -- if (taginst = {TYPE tagtype}) ;; 9-module.watsup rec { @@ -6562,11 +6579,11 @@ def $allocmodule(store : store, module : module, externaddr*, val*, ref*, ref**) -- if (da*{da <- `da*`} = (|s.DATAS_store| + i_D)^(i_D<|data*{data <- `data*`}|){i_D <- `i_D*`}) -- if (dt*{dt <- `dt*`} = $alloctypes(type*{type <- `type*`})) -- if ((s_1, fa*{fa <- `fa*`}) = $allocfuncs(s, dt*{dt <- `dt*`}[x!`%`_idx.0]*{x <- `x*`}, FUNC_funccode(x, local*{local <- `local*`}, expr_F)*{expr_F <- `expr_F*`, `local*` <- `local**`, x <- `x*`}, moduleinst^|func*{func <- `func*`}|{})) - -- if ((s_2, ga*{ga <- `ga*`}) = $allocglobals(s_1, globaltype*{globaltype <- `globaltype*`}, val_G*{val_G <- `val_G*`})) - -- if ((s_3, ta*{ta <- `ta*`}) = $alloctables(s_2, tabletype*{tabletype <- `tabletype*`}, ref_T*{ref_T <- `ref_T*`})) - -- if ((s_4, ma*{ma <- `ma*`}) = $allocmems(s_3, memtype*{memtype <- `memtype*`})) + -- if ((s_2, ga*{ga <- `ga*`}) = $allocglobals(s_1, $subst_all_globaltype(globaltype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{globaltype <- `globaltype*`}, val_G*{val_G <- `val_G*`})) + -- if ((s_3, ta*{ta <- `ta*`}) = $alloctables(s_2, $subst_all_tabletype(tabletype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{tabletype <- `tabletype*`}, ref_T*{ref_T <- `ref_T*`})) + -- if ((s_4, ma*{ma <- `ma*`}) = $allocmems(s_3, $subst_all_memtype(memtype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{memtype <- `memtype*`})) -- if ((s_5, aa*{aa <- `aa*`}) = $alloctags(s_4, dt*{dt <- `dt*`}[y!`%`_idx.0]*{y <- `y*`})) - -- if ((s_6, ea*{ea <- `ea*`}) = $allocelems(s_5, elemtype*{elemtype <- `elemtype*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) + -- if ((s_6, ea*{ea <- `ea*`}) = $allocelems(s_5, $subst_all_reftype(elemtype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{elemtype <- `elemtype*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) -- if ((s_7, da*{da <- `da*`}) = $allocdatas(s_6, OK_datatype^|data*{data <- `data*`}|{}, byte*{byte <- `byte*`}*{`byte*` <- `byte**`})) -- if (xi*{xi <- `xi*`} = $allocexports({TYPES [], FUNCS fa_I*{fa_I <- `fa_I*`} ++ fa*{fa <- `fa*`}, GLOBALS ga_I*{ga_I <- `ga_I*`} ++ ga*{ga <- `ga*`}, TABLES ta_I*{ta_I <- `ta_I*`} ++ ta*{ta <- `ta*`}, MEMS ma_I*{ma_I <- `ma_I*`} ++ ma*{ma <- `ma*`}, TAGS aa_I*{aa_I <- `aa_I*`} ++ aa*{aa <- `aa*`}, ELEMS [], DATAS [], EXPORTS []}, export*{export <- `export*`})) -- if (moduleinst = {TYPES dt*{dt <- `dt*`}, FUNCS fa_I*{fa_I <- `fa_I*`} ++ fa*{fa <- `fa*`}, GLOBALS ga_I*{ga_I <- `ga_I*`} ++ ga*{ga <- `ga*`}, TABLES ta_I*{ta_I <- `ta_I*`} ++ ta*{ta <- `ta*`}, MEMS ma_I*{ma_I <- `ma_I*`} ++ ma*{ma <- `ma*`}, TAGS aa_I*{aa_I <- `aa_I*`} ++ aa*{aa <- `aa*`}, ELEMS ea*{ea <- `ea*`}, DATAS da*{da <- `da*`}, EXPORTS xi*{xi <- `xi*`}}) @@ -10563,6 +10580,21 @@ def $subst_all_deftype(deftype : deftype, heaptype*) : deftype ;; 2-syntax-aux.watsup def $subst_all_deftype{dt : deftype, `tu*` : typeuse*, n : n, `i*` : nat*}(dt, (tu : typeuse <: heaptype)^n{tu <- `tu*`}) = $subst_deftype(dt, _IDX_typevar(`%`_typeidx(i))^(i_%%`_instrtype(`%`_resulttype([REF_valtype(nul, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(nul, EXTERN_heaptype)]))) + ;; 6-typing.watsup:916.1-918.20 + rule extern.convert_any{C : context, nul1 : nul1, nul2 : nul2}: + `%|-%:%`(C, EXTERN.CONVERT_ANY_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul1, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(nul2, EXTERN_heaptype)]))) + -- if (nul1 = nul2) - ;; 6-typing.watsup:919.1-920.62 - rule any.convert_extern{C : context, nul : nul}: - `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(nul, ANY_heaptype)]))) + ;; 6-typing.watsup:920.1-922.20 + rule any.convert_extern{C : context, nul1 : nul1, nul2 : nul2}: + `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul1, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(nul2, ANY_heaptype)]))) + -- if (nul1 = nul2) - ;; 6-typing.watsup:925.1-926.35 + ;; 6-typing.watsup:927.1-928.35 rule vconst{C : context, c : vec_(V128_Vnn)}: `%|-%:%`(C, VCONST_instr(V128_vectype, c), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:928.1-929.41 + ;; 6-typing.watsup:930.1-931.41 rule vvunop{C : context, vvunop : vvunop}: `%|-%:%`(C, VVUNOP_instr(V128_vectype, vvunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:931.1-932.48 + ;; 6-typing.watsup:933.1-934.48 rule vvbinop{C : context, vvbinop : vvbinop}: `%|-%:%`(C, VVBINOP_instr(V128_vectype, vvbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:934.1-935.55 + ;; 6-typing.watsup:936.1-937.55 rule vvternop{C : context, vvternop : vvternop}: `%|-%:%`(C, VVTERNOP_instr(V128_vectype, vvternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:937.1-938.44 + ;; 6-typing.watsup:939.1-940.44 rule vvtestop{C : context, vvtestop : vvtestop}: `%|-%:%`(C, VVTESTOP_instr(V128_vectype, vvtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:940.1-941.37 + ;; 6-typing.watsup:942.1-943.37 rule vunop{C : context, sh : shape, vunop : vunop_(sh)}: `%|-%:%`(C, VUNOP_instr(sh, vunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:943.1-944.44 + ;; 6-typing.watsup:945.1-946.44 rule vbinop{C : context, sh : shape, vbinop : vbinop_(sh)}: `%|-%:%`(C, VBINOP_instr(sh, vbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:946.1-947.40 + ;; 6-typing.watsup:948.1-949.40 rule vtestop{C : context, sh : shape, vtestop : vtestop_(sh)}: `%|-%:%`(C, VTESTOP_instr(sh, vtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:949.1-950.44 + ;; 6-typing.watsup:951.1-952.44 rule vrelop{C : context, sh : shape, vrelop : vrelop_(sh)}: `%|-%:%`(C, VRELOP_instr(sh, vrelop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:952.1-953.47 + ;; 6-typing.watsup:954.1-955.47 rule vshiftop{C : context, sh : ishape, vshiftop : vshiftop_(sh)}: `%|-%:%`(C, VSHIFTOP_instr(sh, vshiftop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype I32_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:955.1-956.33 + ;; 6-typing.watsup:957.1-958.33 rule vbitmask{C : context, sh : ishape}: `%|-%:%`(C, VBITMASK_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:958.1-959.39 + ;; 6-typing.watsup:960.1-961.39 rule vswizzle{C : context, sh : ishape}: `%|-%:%`(C, VSWIZZLE_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:961.1-963.29 + ;; 6-typing.watsup:963.1-965.29 rule vshuffle{C : context, sh : ishape, `i*` : nat*}: `%|-%:%`(C, VSHUFFLE_instr(sh, `%`_laneidx(i)*{i <- `i*`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- (if (i < (2 * $dim((sh : ishape <: shape))!`%`_dim.0)))*{i <- `i*`} - ;; 6-typing.watsup:965.1-966.44 + ;; 6-typing.watsup:967.1-968.44 rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:968.1-970.21 + ;; 6-typing.watsup:970.1-972.21 rule vextract_lane{C : context, sh : shape, `sx?` : sx?, i : nat}: `%|-%:%`(C, VEXTRACT_LANE_instr(sh, sx?{sx <- `sx?`}, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([($unpackshape(sh) : numtype <: valtype)]))) -- if (i < $dim(sh)!`%`_dim.0) - ;; 6-typing.watsup:972.1-974.21 + ;; 6-typing.watsup:974.1-976.21 rule vreplace_lane{C : context, sh : shape, i : nat}: `%|-%:%`(C, VREPLACE_LANE_instr(sh, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([V128_valtype ($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (i < $dim(sh)!`%`_dim.0) - ;; 6-typing.watsup:976.1-977.50 + ;; 6-typing.watsup:978.1-979.50 rule vextunop{C : context, sh_1 : ishape, sh_2 : ishape, vextunop : vextunop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTUNOP_instr(sh_1, sh_2, vextunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:979.1-980.57 + ;; 6-typing.watsup:981.1-982.57 rule vextbinop{C : context, sh_1 : ishape, sh_2 : ishape, vextbinop : vextbinop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTBINOP_instr(sh_1, sh_2, vextbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:982.1-983.48 + ;; 6-typing.watsup:984.1-985.48 rule vnarrow{C : context, sh_1 : ishape, sh_2 : ishape, sx : sx}: `%|-%:%`(C, VNARROW_instr(sh_1, sh_2, sx), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:985.1-986.58 + ;; 6-typing.watsup:987.1-988.58 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop__(sh_2, sh_1), `half?` : half__(sh_2, sh_1)?, `zero?` : zero__(sh_2, sh_1)?}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop, half?{half <- `half?`}, zero?{zero <- `zero?`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:991.1-993.28 + ;; 6-typing.watsup:993.1-995.28 rule local.get{C : context, x : idx, t : valtype}: `%|-%:%`(C, LOCAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(SET_init, t)) - ;; 6-typing.watsup:995.1-997.29 + ;; 6-typing.watsup:997.1-999.29 rule local.set{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; 6-typing.watsup:999.1-1001.29 + ;; 6-typing.watsup:1001.1-1003.29 rule local.tee{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.TEE_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; 6-typing.watsup:1006.1-1008.29 + ;; 6-typing.watsup:1008.1-1010.29 rule global.get{C : context, x : idx, t : valtype, mut : mut}: `%|-%:%`(C, GLOBAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(mut, t)) - ;; 6-typing.watsup:1010.1-1012.29 + ;; 6-typing.watsup:1012.1-1014.29 rule global.set{C : context, x : idx, t : valtype}: `%|-%:%`(C, GLOBAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [], `%`_resulttype([]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(`MUT%?`_mut(?(())), t)) - ;; 6-typing.watsup:1017.1-1019.29 + ;; 6-typing.watsup:1019.1-1021.29 rule table.get{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(rt : reftype <: valtype)]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1021.1-1023.29 + ;; 6-typing.watsup:1023.1-1025.29 rule table.set{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (rt : reftype <: valtype)]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1025.1-1027.29 + ;; 6-typing.watsup:1027.1-1029.29 rule table.size{C : context, x : idx, lim : limits, rt : reftype}: `%|-%:%`(C, TABLE.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([I32_valtype]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1029.1-1031.29 + ;; 6-typing.watsup:1031.1-1033.29 rule table.grow{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) I32_valtype]), [], `%`_resulttype([I32_valtype]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1033.1-1035.29 + ;; 6-typing.watsup:1035.1-1037.29 rule table.fill{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (rt : reftype <: valtype) I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1037.1-1041.36 + ;; 6-typing.watsup:1039.1-1043.36 rule table.copy{C : context, x_1 : idx, x_2 : idx, lim_1 : limits, rt_1 : reftype, lim_2 : limits, rt_2 : reftype}: `%|-%:%`(C, TABLE.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x_1!`%`_idx.0] = `%%`_tabletype(lim_1, rt_1)) -- if (C.TABLES_context[x_2!`%`_idx.0] = `%%`_tabletype(lim_2, rt_2)) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; 6-typing.watsup:1043.1-1047.36 + ;; 6-typing.watsup:1045.1-1049.36 rule table.init{C : context, x : idx, y : idx, lim : limits, rt_1 : reftype, rt_2 : reftype}: `%|-%:%`(C, TABLE.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt_1)) -- if (C.ELEMS_context[y!`%`_idx.0] = rt_2) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; 6-typing.watsup:1049.1-1051.24 + ;; 6-typing.watsup:1051.1-1053.24 rule elem.drop{C : context, x : idx, rt : reftype}: `%|-%:%`(C, ELEM.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.ELEMS_context[x!`%`_idx.0] = rt) - ;; 6-typing.watsup:1056.1-1058.23 + ;; 6-typing.watsup:1058.1-1060.23 rule memory.size{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([I32_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1060.1-1062.23 + ;; 6-typing.watsup:1062.1-1064.23 rule memory.grow{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([I32_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1064.1-1066.23 + ;; 6-typing.watsup:1066.1-1068.23 rule memory.fill{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1068.1-1071.27 + ;; 6-typing.watsup:1070.1-1073.27 rule memory.copy{C : context, x_1 : idx, x_2 : idx, mt_1 : memtype, mt_2 : memtype}: `%|-%:%`(C, MEMORY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x_1!`%`_idx.0] = mt_1) -- if (C.MEMS_context[x_2!`%`_idx.0] = mt_2) - ;; 6-typing.watsup:1073.1-1076.24 + ;; 6-typing.watsup:1075.1-1078.24 rule memory.init{C : context, x : idx, y : idx, mt : memtype}: `%|-%:%`(C, MEMORY.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; 6-typing.watsup:1078.1-1080.24 + ;; 6-typing.watsup:1080.1-1082.24 rule data.drop{C : context, x : idx}: `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) - ;; 6-typing.watsup:1091.1-1094.43 + ;; 6-typing.watsup:1093.1-1096.43 rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8)) - ;; 6-typing.watsup:1096.1-1099.35 + ;; 6-typing.watsup:1098.1-1101.35 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8)) - ;; 6-typing.watsup:1110.1-1113.43 + ;; 6-typing.watsup:1112.1-1115.43 rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8)) - ;; 6-typing.watsup:1115.1-1118.35 + ;; 6-typing.watsup:1117.1-1120.35 rule `store-pack`{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8)) - ;; 6-typing.watsup:1120.1-1123.46 + ;; 6-typing.watsup:1122.1-1125.46 rule `vload-val`{C : context, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8)) - ;; 6-typing.watsup:1125.1-1128.39 + ;; 6-typing.watsup:1127.1-1130.39 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N)) - ;; 6-typing.watsup:1130.1-1133.35 + ;; 6-typing.watsup:1132.1-1135.35 rule `vload-splat`{C : context, N : N, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) - ;; 6-typing.watsup:1135.1-1138.35 + ;; 6-typing.watsup:1137.1-1140.35 rule `vload-zero`{C : context, N : N, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) - ;; 6-typing.watsup:1140.1-1144.21 + ;; 6-typing.watsup:1142.1-1146.21 rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}: `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) -- if (i < (128 / N)) - ;; 6-typing.watsup:1146.1-1149.46 + ;; 6-typing.watsup:1148.1-1151.46 rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8)) - ;; 6-typing.watsup:1151.1-1155.21 + ;; 6-typing.watsup:1153.1-1157.21 rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}: `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) @@ -13379,13 +13413,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1356.1-1356.100 +;; 6-typing.watsup:1358.1-1358.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1400.1-1401.17 + ;; 6-typing.watsup:1402.1-1403.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1403.1-1406.54 + ;; 6-typing.watsup:1405.1-1408.54 rule cons{C : context, global_1 : global, `global*` : global*, gt_1 : globaltype, `gt*` : globaltype*}: `%|-%:%`(C, [global_1] ++ global*{global <- `global*`}, [gt_1] ++ gt*{gt <- `gt*`}) -- Global_ok: `%|-%:%`(C, global_1, gt_1) @@ -13395,13 +13429,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1355.1-1355.98 +;; 6-typing.watsup:1357.1-1357.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1392.1-1393.17 + ;; 6-typing.watsup:1394.1-1395.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1395.1-1398.49 + ;; 6-typing.watsup:1397.1-1400.49 rule cons{C : context, type_1 : type, `type*` : type*, `dt_1*` : deftype*, `dt*` : deftype*}: `%|-%:%`(C, [type_1] ++ type*{type <- `type*`}, dt_1*{dt_1 <- `dt_1*`} ++ dt*{dt <- `dt*`}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 <- `dt_1*`}) @@ -14769,8 +14803,8 @@ def $allocmems(store : store, memtype*) : (store, memaddr*) ;; 9-module.watsup def $alloctag(store : store, tagtype : tagtype) : (store, tagaddr) ;; 9-module.watsup - def $alloctag{s : store, at : tagtype, taginst : taginst}(s, at) = (s +++ {FUNCS [], GLOBALS [], TABLES [], MEMS [], TAGS [taginst], ELEMS [], DATAS [], STRUCTS [], ARRAYS [], EXNS []}, |s.TAGS_store|) - -- if (taginst = {TYPE at}) + def $alloctag{s : store, tagtype : tagtype, taginst : taginst}(s, tagtype) = (s +++ {FUNCS [], GLOBALS [], TABLES [], MEMS [], TAGS [taginst], ELEMS [], DATAS [], STRUCTS [], ARRAYS [], EXNS []}, |s.TAGS_store|) + -- if (taginst = {TYPE tagtype}) ;; 9-module.watsup rec { @@ -14867,11 +14901,11 @@ def $allocmodule(store : store, module : module, externaddr*, val*, ref*, ref**) -- if (da*{da <- `da*`} = (|s.DATAS_store| + i_D)^(i_D<|data*{data <- `data*`}|){i_D <- `i_D*`}) -- if (dt*{dt <- `dt*`} = $alloctypes(type*{type <- `type*`})) -- if ((s_1, fa*{fa <- `fa*`}) = $allocfuncs(s, dt*{dt <- `dt*`}[x!`%`_idx.0]*{x <- `x*`}, FUNC_funccode(x, local*{local <- `local*`}, expr_F)*{expr_F <- `expr_F*`, `local*` <- `local**`, x <- `x*`}, moduleinst^|func*{func <- `func*`}|{})) - -- if ((s_2, ga*{ga <- `ga*`}) = $allocglobals(s_1, globaltype*{globaltype <- `globaltype*`}, val_G*{val_G <- `val_G*`})) - -- if ((s_3, ta*{ta <- `ta*`}) = $alloctables(s_2, tabletype*{tabletype <- `tabletype*`}, ref_T*{ref_T <- `ref_T*`})) - -- if ((s_4, ma*{ma <- `ma*`}) = $allocmems(s_3, memtype*{memtype <- `memtype*`})) + -- if ((s_2, ga*{ga <- `ga*`}) = $allocglobals(s_1, $subst_all_globaltype(globaltype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{globaltype <- `globaltype*`}, val_G*{val_G <- `val_G*`})) + -- if ((s_3, ta*{ta <- `ta*`}) = $alloctables(s_2, $subst_all_tabletype(tabletype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{tabletype <- `tabletype*`}, ref_T*{ref_T <- `ref_T*`})) + -- if ((s_4, ma*{ma <- `ma*`}) = $allocmems(s_3, $subst_all_memtype(memtype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{memtype <- `memtype*`})) -- if ((s_5, aa*{aa <- `aa*`}) = $alloctags(s_4, dt*{dt <- `dt*`}[y!`%`_idx.0]*{y <- `y*`})) - -- if ((s_6, ea*{ea <- `ea*`}) = $allocelems(s_5, elemtype*{elemtype <- `elemtype*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) + -- if ((s_6, ea*{ea <- `ea*`}) = $allocelems(s_5, $subst_all_reftype(elemtype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{elemtype <- `elemtype*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) -- if ((s_7, da*{da <- `da*`}) = $allocdatas(s_6, OK_datatype^|data*{data <- `data*`}|{}, byte*{byte <- `byte*`}*{`byte*` <- `byte**`})) -- if (xi*{xi <- `xi*`} = $allocexports({TYPES [], FUNCS fa_I*{fa_I <- `fa_I*`} ++ fa*{fa <- `fa*`}, GLOBALS ga_I*{ga_I <- `ga_I*`} ++ ga*{ga <- `ga*`}, TABLES ta_I*{ta_I <- `ta_I*`} ++ ta*{ta <- `ta*`}, MEMS ma_I*{ma_I <- `ma_I*`} ++ ma*{ma <- `ma*`}, TAGS aa_I*{aa_I <- `aa_I*`} ++ aa*{aa <- `aa*`}, ELEMS [], DATAS [], EXPORTS []}, export*{export <- `export*`})) -- if (moduleinst = {TYPES dt*{dt <- `dt*`}, FUNCS fa_I*{fa_I <- `fa_I*`} ++ fa*{fa <- `fa*`}, GLOBALS ga_I*{ga_I <- `ga_I*`} ++ ga*{ga <- `ga*`}, TABLES ta_I*{ta_I <- `ta_I*`} ++ ta*{ta <- `ta*`}, MEMS ma_I*{ma_I <- `ma_I*`} ++ ma*{ma <- `ma*`}, TAGS aa_I*{aa_I <- `aa_I*`} ++ aa*{aa <- `aa*`}, ELEMS ea*{ea <- `ea*`}, DATAS da*{da <- `da*`}, EXPORTS xi*{xi <- `xi*`}}) @@ -18868,6 +18902,21 @@ def $subst_all_deftype(deftype : deftype, heaptype*) : deftype ;; 2-syntax-aux.watsup def $subst_all_deftype{dt : deftype, `tu*` : typeuse*, n : n, `i*` : nat*}(dt, (tu : typeuse <: heaptype)^n{tu <- `tu*`}) = $subst_deftype(dt, _IDX_typevar(`%`_typeidx(i))^(i_%%`_instrtype(`%`_resulttype([REF_valtype(nul, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(nul, EXTERN_heaptype)]))) + ;; 6-typing.watsup:916.1-918.20 + rule extern.convert_any{C : context, nul1 : nul1, nul2 : nul2}: + `%|-%:%`(C, EXTERN.CONVERT_ANY_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul1, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(nul2, EXTERN_heaptype)]))) + -- if (nul1 = nul2) - ;; 6-typing.watsup:919.1-920.62 - rule any.convert_extern{C : context, nul : nul}: - `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(nul, ANY_heaptype)]))) + ;; 6-typing.watsup:920.1-922.20 + rule any.convert_extern{C : context, nul1 : nul1, nul2 : nul2}: + `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul1, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(nul2, ANY_heaptype)]))) + -- if (nul1 = nul2) - ;; 6-typing.watsup:925.1-926.35 + ;; 6-typing.watsup:927.1-928.35 rule vconst{C : context, c : vec_(V128_Vnn)}: `%|-%:%`(C, VCONST_instr(V128_vectype, c), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:928.1-929.41 + ;; 6-typing.watsup:930.1-931.41 rule vvunop{C : context, vvunop : vvunop}: `%|-%:%`(C, VVUNOP_instr(V128_vectype, vvunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:931.1-932.48 + ;; 6-typing.watsup:933.1-934.48 rule vvbinop{C : context, vvbinop : vvbinop}: `%|-%:%`(C, VVBINOP_instr(V128_vectype, vvbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:934.1-935.55 + ;; 6-typing.watsup:936.1-937.55 rule vvternop{C : context, vvternop : vvternop}: `%|-%:%`(C, VVTERNOP_instr(V128_vectype, vvternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:937.1-938.44 + ;; 6-typing.watsup:939.1-940.44 rule vvtestop{C : context, vvtestop : vvtestop}: `%|-%:%`(C, VVTESTOP_instr(V128_vectype, vvtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:940.1-941.37 + ;; 6-typing.watsup:942.1-943.37 rule vunop{C : context, sh : shape, vunop : vunop_(sh)}: `%|-%:%`(C, VUNOP_instr(sh, vunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:943.1-944.44 + ;; 6-typing.watsup:945.1-946.44 rule vbinop{C : context, sh : shape, vbinop : vbinop_(sh)}: `%|-%:%`(C, VBINOP_instr(sh, vbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:946.1-947.40 + ;; 6-typing.watsup:948.1-949.40 rule vtestop{C : context, sh : shape, vtestop : vtestop_(sh)}: `%|-%:%`(C, VTESTOP_instr(sh, vtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:949.1-950.44 + ;; 6-typing.watsup:951.1-952.44 rule vrelop{C : context, sh : shape, vrelop : vrelop_(sh)}: `%|-%:%`(C, VRELOP_instr(sh, vrelop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:952.1-953.47 + ;; 6-typing.watsup:954.1-955.47 rule vshiftop{C : context, sh : ishape, vshiftop : vshiftop_(sh)}: `%|-%:%`(C, VSHIFTOP_instr(sh, vshiftop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype I32_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:955.1-956.33 + ;; 6-typing.watsup:957.1-958.33 rule vbitmask{C : context, sh : ishape}: `%|-%:%`(C, VBITMASK_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:958.1-959.39 + ;; 6-typing.watsup:960.1-961.39 rule vswizzle{C : context, sh : ishape}: `%|-%:%`(C, VSWIZZLE_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:961.1-963.29 + ;; 6-typing.watsup:963.1-965.29 rule vshuffle{C : context, sh : ishape, `i*` : nat*}: `%|-%:%`(C, VSHUFFLE_instr(sh, `%`_laneidx(i)*{i <- `i*`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- (if (i < (2 * $dim((sh : ishape <: shape))!`%`_dim.0)))*{i <- `i*`} - ;; 6-typing.watsup:965.1-966.44 + ;; 6-typing.watsup:967.1-968.44 rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:968.1-970.21 + ;; 6-typing.watsup:970.1-972.21 rule vextract_lane{C : context, sh : shape, `sx?` : sx?, i : nat}: `%|-%:%`(C, VEXTRACT_LANE_instr(sh, sx?{sx <- `sx?`}, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([($unpackshape(sh) : numtype <: valtype)]))) -- if (i < $dim(sh)!`%`_dim.0) - ;; 6-typing.watsup:972.1-974.21 + ;; 6-typing.watsup:974.1-976.21 rule vreplace_lane{C : context, sh : shape, i : nat}: `%|-%:%`(C, VREPLACE_LANE_instr(sh, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([V128_valtype ($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (i < $dim(sh)!`%`_dim.0) - ;; 6-typing.watsup:976.1-977.50 + ;; 6-typing.watsup:978.1-979.50 rule vextunop{C : context, sh_1 : ishape, sh_2 : ishape, vextunop : vextunop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTUNOP_instr(sh_1, sh_2, vextunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:979.1-980.57 + ;; 6-typing.watsup:981.1-982.57 rule vextbinop{C : context, sh_1 : ishape, sh_2 : ishape, vextbinop : vextbinop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTBINOP_instr(sh_1, sh_2, vextbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:982.1-983.48 + ;; 6-typing.watsup:984.1-985.48 rule vnarrow{C : context, sh_1 : ishape, sh_2 : ishape, sx : sx}: `%|-%:%`(C, VNARROW_instr(sh_1, sh_2, sx), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:985.1-986.58 + ;; 6-typing.watsup:987.1-988.58 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop__(sh_2, sh_1), `half?` : half__(sh_2, sh_1)?, `zero?` : zero__(sh_2, sh_1)?}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop, half?{half <- `half?`}, zero?{zero <- `zero?`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:991.1-993.28 + ;; 6-typing.watsup:993.1-995.28 rule local.get{C : context, x : idx, t : valtype}: `%|-%:%`(C, LOCAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(SET_init, t)) - ;; 6-typing.watsup:995.1-997.29 + ;; 6-typing.watsup:997.1-999.29 rule local.set{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; 6-typing.watsup:999.1-1001.29 + ;; 6-typing.watsup:1001.1-1003.29 rule local.tee{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.TEE_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; 6-typing.watsup:1006.1-1008.29 + ;; 6-typing.watsup:1008.1-1010.29 rule global.get{C : context, x : idx, t : valtype, mut : mut}: `%|-%:%`(C, GLOBAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(mut, t)) - ;; 6-typing.watsup:1010.1-1012.29 + ;; 6-typing.watsup:1012.1-1014.29 rule global.set{C : context, x : idx, t : valtype}: `%|-%:%`(C, GLOBAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [], `%`_resulttype([]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(`MUT%?`_mut(?(())), t)) - ;; 6-typing.watsup:1017.1-1019.29 + ;; 6-typing.watsup:1019.1-1021.29 rule table.get{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(rt : reftype <: valtype)]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1021.1-1023.29 + ;; 6-typing.watsup:1023.1-1025.29 rule table.set{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (rt : reftype <: valtype)]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1025.1-1027.29 + ;; 6-typing.watsup:1027.1-1029.29 rule table.size{C : context, x : idx, lim : limits, rt : reftype}: `%|-%:%`(C, TABLE.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([I32_valtype]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1029.1-1031.29 + ;; 6-typing.watsup:1031.1-1033.29 rule table.grow{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) I32_valtype]), [], `%`_resulttype([I32_valtype]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1033.1-1035.29 + ;; 6-typing.watsup:1035.1-1037.29 rule table.fill{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (rt : reftype <: valtype) I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1037.1-1041.36 + ;; 6-typing.watsup:1039.1-1043.36 rule table.copy{C : context, x_1 : idx, x_2 : idx, lim_1 : limits, rt_1 : reftype, lim_2 : limits, rt_2 : reftype}: `%|-%:%`(C, TABLE.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x_1!`%`_idx.0] = `%%`_tabletype(lim_1, rt_1)) -- if (C.TABLES_context[x_2!`%`_idx.0] = `%%`_tabletype(lim_2, rt_2)) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; 6-typing.watsup:1043.1-1047.36 + ;; 6-typing.watsup:1045.1-1049.36 rule table.init{C : context, x : idx, y : idx, lim : limits, rt_1 : reftype, rt_2 : reftype}: `%|-%:%`(C, TABLE.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt_1)) -- if (C.ELEMS_context[y!`%`_idx.0] = rt_2) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; 6-typing.watsup:1049.1-1051.24 + ;; 6-typing.watsup:1051.1-1053.24 rule elem.drop{C : context, x : idx, rt : reftype}: `%|-%:%`(C, ELEM.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.ELEMS_context[x!`%`_idx.0] = rt) - ;; 6-typing.watsup:1056.1-1058.23 + ;; 6-typing.watsup:1058.1-1060.23 rule memory.size{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([I32_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1060.1-1062.23 + ;; 6-typing.watsup:1062.1-1064.23 rule memory.grow{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([I32_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1064.1-1066.23 + ;; 6-typing.watsup:1066.1-1068.23 rule memory.fill{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1068.1-1071.27 + ;; 6-typing.watsup:1070.1-1073.27 rule memory.copy{C : context, x_1 : idx, x_2 : idx, mt_1 : memtype, mt_2 : memtype}: `%|-%:%`(C, MEMORY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x_1!`%`_idx.0] = mt_1) -- if (C.MEMS_context[x_2!`%`_idx.0] = mt_2) - ;; 6-typing.watsup:1073.1-1076.24 + ;; 6-typing.watsup:1075.1-1078.24 rule memory.init{C : context, x : idx, y : idx, mt : memtype}: `%|-%:%`(C, MEMORY.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; 6-typing.watsup:1078.1-1080.24 + ;; 6-typing.watsup:1080.1-1082.24 rule data.drop{C : context, x : idx}: `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) - ;; 6-typing.watsup:1091.1-1094.43 + ;; 6-typing.watsup:1093.1-1096.43 rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8)) - ;; 6-typing.watsup:1096.1-1099.35 + ;; 6-typing.watsup:1098.1-1101.35 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8)) - ;; 6-typing.watsup:1110.1-1113.43 + ;; 6-typing.watsup:1112.1-1115.43 rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8)) - ;; 6-typing.watsup:1115.1-1118.35 + ;; 6-typing.watsup:1117.1-1120.35 rule `store-pack`{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8)) - ;; 6-typing.watsup:1120.1-1123.46 + ;; 6-typing.watsup:1122.1-1125.46 rule `vload-val`{C : context, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8)) - ;; 6-typing.watsup:1125.1-1128.39 + ;; 6-typing.watsup:1127.1-1130.39 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N)) - ;; 6-typing.watsup:1130.1-1133.35 + ;; 6-typing.watsup:1132.1-1135.35 rule `vload-splat`{C : context, N : N, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) - ;; 6-typing.watsup:1135.1-1138.35 + ;; 6-typing.watsup:1137.1-1140.35 rule `vload-zero`{C : context, N : N, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) - ;; 6-typing.watsup:1140.1-1144.21 + ;; 6-typing.watsup:1142.1-1146.21 rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}: `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) -- if (i < (128 / N)) - ;; 6-typing.watsup:1146.1-1149.46 + ;; 6-typing.watsup:1148.1-1151.46 rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8)) - ;; 6-typing.watsup:1151.1-1155.21 + ;; 6-typing.watsup:1153.1-1157.21 rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}: `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = mt) @@ -21684,13 +21735,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1356.1-1356.100 +;; 6-typing.watsup:1358.1-1358.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1400.1-1401.17 + ;; 6-typing.watsup:1402.1-1403.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1403.1-1406.54 + ;; 6-typing.watsup:1405.1-1408.54 rule cons{C : context, global_1 : global, `global*` : global*, gt_1 : globaltype, `gt*` : globaltype*}: `%|-%:%`(C, [global_1] ++ global*{global <- `global*`}, [gt_1] ++ gt*{gt <- `gt*`}) -- Global_ok: `%|-%:%`(C, global_1, gt_1) @@ -21700,13 +21751,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1355.1-1355.98 +;; 6-typing.watsup:1357.1-1357.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1392.1-1393.17 + ;; 6-typing.watsup:1394.1-1395.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1395.1-1398.49 + ;; 6-typing.watsup:1397.1-1400.49 rule cons{C : context, type_1 : type, `type*` : type*, `dt_1*` : deftype*, `dt*` : deftype*}: `%|-%:%`(C, [type_1] ++ type*{type <- `type*`}, dt_1*{dt_1 <- `dt_1*`} ++ dt*{dt <- `dt*`}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 <- `dt_1*`}) @@ -23074,8 +23125,8 @@ def $allocmems(store : store, memtype*) : (store, memaddr*) ;; 9-module.watsup def $alloctag(store : store, tagtype : tagtype) : (store, tagaddr) ;; 9-module.watsup - def $alloctag{s : store, at : tagtype, taginst : taginst}(s, at) = (s +++ {FUNCS [], GLOBALS [], TABLES [], MEMS [], TAGS [taginst], ELEMS [], DATAS [], STRUCTS [], ARRAYS [], EXNS []}, |s.TAGS_store|) - -- if (taginst = {TYPE at}) + def $alloctag{s : store, tagtype : tagtype, taginst : taginst}(s, tagtype) = (s +++ {FUNCS [], GLOBALS [], TABLES [], MEMS [], TAGS [taginst], ELEMS [], DATAS [], STRUCTS [], ARRAYS [], EXNS []}, |s.TAGS_store|) + -- if (taginst = {TYPE tagtype}) ;; 9-module.watsup rec { @@ -23172,11 +23223,11 @@ def $allocmodule(store : store, module : module, externaddr*, val*, ref*, ref**) -- if (da*{da <- `da*`} = (|s.DATAS_store| + i_D)^(i_D<|data*{data <- `data*`}|){i_D <- `i_D*`}) -- if (dt*{dt <- `dt*`} = $alloctypes(type*{type <- `type*`})) -- if ((s_1, fa*{fa <- `fa*`}) = $allocfuncs(s, dt*{dt <- `dt*`}[x!`%`_idx.0]*{x <- `x*`}, FUNC_funccode(x, local*{local <- `local*`}, expr_F)*{expr_F <- `expr_F*`, `local*` <- `local**`, x <- `x*`}, moduleinst^|func*{func <- `func*`}|{})) - -- if ((s_2, ga*{ga <- `ga*`}) = $allocglobals(s_1, globaltype*{globaltype <- `globaltype*`}, val_G*{val_G <- `val_G*`})) - -- if ((s_3, ta*{ta <- `ta*`}) = $alloctables(s_2, tabletype*{tabletype <- `tabletype*`}, ref_T*{ref_T <- `ref_T*`})) - -- if ((s_4, ma*{ma <- `ma*`}) = $allocmems(s_3, memtype*{memtype <- `memtype*`})) + -- if ((s_2, ga*{ga <- `ga*`}) = $allocglobals(s_1, $subst_all_globaltype(globaltype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{globaltype <- `globaltype*`}, val_G*{val_G <- `val_G*`})) + -- if ((s_3, ta*{ta <- `ta*`}) = $alloctables(s_2, $subst_all_tabletype(tabletype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{tabletype <- `tabletype*`}, ref_T*{ref_T <- `ref_T*`})) + -- if ((s_4, ma*{ma <- `ma*`}) = $allocmems(s_3, $subst_all_memtype(memtype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{memtype <- `memtype*`})) -- if ((s_5, aa*{aa <- `aa*`}) = $alloctags(s_4, dt*{dt <- `dt*`}[y!`%`_idx.0]*{y <- `y*`})) - -- if ((s_6, ea*{ea <- `ea*`}) = $allocelems(s_5, elemtype*{elemtype <- `elemtype*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) + -- if ((s_6, ea*{ea <- `ea*`}) = $allocelems(s_5, $subst_all_reftype(elemtype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{elemtype <- `elemtype*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) -- if ((s_7, da*{da <- `da*`}) = $allocdatas(s_6, OK_datatype^|data*{data <- `data*`}|{}, byte*{byte <- `byte*`}*{`byte*` <- `byte**`})) -- if (xi*{xi <- `xi*`} = $allocexports({TYPES [], FUNCS fa_I*{fa_I <- `fa_I*`} ++ fa*{fa <- `fa*`}, GLOBALS ga_I*{ga_I <- `ga_I*`} ++ ga*{ga <- `ga*`}, TABLES ta_I*{ta_I <- `ta_I*`} ++ ta*{ta <- `ta*`}, MEMS ma_I*{ma_I <- `ma_I*`} ++ ma*{ma <- `ma*`}, TAGS aa_I*{aa_I <- `aa_I*`} ++ aa*{aa <- `aa*`}, ELEMS [], DATAS [], EXPORTS []}, export*{export <- `export*`})) -- if (moduleinst = {TYPES dt*{dt <- `dt*`}, FUNCS fa_I*{fa_I <- `fa_I*`} ++ fa*{fa <- `fa*`}, GLOBALS ga_I*{ga_I <- `ga_I*`} ++ ga*{ga <- `ga*`}, TABLES ta_I*{ta_I <- `ta_I*`} ++ ta*{ta <- `ta*`}, MEMS ma_I*{ma_I <- `ma_I*`} ++ ma*{ma <- `ma*`}, TAGS aa_I*{aa_I <- `aa_I*`} ++ aa*{aa <- `aa*`}, ELEMS ea*{ea <- `ea*`}, DATAS da*{da <- `da*`}, EXPORTS xi*{xi <- `xi*`}}) @@ -27173,6 +27224,21 @@ def $subst_all_deftype(deftype : deftype, heaptype*) : deftype ;; 2-syntax-aux.watsup def $subst_all_deftype{dt : deftype, `tu*` : typeuse*, n : n, `i*` : nat*}(dt, (tu : typeuse <: heaptype)^n{tu <- `tu*`}) = $subst_deftype(dt, _IDX_typevar(`%`_typeidx(i))^(i_%%`_instrtype(`%`_resulttype([REF_valtype(nul, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(nul, EXTERN_heaptype)]))) + ;; 6-typing.watsup:916.1-918.20 + rule extern.convert_any{C : context, nul1 : nul1, nul2 : nul2}: + `%|-%:%`(C, EXTERN.CONVERT_ANY_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul1, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(nul2, EXTERN_heaptype)]))) + -- if (nul1 = nul2) - ;; 6-typing.watsup:919.1-920.62 - rule any.convert_extern{C : context, nul : nul}: - `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(nul, ANY_heaptype)]))) + ;; 6-typing.watsup:920.1-922.20 + rule any.convert_extern{C : context, nul1 : nul1, nul2 : nul2}: + `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(nul1, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(nul2, ANY_heaptype)]))) + -- if (nul1 = nul2) - ;; 6-typing.watsup:925.1-926.35 + ;; 6-typing.watsup:927.1-928.35 rule vconst{C : context, c : vec_(V128_Vnn)}: `%|-%:%`(C, VCONST_instr(V128_vectype, c), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:928.1-929.41 + ;; 6-typing.watsup:930.1-931.41 rule vvunop{C : context, vvunop : vvunop}: `%|-%:%`(C, VVUNOP_instr(V128_vectype, vvunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:931.1-932.48 + ;; 6-typing.watsup:933.1-934.48 rule vvbinop{C : context, vvbinop : vvbinop}: `%|-%:%`(C, VVBINOP_instr(V128_vectype, vvbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:934.1-935.55 + ;; 6-typing.watsup:936.1-937.55 rule vvternop{C : context, vvternop : vvternop}: `%|-%:%`(C, VVTERNOP_instr(V128_vectype, vvternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:937.1-938.44 + ;; 6-typing.watsup:939.1-940.44 rule vvtestop{C : context, vvtestop : vvtestop}: `%|-%:%`(C, VVTESTOP_instr(V128_vectype, vvtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:940.1-941.37 + ;; 6-typing.watsup:942.1-943.37 rule vunop{C : context, sh : shape, vunop : vunop_(sh)}: `%|-%:%`(C, VUNOP_instr(sh, vunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:943.1-944.44 + ;; 6-typing.watsup:945.1-946.44 rule vbinop{C : context, sh : shape, vbinop : vbinop_(sh)}: `%|-%:%`(C, VBINOP_instr(sh, vbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:946.1-947.40 + ;; 6-typing.watsup:948.1-949.40 rule vtestop{C : context, sh : shape, vtestop : vtestop_(sh)}: `%|-%:%`(C, VTESTOP_instr(sh, vtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:949.1-950.44 + ;; 6-typing.watsup:951.1-952.44 rule vrelop{C : context, sh : shape, vrelop : vrelop_(sh)}: `%|-%:%`(C, VRELOP_instr(sh, vrelop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:952.1-953.47 + ;; 6-typing.watsup:954.1-955.47 rule vshiftop{C : context, sh : ishape, vshiftop : vshiftop_(sh)}: `%|-%:%`(C, VSHIFTOP_instr(sh, vshiftop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype I32_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:955.1-956.33 + ;; 6-typing.watsup:957.1-958.33 rule vbitmask{C : context, sh : ishape}: `%|-%:%`(C, VBITMASK_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; 6-typing.watsup:958.1-959.39 + ;; 6-typing.watsup:960.1-961.39 rule vswizzle{C : context, sh : ishape}: `%|-%:%`(C, VSWIZZLE_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:961.1-963.29 + ;; 6-typing.watsup:963.1-965.29 rule vshuffle{C : context, sh : ishape, `i*` : nat*}: `%|-%:%`(C, VSHUFFLE_instr(sh, `%`_laneidx(i)*{i <- `i*`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- (if (i < (2 * $dim((sh : ishape <: shape))!`%`_dim.0)))*{i <- `i*`} - ;; 6-typing.watsup:965.1-966.44 + ;; 6-typing.watsup:967.1-968.44 rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:968.1-970.21 + ;; 6-typing.watsup:970.1-972.21 rule vextract_lane{C : context, sh : shape, `sx?` : sx?, i : nat}: `%|-%:%`(C, VEXTRACT_LANE_instr(sh, sx?{sx <- `sx?`}, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([($unpackshape(sh) : numtype <: valtype)]))) -- if (i < $dim(sh)!`%`_dim.0) - ;; 6-typing.watsup:972.1-974.21 + ;; 6-typing.watsup:974.1-976.21 rule vreplace_lane{C : context, sh : shape, i : nat}: `%|-%:%`(C, VREPLACE_LANE_instr(sh, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([V128_valtype ($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (i < $dim(sh)!`%`_dim.0) - ;; 6-typing.watsup:976.1-977.50 + ;; 6-typing.watsup:978.1-979.50 rule vextunop{C : context, sh_1 : ishape, sh_2 : ishape, vextunop : vextunop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTUNOP_instr(sh_1, sh_2, vextunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:979.1-980.57 + ;; 6-typing.watsup:981.1-982.57 rule vextbinop{C : context, sh_1 : ishape, sh_2 : ishape, vextbinop : vextbinop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTBINOP_instr(sh_1, sh_2, vextbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:982.1-983.48 + ;; 6-typing.watsup:984.1-985.48 rule vnarrow{C : context, sh_1 : ishape, sh_2 : ishape, sx : sx}: `%|-%:%`(C, VNARROW_instr(sh_1, sh_2, sx), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:985.1-986.58 + ;; 6-typing.watsup:987.1-988.58 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop__(sh_2, sh_1), `half?` : half__(sh_2, sh_1)?, `zero?` : zero__(sh_2, sh_1)?}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop, half?{half <- `half?`}, zero?{zero <- `zero?`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:991.1-993.28 + ;; 6-typing.watsup:993.1-995.28 rule local.get{C : context, x : idx, t : valtype}: `%|-%:%`(C, LOCAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (x!`%`_idx.0 < |C.LOCALS_context|) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(SET_init, t)) - ;; 6-typing.watsup:995.1-997.29 + ;; 6-typing.watsup:997.1-999.29 rule local.set{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.LOCALS_context|) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; 6-typing.watsup:999.1-1001.29 + ;; 6-typing.watsup:1001.1-1003.29 rule local.tee{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.TEE_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([t]))) -- if (x!`%`_idx.0 < |C.LOCALS_context|) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; 6-typing.watsup:1006.1-1008.29 + ;; 6-typing.watsup:1008.1-1010.29 rule global.get{C : context, x : idx, t : valtype, mut : mut}: `%|-%:%`(C, GLOBAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (x!`%`_idx.0 < |C.GLOBALS_context|) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(mut, t)) - ;; 6-typing.watsup:1010.1-1012.29 + ;; 6-typing.watsup:1012.1-1014.29 rule global.set{C : context, x : idx, t : valtype}: `%|-%:%`(C, GLOBAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.GLOBALS_context|) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(`MUT%?`_mut(?(())), t)) - ;; 6-typing.watsup:1017.1-1019.29 + ;; 6-typing.watsup:1019.1-1021.29 rule table.get{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(rt : reftype <: valtype)]))) -- if (x!`%`_idx.0 < |C.TABLES_context|) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1021.1-1023.29 + ;; 6-typing.watsup:1023.1-1025.29 rule table.set{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (rt : reftype <: valtype)]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.TABLES_context|) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1025.1-1027.29 + ;; 6-typing.watsup:1027.1-1029.29 rule table.size{C : context, x : idx, lim : limits, rt : reftype}: `%|-%:%`(C, TABLE.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([I32_valtype]))) -- if (x!`%`_idx.0 < |C.TABLES_context|) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1029.1-1031.29 + ;; 6-typing.watsup:1031.1-1033.29 rule table.grow{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) I32_valtype]), [], `%`_resulttype([I32_valtype]))) -- if (x!`%`_idx.0 < |C.TABLES_context|) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1033.1-1035.29 + ;; 6-typing.watsup:1035.1-1037.29 rule table.fill{C : context, x : idx, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (rt : reftype <: valtype) I32_valtype]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.TABLES_context|) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) - ;; 6-typing.watsup:1037.1-1041.36 + ;; 6-typing.watsup:1039.1-1043.36 rule table.copy{C : context, x_1 : idx, x_2 : idx, lim_1 : limits, rt_1 : reftype, lim_2 : limits, rt_2 : reftype}: `%|-%:%`(C, TABLE.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (x_1!`%`_idx.0 < |C.TABLES_context|) @@ -29691,7 +29759,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- if (C.TABLES_context[x_2!`%`_idx.0] = `%%`_tabletype(lim_2, rt_2)) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; 6-typing.watsup:1043.1-1047.36 + ;; 6-typing.watsup:1045.1-1049.36 rule table.init{C : context, x : idx, y : idx, lim : limits, rt_1 : reftype, rt_2 : reftype}: `%|-%:%`(C, TABLE.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.TABLES_context|) @@ -29700,31 +29768,31 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- if (C.ELEMS_context[y!`%`_idx.0] = rt_2) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; 6-typing.watsup:1049.1-1051.24 + ;; 6-typing.watsup:1051.1-1053.24 rule elem.drop{C : context, x : idx, rt : reftype}: `%|-%:%`(C, ELEM.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.ELEMS_context|) -- if (C.ELEMS_context[x!`%`_idx.0] = rt) - ;; 6-typing.watsup:1056.1-1058.23 + ;; 6-typing.watsup:1058.1-1060.23 rule memory.size{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([I32_valtype]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1060.1-1062.23 + ;; 6-typing.watsup:1062.1-1064.23 rule memory.grow{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([I32_valtype]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1064.1-1066.23 + ;; 6-typing.watsup:1066.1-1068.23 rule memory.fill{C : context, x : idx, mt : memtype}: `%|-%:%`(C, MEMORY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) - ;; 6-typing.watsup:1068.1-1071.27 + ;; 6-typing.watsup:1070.1-1073.27 rule memory.copy{C : context, x_1 : idx, x_2 : idx, mt_1 : memtype, mt_2 : memtype}: `%|-%:%`(C, MEMORY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (x_1!`%`_idx.0 < |C.MEMS_context|) @@ -29732,7 +29800,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- if (C.MEMS_context[x_1!`%`_idx.0] = mt_1) -- if (C.MEMS_context[x_2!`%`_idx.0] = mt_2) - ;; 6-typing.watsup:1073.1-1076.24 + ;; 6-typing.watsup:1075.1-1078.24 rule memory.init{C : context, x : idx, y : idx, mt : memtype}: `%|-%:%`(C, MEMORY.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) @@ -29740,69 +29808,69 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; 6-typing.watsup:1078.1-1080.24 + ;; 6-typing.watsup:1080.1-1082.24 rule data.drop{C : context, x : idx}: `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.DATAS_context|) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) - ;; 6-typing.watsup:1091.1-1094.43 + ;; 6-typing.watsup:1093.1-1096.43 rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8)) - ;; 6-typing.watsup:1096.1-1099.35 + ;; 6-typing.watsup:1098.1-1101.35 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8)) - ;; 6-typing.watsup:1110.1-1113.43 + ;; 6-typing.watsup:1112.1-1115.43 rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8)) - ;; 6-typing.watsup:1115.1-1118.35 + ;; 6-typing.watsup:1117.1-1120.35 rule `store-pack`{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8)) - ;; 6-typing.watsup:1120.1-1123.46 + ;; 6-typing.watsup:1122.1-1125.46 rule `vload-val`{C : context, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8)) - ;; 6-typing.watsup:1125.1-1128.39 + ;; 6-typing.watsup:1127.1-1130.39 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N)) - ;; 6-typing.watsup:1130.1-1133.35 + ;; 6-typing.watsup:1132.1-1135.35 rule `vload-splat`{C : context, N : N, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) - ;; 6-typing.watsup:1135.1-1138.35 + ;; 6-typing.watsup:1137.1-1140.35 rule `vload-zero`{C : context, N : N, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) - ;; 6-typing.watsup:1140.1-1144.21 + ;; 6-typing.watsup:1142.1-1146.21 rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}: `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) @@ -29810,14 +29878,14 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) -- if (i < (128 / N)) - ;; 6-typing.watsup:1146.1-1149.46 + ;; 6-typing.watsup:1148.1-1151.46 rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}: `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = mt) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8)) - ;; 6-typing.watsup:1151.1-1155.21 + ;; 6-typing.watsup:1153.1-1157.21 rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}: `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) @@ -30110,13 +30178,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1356.1-1356.100 +;; 6-typing.watsup:1358.1-1358.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1400.1-1401.17 + ;; 6-typing.watsup:1402.1-1403.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1403.1-1406.54 + ;; 6-typing.watsup:1405.1-1408.54 rule cons{C : context, global_1 : global, `global*` : global*, gt_1 : globaltype, `gt*` : globaltype*}: `%|-%:%`(C, [global_1] ++ global*{global <- `global*`}, [gt_1] ++ gt*{gt <- `gt*`}) -- Global_ok: `%|-%:%`(C, global_1, gt_1) @@ -30126,13 +30194,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1355.1-1355.98 +;; 6-typing.watsup:1357.1-1357.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1392.1-1393.17 + ;; 6-typing.watsup:1394.1-1395.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1395.1-1398.49 + ;; 6-typing.watsup:1397.1-1400.49 rule cons{C : context, type_1 : type, `type*` : type*, `dt_1*` : deftype*, `dt*` : deftype*}: `%|-%:%`(C, [type_1] ++ type*{type <- `type*`}, dt_1*{dt_1 <- `dt_1*`} ++ dt*{dt <- `dt*`}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 <- `dt_1*`}) @@ -31572,8 +31640,8 @@ def $allocmems(store : store, memtype*) : (store, memaddr*) ;; 9-module.watsup def $alloctag(store : store, tagtype : tagtype) : (store, tagaddr) ;; 9-module.watsup - def $alloctag{s : store, at : tagtype, taginst : taginst}(s, at) = (s +++ {FUNCS [], GLOBALS [], TABLES [], MEMS [], TAGS [taginst], ELEMS [], DATAS [], STRUCTS [], ARRAYS [], EXNS []}, |s.TAGS_store|) - -- if (taginst = {TYPE at}) + def $alloctag{s : store, tagtype : tagtype, taginst : taginst}(s, tagtype) = (s +++ {FUNCS [], GLOBALS [], TABLES [], MEMS [], TAGS [taginst], ELEMS [], DATAS [], STRUCTS [], ARRAYS [], EXNS []}, |s.TAGS_store|) + -- if (taginst = {TYPE tagtype}) ;; 9-module.watsup rec { @@ -31670,11 +31738,11 @@ def $allocmodule(store : store, module : module, externaddr*, val*, ref*, ref**) -- if (da*{da <- `da*`} = (|s.DATAS_store| + i_D)^(i_D<|data*{data <- `data*`}|){i_D <- `i_D*`}) -- if (dt*{dt <- `dt*`} = $alloctypes(type*{type <- `type*`})) -- if ((s_1, fa*{fa <- `fa*`}) = $allocfuncs(s, dt*{dt <- `dt*`}[x!`%`_idx.0]*{x <- `x*`}, FUNC_funccode(x, local*{local <- `local*`}, expr_F)*{expr_F <- `expr_F*`, `local*` <- `local**`, x <- `x*`}, moduleinst^|func*{func <- `func*`}|{})) - -- if ((s_2, ga*{ga <- `ga*`}) = $allocglobals(s_1, globaltype*{globaltype <- `globaltype*`}, val_G*{val_G <- `val_G*`})) - -- if ((s_3, ta*{ta <- `ta*`}) = $alloctables(s_2, tabletype*{tabletype <- `tabletype*`}, ref_T*{ref_T <- `ref_T*`})) - -- if ((s_4, ma*{ma <- `ma*`}) = $allocmems(s_3, memtype*{memtype <- `memtype*`})) + -- if ((s_2, ga*{ga <- `ga*`}) = $allocglobals(s_1, $subst_all_globaltype(globaltype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{globaltype <- `globaltype*`}, val_G*{val_G <- `val_G*`})) + -- if ((s_3, ta*{ta <- `ta*`}) = $alloctables(s_2, $subst_all_tabletype(tabletype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{tabletype <- `tabletype*`}, ref_T*{ref_T <- `ref_T*`})) + -- if ((s_4, ma*{ma <- `ma*`}) = $allocmems(s_3, $subst_all_memtype(memtype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{memtype <- `memtype*`})) -- if ((s_5, aa*{aa <- `aa*`}) = $alloctags(s_4, dt*{dt <- `dt*`}[y!`%`_idx.0]*{y <- `y*`})) - -- if ((s_6, ea*{ea <- `ea*`}) = $allocelems(s_5, elemtype*{elemtype <- `elemtype*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) + -- if ((s_6, ea*{ea <- `ea*`}) = $allocelems(s_5, $subst_all_reftype(elemtype, (dt : deftype <: heaptype)*{dt <- `dt*`})*{elemtype <- `elemtype*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) -- if ((s_7, da*{da <- `da*`}) = $allocdatas(s_6, OK_datatype^|data*{data <- `data*`}|{}, byte*{byte <- `byte*`}*{`byte*` <- `byte**`})) -- if (xi*{xi <- `xi*`} = $allocexports({TYPES [], FUNCS fa_I*{fa_I <- `fa_I*`} ++ fa*{fa <- `fa*`}, GLOBALS ga_I*{ga_I <- `ga_I*`} ++ ga*{ga <- `ga*`}, TABLES ta_I*{ta_I <- `ta_I*`} ++ ta*{ta <- `ta*`}, MEMS ma_I*{ma_I <- `ma_I*`} ++ ma*{ma <- `ma*`}, TAGS aa_I*{aa_I <- `aa_I*`} ++ aa*{aa <- `aa*`}, ELEMS [], DATAS [], EXPORTS []}, export*{export <- `export*`})) -- if (moduleinst = {TYPES dt*{dt <- `dt*`}, FUNCS fa_I*{fa_I <- `fa_I*`} ++ fa*{fa <- `fa*`}, GLOBALS ga_I*{ga_I <- `ga_I*`} ++ ga*{ga <- `ga*`}, TABLES ta_I*{ta_I <- `ta_I*`} ++ ta*{ta <- `ta*`}, MEMS ma_I*{ma_I <- `ma_I*`} ++ ma*{ma <- `ma*`}, TAGS aa_I*{aa_I <- `aa_I*`} ++ aa*{aa <- `aa*`}, ELEMS ea*{ea <- `ea*`}, DATAS da*{da <- `da*`}, EXPORTS xi*{xi <- `xi*`}}) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 71f9900b89..1685587196 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -12363,7 +12363,7 @@ watsup 0.4 generator == Translating to AL... == Prose Generation... 6-typing.watsup:195.10-195.32: if_expr_to_instrs: Yet `$before(typeuse, x, i)` -6-typing.watsup:1378.9-1378.30: if_expr_to_instrs: Yet `$disjoint_(syntax name, nm*{nm <- `nm*`})` +6-typing.watsup:1380.9-1380.30: if_expr_to_instrs: Yet `$disjoint_(syntax name, nm*{nm <- `nm*`})` * :math:`{\mathit{numtype}}` is valid. @@ -13641,10 +13641,16 @@ watsup 0.4 generator * :math:`C{.}\mathsf{datas}{}[y]` must be equal to :math:`\mathsf{ok}`. -* :math:`\mathsf{extern{.}convert\_any}` is valid with type :math:`((\mathsf{ref}~{\mathsf{null}^?}~\mathsf{any})~{\rightarrow}_{\epsilon}\,(\mathsf{ref}~{\mathsf{null}^?}~\mathsf{extern}))`. +* :math:`\mathsf{extern{.}convert\_any}` is valid with type :math:`((\mathsf{ref}~{\mathsf{null}}{{{}_{1}^?}}~\mathsf{any})~{\rightarrow}_{\epsilon}\,(\mathsf{ref}~{\mathsf{null}}{{{}_{2}^?}}~\mathsf{extern}))` if and only if: -* :math:`\mathsf{any{.}convert\_extern}` is valid with type :math:`((\mathsf{ref}~{\mathsf{null}^?}~\mathsf{extern})~{\rightarrow}_{\epsilon}\,(\mathsf{ref}~{\mathsf{null}^?}~\mathsf{any}))`. + * :math:`{\mathsf{null}}{{{}_{1}^?}}` must be equal to :math:`{\mathsf{null}}{{{}_{2}^?}}`. + + +* :math:`\mathsf{any{.}convert\_extern}` is valid with type :math:`((\mathsf{ref}~{\mathsf{null}}{{{}_{1}^?}}~\mathsf{extern})~{\rightarrow}_{\epsilon}\,(\mathsf{ref}~{\mathsf{null}}{{{}_{2}^?}}~\mathsf{any}))` if and only if: + + + * :math:`{\mathsf{null}}{{{}_{1}^?}}` must be equal to :math:`{\mathsf{null}}{{{}_{2}^?}}`. * :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c)` is valid with type :math:`(\epsilon~{\rightarrow}_{\epsilon}\,\mathsf{v{\scriptstyle 128}})`. @@ -19573,6 +19579,27 @@ watsup 0.4 generator 1. Return :math:`{{\mathit{dt}}}{{}[ {i^{i_ [] [(REF nul EXTERN)]). +- the instr EXTERN.CONVERT_ANY is valid with the instruction type ([(REF nul1 ANY)] ->_ [] [(REF nul2 EXTERN)]) if and only if: + - nul1 is nul2. Instr_ok/any.convert_extern -- the instr ANY.CONVERT_EXTERN is valid with the instruction type ([(REF nul EXTERN)] ->_ [] [(REF nul ANY)]). +- the instr ANY.CONVERT_EXTERN is valid with the instruction type ([(REF nul1 EXTERN)] ->_ [] [(REF nul2 ANY)]) if and only if: + - nul1 is nul2. Instr_ok/vconst - the instr (V128.CONST c) is valid with the instruction type ([] ->_ [] [V128]). @@ -26002,6 +26031,15 @@ subst_all_reftype rt tu^n subst_all_deftype dt tu^n 1. Return $subst_deftype(dt, (_IDX i)^(i Date: Thu, 12 Sep 2024 09:50:44 +0200 Subject: [PATCH 2/3] Bump CI upload/download version --- .github/workflows/ci-spec.yml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/ci-spec.yml b/.github/workflows/ci-spec.yml index 56b92e0b79..6c790aa28d 100644 --- a/.github/workflows/ci-spec.yml +++ b/.github/workflows/ci-spec.yml @@ -43,7 +43,7 @@ jobs: #- name: Run Bikeshed # run: cd document/core && opam exec make bikeshed - name: Upload artifact - uses: actions/upload-artifact@v2 + uses: actions/upload-artifact@v4 with: name: core-rendered path: document/core/_build/html @@ -58,7 +58,7 @@ jobs: - name: Run Bikeshed run: bikeshed spec "document/js-api/index.bs" "document/js-api/index.html" - name: Upload artifact - uses: actions/upload-artifact@v2 + uses: actions/upload-artifact@v4 with: name: js-api-rendered path: document/js-api/index.html @@ -73,7 +73,7 @@ jobs: - name: Run Bikeshed run: bikeshed spec "document/web-api/index.bs" "document/web-api/index.html" - name: Upload artifact - uses: actions/upload-artifact@v2 + uses: actions/upload-artifact@v4 with: name: web-api-rendered path: document/web-api/index.html @@ -93,7 +93,7 @@ jobs: - name: Build main spec run: cd document/metadata/code && make main - name: Upload artifact - uses: actions/upload-artifact@v2 + uses: actions/upload-artifact@v4 with: name: code-metadata-rendered path: document/metadata/code/_build/html @@ -112,7 +112,7 @@ jobs: - name: Build main spec run: cd document/legacy/exceptions/core && make main - name: Upload artifact - uses: actions/upload-artifact@v2 + uses: actions/upload-artifact@v4 with: name: legacy-exceptions-core-rendered path: document/legacy/exceptions/core/_build/html @@ -127,7 +127,7 @@ jobs: - name: Run Bikeshed run: bikeshed spec "document/legacy/exceptions/js-api/index.bs" "document/legacy/exceptions/js-api/index.html" - name: Upload artifact - uses: actions/upload-artifact@v2 + uses: actions/upload-artifact@v4 with: name: legacy-exceptions-js-api-rendered path: document/legacy/exceptions/js-api/index.html @@ -141,32 +141,32 @@ jobs: - name: Create output directory run: mkdir _output && cp document/index.html _output/index.html - name: Download core spec artifact - uses: actions/download-artifact@v2 + uses: actions/download-artifact@v4 with: name: core-rendered path: _output/core - name: Download JS API spec artifact - uses: actions/download-artifact@v2 + uses: actions/download-artifact@v4 with: name: js-api-rendered path: _output/js-api - name: Download Web API spec artifact - uses: actions/download-artifact@v2 + uses: actions/download-artifact@v4 with: name: web-api-rendered path: _output/web-api - name: Download code metadata spec artifact - uses: actions/download-artifact@v2 + uses: actions/download-artifact@v4 with: name: code-metadata-rendered path: _output/metadata/code - name: Download legacy exceptions core spec artifact - uses: actions/download-artifact@v2 + uses: actions/download-artifact@v4 with: name: legacy-exceptions-core-rendered path: _output/legacy/exceptions/core - name: Download legacy exceptions JS API spec artifact - uses: actions/download-artifact@v2 + uses: actions/download-artifact@v4 with: name: legacy-exceptions-js-api-rendered path: _output/legacy/exceptions/js-api From 5ec16fa97f4deb2dd3aecf1ea5ea5b5244fb35fc Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 12 Sep 2024 11:48:15 +0200 Subject: [PATCH 3/3] TODO --- spectec/spec/wasm-3.0/5-runtime-aux.watsup | 9 + spectec/spec/wasm-3.0/9-module.watsup | 1 + spectec/test-frontend/TEST.md | 64 ++++-- spectec/test-latex/TEST.md | 21 ++ spectec/test-middlend/TEST.md | 256 +++++++++++++-------- spectec/test-prose/TEST.md | 39 ++++ spectec/test-splice/TEST.md | 6 + 7 files changed, 281 insertions(+), 115 deletions(-) diff --git a/spectec/spec/wasm-3.0/5-runtime-aux.watsup b/spectec/spec/wasm-3.0/5-runtime-aux.watsup index 3dcf72c802..a12583afe9 100644 --- a/spectec/spec/wasm-3.0/5-runtime-aux.watsup +++ b/spectec/spec/wasm-3.0/5-runtime-aux.watsup @@ -6,12 +6,21 @@ def $inst_valtype(moduleinst, valtype) : valtype hint(show $inst_(%,%)) hint(macro "insttype") def $inst_reftype(moduleinst, reftype) : reftype hint(show $inst_(%,%)) hint(macro "insttype") +def $inst_globaltype(moduleinst, globaltype) : globaltype hint(show $inst_(%,%)) hint(macro "insttype") +def $inst_tabletype(moduleinst, tabletype) : tabletype hint(show $inst_(%,%)) hint(macro "insttype") +def $inst_memtype(moduleinst, memtype) : memtype hint(show $inst_(%,%)) hint(macro "insttype") ;; TODO(3, rossberg): make inlining moduleinst.TYPES work def $inst_valtype(moduleinst, t) = $subst_all_valtype(t, dt*) -- if dt* = moduleinst.TYPES def $inst_reftype(moduleinst, rt) = $subst_all_reftype(rt, dt*) -- if dt* = moduleinst.TYPES +def $inst_globaltype(moduleinst, gt) = $subst_all_globaltype(gt, dt*) + -- if dt* = moduleinst.TYPES +def $inst_tabletype(moduleinst, tt) = $subst_all_tabletype(tt, dt*) + -- if dt* = moduleinst.TYPES +def $inst_memtype(moduleinst, mt) = $subst_all_memtype(mt, dt*) + -- if dt* = moduleinst.TYPES ;; diff --git a/spectec/spec/wasm-3.0/9-module.watsup b/spectec/spec/wasm-3.0/9-module.watsup index da7e945483..278579ce77 100644 --- a/spectec/spec/wasm-3.0/9-module.watsup +++ b/spectec/spec/wasm-3.0/9-module.watsup @@ -128,6 +128,7 @@ def $allocmodule(s, module, externaddr*, val_G*, ref_T*, (ref_E*)*) = (s_7, modu -- if ea* = ($(|s.ELEMS|+i_E))^(i_E<|elem*|) -- if da* = ($(|s.DATAS|+i_D))^(i_D<|data*|) -- if dt* = $alloctypes(type*) + ;; TODO(2, rossberg): use $inst_type(_, moduleinst) instead of $subst_all_type(_, dt*) below -- if (s_1, fa*) = $allocfuncs(s, dt*[x]*, (FUNC x local* expr_F)*, moduleinst^(|func*|)) -- if (s_2, ga*) = $allocglobals(s_1, $subst_all_globaltype(globaltype, dt*)*, val_G*) -- if (s_3, ta*) = $alloctables(s_2, $subst_all_tabletype(tabletype, dt*)*, ref_T*) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 110b985a80..b0b0d5e4e5 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -3270,6 +3270,24 @@ def $inst_reftype(moduleinst : moduleinst, reftype : reftype) : reftype def $inst_reftype{moduleinst : moduleinst, rt : reftype, `dt*` : deftype*}(moduleinst, rt) = $subst_all_reftype(rt, (dt : deftype <: heaptype)*{dt <- `dt*`}) -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) +;; 5-runtime-aux.watsup +def $inst_globaltype(moduleinst : moduleinst, globaltype : globaltype) : globaltype + ;; 5-runtime-aux.watsup + def $inst_globaltype{moduleinst : moduleinst, gt : globaltype, `dt*` : deftype*}(moduleinst, gt) = $subst_all_globaltype(gt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + +;; 5-runtime-aux.watsup +def $inst_tabletype(moduleinst : moduleinst, tabletype : tabletype) : tabletype + ;; 5-runtime-aux.watsup + def $inst_tabletype{moduleinst : moduleinst, tt : tabletype, `dt*` : deftype*}(moduleinst, tt) = $subst_all_tabletype(tt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + +;; 5-runtime-aux.watsup +def $inst_memtype(moduleinst : moduleinst, memtype : memtype) : memtype + ;; 5-runtime-aux.watsup + def $inst_memtype{moduleinst : moduleinst, mt : memtype, `dt*` : deftype*}(moduleinst, mt) = $subst_all_memtype(mt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + ;; 5-runtime-aux.watsup def $default_(valtype : valtype) : val? ;; 5-runtime-aux.watsup @@ -3300,13 +3318,13 @@ def $unpackfield_(storagetype : storagetype, sx?, fieldval : fieldval) : val ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:46.1-46.87 +;; 5-runtime-aux.watsup:55.1-55.87 def $funcsxa(externaddr*) : funcaddr* - ;; 5-runtime-aux.watsup:52.1-52.24 + ;; 5-runtime-aux.watsup:61.1-61.24 def $funcsxa([]) = [] - ;; 5-runtime-aux.watsup:53.1-53.47 + ;; 5-runtime-aux.watsup:62.1-62.47 def $funcsxa{fa : funcaddr, `xa*` : externaddr*}([FUNC_externaddr(fa)] ++ xa*{xa <- `xa*`}) = [fa] ++ $funcsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:54.1-54.59 + ;; 5-runtime-aux.watsup:63.1-63.59 def $funcsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $funcsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -3314,13 +3332,13 @@ def $funcsxa(externaddr*) : funcaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:47.1-47.89 +;; 5-runtime-aux.watsup:56.1-56.89 def $globalsxa(externaddr*) : globaladdr* - ;; 5-runtime-aux.watsup:56.1-56.26 + ;; 5-runtime-aux.watsup:65.1-65.26 def $globalsxa([]) = [] - ;; 5-runtime-aux.watsup:57.1-57.53 + ;; 5-runtime-aux.watsup:66.1-66.53 def $globalsxa{ga : globaladdr, `xa*` : externaddr*}([GLOBAL_externaddr(ga)] ++ xa*{xa <- `xa*`}) = [ga] ++ $globalsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:58.1-58.63 + ;; 5-runtime-aux.watsup:67.1-67.63 def $globalsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $globalsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -3328,13 +3346,13 @@ def $globalsxa(externaddr*) : globaladdr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:48.1-48.88 +;; 5-runtime-aux.watsup:57.1-57.88 def $tablesxa(externaddr*) : tableaddr* - ;; 5-runtime-aux.watsup:60.1-60.25 + ;; 5-runtime-aux.watsup:69.1-69.25 def $tablesxa([]) = [] - ;; 5-runtime-aux.watsup:61.1-61.50 + ;; 5-runtime-aux.watsup:70.1-70.50 def $tablesxa{ta : tableaddr, `xa*` : externaddr*}([TABLE_externaddr(ta)] ++ xa*{xa <- `xa*`}) = [ta] ++ $tablesxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:62.1-62.61 + ;; 5-runtime-aux.watsup:71.1-71.61 def $tablesxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $tablesxa(xa*{xa <- `xa*`}) -- otherwise } @@ -3342,13 +3360,13 @@ def $tablesxa(externaddr*) : tableaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:49.1-49.86 +;; 5-runtime-aux.watsup:58.1-58.86 def $memsxa(externaddr*) : memaddr* - ;; 5-runtime-aux.watsup:64.1-64.23 + ;; 5-runtime-aux.watsup:73.1-73.23 def $memsxa([]) = [] - ;; 5-runtime-aux.watsup:65.1-65.44 + ;; 5-runtime-aux.watsup:74.1-74.44 def $memsxa{ma : memaddr, `xa*` : externaddr*}([MEM_externaddr(ma)] ++ xa*{xa <- `xa*`}) = [ma] ++ $memsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:66.1-66.57 + ;; 5-runtime-aux.watsup:75.1-75.57 def $memsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $memsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -3356,13 +3374,13 @@ def $memsxa(externaddr*) : memaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:50.1-50.86 +;; 5-runtime-aux.watsup:59.1-59.86 def $tagsxa(externaddr*) : tagaddr* - ;; 5-runtime-aux.watsup:68.1-68.23 + ;; 5-runtime-aux.watsup:77.1-77.23 def $tagsxa([]) = [] - ;; 5-runtime-aux.watsup:69.1-69.44 + ;; 5-runtime-aux.watsup:78.1-78.44 def $tagsxa{ha : tagaddr, `xa*` : externaddr*}([TAG_externaddr(ha)] ++ xa*{xa <- `xa*`}) = [ha] ++ $tagsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:70.1-70.57 + ;; 5-runtime-aux.watsup:79.1-79.57 def $tagsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $tagsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -6617,11 +6635,11 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup rec { -;; 9-module.watsup:169.1-169.94 +;; 9-module.watsup:170.1-170.94 def $evalglobals(state : state, globaltype*, expr*) : (state, val*) - ;; 9-module.watsup:170.1-170.41 + ;; 9-module.watsup:171.1-171.41 def $evalglobals{z : state}(z, [], []) = (z, []) - ;; 9-module.watsup:171.1-176.81 + ;; 9-module.watsup:172.1-177.81 def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z' : state, val : val, `val'*` : val*, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z', [val] ++ val'*{val' <- `val'*`}) -- Eval_expr: `%;%~>*%;%`(z, expr, z, [val]) -- if (z = `%;%`_state(s, f)) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 27cb1b7775..53e1449d5c 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -4018,6 +4018,27 @@ $$ \end{array} $$ +$$ +\begin{array}{@{}lcl@{}l@{}} +{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{gt}}) &=& {{\mathit{gt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]} + &\qquad \mbox{if}~{{\mathit{dt}}^\ast} = {\mathit{moduleinst}}{.}\mathsf{types} \\ +\end{array} +$$ + +$$ +\begin{array}{@{}lcl@{}l@{}} +{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{tt}}) &=& {{\mathit{tt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]} + &\qquad \mbox{if}~{{\mathit{dt}}^\ast} = {\mathit{moduleinst}}{.}\mathsf{types} \\ +\end{array} +$$ + +$$ +\begin{array}{@{}lcl@{}l@{}} +{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{mt}}) &=& {{\mathit{mt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]} + &\qquad \mbox{if}~{{\mathit{dt}}^\ast} = {\mathit{moduleinst}}{.}\mathsf{types} \\ +\end{array} +$$ + \vspace{1ex} \vspace{1ex} diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index c4613618b9..034f777e35 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -3260,6 +3260,24 @@ def $inst_reftype(moduleinst : moduleinst, reftype : reftype) : reftype def $inst_reftype{moduleinst : moduleinst, rt : reftype, `dt*` : deftype*}(moduleinst, rt) = $subst_all_reftype(rt, (dt : deftype <: heaptype)*{dt <- `dt*`}) -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) +;; 5-runtime-aux.watsup +def $inst_globaltype(moduleinst : moduleinst, globaltype : globaltype) : globaltype + ;; 5-runtime-aux.watsup + def $inst_globaltype{moduleinst : moduleinst, gt : globaltype, `dt*` : deftype*}(moduleinst, gt) = $subst_all_globaltype(gt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + +;; 5-runtime-aux.watsup +def $inst_tabletype(moduleinst : moduleinst, tabletype : tabletype) : tabletype + ;; 5-runtime-aux.watsup + def $inst_tabletype{moduleinst : moduleinst, tt : tabletype, `dt*` : deftype*}(moduleinst, tt) = $subst_all_tabletype(tt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + +;; 5-runtime-aux.watsup +def $inst_memtype(moduleinst : moduleinst, memtype : memtype) : memtype + ;; 5-runtime-aux.watsup + def $inst_memtype{moduleinst : moduleinst, mt : memtype, `dt*` : deftype*}(moduleinst, mt) = $subst_all_memtype(mt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + ;; 5-runtime-aux.watsup def $default_(valtype : valtype) : val? ;; 5-runtime-aux.watsup @@ -3290,13 +3308,13 @@ def $unpackfield_(storagetype : storagetype, sx?, fieldval : fieldval) : val ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:46.1-46.87 +;; 5-runtime-aux.watsup:55.1-55.87 def $funcsxa(externaddr*) : funcaddr* - ;; 5-runtime-aux.watsup:52.1-52.24 + ;; 5-runtime-aux.watsup:61.1-61.24 def $funcsxa([]) = [] - ;; 5-runtime-aux.watsup:53.1-53.47 + ;; 5-runtime-aux.watsup:62.1-62.47 def $funcsxa{fa : funcaddr, `xa*` : externaddr*}([FUNC_externaddr(fa)] ++ xa*{xa <- `xa*`}) = [fa] ++ $funcsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:54.1-54.59 + ;; 5-runtime-aux.watsup:63.1-63.59 def $funcsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $funcsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -3304,13 +3322,13 @@ def $funcsxa(externaddr*) : funcaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:47.1-47.89 +;; 5-runtime-aux.watsup:56.1-56.89 def $globalsxa(externaddr*) : globaladdr* - ;; 5-runtime-aux.watsup:56.1-56.26 + ;; 5-runtime-aux.watsup:65.1-65.26 def $globalsxa([]) = [] - ;; 5-runtime-aux.watsup:57.1-57.53 + ;; 5-runtime-aux.watsup:66.1-66.53 def $globalsxa{ga : globaladdr, `xa*` : externaddr*}([GLOBAL_externaddr(ga)] ++ xa*{xa <- `xa*`}) = [ga] ++ $globalsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:58.1-58.63 + ;; 5-runtime-aux.watsup:67.1-67.63 def $globalsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $globalsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -3318,13 +3336,13 @@ def $globalsxa(externaddr*) : globaladdr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:48.1-48.88 +;; 5-runtime-aux.watsup:57.1-57.88 def $tablesxa(externaddr*) : tableaddr* - ;; 5-runtime-aux.watsup:60.1-60.25 + ;; 5-runtime-aux.watsup:69.1-69.25 def $tablesxa([]) = [] - ;; 5-runtime-aux.watsup:61.1-61.50 + ;; 5-runtime-aux.watsup:70.1-70.50 def $tablesxa{ta : tableaddr, `xa*` : externaddr*}([TABLE_externaddr(ta)] ++ xa*{xa <- `xa*`}) = [ta] ++ $tablesxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:62.1-62.61 + ;; 5-runtime-aux.watsup:71.1-71.61 def $tablesxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $tablesxa(xa*{xa <- `xa*`}) -- otherwise } @@ -3332,13 +3350,13 @@ def $tablesxa(externaddr*) : tableaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:49.1-49.86 +;; 5-runtime-aux.watsup:58.1-58.86 def $memsxa(externaddr*) : memaddr* - ;; 5-runtime-aux.watsup:64.1-64.23 + ;; 5-runtime-aux.watsup:73.1-73.23 def $memsxa([]) = [] - ;; 5-runtime-aux.watsup:65.1-65.44 + ;; 5-runtime-aux.watsup:74.1-74.44 def $memsxa{ma : memaddr, `xa*` : externaddr*}([MEM_externaddr(ma)] ++ xa*{xa <- `xa*`}) = [ma] ++ $memsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:66.1-66.57 + ;; 5-runtime-aux.watsup:75.1-75.57 def $memsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $memsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -3346,13 +3364,13 @@ def $memsxa(externaddr*) : memaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:50.1-50.86 +;; 5-runtime-aux.watsup:59.1-59.86 def $tagsxa(externaddr*) : tagaddr* - ;; 5-runtime-aux.watsup:68.1-68.23 + ;; 5-runtime-aux.watsup:77.1-77.23 def $tagsxa([]) = [] - ;; 5-runtime-aux.watsup:69.1-69.44 + ;; 5-runtime-aux.watsup:78.1-78.44 def $tagsxa{ha : tagaddr, `xa*` : externaddr*}([TAG_externaddr(ha)] ++ xa*{xa <- `xa*`}) = [ha] ++ $tagsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:70.1-70.57 + ;; 5-runtime-aux.watsup:79.1-79.57 def $tagsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $tagsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -6607,11 +6625,11 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup rec { -;; 9-module.watsup:169.1-169.94 +;; 9-module.watsup:170.1-170.94 def $evalglobals(state : state, globaltype*, expr*) : (state, val*) - ;; 9-module.watsup:170.1-170.41 + ;; 9-module.watsup:171.1-171.41 def $evalglobals{z : state}(z, [], []) = (z, []) - ;; 9-module.watsup:171.1-176.81 + ;; 9-module.watsup:172.1-177.81 def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z' : state, val : val, `val'*` : val*, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z', [val] ++ val'*{val' <- `val'*`}) -- Eval_expr: `%;%~>*%;%`(z, expr, z, [val]) -- if (z = `%;%`_state(s, f)) @@ -11580,6 +11598,24 @@ def $inst_reftype(moduleinst : moduleinst, reftype : reftype) : reftype def $inst_reftype{moduleinst : moduleinst, rt : reftype, `dt*` : deftype*}(moduleinst, rt) = $subst_all_reftype(rt, (dt : deftype <: heaptype)*{dt <- `dt*`}) -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) +;; 5-runtime-aux.watsup +def $inst_globaltype(moduleinst : moduleinst, globaltype : globaltype) : globaltype + ;; 5-runtime-aux.watsup + def $inst_globaltype{moduleinst : moduleinst, gt : globaltype, `dt*` : deftype*}(moduleinst, gt) = $subst_all_globaltype(gt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + +;; 5-runtime-aux.watsup +def $inst_tabletype(moduleinst : moduleinst, tabletype : tabletype) : tabletype + ;; 5-runtime-aux.watsup + def $inst_tabletype{moduleinst : moduleinst, tt : tabletype, `dt*` : deftype*}(moduleinst, tt) = $subst_all_tabletype(tt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + +;; 5-runtime-aux.watsup +def $inst_memtype(moduleinst : moduleinst, memtype : memtype) : memtype + ;; 5-runtime-aux.watsup + def $inst_memtype{moduleinst : moduleinst, mt : memtype, `dt*` : deftype*}(moduleinst, mt) = $subst_all_memtype(mt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + ;; 5-runtime-aux.watsup def $default_(valtype : valtype) : val? ;; 5-runtime-aux.watsup @@ -11610,13 +11646,13 @@ def $unpackfield_(storagetype : storagetype, sx?, fieldval : fieldval) : val ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:46.1-46.87 +;; 5-runtime-aux.watsup:55.1-55.87 def $funcsxa(externaddr*) : funcaddr* - ;; 5-runtime-aux.watsup:52.1-52.24 + ;; 5-runtime-aux.watsup:61.1-61.24 def $funcsxa([]) = [] - ;; 5-runtime-aux.watsup:53.1-53.47 + ;; 5-runtime-aux.watsup:62.1-62.47 def $funcsxa{fa : funcaddr, `xa*` : externaddr*}([FUNC_externaddr(fa)] ++ xa*{xa <- `xa*`}) = [fa] ++ $funcsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:54.1-54.59 + ;; 5-runtime-aux.watsup:63.1-63.59 def $funcsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $funcsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -11624,13 +11660,13 @@ def $funcsxa(externaddr*) : funcaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:47.1-47.89 +;; 5-runtime-aux.watsup:56.1-56.89 def $globalsxa(externaddr*) : globaladdr* - ;; 5-runtime-aux.watsup:56.1-56.26 + ;; 5-runtime-aux.watsup:65.1-65.26 def $globalsxa([]) = [] - ;; 5-runtime-aux.watsup:57.1-57.53 + ;; 5-runtime-aux.watsup:66.1-66.53 def $globalsxa{ga : globaladdr, `xa*` : externaddr*}([GLOBAL_externaddr(ga)] ++ xa*{xa <- `xa*`}) = [ga] ++ $globalsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:58.1-58.63 + ;; 5-runtime-aux.watsup:67.1-67.63 def $globalsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $globalsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -11638,13 +11674,13 @@ def $globalsxa(externaddr*) : globaladdr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:48.1-48.88 +;; 5-runtime-aux.watsup:57.1-57.88 def $tablesxa(externaddr*) : tableaddr* - ;; 5-runtime-aux.watsup:60.1-60.25 + ;; 5-runtime-aux.watsup:69.1-69.25 def $tablesxa([]) = [] - ;; 5-runtime-aux.watsup:61.1-61.50 + ;; 5-runtime-aux.watsup:70.1-70.50 def $tablesxa{ta : tableaddr, `xa*` : externaddr*}([TABLE_externaddr(ta)] ++ xa*{xa <- `xa*`}) = [ta] ++ $tablesxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:62.1-62.61 + ;; 5-runtime-aux.watsup:71.1-71.61 def $tablesxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $tablesxa(xa*{xa <- `xa*`}) -- otherwise } @@ -11652,13 +11688,13 @@ def $tablesxa(externaddr*) : tableaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:49.1-49.86 +;; 5-runtime-aux.watsup:58.1-58.86 def $memsxa(externaddr*) : memaddr* - ;; 5-runtime-aux.watsup:64.1-64.23 + ;; 5-runtime-aux.watsup:73.1-73.23 def $memsxa([]) = [] - ;; 5-runtime-aux.watsup:65.1-65.44 + ;; 5-runtime-aux.watsup:74.1-74.44 def $memsxa{ma : memaddr, `xa*` : externaddr*}([MEM_externaddr(ma)] ++ xa*{xa <- `xa*`}) = [ma] ++ $memsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:66.1-66.57 + ;; 5-runtime-aux.watsup:75.1-75.57 def $memsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $memsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -11666,13 +11702,13 @@ def $memsxa(externaddr*) : memaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:50.1-50.86 +;; 5-runtime-aux.watsup:59.1-59.86 def $tagsxa(externaddr*) : tagaddr* - ;; 5-runtime-aux.watsup:68.1-68.23 + ;; 5-runtime-aux.watsup:77.1-77.23 def $tagsxa([]) = [] - ;; 5-runtime-aux.watsup:69.1-69.44 + ;; 5-runtime-aux.watsup:78.1-78.44 def $tagsxa{ha : tagaddr, `xa*` : externaddr*}([TAG_externaddr(ha)] ++ xa*{xa <- `xa*`}) = [ha] ++ $tagsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:70.1-70.57 + ;; 5-runtime-aux.watsup:79.1-79.57 def $tagsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $tagsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -14929,11 +14965,11 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup rec { -;; 9-module.watsup:169.1-169.94 +;; 9-module.watsup:170.1-170.94 def $evalglobals(state : state, globaltype*, expr*) : (state, val*) - ;; 9-module.watsup:170.1-170.41 + ;; 9-module.watsup:171.1-171.41 def $evalglobals{z : state}(z, [], []) = (z, []) - ;; 9-module.watsup:171.1-176.81 + ;; 9-module.watsup:172.1-177.81 def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z' : state, val : val, `val'*` : val*, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z', [val] ++ val'*{val' <- `val'*`}) -- Eval_expr: `%;%~>*%;%`(z, expr, z, [val]) -- if (z = `%;%`_state(s, f)) @@ -19902,6 +19938,24 @@ def $inst_reftype(moduleinst : moduleinst, reftype : reftype) : reftype def $inst_reftype{moduleinst : moduleinst, rt : reftype, `dt*` : deftype*}(moduleinst, rt) = $subst_all_reftype(rt, (dt : deftype <: heaptype)*{dt <- `dt*`}) -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) +;; 5-runtime-aux.watsup +def $inst_globaltype(moduleinst : moduleinst, globaltype : globaltype) : globaltype + ;; 5-runtime-aux.watsup + def $inst_globaltype{moduleinst : moduleinst, gt : globaltype, `dt*` : deftype*}(moduleinst, gt) = $subst_all_globaltype(gt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + +;; 5-runtime-aux.watsup +def $inst_tabletype(moduleinst : moduleinst, tabletype : tabletype) : tabletype + ;; 5-runtime-aux.watsup + def $inst_tabletype{moduleinst : moduleinst, tt : tabletype, `dt*` : deftype*}(moduleinst, tt) = $subst_all_tabletype(tt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + +;; 5-runtime-aux.watsup +def $inst_memtype(moduleinst : moduleinst, memtype : memtype) : memtype + ;; 5-runtime-aux.watsup + def $inst_memtype{moduleinst : moduleinst, mt : memtype, `dt*` : deftype*}(moduleinst, mt) = $subst_all_memtype(mt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + ;; 5-runtime-aux.watsup def $default_(valtype : valtype) : val? ;; 5-runtime-aux.watsup @@ -19932,13 +19986,13 @@ def $unpackfield_(storagetype : storagetype, sx?, fieldval : fieldval) : val ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:46.1-46.87 +;; 5-runtime-aux.watsup:55.1-55.87 def $funcsxa(externaddr*) : funcaddr* - ;; 5-runtime-aux.watsup:52.1-52.24 + ;; 5-runtime-aux.watsup:61.1-61.24 def $funcsxa([]) = [] - ;; 5-runtime-aux.watsup:53.1-53.47 + ;; 5-runtime-aux.watsup:62.1-62.47 def $funcsxa{fa : funcaddr, `xa*` : externaddr*}([FUNC_externaddr(fa)] ++ xa*{xa <- `xa*`}) = [fa] ++ $funcsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:54.1-54.59 + ;; 5-runtime-aux.watsup:63.1-63.59 def $funcsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $funcsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -19946,13 +20000,13 @@ def $funcsxa(externaddr*) : funcaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:47.1-47.89 +;; 5-runtime-aux.watsup:56.1-56.89 def $globalsxa(externaddr*) : globaladdr* - ;; 5-runtime-aux.watsup:56.1-56.26 + ;; 5-runtime-aux.watsup:65.1-65.26 def $globalsxa([]) = [] - ;; 5-runtime-aux.watsup:57.1-57.53 + ;; 5-runtime-aux.watsup:66.1-66.53 def $globalsxa{ga : globaladdr, `xa*` : externaddr*}([GLOBAL_externaddr(ga)] ++ xa*{xa <- `xa*`}) = [ga] ++ $globalsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:58.1-58.63 + ;; 5-runtime-aux.watsup:67.1-67.63 def $globalsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $globalsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -19960,13 +20014,13 @@ def $globalsxa(externaddr*) : globaladdr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:48.1-48.88 +;; 5-runtime-aux.watsup:57.1-57.88 def $tablesxa(externaddr*) : tableaddr* - ;; 5-runtime-aux.watsup:60.1-60.25 + ;; 5-runtime-aux.watsup:69.1-69.25 def $tablesxa([]) = [] - ;; 5-runtime-aux.watsup:61.1-61.50 + ;; 5-runtime-aux.watsup:70.1-70.50 def $tablesxa{ta : tableaddr, `xa*` : externaddr*}([TABLE_externaddr(ta)] ++ xa*{xa <- `xa*`}) = [ta] ++ $tablesxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:62.1-62.61 + ;; 5-runtime-aux.watsup:71.1-71.61 def $tablesxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $tablesxa(xa*{xa <- `xa*`}) -- otherwise } @@ -19974,13 +20028,13 @@ def $tablesxa(externaddr*) : tableaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:49.1-49.86 +;; 5-runtime-aux.watsup:58.1-58.86 def $memsxa(externaddr*) : memaddr* - ;; 5-runtime-aux.watsup:64.1-64.23 + ;; 5-runtime-aux.watsup:73.1-73.23 def $memsxa([]) = [] - ;; 5-runtime-aux.watsup:65.1-65.44 + ;; 5-runtime-aux.watsup:74.1-74.44 def $memsxa{ma : memaddr, `xa*` : externaddr*}([MEM_externaddr(ma)] ++ xa*{xa <- `xa*`}) = [ma] ++ $memsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:66.1-66.57 + ;; 5-runtime-aux.watsup:75.1-75.57 def $memsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $memsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -19988,13 +20042,13 @@ def $memsxa(externaddr*) : memaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:50.1-50.86 +;; 5-runtime-aux.watsup:59.1-59.86 def $tagsxa(externaddr*) : tagaddr* - ;; 5-runtime-aux.watsup:68.1-68.23 + ;; 5-runtime-aux.watsup:77.1-77.23 def $tagsxa([]) = [] - ;; 5-runtime-aux.watsup:69.1-69.44 + ;; 5-runtime-aux.watsup:78.1-78.44 def $tagsxa{ha : tagaddr, `xa*` : externaddr*}([TAG_externaddr(ha)] ++ xa*{xa <- `xa*`}) = [ha] ++ $tagsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:70.1-70.57 + ;; 5-runtime-aux.watsup:79.1-79.57 def $tagsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $tagsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -23251,11 +23305,11 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup rec { -;; 9-module.watsup:169.1-169.94 +;; 9-module.watsup:170.1-170.94 def $evalglobals(state : state, globaltype*, expr*) : (state, val*) - ;; 9-module.watsup:170.1-170.41 + ;; 9-module.watsup:171.1-171.41 def $evalglobals{z : state}(z, [], []) = (z, []) - ;; 9-module.watsup:171.1-176.81 + ;; 9-module.watsup:172.1-177.81 def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z' : state, val : val, `val'*` : val*, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z', [val] ++ val'*{val' <- `val'*`}) -- Eval_expr: `%;%~>*%;%`(z, expr, z, [val]) -- if (z = `%;%`_state(s, f)) @@ -28224,6 +28278,24 @@ def $inst_reftype(moduleinst : moduleinst, reftype : reftype) : reftype def $inst_reftype{moduleinst : moduleinst, rt : reftype, `dt*` : deftype*}(moduleinst, rt) = $subst_all_reftype(rt, (dt : deftype <: heaptype)*{dt <- `dt*`}) -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) +;; 5-runtime-aux.watsup +def $inst_globaltype(moduleinst : moduleinst, globaltype : globaltype) : globaltype + ;; 5-runtime-aux.watsup + def $inst_globaltype{moduleinst : moduleinst, gt : globaltype, `dt*` : deftype*}(moduleinst, gt) = $subst_all_globaltype(gt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + +;; 5-runtime-aux.watsup +def $inst_tabletype(moduleinst : moduleinst, tabletype : tabletype) : tabletype + ;; 5-runtime-aux.watsup + def $inst_tabletype{moduleinst : moduleinst, tt : tabletype, `dt*` : deftype*}(moduleinst, tt) = $subst_all_tabletype(tt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + +;; 5-runtime-aux.watsup +def $inst_memtype(moduleinst : moduleinst, memtype : memtype) : memtype + ;; 5-runtime-aux.watsup + def $inst_memtype{moduleinst : moduleinst, mt : memtype, `dt*` : deftype*}(moduleinst, mt) = $subst_all_memtype(mt, (dt : deftype <: heaptype)*{dt <- `dt*`}) + -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + ;; 5-runtime-aux.watsup def $default_(valtype : valtype) : val? ;; 5-runtime-aux.watsup @@ -28254,13 +28326,13 @@ def $unpackfield_(storagetype : storagetype, sx?, fieldval : fieldval) : val ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:46.1-46.87 +;; 5-runtime-aux.watsup:55.1-55.87 def $funcsxa(externaddr*) : funcaddr* - ;; 5-runtime-aux.watsup:52.1-52.24 + ;; 5-runtime-aux.watsup:61.1-61.24 def $funcsxa([]) = [] - ;; 5-runtime-aux.watsup:53.1-53.47 + ;; 5-runtime-aux.watsup:62.1-62.47 def $funcsxa{fa : funcaddr, `xa*` : externaddr*}([FUNC_externaddr(fa)] ++ xa*{xa <- `xa*`}) = [fa] ++ $funcsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:54.1-54.59 + ;; 5-runtime-aux.watsup:63.1-63.59 def $funcsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $funcsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -28268,13 +28340,13 @@ def $funcsxa(externaddr*) : funcaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:47.1-47.89 +;; 5-runtime-aux.watsup:56.1-56.89 def $globalsxa(externaddr*) : globaladdr* - ;; 5-runtime-aux.watsup:56.1-56.26 + ;; 5-runtime-aux.watsup:65.1-65.26 def $globalsxa([]) = [] - ;; 5-runtime-aux.watsup:57.1-57.53 + ;; 5-runtime-aux.watsup:66.1-66.53 def $globalsxa{ga : globaladdr, `xa*` : externaddr*}([GLOBAL_externaddr(ga)] ++ xa*{xa <- `xa*`}) = [ga] ++ $globalsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:58.1-58.63 + ;; 5-runtime-aux.watsup:67.1-67.63 def $globalsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $globalsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -28282,13 +28354,13 @@ def $globalsxa(externaddr*) : globaladdr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:48.1-48.88 +;; 5-runtime-aux.watsup:57.1-57.88 def $tablesxa(externaddr*) : tableaddr* - ;; 5-runtime-aux.watsup:60.1-60.25 + ;; 5-runtime-aux.watsup:69.1-69.25 def $tablesxa([]) = [] - ;; 5-runtime-aux.watsup:61.1-61.50 + ;; 5-runtime-aux.watsup:70.1-70.50 def $tablesxa{ta : tableaddr, `xa*` : externaddr*}([TABLE_externaddr(ta)] ++ xa*{xa <- `xa*`}) = [ta] ++ $tablesxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:62.1-62.61 + ;; 5-runtime-aux.watsup:71.1-71.61 def $tablesxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $tablesxa(xa*{xa <- `xa*`}) -- otherwise } @@ -28296,13 +28368,13 @@ def $tablesxa(externaddr*) : tableaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:49.1-49.86 +;; 5-runtime-aux.watsup:58.1-58.86 def $memsxa(externaddr*) : memaddr* - ;; 5-runtime-aux.watsup:64.1-64.23 + ;; 5-runtime-aux.watsup:73.1-73.23 def $memsxa([]) = [] - ;; 5-runtime-aux.watsup:65.1-65.44 + ;; 5-runtime-aux.watsup:74.1-74.44 def $memsxa{ma : memaddr, `xa*` : externaddr*}([MEM_externaddr(ma)] ++ xa*{xa <- `xa*`}) = [ma] ++ $memsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:66.1-66.57 + ;; 5-runtime-aux.watsup:75.1-75.57 def $memsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $memsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -28310,13 +28382,13 @@ def $memsxa(externaddr*) : memaddr* ;; 5-runtime-aux.watsup rec { -;; 5-runtime-aux.watsup:50.1-50.86 +;; 5-runtime-aux.watsup:59.1-59.86 def $tagsxa(externaddr*) : tagaddr* - ;; 5-runtime-aux.watsup:68.1-68.23 + ;; 5-runtime-aux.watsup:77.1-77.23 def $tagsxa([]) = [] - ;; 5-runtime-aux.watsup:69.1-69.44 + ;; 5-runtime-aux.watsup:78.1-78.44 def $tagsxa{ha : tagaddr, `xa*` : externaddr*}([TAG_externaddr(ha)] ++ xa*{xa <- `xa*`}) = [ha] ++ $tagsxa(xa*{xa <- `xa*`}) - ;; 5-runtime-aux.watsup:70.1-70.57 + ;; 5-runtime-aux.watsup:79.1-79.57 def $tagsxa{externaddr : externaddr, `xa*` : externaddr*}([externaddr] ++ xa*{xa <- `xa*`}) = $tagsxa(xa*{xa <- `xa*`}) -- otherwise } @@ -31766,11 +31838,11 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup rec { -;; 9-module.watsup:169.1-169.94 +;; 9-module.watsup:170.1-170.94 def $evalglobals(state : state, globaltype*, expr*) : (state, val*) - ;; 9-module.watsup:170.1-170.41 + ;; 9-module.watsup:171.1-171.41 def $evalglobals{z : state}(z, [], []) = (z, []) - ;; 9-module.watsup:171.1-176.81 + ;; 9-module.watsup:172.1-177.81 def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z' : state, val : val, `val'*` : val*, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z', [val] ++ val'*{val' <- `val'*`}) -- Eval_expr: `%;%~>*%;%`(z, expr, z, [val]) -- if (z = `%;%`_state(s, f)) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 1685587196..07c1f947fe 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -21139,6 +21139,33 @@ watsup 0.4 generator #. Return :math:`{{\mathit{rt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]}`. +:math:`{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{gt}})` +................................................................ + + +1. Let :math:`{{\mathit{dt}}^\ast}` be :math:`{\mathit{moduleinst}}{.}\mathsf{types}`. + +#. Return :math:`{{\mathit{gt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]}`. + + +:math:`{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{tt}})` +................................................................ + + +1. Let :math:`{{\mathit{dt}}^\ast}` be :math:`{\mathit{moduleinst}}{.}\mathsf{types}`. + +#. Return :math:`{{\mathit{tt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]}`. + + +:math:`{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{mt}})` +................................................................ + + +1. Let :math:`{{\mathit{dt}}^\ast}` be :math:`{\mathit{moduleinst}}{.}\mathsf{types}`. + +#. Return :math:`{{\mathit{mt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]}`. + + :math:`{{\mathrm{default}}}_{{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}}` ......................................................................................... @@ -26783,6 +26810,18 @@ inst_reftype moduleinst rt 1. Let dt* be moduleinst.TYPES. 2. Return $subst_all_reftype(rt, dt*). +inst_globaltype moduleinst gt +1. Let dt* be moduleinst.TYPES. +2. Return $subst_all_globaltype(gt, dt*). + +inst_tabletype moduleinst tt +1. Let dt* be moduleinst.TYPES. +2. Return $subst_all_tabletype(tt, dt*). + +inst_memtype moduleinst mt +1. Let dt* be moduleinst.TYPES. +2. Return $subst_all_memtype(mt, dt*). + default_ valtype_u0 1. If the type of valtype_u0 is Inn, then: a. Let Inn be valtype_u0. diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 34f8065f87..7cc9c0e8cd 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -1365,7 +1365,10 @@ warning: definition `imul_` was never spliced warning: definition `ine_` was never spliced warning: definition `ineg_` was never spliced warning: definition `inot_` was never spliced +warning: definition `inst_globaltype` was never spliced +warning: definition `inst_memtype` was never spliced warning: definition `inst_reftype` was never spliced +warning: definition `inst_tabletype` was never spliced warning: definition `inst_valtype` was never spliced warning: definition `instantiate` was never spliced warning: definition `instrdots` was never spliced @@ -1935,7 +1938,10 @@ warning: definition prose `globalsxx` was never spliced warning: definition prose `growmem` was never spliced warning: definition prose `growtable` was never spliced warning: definition prose `half__` was never spliced +warning: definition prose `inst_globaltype` was never spliced +warning: definition prose `inst_memtype` was never spliced warning: definition prose `inst_reftype` was never spliced +warning: definition prose `inst_tabletype` was never spliced warning: definition prose `inst_valtype` was never spliced warning: definition prose `instantiate` was never spliced warning: definition prose `invfbytes_` was never spliced