diff --git a/spectec/src/backend-prose/dune b/spectec/src/backend-prose/dune index a77e425d0a..557480b148 100644 --- a/spectec/src/backend-prose/dune +++ b/spectec/src/backend-prose/dune @@ -8,5 +8,6 @@ gen render macro - langs) + langs + eq) ) diff --git a/spectec/src/backend-prose/eq.ml b/spectec/src/backend-prose/eq.ml new file mode 100644 index 0000000000..60c39e6690 --- /dev/null +++ b/spectec/src/backend-prose/eq.ml @@ -0,0 +1,43 @@ +open Prose + +let eq_list eq l1 l2 = + List.length l1 = List.length l2 + && List.for_all2 eq l1 l2 + +let eq_cmpop = (=) + +let eq_expr = Al.Eq.eq_expr + +let rec eq_instr i1 i2 = + match (i1, i2) with + | LetI (e11, e12), LetI (e21, e22) -> + eq_expr e11 e21 + && eq_expr e12 e22 + | CmpI (e11, cmp1, e12), CmpI (e21, cmp2, e22) -> + eq_expr e11 e21 + && eq_cmpop cmp1 cmp2 + && eq_expr e12 e22 + | MemI (e11, e12), MemI (e21, e22) -> + eq_expr e11 e21 && eq_expr e12 e22 + | IsValidI (opt1, e11, l1), IsValidI (opt2, e21, l2) -> + Option.equal eq_expr opt1 opt2 + && eq_expr e11 e21 + && eq_list eq_expr l1 l2 + | MatchesI (e11, e12), MatchesI (e21, e22) -> + eq_expr e11 e21 + && eq_expr e12 e22 + | IsConstI (opt1, e11), IsConstI (opt2, e21) -> + Option.equal eq_expr opt1 opt2 + && eq_expr e11 e21 + | IfI (e11, il1), IfI (e21, il2) -> + eq_expr e11 e21 + && List.for_all2 eq_instr il1 il2 + | ForallI (l1, il1), ForallI (l2, il2) -> + eq_list (fun (e11, e12) (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22) l1 l2 + && eq_list eq_instr il1 il2 + | EquivI (e11, e12), EquivI (e21, e22) -> + eq_expr e11 e21 + && eq_expr e12 e22 + | EitherI (il1), EitherI (il2) -> + eq_list (fun l1 l2 -> eq_list eq_instr l1 l2) il1 il2 + | _, _ -> i1 = i2 diff --git a/spectec/src/backend-prose/eq.mli b/spectec/src/backend-prose/eq.mli new file mode 100644 index 0000000000..b77fb70273 --- /dev/null +++ b/spectec/src/backend-prose/eq.mli @@ -0,0 +1,3 @@ +open Prose + +val eq_instr : instr -> instr -> bool diff --git a/spectec/src/backend-prose/gen.ml b/spectec/src/backend-prose/gen.ml index 78f5d873e2..ef8b348e87 100644 --- a/spectec/src/backend-prose/gen.ml +++ b/spectec/src/backend-prose/gen.ml @@ -1,4 +1,6 @@ open Prose +open Eq + open Il open Al.Al_util open Il2al.Translate @@ -467,6 +469,46 @@ let prose_of_rel rel = match get_rel_kind rel with let prose_of_rels = List.concat_map prose_of_rel +(** Postprocess of generated prose **) +let unify_either instrs = + let f instr = + match instr with + | EitherI iss -> + let unified, bodies = List.fold_left (fun (commons, instrss) i -> + let pairs = List.map (List.partition (eq_instr i)) instrss in + let fsts = List.map fst pairs in + let snds = List.map snd pairs in + if List.for_all (fun l -> List.length l = 1) fsts then + i :: commons, snds + else + commons, instrss + ) ([], iss) (List.hd iss) in + let unified = List.rev unified in + unified @ [ EitherI bodies ] + | _ -> [instr] + in + let rec walk instrs = List.concat_map walk' instrs + and walk' instr = + f instr + |> List.map (function + | IfI (e, il) -> IfI (e, walk il) + | ForallI (vars, il) -> ForallI (vars, walk il) + | EitherI ill -> EitherI (List.map walk ill) + | i -> i + ) + in + walk instrs + +let postprocess_prose defs = + List.map (fun def -> + match def with + | Iff (anchor, e, i, il) -> + let new_il = unify_either il in + Iff (anchor, e, i, new_il) + | Algo _ -> def + ) defs + + (** Entry for generating validation prose **) let gen_validation_prose () = prose_of_rels !Langs.il @@ -494,6 +536,7 @@ let gen_prose el il al = let execution_prose = gen_execution_prose () in validation_prose @ execution_prose + |> postprocess_prose (** Main entry for generating stringified prose **) let gen_string cfg_latex cfg_prose el il al = diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 2ef924dd28..b055b5aba5 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -4809,13 +4809,13 @@ watsup 0.4 generator * :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~{\mathit{vloadop}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}~{\mathit{memarg}})` is valid with type :math:`(\mathsf{i{\scriptstyle 32}}~\rightarrow~\mathsf{v{\scriptstyle 128}})` if and only if: - * Either: + * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`0`. - * :math:`{\mathit{vloadop}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` must be equal to :math:`({M}{\mathsf{x}}{\mathsf{x}}{\mathsf{\_}}{N})`. + * :math:`C{.}\mathsf{mems}{}[0]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`0`. + * Either: - * :math:`C{.}\mathsf{mems}{}[0]` must be equal to :math:`{\mathit{mt}}`. + * :math:`{\mathit{vloadop}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` must be equal to :math:`({M}{\mathsf{x}}{\mathsf{x}}{\mathsf{\_}}{N})`. * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`M / 8 \cdot N`. @@ -4823,18 +4823,10 @@ watsup 0.4 generator * :math:`{\mathit{vloadop}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` must be equal to :math:`({n}{\mathsf{\_}}{\mathsf{splat}})`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`0`. - - * :math:`C{.}\mathsf{mems}{}[0]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`n / 8`. * Or: * :math:`{\mathit{vloadop}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` must be equal to :math:`({n}{\mathsf{\_}}{\mathsf{zero}})`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`0`. - - * :math:`C{.}\mathsf{mems}{}[0]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`n / 8`. @@ -10027,20 +10019,16 @@ Instr_ok/store Instr_ok/vload - the instr (VLOAD V128 ?(vloadop_u0) memarg) is valid with the function type ([I32] -> [V128]) if and only if: + - |C.MEMS| is greater than 0. + - C.MEMS[0] is mt. - Either: - vloadop_u0 is (SHAPE M X N sx). - - |C.MEMS| is greater than 0. - - C.MEMS[0] is mt. - (2 ^ memarg.ALIGN) is less than or equal to ((M / 8) · N). - Or: - vloadop_u0 is (SPLAT n). - - |C.MEMS| is greater than 0. - - C.MEMS[0] is mt. - (2 ^ memarg.ALIGN) is less than or equal to (n / 8). - Or: - vloadop_u0 is (ZERO n). - - |C.MEMS| is greater than 0. - - C.MEMS[0] is mt. - (2 ^ memarg.ALIGN) is less than or equal to (n / 8). Instr_ok/vload_lane @@ -12655,22 +12643,20 @@ watsup 0.4 generator * :math:`(\mathsf{ref}~(\mathsf{null}~{{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}~{}^?)~{\mathit{ht}}_1)` matches :math:`(\mathsf{ref}~(\mathsf{null}~{{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}~{}^?)~{\mathit{ht}}_2)` if and only if: + * :math:`{\mathit{ht}}_1` matches :math:`{\mathit{ht}}_2`. + * Either: * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`\epsilon`. * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}` must be equal to :math:`\epsilon`. - * :math:`{\mathit{ht}}_1` matches :math:`{\mathit{ht}}_2`. - * Or: * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`{()^?}`. * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}` must be equal to :math:`()`. - * :math:`{\mathit{ht}}_1` matches :math:`{\mathit{ht}}_2`. - * :math:`{\mathit{vectype}}` matches :math:`{\mathit{vectype}}`. @@ -12728,22 +12714,20 @@ watsup 0.4 generator * :math:`((\mathsf{mut}~{{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}~{}^?), {\mathit{zt}}_1)` matches :math:`((\mathsf{mut}~{{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}~{}^?), {\mathit{zt}}_2)` if and only if: + * :math:`{\mathit{zt}}_1` matches :math:`{\mathit{zt}}_2`. + * Either: * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`\epsilon`. * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}` must be equal to :math:`\epsilon`. - * :math:`{\mathit{zt}}_1` matches :math:`{\mathit{zt}}_2`. - * Or: * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`()`. * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}` must be equal to :math:`()`. - * :math:`{\mathit{zt}}_1` matches :math:`{\mathit{zt}}_2`. - * :math:`{\mathit{zt}}_2` matches :math:`{\mathit{zt}}_1`. @@ -12990,22 +12974,20 @@ watsup 0.4 generator * :math:`((\mathsf{mut}~{{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}~{}^?), {\mathit{valtype}}_1)` matches :math:`((\mathsf{mut}~{{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}~{}^?), {\mathit{valtype}}_2)` if and only if: + * :math:`{\mathit{valtype}}_1` matches :math:`{\mathit{valtype}}_2`. + * Either: * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`\epsilon`. * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}` must be equal to :math:`\epsilon`. - * :math:`{\mathit{valtype}}_1` matches :math:`{\mathit{valtype}}_2`. - * Or: * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`()`. * :math:`{{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}` must be equal to :math:`()`. - * :math:`{\mathit{valtype}}_1` matches :math:`{\mathit{valtype}}_2`. - * :math:`{\mathit{valtype}}_2` matches :math:`{\mathit{valtype}}_1`. @@ -13102,14 +13084,14 @@ watsup 0.4 generator * :math:`{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is valid if and only if: + * :math:`{|C{.}\mathsf{labels}|}` must be greater than :math:`l`. + * Either: * :math:`{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` must be equal to :math:`(\mathsf{catch}~x~l)`. * :math:`{|C{.}\mathsf{tags}|}` must be greater than :math:`x`. - * :math:`{|C{.}\mathsf{labels}|}` must be greater than :math:`l`. - * :math:`{\mathrm{expand}}(C{.}\mathsf{tags}{}[x])` must be equal to :math:`(\mathsf{func}~({t^\ast}~\rightarrow~\epsilon))`. * :math:`{t^\ast}` matches :math:`C{.}\mathsf{labels}{}[l]`. @@ -13120,22 +13102,16 @@ watsup 0.4 generator * :math:`{|C{.}\mathsf{tags}|}` must be greater than :math:`x`. - * :math:`{|C{.}\mathsf{labels}|}` must be greater than :math:`l`. - * :math:`{\mathrm{expand}}(C{.}\mathsf{tags}{}[x])` must be equal to :math:`(\mathsf{func}~({t^\ast}~\rightarrow~\epsilon))`. * :math:`{t^\ast}~(\mathsf{ref}~(\mathsf{null}~\epsilon~{}^?)~\mathsf{exn})` matches :math:`C{.}\mathsf{labels}{}[l]`. * Or: * :math:`{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` must be equal to :math:`(\mathsf{catch\_all}~l)`. - * :math:`{|C{.}\mathsf{labels}|}` must be greater than :math:`l`. - * :math:`\epsilon` matches :math:`C{.}\mathsf{labels}{}[l]`. * Or: * :math:`{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` must be equal to :math:`(\mathsf{catch\_all\_ref}~l)`. - * :math:`{|C{.}\mathsf{labels}|}` must be greater than :math:`l`. - * :math:`(\mathsf{ref}~(\mathsf{null}~\epsilon~{}^?)~\mathsf{exn})` matches :math:`C{.}\mathsf{labels}{}[l]`. @@ -13157,18 +13133,16 @@ watsup 0.4 generator * :math:`({{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}~{}^?)` is valid with type :math:`(t~t~\mathsf{i{\scriptstyle 32}}~{\rightarrow}_{\epsilon}\,t)` if and only if: + * :math:`t` is valid. + * Either: * :math:`{{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`t`. - * :math:`t` is valid. - * Or: * :math:`{{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`\epsilon`. - * :math:`t` is valid. - * :math:`t` matches :math:`{t'}`. * Either: @@ -13925,6 +13899,10 @@ watsup 0.4 generator * :math:`({{\mathit{numtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}{.}\mathsf{load}}{{{\mathit{loadop\_u{\kern-0.1em\scriptstyle 2}}}^?}}~x~{\mathit{memarg}})` is valid with type :math:`(\mathsf{i{\scriptstyle 32}}~{\rightarrow}_{\epsilon}\,{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 3}}})` if and only if: + * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. + + * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. + * Either: * :math:`{\mathit{numtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` must be equal to :math:`{\mathit{nt}}`. @@ -13933,10 +13911,6 @@ watsup 0.4 generator * :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 3}}}` must be equal to :math:`{\mathit{nt}}`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. - - * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`{|{\mathit{nt}}|} / 8`. * Or: @@ -13947,16 +13921,16 @@ watsup 0.4 generator * :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 3}}}` must be equal to :math:`{\mathsf{i}}{N}`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. - - * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`M / 8`. * :math:`({{\mathit{numtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}{.}\mathsf{store}}{{{\mathit{sz}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}}~x~{\mathit{memarg}})` is valid with type :math:`(\mathsf{i{\scriptstyle 32}}~{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}~{\rightarrow}_{\epsilon}\,\epsilon)` if and only if: + * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. + + * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. + * Either: * :math:`{\mathit{numtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` must be equal to :math:`{\mathit{nt}}`. @@ -13965,10 +13939,6 @@ watsup 0.4 generator * :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` must be equal to :math:`{\mathit{nt}}`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. - - * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`{|{\mathit{nt}}|} / 8`. * Or: @@ -13979,23 +13949,19 @@ watsup 0.4 generator * :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` must be equal to :math:`{\mathsf{i}}{N}`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. - - * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`M / 8`. * :math:`({\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}}{{{\mathit{vloadop\_u{\kern-0.1em\scriptstyle 0}}}^?}}~x~{\mathit{memarg}})` is valid with type :math:`(\mathsf{i{\scriptstyle 32}}~{\rightarrow}_{\epsilon}\,\mathsf{v{\scriptstyle 128}})` if and only if: - * Either: + * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. - * :math:`{{\mathit{vloadop\_u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`\epsilon`. + * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. + * Either: - * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. + * :math:`{{\mathit{vloadop\_u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`\epsilon`. * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`{|\mathsf{v{\scriptstyle 128}}|} / 8`. @@ -14003,26 +13969,14 @@ watsup 0.4 generator * :math:`{{\mathit{vloadop\_u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`({M}{\mathsf{x}}{N}{\mathsf{\_}}{{\mathit{sx}}})`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. - - * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`M / 8 \cdot N`. * Or: * :math:`{{\mathit{vloadop\_u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`({N}{\mathsf{\_}}{\mathsf{splat}})`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. - - * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`N / 8`. * Or: * :math:`{{\mathit{vloadop\_u{\kern-0.1em\scriptstyle 0}}}^?}` must be equal to :math:`({N}{\mathsf{\_}}{\mathsf{zero}})`. - * :math:`{|C{.}\mathsf{mems}|}` must be greater than :math:`x`. - - * :math:`C{.}\mathsf{mems}{}[x]` must be equal to :math:`{\mathit{mt}}`. - * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` must be less than or equal to :math:`N / 8`. @@ -22759,14 +22713,13 @@ Heaptype_sub Reftype_sub - the reference type (REF (NULL _u0? ?) ht_1) matches the reference type (REF (NULL _u1? ?) ht_2) if and only if: + - the heap type ht_1 matches the heap type ht_2. - Either: - _u0? is ?(). - _u1? is ?(). - - the heap type ht_1 matches the heap type ht_2. - Or: - _u0? is ()?. - _u1? is ?(()). - - the heap type ht_1 matches the heap type ht_2. Vectype_sub - the vector type vectype matches the vector type vectype. @@ -22802,14 +22755,13 @@ Storagetype_sub Fieldtype_sub - the field type ((MUT _u0? ?), zt_1) matches the field type ((MUT _u1? ?), zt_2) if and only if: + - the storage type zt_1 matches the storage type zt_2. - Either: - _u0? is ?(). - _u1? is ?(). - - the storage type zt_1 matches the storage type zt_2. - Or: - _u0? is ?(()). - _u1? is ?(()). - - the storage type zt_1 matches the storage type zt_2. - the storage type zt_2 matches the storage type zt_1. Resulttype_sub @@ -22955,14 +22907,13 @@ Limits_sub Globaltype_sub - the global type ((MUT _u0? ?), valtype_1) matches the global type ((MUT _u1? ?), valtype_2) if and only if: + - the value type valtype_1 matches the value type valtype_2. - Either: - _u0? is ?(). - _u1? is ?(). - - the value type valtype_1 matches the value type valtype_2. - Or: - _u0? is ?(()). - _u1? is ?(()). - - the value type valtype_1 matches the value type valtype_2. - the value type valtype_2 matches the value type valtype_1. Tabletype_sub @@ -23020,25 +22971,22 @@ Blocktype_ok Catch_ok - the catch clause catch_u0 is valid if and only if: + - |C.LABELS| is greater than l. - Either: - catch_u0 is (CATCH x l). - |C.TAGS| is greater than x. - - |C.LABELS| is greater than l. - $expanddt(C.TAGS[x]) is (FUNC (t* -> [])). - the value type sequence t* matches the result type C.LABELS[l]. - Or: - catch_u0 is (CATCH_REF x l). - |C.TAGS| is greater than x. - - |C.LABELS| is greater than l. - $expanddt(C.TAGS[x]) is (FUNC (t* -> [])). - the value type sequence t* ++ [(REF (NULL ?() ?) EXN)] matches the result type C.LABELS[l]. - Or: - catch_u0 is (CATCH_ALL l). - - |C.LABELS| is greater than l. - the value type sequence [] matches the result type C.LABELS[l]. - Or: - catch_u0 is (CATCH_ALL_REF l). - - |C.LABELS| is greater than l. - the value type sequence [(REF (NULL ?() ?) EXN)] matches the result type C.LABELS[l]. Instr_ok/nop @@ -23054,12 +23002,11 @@ Instr_ok/drop Instr_ok/select - the instr (SELECT() valtype_u0? ?) is valid with the instruction type ([t, t, I32] ->_ [] [t]) if and only if: + - the value type t is valid. - Either: - valtype_u0? is ?([t]). - - the value type t is valid. - Or: - valtype_u0? is ?(). - - the value type t is valid. - the value type t matches the value type t'. - Either: - t' is numtype. @@ -23545,59 +23492,49 @@ Instr_ok/data.drop Instr_ok/load - the instr (LOAD numtype_u0 loadop__u2? x memarg) is valid with the instruction type ([I32] ->_ [] [valtype_u3]) if and only if: + - |C.MEMS| is greater than x. + - C.MEMS[x] is mt. - Either: - numtype_u0 is nt. - loadop__u2? is ?(). - valtype_u3 is nt. - - |C.MEMS| is greater than x. - - C.MEMS[x] is mt. - (2 ^ memarg.ALIGN) is less than or equal to ($size(nt) / 8). - Or: - numtype_u0 is Inn. - loadop__u2? is ?((M, sx)). - valtype_u3 is Inn. - - |C.MEMS| is greater than x. - - C.MEMS[x] is mt. - (2 ^ memarg.ALIGN) is less than or equal to (M / 8). Instr_ok/store - the instr (STORE numtype_u0 sz_u1? x memarg) is valid with the instruction type ([I32, valtype_u2] ->_ [] []) if and only if: + - |C.MEMS| is greater than x. + - C.MEMS[x] is mt. - Either: - numtype_u0 is nt. - sz_u1? is ?(). - valtype_u2 is nt. - - |C.MEMS| is greater than x. - - C.MEMS[x] is mt. - (2 ^ memarg.ALIGN) is less than or equal to ($size(nt) / 8). - Or: - numtype_u0 is Inn. - sz_u1? is ?(M). - valtype_u2 is Inn. - - |C.MEMS| is greater than x. - - C.MEMS[x] is mt. - (2 ^ memarg.ALIGN) is less than or equal to (M / 8). Instr_ok/vload - the instr (VLOAD V128 vloadop__u0? x memarg) is valid with the instruction type ([I32] ->_ [] [V128]) if and only if: + - |C.MEMS| is greater than x. + - C.MEMS[x] is mt. - Either: - vloadop__u0? is ?(). - - |C.MEMS| is greater than x. - - C.MEMS[x] is mt. - (2 ^ memarg.ALIGN) is less than or equal to ($vsize(V128) / 8). - Or: - vloadop__u0? is ?((SHAPE M X N sx)). - - |C.MEMS| is greater than x. - - C.MEMS[x] is mt. - (2 ^ memarg.ALIGN) is less than or equal to ((M / 8) · N). - Or: - vloadop__u0? is ?((SPLAT N)). - - |C.MEMS| is greater than x. - - C.MEMS[x] is mt. - (2 ^ memarg.ALIGN) is less than or equal to (N / 8). - Or: - vloadop__u0? is ?((ZERO N)). - - |C.MEMS| is greater than x. - - C.MEMS[x] is mt. - (2 ^ memarg.ALIGN) is less than or equal to (N / 8). Instr_ok/vload_lane