diff --git a/spectec/spec/wasm-3.0/1-syntax.watsup b/spectec/spec/wasm-3.0/1-syntax.watsup index b42ca04701..0504012e3a 100644 --- a/spectec/spec/wasm-3.0/1-syntax.watsup +++ b/spectec/spec/wasm-3.0/1-syntax.watsup @@ -560,7 +560,7 @@ syntax instr/vec hint(desc "vector instruction") = ... -- if sx? =/= eps <=> $lanetype(shape_1) = Jnn_1 /\ $lanetype(shape_2) = Jnn_2 /\ $lsizenn1(Jnn_1) > $lsizenn2(Jnn_2) | VSPLAT shape hint(show ##%.SPLAT) hint(macro "VSPLAT") | VEXTRACT_LANE shape sx? laneidx hint(show ##%.EXTRACT_LANE %) hint(show ##%.EXTRACT_LANE#_#% %) hint(macro "VEXTRACT_LANE") - -- if $lanetype(shape) = numtype <=> sx? = eps + -- if sx? = eps <=> $lanetype(shape) = numtype | VREPLACE_LANE shape laneidx hint(show ##%.REPLACE_LANE %) hint(macro "VREPLACE_LANE") | ... diff --git a/spectec/spec/wasm-3.0/6-typing.watsup b/spectec/spec/wasm-3.0/6-typing.watsup index f77075a4bd..4b294ed187 100644 --- a/spectec/spec/wasm-3.0/6-typing.watsup +++ b/spectec/spec/wasm-3.0/6-typing.watsup @@ -906,7 +906,6 @@ rule Instr_ok/vshuffle: rule Instr_ok/vsplat: C |- VSPLAT sh : $unpackshape(sh) -> V128 -;; TODO(1, rossberg): This rule (or the abstract syntax) is too liberal, since some combinations are illegal rule Instr_ok/vextract_lane: C |- VEXTRACT_LANE sh sx? i : V128 -> $unpackshape(sh) -- if i < $dim(sh) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 0a4c820588..ad30c7d816 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -1185,7 +1185,7 @@ syntax instr = -- if ((sx?{sx : sx} =/= ?()) <=> ((($lanetype(shape_1) = (Jnn_1 : Jnn <: lanetype)) /\ ($lanetype(shape_2) = (Jnn_2 : Jnn <: lanetype))) /\ ($lsizenn1((Jnn_1 : Jnn <: lanetype)) > $lsizenn2((Jnn_2 : Jnn <: lanetype))))) | VSPLAT{shape : shape}(shape : shape) | VEXTRACT_LANE{shape : shape, sx? : sx?, laneidx : laneidx, numtype : numtype}(shape : shape, sx?{sx : sx} : sx?, laneidx : laneidx) - -- if (($lanetype(shape) = (numtype : numtype <: lanetype)) <=> (sx?{sx : sx} = ?())) + -- if ((sx?{sx : sx} = ?()) <=> ($lanetype(shape) = (numtype : numtype <: lanetype))) | VREPLACE_LANE{shape : shape, laneidx : laneidx}(shape : shape, laneidx : laneidx) | REF.NULL{heaptype : heaptype}(heaptype : heaptype) | REF.IS_NULL @@ -4448,195 +4448,195 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:910.1-912.21 + ;; 6-typing.watsup:909.1-911.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:914.1-916.21 + ;; 6-typing.watsup:913.1-915.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:918.1-919.50 + ;; 6-typing.watsup:917.1-918.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:921.1-922.57 + ;; 6-typing.watsup:920.1-921.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:924.1-925.48 + ;; 6-typing.watsup:923.1-924.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:927.1-928.62 + ;; 6-typing.watsup:926.1-927.62 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop_(sh_2, sh_1), half? : half_(sh_2, sh_1)?, sx? : sx?, zero? : zero_(sh_2, sh_1)?}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop, half?{half : half_(sh_2, sh_1)}, sx?{sx : sx}, zero?{zero : zero_(sh_2, sh_1)}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:933.1-935.28 + ;; 6-typing.watsup:932.1-934.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:937.1-939.29 + ;; 6-typing.watsup:936.1-938.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:941.1-943.29 + ;; 6-typing.watsup:940.1-942.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:948.1-950.29 + ;; 6-typing.watsup:947.1-949.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:952.1-954.29 + ;; 6-typing.watsup:951.1-953.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:959.1-961.29 + ;; 6-typing.watsup:958.1-960.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:963.1-965.29 + ;; 6-typing.watsup:962.1-964.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:967.1-969.29 + ;; 6-typing.watsup:966.1-968.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:971.1-973.29 + ;; 6-typing.watsup:970.1-972.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:975.1-977.29 + ;; 6-typing.watsup:974.1-976.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:979.1-983.36 + ;; 6-typing.watsup:978.1-982.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:985.1-989.36 + ;; 6-typing.watsup:984.1-988.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:991.1-993.24 + ;; 6-typing.watsup:990.1-992.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:998.1-1000.23 + ;; 6-typing.watsup:997.1-999.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:1002.1-1004.23 + ;; 6-typing.watsup:1001.1-1003.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:1006.1-1008.23 + ;; 6-typing.watsup:1005.1-1007.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:1010.1-1013.27 + ;; 6-typing.watsup:1009.1-1012.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:1015.1-1018.24 + ;; 6-typing.watsup:1014.1-1017.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:1020.1-1022.24 + ;; 6-typing.watsup:1019.1-1021.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:1033.1-1036.43 + ;; 6-typing.watsup:1032.1-1035.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:1038.1-1041.35 + ;; 6-typing.watsup:1037.1-1040.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:1052.1-1055.43 + ;; 6-typing.watsup:1051.1-1054.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:1057.1-1060.35 + ;; 6-typing.watsup:1056.1-1059.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:1062.1-1065.46 + ;; 6-typing.watsup:1061.1-1064.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:1067.1-1070.39 + ;; 6-typing.watsup:1066.1-1069.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:1072.1-1075.35 + ;; 6-typing.watsup:1071.1-1074.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:1077.1-1080.35 + ;; 6-typing.watsup:1076.1-1079.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:1082.1-1086.21 + ;; 6-typing.watsup:1081.1-1085.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:1088.1-1091.46 + ;; 6-typing.watsup:1087.1-1090.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:1093.1-1097.21 + ;; 6-typing.watsup:1092.1-1096.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) @@ -4899,13 +4899,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1289.1-1289.100 +;; 6-typing.watsup:1288.1-1288.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1331.1-1332.17 + ;; 6-typing.watsup:1330.1-1331.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1334.1-1337.54 + ;; 6-typing.watsup:1333.1-1336.54 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -4915,13 +4915,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1288.1-1288.98 +;; 6-typing.watsup:1287.1-1287.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1323.1-1324.17 + ;; 6-typing.watsup:1322.1-1323.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1326.1-1329.49 + ;; 6-typing.watsup:1325.1-1328.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 : deftype} :: dt*{dt : deftype}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index cc2bf4f811..5a25156c7c 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -2249,7 +2249,7 @@ $$ &&&&\qquad {\land}~{{\mathit{sx}}^?} \neq \epsilon \Leftrightarrow {\mathrm{lanetype}}({\mathit{shape}}_1) = {{\mathsf{i}}{N}}_1 \land {\mathrm{lanetype}}({\mathit{shape}}_2) = {{\mathsf{i}}{N}}_2 \land N_1 > N_2 \\ &&|& {\mathit{shape}}{.}\mathsf{splat} \\ &&|& {{\mathit{shape}}{.}\mathsf{extract\_lane}}{\mathsf{\_}}{{{\mathit{sx}}^?}}~{\mathit{laneidx}} - &\qquad \mbox{if}~{\mathrm{lanetype}}({\mathit{shape}}) = {\mathit{numtype}} \Leftrightarrow {{\mathit{sx}}^?} = \epsilon \\ &&|& + &\qquad \mbox{if}~{{\mathit{sx}}^?} = \epsilon \Leftrightarrow {\mathrm{lanetype}}({\mathit{shape}}) = {\mathit{numtype}} \\ &&|& {\mathit{shape}}{.}\mathsf{replace\_lane}~{\mathit{laneidx}} \\ &&|& \mathsf{ref{.}null}~{\mathit{heaptype}} \\ &&|& \mathsf{ref{.}is\_null} \\ &&|& diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index c5677bd33c..2a4d118de2 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -1175,7 +1175,7 @@ syntax instr = -- if ((sx?{sx : sx} =/= ?()) <=> ((($lanetype(shape_1) = (Jnn_1 : Jnn <: lanetype)) /\ ($lanetype(shape_2) = (Jnn_2 : Jnn <: lanetype))) /\ ($lsizenn1((Jnn_1 : Jnn <: lanetype)) > $lsizenn2((Jnn_2 : Jnn <: lanetype))))) | VSPLAT{shape : shape}(shape : shape) | VEXTRACT_LANE{shape : shape, sx? : sx?, laneidx : laneidx, numtype : numtype}(shape : shape, sx?{sx : sx} : sx?, laneidx : laneidx) - -- if (($lanetype(shape) = (numtype : numtype <: lanetype)) <=> (sx?{sx : sx} = ?())) + -- if ((sx?{sx : sx} = ?()) <=> ($lanetype(shape) = (numtype : numtype <: lanetype))) | VREPLACE_LANE{shape : shape, laneidx : laneidx}(shape : shape, laneidx : laneidx) | REF.NULL{heaptype : heaptype}(heaptype : heaptype) | REF.IS_NULL @@ -4438,195 +4438,195 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:910.1-912.21 + ;; 6-typing.watsup:909.1-911.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:914.1-916.21 + ;; 6-typing.watsup:913.1-915.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:918.1-919.50 + ;; 6-typing.watsup:917.1-918.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:921.1-922.57 + ;; 6-typing.watsup:920.1-921.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:924.1-925.48 + ;; 6-typing.watsup:923.1-924.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:927.1-928.62 + ;; 6-typing.watsup:926.1-927.62 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop_(sh_2, sh_1), half? : half_(sh_2, sh_1)?, sx? : sx?, zero? : zero_(sh_2, sh_1)?}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop, half?{half : half_(sh_2, sh_1)}, sx?{sx : sx}, zero?{zero : zero_(sh_2, sh_1)}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:933.1-935.28 + ;; 6-typing.watsup:932.1-934.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:937.1-939.29 + ;; 6-typing.watsup:936.1-938.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:941.1-943.29 + ;; 6-typing.watsup:940.1-942.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:948.1-950.29 + ;; 6-typing.watsup:947.1-949.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:952.1-954.29 + ;; 6-typing.watsup:951.1-953.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:959.1-961.29 + ;; 6-typing.watsup:958.1-960.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:963.1-965.29 + ;; 6-typing.watsup:962.1-964.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:967.1-969.29 + ;; 6-typing.watsup:966.1-968.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:971.1-973.29 + ;; 6-typing.watsup:970.1-972.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:975.1-977.29 + ;; 6-typing.watsup:974.1-976.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:979.1-983.36 + ;; 6-typing.watsup:978.1-982.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:985.1-989.36 + ;; 6-typing.watsup:984.1-988.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:991.1-993.24 + ;; 6-typing.watsup:990.1-992.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:998.1-1000.23 + ;; 6-typing.watsup:997.1-999.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:1002.1-1004.23 + ;; 6-typing.watsup:1001.1-1003.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:1006.1-1008.23 + ;; 6-typing.watsup:1005.1-1007.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:1010.1-1013.27 + ;; 6-typing.watsup:1009.1-1012.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:1015.1-1018.24 + ;; 6-typing.watsup:1014.1-1017.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:1020.1-1022.24 + ;; 6-typing.watsup:1019.1-1021.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:1033.1-1036.43 + ;; 6-typing.watsup:1032.1-1035.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:1038.1-1041.35 + ;; 6-typing.watsup:1037.1-1040.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:1052.1-1055.43 + ;; 6-typing.watsup:1051.1-1054.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:1057.1-1060.35 + ;; 6-typing.watsup:1056.1-1059.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:1062.1-1065.46 + ;; 6-typing.watsup:1061.1-1064.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:1067.1-1070.39 + ;; 6-typing.watsup:1066.1-1069.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:1072.1-1075.35 + ;; 6-typing.watsup:1071.1-1074.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:1077.1-1080.35 + ;; 6-typing.watsup:1076.1-1079.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:1082.1-1086.21 + ;; 6-typing.watsup:1081.1-1085.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:1088.1-1091.46 + ;; 6-typing.watsup:1087.1-1090.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:1093.1-1097.21 + ;; 6-typing.watsup:1092.1-1096.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) @@ -4889,13 +4889,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1289.1-1289.100 +;; 6-typing.watsup:1288.1-1288.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1331.1-1332.17 + ;; 6-typing.watsup:1330.1-1331.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1334.1-1337.54 + ;; 6-typing.watsup:1333.1-1336.54 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -4905,13 +4905,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1288.1-1288.98 +;; 6-typing.watsup:1287.1-1287.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1323.1-1324.17 + ;; 6-typing.watsup:1322.1-1323.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1326.1-1329.49 + ;; 6-typing.watsup:1325.1-1328.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 : deftype} :: dt*{dt : deftype}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) @@ -7614,7 +7614,7 @@ syntax instr = -- if ((sx?{sx : sx} =/= ?()) <=> ((($lanetype(shape_1) = (Jnn_1 : Jnn <: lanetype)) /\ ($lanetype(shape_2) = (Jnn_2 : Jnn <: lanetype))) /\ ($lsizenn1((Jnn_1 : Jnn <: lanetype)) > $lsizenn2((Jnn_2 : Jnn <: lanetype))))) | VSPLAT{shape : shape}(shape : shape) | VEXTRACT_LANE{shape : shape, sx? : sx?, laneidx : laneidx, numtype : numtype}(shape : shape, sx?{sx : sx} : sx?, laneidx : laneidx) - -- if (($lanetype(shape) = (numtype : numtype <: lanetype)) <=> (sx?{sx : sx} = ?())) + -- if ((sx?{sx : sx} = ?()) <=> ($lanetype(shape) = (numtype : numtype <: lanetype))) | VREPLACE_LANE{shape : shape, laneidx : laneidx}(shape : shape, laneidx : laneidx) | REF.NULL{heaptype : heaptype}(heaptype : heaptype) | REF.IS_NULL @@ -10882,195 +10882,195 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:910.1-912.21 + ;; 6-typing.watsup:909.1-911.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:914.1-916.21 + ;; 6-typing.watsup:913.1-915.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:918.1-919.50 + ;; 6-typing.watsup:917.1-918.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:921.1-922.57 + ;; 6-typing.watsup:920.1-921.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:924.1-925.48 + ;; 6-typing.watsup:923.1-924.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:927.1-928.62 + ;; 6-typing.watsup:926.1-927.62 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop_(sh_2, sh_1), half? : half_(sh_2, sh_1)?, sx? : sx?, zero? : zero_(sh_2, sh_1)?}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop, half?{half : half_(sh_2, sh_1)}, sx?{sx : sx}, zero?{zero : zero_(sh_2, sh_1)}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:933.1-935.28 + ;; 6-typing.watsup:932.1-934.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:937.1-939.29 + ;; 6-typing.watsup:936.1-938.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:941.1-943.29 + ;; 6-typing.watsup:940.1-942.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:948.1-950.29 + ;; 6-typing.watsup:947.1-949.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:952.1-954.29 + ;; 6-typing.watsup:951.1-953.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:959.1-961.29 + ;; 6-typing.watsup:958.1-960.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:963.1-965.29 + ;; 6-typing.watsup:962.1-964.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:967.1-969.29 + ;; 6-typing.watsup:966.1-968.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:971.1-973.29 + ;; 6-typing.watsup:970.1-972.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:975.1-977.29 + ;; 6-typing.watsup:974.1-976.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:979.1-983.36 + ;; 6-typing.watsup:978.1-982.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:985.1-989.36 + ;; 6-typing.watsup:984.1-988.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:991.1-993.24 + ;; 6-typing.watsup:990.1-992.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:998.1-1000.23 + ;; 6-typing.watsup:997.1-999.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:1002.1-1004.23 + ;; 6-typing.watsup:1001.1-1003.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:1006.1-1008.23 + ;; 6-typing.watsup:1005.1-1007.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:1010.1-1013.27 + ;; 6-typing.watsup:1009.1-1012.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:1015.1-1018.24 + ;; 6-typing.watsup:1014.1-1017.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:1020.1-1022.24 + ;; 6-typing.watsup:1019.1-1021.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:1033.1-1036.43 + ;; 6-typing.watsup:1032.1-1035.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:1038.1-1041.35 + ;; 6-typing.watsup:1037.1-1040.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:1052.1-1055.43 + ;; 6-typing.watsup:1051.1-1054.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:1057.1-1060.35 + ;; 6-typing.watsup:1056.1-1059.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:1062.1-1065.46 + ;; 6-typing.watsup:1061.1-1064.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:1067.1-1070.39 + ;; 6-typing.watsup:1066.1-1069.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:1072.1-1075.35 + ;; 6-typing.watsup:1071.1-1074.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:1077.1-1080.35 + ;; 6-typing.watsup:1076.1-1079.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:1082.1-1086.21 + ;; 6-typing.watsup:1081.1-1085.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:1088.1-1091.46 + ;; 6-typing.watsup:1087.1-1090.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:1093.1-1097.21 + ;; 6-typing.watsup:1092.1-1096.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) @@ -11333,13 +11333,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1289.1-1289.100 +;; 6-typing.watsup:1288.1-1288.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1331.1-1332.17 + ;; 6-typing.watsup:1330.1-1331.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1334.1-1337.54 + ;; 6-typing.watsup:1333.1-1336.54 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -11349,13 +11349,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1288.1-1288.98 +;; 6-typing.watsup:1287.1-1287.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1323.1-1324.17 + ;; 6-typing.watsup:1322.1-1323.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1326.1-1329.49 + ;; 6-typing.watsup:1325.1-1328.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 : deftype} :: dt*{dt : deftype}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) @@ -14058,7 +14058,7 @@ syntax instr = -- if ((sx?{sx : sx} =/= ?()) <=> ((($lanetype(shape_1) = (Jnn_1 : Jnn <: lanetype)) /\ ($lanetype(shape_2) = (Jnn_2 : Jnn <: lanetype))) /\ ($lsizenn1((Jnn_1 : Jnn <: lanetype)) > $lsizenn2((Jnn_2 : Jnn <: lanetype))))) | VSPLAT{shape : shape}(shape : shape) | VEXTRACT_LANE{shape : shape, sx? : sx?, laneidx : laneidx, numtype : numtype}(shape : shape, sx?{sx : sx} : sx?, laneidx : laneidx) - -- if (($lanetype(shape) = (numtype : numtype <: lanetype)) <=> (sx?{sx : sx} = ?())) + -- if ((sx?{sx : sx} = ?()) <=> ($lanetype(shape) = (numtype : numtype <: lanetype))) | VREPLACE_LANE{shape : shape, laneidx : laneidx}(shape : shape, laneidx : laneidx) | REF.NULL{heaptype : heaptype}(heaptype : heaptype) | REF.IS_NULL @@ -17326,195 +17326,195 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:910.1-912.21 + ;; 6-typing.watsup:909.1-911.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:914.1-916.21 + ;; 6-typing.watsup:913.1-915.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:918.1-919.50 + ;; 6-typing.watsup:917.1-918.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:921.1-922.57 + ;; 6-typing.watsup:920.1-921.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:924.1-925.48 + ;; 6-typing.watsup:923.1-924.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:927.1-928.62 + ;; 6-typing.watsup:926.1-927.62 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop_(sh_2, sh_1), half? : half_(sh_2, sh_1)?, sx? : sx?, zero? : zero_(sh_2, sh_1)?}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop, half?{half : half_(sh_2, sh_1)}, sx?{sx : sx}, zero?{zero : zero_(sh_2, sh_1)}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:933.1-935.28 + ;; 6-typing.watsup:932.1-934.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:937.1-939.29 + ;; 6-typing.watsup:936.1-938.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:941.1-943.29 + ;; 6-typing.watsup:940.1-942.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:948.1-950.29 + ;; 6-typing.watsup:947.1-949.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:952.1-954.29 + ;; 6-typing.watsup:951.1-953.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:959.1-961.29 + ;; 6-typing.watsup:958.1-960.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:963.1-965.29 + ;; 6-typing.watsup:962.1-964.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:967.1-969.29 + ;; 6-typing.watsup:966.1-968.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:971.1-973.29 + ;; 6-typing.watsup:970.1-972.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:975.1-977.29 + ;; 6-typing.watsup:974.1-976.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:979.1-983.36 + ;; 6-typing.watsup:978.1-982.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:985.1-989.36 + ;; 6-typing.watsup:984.1-988.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:991.1-993.24 + ;; 6-typing.watsup:990.1-992.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:998.1-1000.23 + ;; 6-typing.watsup:997.1-999.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:1002.1-1004.23 + ;; 6-typing.watsup:1001.1-1003.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:1006.1-1008.23 + ;; 6-typing.watsup:1005.1-1007.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:1010.1-1013.27 + ;; 6-typing.watsup:1009.1-1012.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:1015.1-1018.24 + ;; 6-typing.watsup:1014.1-1017.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:1020.1-1022.24 + ;; 6-typing.watsup:1019.1-1021.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:1033.1-1036.43 + ;; 6-typing.watsup:1032.1-1035.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:1038.1-1041.35 + ;; 6-typing.watsup:1037.1-1040.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:1052.1-1055.43 + ;; 6-typing.watsup:1051.1-1054.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:1057.1-1060.35 + ;; 6-typing.watsup:1056.1-1059.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:1062.1-1065.46 + ;; 6-typing.watsup:1061.1-1064.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:1067.1-1070.39 + ;; 6-typing.watsup:1066.1-1069.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:1072.1-1075.35 + ;; 6-typing.watsup:1071.1-1074.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:1077.1-1080.35 + ;; 6-typing.watsup:1076.1-1079.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:1082.1-1086.21 + ;; 6-typing.watsup:1081.1-1085.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:1088.1-1091.46 + ;; 6-typing.watsup:1087.1-1090.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:1093.1-1097.21 + ;; 6-typing.watsup:1092.1-1096.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) @@ -17777,13 +17777,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1289.1-1289.100 +;; 6-typing.watsup:1288.1-1288.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1331.1-1332.17 + ;; 6-typing.watsup:1330.1-1331.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1334.1-1337.54 + ;; 6-typing.watsup:1333.1-1336.54 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -17793,13 +17793,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1288.1-1288.98 +;; 6-typing.watsup:1287.1-1287.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1323.1-1324.17 + ;; 6-typing.watsup:1322.1-1323.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1326.1-1329.49 + ;; 6-typing.watsup:1325.1-1328.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 : deftype} :: dt*{dt : deftype}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) @@ -20502,7 +20502,7 @@ syntax instr = -- if ((sx?{sx : sx} =/= ?()) <=> ((($lanetype(shape_1) = (Jnn_1 : Jnn <: lanetype)) /\ ($lanetype(shape_2) = (Jnn_2 : Jnn <: lanetype))) /\ ($lsizenn1((Jnn_1 : Jnn <: lanetype)) > $lsizenn2((Jnn_2 : Jnn <: lanetype))))) | VSPLAT{shape : shape}(shape : shape) | VEXTRACT_LANE{shape : shape, sx? : sx?, laneidx : laneidx, numtype : numtype}(shape : shape, sx?{sx : sx} : sx?, laneidx : laneidx) - -- if (($lanetype(shape) = (numtype : numtype <: lanetype)) <=> (sx?{sx : sx} = ?())) + -- if ((sx?{sx : sx} = ?()) <=> ($lanetype(shape) = (numtype : numtype <: lanetype))) | VREPLACE_LANE{shape : shape, laneidx : laneidx}(shape : shape, laneidx : laneidx) | REF.NULL{heaptype : heaptype}(heaptype : heaptype) | REF.IS_NULL @@ -23832,93 +23832,93 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:910.1-912.21 + ;; 6-typing.watsup:909.1-911.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:914.1-916.21 + ;; 6-typing.watsup:913.1-915.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:918.1-919.50 + ;; 6-typing.watsup:917.1-918.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:921.1-922.57 + ;; 6-typing.watsup:920.1-921.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:924.1-925.48 + ;; 6-typing.watsup:923.1-924.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:927.1-928.62 + ;; 6-typing.watsup:926.1-927.62 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop_(sh_2, sh_1), half? : half_(sh_2, sh_1)?, sx? : sx?, zero? : zero_(sh_2, sh_1)?}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop, half?{half : half_(sh_2, sh_1)}, sx?{sx : sx}, zero?{zero : zero_(sh_2, sh_1)}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; 6-typing.watsup:933.1-935.28 + ;; 6-typing.watsup:932.1-934.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:937.1-939.29 + ;; 6-typing.watsup:936.1-938.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:941.1-943.29 + ;; 6-typing.watsup:940.1-942.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:948.1-950.29 + ;; 6-typing.watsup:947.1-949.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:952.1-954.29 + ;; 6-typing.watsup:951.1-953.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:959.1-961.29 + ;; 6-typing.watsup:958.1-960.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:963.1-965.29 + ;; 6-typing.watsup:962.1-964.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:967.1-969.29 + ;; 6-typing.watsup:966.1-968.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:971.1-973.29 + ;; 6-typing.watsup:970.1-972.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:975.1-977.29 + ;; 6-typing.watsup:974.1-976.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:979.1-983.36 + ;; 6-typing.watsup:978.1-982.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|) @@ -23927,7 +23927,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:985.1-989.36 + ;; 6-typing.watsup:984.1-988.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|) @@ -23936,31 +23936,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:991.1-993.24 + ;; 6-typing.watsup:990.1-992.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:998.1-1000.23 + ;; 6-typing.watsup:997.1-999.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:1002.1-1004.23 + ;; 6-typing.watsup:1001.1-1003.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:1006.1-1008.23 + ;; 6-typing.watsup:1005.1-1007.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:1010.1-1013.27 + ;; 6-typing.watsup:1009.1-1012.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|) @@ -23968,7 +23968,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:1015.1-1018.24 + ;; 6-typing.watsup:1014.1-1017.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|) @@ -23976,69 +23976,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:1020.1-1022.24 + ;; 6-typing.watsup:1019.1-1021.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:1033.1-1036.43 + ;; 6-typing.watsup:1032.1-1035.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:1038.1-1041.35 + ;; 6-typing.watsup:1037.1-1040.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:1052.1-1055.43 + ;; 6-typing.watsup:1051.1-1054.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:1057.1-1060.35 + ;; 6-typing.watsup:1056.1-1059.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:1062.1-1065.46 + ;; 6-typing.watsup:1061.1-1064.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:1067.1-1070.39 + ;; 6-typing.watsup:1066.1-1069.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:1072.1-1075.35 + ;; 6-typing.watsup:1071.1-1074.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:1077.1-1080.35 + ;; 6-typing.watsup:1076.1-1079.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:1082.1-1086.21 + ;; 6-typing.watsup:1081.1-1085.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|) @@ -24046,14 +24046,14 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8)) -- if (i < (128 / N)) - ;; 6-typing.watsup:1088.1-1091.46 + ;; 6-typing.watsup:1087.1-1090.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:1093.1-1097.21 + ;; 6-typing.watsup:1092.1-1096.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|) @@ -24330,13 +24330,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1289.1-1289.100 +;; 6-typing.watsup:1288.1-1288.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; 6-typing.watsup:1331.1-1332.17 + ;; 6-typing.watsup:1330.1-1331.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1334.1-1337.54 + ;; 6-typing.watsup:1333.1-1336.54 rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}: `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype}) -- Global_ok: `%|-%:%`(C, global, gt_1) @@ -24346,13 +24346,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; 6-typing.watsup rec { -;; 6-typing.watsup:1288.1-1288.98 +;; 6-typing.watsup:1287.1-1287.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; 6-typing.watsup:1323.1-1324.17 + ;; 6-typing.watsup:1322.1-1323.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; 6-typing.watsup:1326.1-1329.49 + ;; 6-typing.watsup:1325.1-1328.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 : deftype} :: dt*{dt : deftype}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype}) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 7827b1897c..e71cb80778 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -4141,7 +4141,7 @@ watsup 0.4 generator 6-typing.watsup:194.10-194.32: if_expr_to_instrs: Yet `$before(typeuse, x, i)` 6-typing.watsup:817.9-817.55: if_expr_to_instrs: Yet `(($unpack(zt) = (numtype : numtype <: valtype)) \/ ($unpack(zt) = (vectype : vectype <: valtype)))` 6-typing.watsup:851.9-851.55: if_expr_to_instrs: Yet `(($unpack(zt) = (numtype : numtype <: valtype)) \/ ($unpack(zt) = (vectype : vectype <: valtype)))` -6-typing.watsup:1310.9-1310.30: if_expr_to_instrs: Yet `$disjoint_(syntax name, nm*{nm : name})` +6-typing.watsup:1309.9-1309.30: if_expr_to_instrs: Yet `$disjoint_(syntax name, nm*{nm : name})` ================= Generated prose ================= diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 5e4270b86a..d1b13552a7 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -12,7 +12,7 @@ $ (../src/exe-watsup/main.exe ../spec/wasm-3.0/*.watsup -l --splice-latex -p spe ../spec/wasm-3.0/6-typing.watsup:194.10-194.32: if_expr_to_instrs: Yet `$before(typeuse, x, i)` ../spec/wasm-3.0/6-typing.watsup:817.9-817.55: if_expr_to_instrs: Yet `(($unpack(zt) = (numtype : numtype <: valtype)) \/ ($unpack(zt) = (vectype : vectype <: valtype)))` ../spec/wasm-3.0/6-typing.watsup:851.9-851.55: if_expr_to_instrs: Yet `(($unpack(zt) = (numtype : numtype <: valtype)) \/ ($unpack(zt) = (vectype : vectype <: valtype)))` -../spec/wasm-3.0/6-typing.watsup:1310.9-1310.30: if_expr_to_instrs: Yet `$disjoint_(syntax name, nm*{nm : name})` +../spec/wasm-3.0/6-typing.watsup:1309.9-1309.30: if_expr_to_instrs: Yet `$disjoint_(syntax name, nm*{nm : name})` == Splicing... \documentclass[a4paper]{scrartcl}