diff --git a/spectec/src/il2al/animate.ml b/spectec/src/il2al/animate.ml index cc55f73d07..c70984492e 100644 --- a/spectec/src/il2al/animate.ml +++ b/spectec/src/il2al/animate.ml @@ -107,12 +107,20 @@ let rec recover_iterexp' iterexp pr = | IterPr (pr, (iter, xes)) -> IterPr (recover_iterexp iterexp pr, (iter, xes |> List.map (fun (x, e) -> (x, new_ e)))) and recover_iterexp iterexp pr = Source.map (recover_iterexp' iterexp) pr +(* is this assign premise a if-let? *) +let is_cond_assign prem = + match prem.it with + | LetPr ({it = CaseE (_, _); _}, _, _) -> true + | _ -> false -(* is this assign premise encoded premise for pop? *) +(* is this assign premise encoded premise for popping one value? *) let is_pop env row = is_assign env row && match (unwrap row).it with - | LetPr (_, rhs, _) -> Il.Print.string_of_typ rhs.note = "stackT" + | LetPr (_, {it = CallE (_, {it = ExpA n; _} :: _); note; _}, _) when Il.Print.string_of_typ note = "stackT" -> + (match n.it with + | NatE i -> Z.equal i (Z.one) + | _ -> false) | _ -> false (* iteratively select pop, condition and assignment premises, @@ -161,7 +169,11 @@ and select_assign prems acc env fb = fb := (len, acc @ List.map unwrap non_assigns); None | _ -> - let assigns' = List.map unwrap assigns in + let cond_assigns, non_cond_assigns = + List.map unwrap assigns + |> List.partition is_cond_assign + in + let assigns' = cond_assigns @ non_cond_assigns in let new_env = assigns |> List.map targets |> List.concat diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index 2a8ba3509f..5deeaf2e72 100644 --- a/spectec/src/il2al/translate.ml +++ b/spectec/src/il2al/translate.ml @@ -107,11 +107,11 @@ let rec insert_instrs target il = h @ [ ifI (cond, insert_instrs (Transpile.insert_nop target) il' , []) ] | _ -> il @ target -(* Insert `target` at the else-branch of innermost if instruction *) -let rec insert_instrs_to_else target il = +(* Insert `target` at the last instruction *) +let insert_to_last target il = match Util.Lib.List.split_last_opt il with - | Some (h, { it = IfI (cond, il1, il2); _ }) -> - h @ [ ifI (cond, il1, insert_instrs_to_else target il2) ] + | Some (hd, tl) -> + hd @ Transpile.merge_blocks [[tl]; [otherwiseI target]] | _ -> il @ target let has_branch = List.exists (fun i -> @@ -1169,8 +1169,8 @@ let rec translate_rgroup' (rule: rule_def) = | None, b -> b | Some b, [] -> b | Some b1, b2 -> - (* Assert: b1 must have the else-less IfI as inner most instruction *) - insert_instrs_to_else b2 (Transpile.flatten_if b1) + (* Assert: last instruction of b1 must be else-less IfI *) + insert_to_last b2 b1 in translate_prems pops body_instrs diff --git a/spectec/src/il2al/unify.ml b/spectec/src/il2al/unify.ml index 86555363ce..7e175d7af1 100644 --- a/spectec/src/il2al/unify.ml +++ b/spectec/src/il2al/unify.ml @@ -354,13 +354,42 @@ let unify_rule_def (rule: rule_def) : rule_def = in (instr_name, rel_id, new_clauses) $ rule.at +let has_substring str sub = + let len_s = String.length str in + let len_sub = String.length sub in + let rec aux i = + if i > len_s - len_sub then false + else if String.sub str i len_sub = sub then true + else aux (i + 1) + in + aux 0 + +let reorder_unified_args args prems = + (* Helpers *) + let has_uarg_on_rhs p = + match p.it with + | LetPr (_, {it = VarE id; _}, _) -> is_unified_id id.it + | _ -> false + in + let on_rhs p a = + match a.it with + | ExpA e -> has_substring (e |> Il.Print.string_of_exp) (rhs_of_prem p |> Il.Print.string_of_exp) + | _ -> false + in + let index_of p = List.find_index (on_rhs p) args |> Option.get in + let cmp p1 p2 = index_of p1 - index_of p2 in + + let uprems, prems = List.partition has_uarg_on_rhs prems in + let uprems' = List.sort cmp uprems in + uprems' @ prems let apply_template_to_def template def = match def.it with | DefD (binds, lhs, rhs, prems) -> let new_prems, new_binds = collect_unified_args template lhs in let animated_prems = Animate.animate_prems (free_list free_arg template) new_prems in - DefD (binds @ new_binds, template, rhs, (animated_prems @ prems) |> prioritize_else) $ def.at + let reordered_prems = reorder_unified_args template animated_prems in + DefD (binds @ new_binds, template, rhs, (reordered_prems @ prems) |> prioritize_else) $ def.at let unify_defs defs = init_unified_idx(); diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index ef1beb595d..aab2bc92d7 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -983,10 +983,6 @@ watsup 0.4 generator #. Let :math:`\{ \begin{array}[t]{@{}l@{}}\mathsf{type}~({t_1^{k}}~\rightarrow~{t_2^{n}}),\; \mathsf{module}~{\mathit{mm}},\; \mathsf{code}~{\mathit{func}} \}\end{array}` be :math:`z{.}\mathsf{funcs}{}[a]`. -#. Assert: Due to validation, there are at least :math:`k` values on the top of the stack. - -#. Pop the values :math:`{{\mathit{val}}^{k}}` from the stack. - #. Assert: Due to validation, :math:`{\mathit{func}}` is of the case :math:`\mathsf{func}`. #. Let :math:`(\mathsf{func}~x~{{\mathit{local}}_0^\ast}~{{\mathit{instr}}^\ast})` be :math:`{\mathit{func}}`. @@ -995,6 +991,10 @@ watsup 0.4 generator #. Let :math:`{(\mathsf{local}~t)^\ast}` be :math:`{{\mathit{local}}_0^\ast}`. +#. Assert: Due to validation, there are at least :math:`k` values on the top of the stack. + +#. Pop the values :math:`{{\mathit{val}}^{k}}` from the stack. + #. Let :math:`f` be :math:`\{ \begin{array}[t]{@{}l@{}}\mathsf{locals}~{{\mathit{val}}^{k}}~{{{\mathrm{default}}}_{t}^\ast},\; \mathsf{module}~{\mathit{mm}} \}\end{array}`. #. Push the evaluation context :math:`({{\mathsf{frame}}_{n}}{\{}~f~\})` to the stack. @@ -1455,86 +1455,56 @@ watsup 0.4 generator ........................................................................................................................................................................ -1. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{clz}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Return :math:`{{\mathrm{iclz}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}})`. - -#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{ctz}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Return :math:`{{\mathrm{ictz}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}})`. - -#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{popcnt}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: +1. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. #. Let :math:`{\mathit{iN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - #. Return :math:`{{\mathrm{ipopcnt}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}})`. - -#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{abs}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: - - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Return :math:`{{\mathrm{fabs}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. + #. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{clz}`, then: -#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{neg}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: + 1) Return :math:`{{\mathrm{iclz}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}})`. - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. + #. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{ctz}`, then: - #. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. + 1) Return :math:`{{\mathrm{ictz}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}})`. - #. Return :math:`{{\mathrm{fneg}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. + #. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{popcnt}`, then: -#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{sqrt}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: + 1) Return :math:`{{\mathrm{ipopcnt}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}})`. - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. +#. Assert: Due to validation, the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn. - #. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. +#. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - #. Return :math:`{{\mathrm{fsqrt}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. +#. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. -#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{ceil}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: +#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{abs}`, then: - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. + a. Return :math:`{{\mathrm{fabs}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. - #. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. +#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{neg}`, then: - #. Return :math:`{{\mathrm{fceil}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. + a. Return :math:`{{\mathrm{fneg}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. -#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{floor}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: +#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{sqrt}`, then: - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. + a. Return :math:`{{\mathrm{fsqrt}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. - #. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. +#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{ceil}`, then: - #. Return :math:`{{\mathrm{ffloor}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. + a. Return :math:`{{\mathrm{fceil}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. -#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{trunc}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: +#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{floor}`, then: - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. + a. Return :math:`{{\mathrm{ffloor}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. - #. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. +#. If :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{trunc}`, then: - #. Return :math:`{{\mathrm{ftrunc}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. + a. Return :math:`{{\mathrm{ftrunc}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. #. Assert: Due to validation, :math:`{\mathit{unop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{nearest}`. -#. Assert: Due to validation, the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn. - -#. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - -#. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - #. Return :math:`{{\mathrm{fnearest}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}})`. @@ -1542,17 +1512,7 @@ watsup 0.4 generator ....................................................................................................................................................................................................................... -1. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{add}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{iadd}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{sub}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: +1. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. @@ -1560,25 +1520,17 @@ watsup 0.4 generator #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - #. Return :math:`{{\mathrm{isub}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{mul}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. + #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{add}`, then: - #. Return :math:`{{\mathrm{imul}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. + 1) Return :math:`{{\mathrm{iadd}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. -#. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: + #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{sub}`, then: - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. + 1) Return :math:`{{\mathrm{isub}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. + #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{mul}`, then: - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. + 1) Return :math:`{{\mathrm{imul}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{div}`, then: @@ -1592,53 +1544,21 @@ watsup 0.4 generator #) Return :math:`{{{{\mathrm{irem}}}_{{|{\mathsf{i}}{n}|}}^{{\mathit{sx}}}}}{({\mathit{iN}}_1, {\mathit{iN}}_2)}`. -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{and}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{iand}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{or}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{ior}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{xor}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{ixor}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{shl}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. + #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{and}`, then: - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. + 1) Return :math:`{{\mathrm{iand}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. + #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{or}`, then: - #. Return :math:`{{\mathrm{ishl}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. + 1) Return :math:`{{\mathrm{ior}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. -#. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: + #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{xor}`, then: - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. + 1) Return :math:`{{\mathrm{ixor}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. + #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{shl}`, then: - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. + 1) Return :math:`{{\mathrm{ishl}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{shr}`, then: @@ -1646,96 +1566,48 @@ watsup 0.4 generator #) Return :math:`{{{{\mathrm{ishr}}}_{{|{\mathsf{i}}{n}|}}^{{\mathit{sx}}}}}{({\mathit{iN}}_1, {\mathit{iN}}_2)}`. -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{rotl}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{irotl}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{rotr}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{irotr}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{add}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: - - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{fadd}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{sub}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: - - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. + #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{rotl}`, then: - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. + 1) Return :math:`{{\mathrm{irotl}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. + #. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{rotr}`, then: - #. Return :math:`{{\mathrm{fsub}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. + 1) Return :math:`{{\mathrm{irotr}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{mul}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: - - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{fmul}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. +#. Assert: Due to validation, the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn. -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{div}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: +#. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. +#. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. +#. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. +#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{add}`, then: - #. Return :math:`{{\mathrm{fdiv}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. + a. Return :math:`{{\mathrm{fadd}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{min}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: +#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{sub}`, then: - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. + a. Return :math:`{{\mathrm{fsub}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. +#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{mul}`, then: - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. + a. Return :math:`{{\mathrm{fmul}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - #. Return :math:`{{\mathrm{fmin}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. +#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{div}`, then: -#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{max}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: + a. Return :math:`{{\mathrm{fdiv}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. +#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{min}`, then: - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. + a. Return :math:`{{\mathrm{fmin}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. +#. If :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{max}`, then: - #. Return :math:`{{\mathrm{fmax}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. + a. Return :math:`{{\mathrm{fmax}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. #. Assert: Due to validation, :math:`{\mathit{binop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{copysign}`. -#. Assert: Due to validation, the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn. - -#. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - -#. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - -#. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - #. Return :math:`{{\mathrm{fcopysign}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. @@ -1750,17 +1622,7 @@ watsup 0.4 generator ....................................................................................................................................................................................................................... -1. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{eq}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: - - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{ieq}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - -#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{ne}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: +1. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. @@ -1768,15 +1630,13 @@ watsup 0.4 generator #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - #. Return :math:`{{\mathrm{ine}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. + #. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{eq}`, then: -#. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Inn, then: + 1) Return :math:`{{\mathrm{ieq}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. - a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{iN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. + #. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{ne}`, then: - #. Let :math:`{\mathit{iN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. + 1) Return :math:`{{\mathrm{ine}}}_{{|{\mathsf{i}}{n}|}}({\mathit{iN}}_1, {\mathit{iN}}_2)`. #. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{lt}`, then: @@ -1802,66 +1662,36 @@ watsup 0.4 generator #) Return :math:`{{{{\mathrm{ige}}}_{{|{\mathsf{i}}{n}|}}^{{\mathit{sx}}}}}{({\mathit{iN}}_1, {\mathit{iN}}_2)}`. -#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{eq}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: - - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{feq}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - -#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{ne}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: - - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - - #. Return :math:`{{\mathrm{fne}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - -#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{lt}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: - - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. +#. Assert: Due to validation, the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn. - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. +#. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. +#. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - #. Return :math:`{{\mathrm{flt}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. +#. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. -#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{gt}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: +#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{eq}`, then: - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. + a. Return :math:`{{\mathrm{feq}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. +#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{ne}`, then: - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. + a. Return :math:`{{\mathrm{fne}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - #. Return :math:`{{\mathrm{fgt}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. +#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{lt}`, then: -#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{le}` and the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: + a. Return :math:`{{\mathrm{flt}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. +#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{gt}`, then: - #. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. + a. Return :math:`{{\mathrm{fgt}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. - #. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. +#. If :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{le}`, then: - #. Return :math:`{{\mathrm{fle}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. + a. Return :math:`{{\mathrm{fle}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. #. Assert: Due to validation, :math:`{\mathit{relop\_u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{ge}`. -#. Assert: Due to validation, the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn. - -#. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - -#. Let :math:`{\mathit{fN}}_1` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 3}}}`. - -#. Let :math:`{\mathit{fN}}_2` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 5}}}`. - #. Return :math:`{{\mathrm{fge}}}_{{|{\mathsf{f}}{n}|}}({\mathit{fN}}_1, {\mathit{fN}}_2)`. @@ -1869,21 +1699,21 @@ watsup 0.4 generator ............................................................................................................................................................................................................................................... -1. If :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{i{\scriptstyle 32}}` and :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is :math:`\mathsf{i{\scriptstyle 64}}`, then: +1. If :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is of the case :math:`\mathsf{extend}`, then: - a. Let :math:`{\mathit{iN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. + a. Let :math:`(\mathsf{extend}~{\mathit{sx}})` be :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}`. - #. If :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is of the case :math:`\mathsf{extend}`, then: + #. Let :math:`{\mathit{iN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. - 1) Let :math:`(\mathsf{extend}~{\mathit{sx}})` be :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}`. + #. If :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{i{\scriptstyle 32}}` and :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is :math:`\mathsf{i{\scriptstyle 64}}`, then: - #) Return :math:`{{{{\mathrm{extend}}}_{32, 64}^{{\mathit{sx}}}}}{({\mathit{iN}})}`. + 1) Return :math:`{{{{\mathrm{extend}}}_{32, 64}^{{\mathit{sx}}}}}{({\mathit{iN}})}`. -#. If :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{i{\scriptstyle 64}}` and :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is :math:`\mathsf{i{\scriptstyle 32}}` and :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is :math:`\mathsf{wrap}`, then: +#. Let :math:`{\mathit{iN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. - a. Let :math:`{\mathit{iN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. +#. If :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{i{\scriptstyle 64}}` and :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is :math:`\mathsf{i{\scriptstyle 32}}` and :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is :math:`\mathsf{wrap}`, then: - #. Return :math:`{{\mathrm{wrap}}}_{64, 32}({\mathit{iN}})`. + a. Return :math:`{{\mathrm{wrap}}}_{64, 32}({\mathit{iN}})`. #. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is Fnn, then: @@ -1893,35 +1723,31 @@ watsup 0.4 generator 1) Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - #) Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. - #) If :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is of the case :math:`\mathsf{trunc}`, then: a) Let :math:`(\mathsf{trunc}~{\mathit{sx}})` be :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}`. + #) Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. + #) Return :math:`{{{{\mathrm{trunc}}}_{{|{\mathsf{f}}{n}|}, {|{\mathsf{i}}{n}|}}^{{\mathit{sx}}}}}{({\mathit{fN}})}`. -#. If :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{f{\scriptstyle 32}}` and :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is :math:`\mathsf{f{\scriptstyle 64}}` and :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is :math:`\mathsf{promote}`, then: +#. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. - a. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. +#. If :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{f{\scriptstyle 32}}` and :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is :math:`\mathsf{f{\scriptstyle 64}}` and :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is :math:`\mathsf{promote}`, then: - #. Return :math:`{{\mathrm{promote}}}_{32, 64}({\mathit{fN}})`. + a. Return :math:`{{\mathrm{promote}}}_{32, 64}({\mathit{fN}})`. #. If :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is :math:`\mathsf{f{\scriptstyle 64}}` and :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is :math:`\mathsf{f{\scriptstyle 32}}` and :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is :math:`\mathsf{demote}`, then: - a. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. - - #. Return :math:`{{\mathrm{demote}}}_{64, 32}({\mathit{fN}})`. - -#. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: + a. Return :math:`{{\mathrm{demote}}}_{64, 32}({\mathit{fN}})`. - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. +#. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is Inn, then: - #. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is Inn, then: + a. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}`. - 1) Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}`. + #. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: - #) Let :math:`{\mathit{iN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. + 1) Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. #) If :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is of the case :math:`\mathsf{convert}`, then: @@ -1929,19 +1755,7 @@ watsup 0.4 generator #) Return :math:`{{{{\mathrm{convert}}}_{{|{\mathsf{i}}{n}|}, {|{\mathsf{f}}{n}|}}^{{\mathit{sx}}}}}{({\mathit{iN}})}`. -#. Assert: Due to validation, :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is :math:`\mathsf{reinterpret}`. - -#. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is Fnn, then: - - a. Let :math:`{\mathsf{f}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. - - #. If the type of :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is Inn, then: - - 1) Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}`. - - #) Let :math:`{\mathit{iN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. - - #) If :math:`{|{\mathsf{i}}{n}|}` is :math:`{|{\mathsf{f}}{n}|}`, then: + #) If :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is :math:`\mathsf{reinterpret}` and :math:`{|{\mathsf{i}}{n}|}` is :math:`{|{\mathsf{f}}{n}|}`, then: a) Return :math:`{{\mathrm{reinterpret}}}_{{\mathsf{i}}{n}, {\mathsf{f}}{n}}({\mathit{iN}})`. @@ -1953,7 +1767,7 @@ watsup 0.4 generator #. Let :math:`{\mathsf{i}}{n}` be :math:`{\mathit{valtype}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}`. -#. Let :math:`{\mathit{fN}}` be :math:`{\mathit{val\_u{\kern-0.1em\scriptstyle 4}}}`. +#. Assert: Due to validation, :math:`{\mathit{cvtop}}_{\mathit{u{\kern-0.1em\scriptstyle 2}}}` is :math:`\mathsf{reinterpret}`. #. Assert: Due to validation, :math:`{|{\mathsf{i}}{n}|}` is :math:`{|{\mathsf{f}}{n}|}`. @@ -2532,15 +2346,7 @@ watsup 0.4 generator ...................................................................................................... -1. Let :math:`{{\mathit{fa}}_{\mathit{ex}}^\ast}` be :math:`{\mathrm{funcs}}({{\mathit{externaddr}}^\ast})`. - -#. Let :math:`{{\mathit{ga}}_{\mathit{ex}}^\ast}` be :math:`{\mathrm{globals}}({{\mathit{externaddr}}^\ast})`. - -#. Let :math:`{{\mathit{ma}}_{\mathit{ex}}^\ast}` be :math:`{\mathrm{mems}}({{\mathit{externaddr}}^\ast})`. - -#. Let :math:`{{\mathit{ta}}_{\mathit{ex}}^\ast}` be :math:`{\mathrm{tables}}({{\mathit{externaddr}}^\ast})`. - -#. Assert: Due to validation, :math:`{\mathit{module}}` is of the case :math:`\mathsf{module}`. +1. Assert: Due to validation, :math:`{\mathit{module}}` is of the case :math:`\mathsf{module}`. #. Let :math:`(\mathsf{module}~{{\mathit{type}}_0^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^{n_{\mathit{func}}}}~{{\mathit{global}}_1^{n_{\mathit{global}}}}~{{\mathit{table}}_2^{n_{\mathit{table}}}}~{{\mathit{mem}}_3^{n_{\mathit{mem}}}}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast})` be :math:`{\mathit{module}}`. @@ -2560,6 +2366,14 @@ watsup 0.4 generator #. Let :math:`{(\mathsf{type}~{\mathit{ft}})^\ast}` be :math:`{{\mathit{type}}_0^\ast}`. +#. Let :math:`{{\mathit{fa}}_{\mathit{ex}}^\ast}` be :math:`{\mathrm{funcs}}({{\mathit{externaddr}}^\ast})`. + +#. Let :math:`{{\mathit{ga}}_{\mathit{ex}}^\ast}` be :math:`{\mathrm{globals}}({{\mathit{externaddr}}^\ast})`. + +#. Let :math:`{{\mathit{ma}}_{\mathit{ex}}^\ast}` be :math:`{\mathrm{mems}}({{\mathit{externaddr}}^\ast})`. + +#. Let :math:`{{\mathit{ta}}_{\mathit{ex}}^\ast}` be :math:`{\mathrm{tables}}({{\mathit{externaddr}}^\ast})`. + #. Let :math:`{{\mathit{fa}}^\ast}` be :math:`{{|s{.}\mathsf{funcs}|} + i_{\mathit{func}}^{i_{\mathit{func}} t_2^n); MODULE: mm; CODE: func; } be $funcinst(z)[a]. -4. Assert: Due to validation, there are at least k values on the top of the stack. -5. Pop the values val^k from the stack. -6. Assert: Due to validation, func is of the case FUNC. -7. Let (FUNC x local_0* instr*) be func. -8. Assert: Due to validation, local_0 is of the case LOCAL*. -9. Let (LOCAL t)* be local_0*. +4. Assert: Due to validation, func is of the case FUNC. +5. Let (FUNC x local_0* instr*) be func. +6. Assert: Due to validation, local_0 is of the case LOCAL*. +7. Let (LOCAL t)* be local_0*. +8. Assert: Due to validation, there are at least k values on the top of the stack. +9. Pop the values val^k from the stack. 10. Let f be { LOCALS: val^k :: $default_(t)*; MODULE: mm; }. 11. Push the evaluation context (FRAME_ n { f }) to the stack. 12. Enter instr* with label (LABEL_ n { [] }). @@ -3523,254 +3337,161 @@ invsigned_ N ii 2. Return j. unop_ valtype_u1 unop__u0 val__u3 -1. If ((unop__u0 is CLZ) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN be val__u3. - c. Return [$iclz_($size(Inn), iN)]. -2. If ((unop__u0 is CTZ) and the type of valtype_u1 is Inn), then: +1. If the type of valtype_u1 is Inn, then: a. Let Inn be valtype_u1. b. Let iN be val__u3. - c. Return [$ictz_($size(Inn), iN)]. -3. If ((unop__u0 is POPCNT) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN be val__u3. - c. Return [$ipopcnt_($size(Inn), iN)]. -4. If ((unop__u0 is ABS) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN be val__u3. - c. Return $fabs_($size(Fnn), fN). -5. If ((unop__u0 is NEG) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN be val__u3. - c. Return $fneg_($size(Fnn), fN). -6. If ((unop__u0 is SQRT) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN be val__u3. - c. Return $fsqrt_($size(Fnn), fN). -7. If ((unop__u0 is CEIL) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN be val__u3. - c. Return $fceil_($size(Fnn), fN). -8. If ((unop__u0 is FLOOR) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN be val__u3. - c. Return $ffloor_($size(Fnn), fN). -9. If ((unop__u0 is TRUNC) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN be val__u3. - c. Return $ftrunc_($size(Fnn), fN). -10. Assert: Due to validation, (unop__u0 is NEAREST). -11. Assert: Due to validation, the type of valtype_u1 is Fnn. -12. Let Fnn be valtype_u1. -13. Let fN be val__u3. -14. Return $fnearest_($size(Fnn), fN). + c. If (unop__u0 is CLZ), then: + 1) Return [$iclz_($size(Inn), iN)]. + d. If (unop__u0 is CTZ), then: + 1) Return [$ictz_($size(Inn), iN)]. + e. If (unop__u0 is POPCNT), then: + 1) Return [$ipopcnt_($size(Inn), iN)]. +2. Assert: Due to validation, the type of valtype_u1 is Fnn. +3. Let Fnn be valtype_u1. +4. Let fN be val__u3. +5. If (unop__u0 is ABS), then: + a. Return $fabs_($size(Fnn), fN). +6. If (unop__u0 is NEG), then: + a. Return $fneg_($size(Fnn), fN). +7. If (unop__u0 is SQRT), then: + a. Return $fsqrt_($size(Fnn), fN). +8. If (unop__u0 is CEIL), then: + a. Return $fceil_($size(Fnn), fN). +9. If (unop__u0 is FLOOR), then: + a. Return $ffloor_($size(Fnn), fN). +10. If (unop__u0 is TRUNC), then: + a. Return $ftrunc_($size(Fnn), fN). +11. Assert: Due to validation, (unop__u0 is NEAREST). +12. Return $fnearest_($size(Fnn), fN). binop_ valtype_u1 binop__u0 val__u3 val__u5 -1. If ((binop__u0 is ADD) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. Return [$iadd_($size(Inn), iN_1, iN_2)]. -2. If ((binop__u0 is SUB) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. Return [$isub_($size(Inn), iN_1, iN_2)]. -3. If ((binop__u0 is MUL) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. Return [$imul_($size(Inn), iN_1, iN_2)]. -4. If the type of valtype_u1 is Inn, then: +1. If the type of valtype_u1 is Inn, then: a. Let Inn be valtype_u1. b. Let iN_1 be val__u3. c. Let iN_2 be val__u5. - d. If binop__u0 is of the case DIV, then: + d. If (binop__u0 is ADD), then: + 1) Return [$iadd_($size(Inn), iN_1, iN_2)]. + e. If (binop__u0 is SUB), then: + 1) Return [$isub_($size(Inn), iN_1, iN_2)]. + f. If (binop__u0 is MUL), then: + 1) Return [$imul_($size(Inn), iN_1, iN_2)]. + g. If binop__u0 is of the case DIV, then: 1) Let (DIV sx) be binop__u0. 2) Return $list_(val_((Inn : Inn <: valtype)), $idiv_($size(Inn), sx, iN_1, iN_2)). - e. If binop__u0 is of the case REM, then: + h. If binop__u0 is of the case REM, then: 1) Let (REM sx) be binop__u0. 2) Return $list_(val_((Inn : Inn <: valtype)), $irem_($size(Inn), sx, iN_1, iN_2)). -5. If ((binop__u0 is AND) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. Return [$iand_($size(Inn), iN_1, iN_2)]. -6. If ((binop__u0 is OR) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. Return [$ior_($size(Inn), iN_1, iN_2)]. -7. If ((binop__u0 is XOR) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. Return [$ixor_($size(Inn), iN_1, iN_2)]. -8. If ((binop__u0 is SHL) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. Return [$ishl_($size(Inn), iN_1, iN_2)]. -9. If the type of valtype_u1 is Inn, then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. If binop__u0 is of the case SHR, then: + i. If (binop__u0 is AND), then: + 1) Return [$iand_($size(Inn), iN_1, iN_2)]. + j. If (binop__u0 is OR), then: + 1) Return [$ior_($size(Inn), iN_1, iN_2)]. + k. If (binop__u0 is XOR), then: + 1) Return [$ixor_($size(Inn), iN_1, iN_2)]. + l. If (binop__u0 is SHL), then: + 1) Return [$ishl_($size(Inn), iN_1, iN_2)]. + m. If binop__u0 is of the case SHR, then: 1) Let (SHR sx) be binop__u0. 2) Return [$ishr_($size(Inn), sx, iN_1, iN_2)]. -10. If ((binop__u0 is ROTL) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. Return [$irotl_($size(Inn), iN_1, iN_2)]. -11. If ((binop__u0 is ROTR) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. Return [$irotr_($size(Inn), iN_1, iN_2)]. -12. If ((binop__u0 is ADD) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $fadd_($size(Fnn), fN_1, fN_2). -13. If ((binop__u0 is SUB) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $fsub_($size(Fnn), fN_1, fN_2). -14. If ((binop__u0 is MUL) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $fmul_($size(Fnn), fN_1, fN_2). -15. If ((binop__u0 is DIV) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $fdiv_($size(Fnn), fN_1, fN_2). -16. If ((binop__u0 is MIN) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $fmin_($size(Fnn), fN_1, fN_2). -17. If ((binop__u0 is MAX) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $fmax_($size(Fnn), fN_1, fN_2). -18. Assert: Due to validation, (binop__u0 is COPYSIGN). -19. Assert: Due to validation, the type of valtype_u1 is Fnn. -20. Let Fnn be valtype_u1. -21. Let fN_1 be val__u3. -22. Let fN_2 be val__u5. -23. Return $fcopysign_($size(Fnn), fN_1, fN_2). + n. If (binop__u0 is ROTL), then: + 1) Return [$irotl_($size(Inn), iN_1, iN_2)]. + o. If (binop__u0 is ROTR), then: + 1) Return [$irotr_($size(Inn), iN_1, iN_2)]. +2. Assert: Due to validation, the type of valtype_u1 is Fnn. +3. Let Fnn be valtype_u1. +4. Let fN_1 be val__u3. +5. Let fN_2 be val__u5. +6. If (binop__u0 is ADD), then: + a. Return $fadd_($size(Fnn), fN_1, fN_2). +7. If (binop__u0 is SUB), then: + a. Return $fsub_($size(Fnn), fN_1, fN_2). +8. If (binop__u0 is MUL), then: + a. Return $fmul_($size(Fnn), fN_1, fN_2). +9. If (binop__u0 is DIV), then: + a. Return $fdiv_($size(Fnn), fN_1, fN_2). +10. If (binop__u0 is MIN), then: + a. Return $fmin_($size(Fnn), fN_1, fN_2). +11. If (binop__u0 is MAX), then: + a. Return $fmax_($size(Fnn), fN_1, fN_2). +12. Assert: Due to validation, (binop__u0 is COPYSIGN). +13. Return $fcopysign_($size(Fnn), fN_1, fN_2). testop_ Inn EQZ iN 1. Return $ieqz_($size(Inn), iN). relop_ valtype_u1 relop__u0 val__u3 val__u5 -1. If ((relop__u0 is EQ) and the type of valtype_u1 is Inn), then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. Return $ieq_($size(Inn), iN_1, iN_2). -2. If ((relop__u0 is NE) and the type of valtype_u1 is Inn), then: +1. If the type of valtype_u1 is Inn, then: a. Let Inn be valtype_u1. b. Let iN_1 be val__u3. c. Let iN_2 be val__u5. - d. Return $ine_($size(Inn), iN_1, iN_2). -3. If the type of valtype_u1 is Inn, then: - a. Let Inn be valtype_u1. - b. Let iN_1 be val__u3. - c. Let iN_2 be val__u5. - d. If relop__u0 is of the case LT, then: + d. If (relop__u0 is EQ), then: + 1) Return $ieq_($size(Inn), iN_1, iN_2). + e. If (relop__u0 is NE), then: + 1) Return $ine_($size(Inn), iN_1, iN_2). + f. If relop__u0 is of the case LT, then: 1) Let (LT sx) be relop__u0. 2) Return $ilt_($size(Inn), sx, iN_1, iN_2). - e. If relop__u0 is of the case GT, then: + g. If relop__u0 is of the case GT, then: 1) Let (GT sx) be relop__u0. 2) Return $igt_($size(Inn), sx, iN_1, iN_2). - f. If relop__u0 is of the case LE, then: + h. If relop__u0 is of the case LE, then: 1) Let (LE sx) be relop__u0. 2) Return $ile_($size(Inn), sx, iN_1, iN_2). - g. If relop__u0 is of the case GE, then: + i. If relop__u0 is of the case GE, then: 1) Let (GE sx) be relop__u0. 2) Return $ige_($size(Inn), sx, iN_1, iN_2). -4. If ((relop__u0 is EQ) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $feq_($size(Fnn), fN_1, fN_2). -5. If ((relop__u0 is NE) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $fne_($size(Fnn), fN_1, fN_2). -6. If ((relop__u0 is LT) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $flt_($size(Fnn), fN_1, fN_2). -7. If ((relop__u0 is GT) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $fgt_($size(Fnn), fN_1, fN_2). -8. If ((relop__u0 is LE) and the type of valtype_u1 is Fnn), then: - a. Let Fnn be valtype_u1. - b. Let fN_1 be val__u3. - c. Let fN_2 be val__u5. - d. Return $fle_($size(Fnn), fN_1, fN_2). -9. Assert: Due to validation, (relop__u0 is GE). -10. Assert: Due to validation, the type of valtype_u1 is Fnn. -11. Let Fnn be valtype_u1. -12. Let fN_1 be val__u3. -13. Let fN_2 be val__u5. -14. Return $fge_($size(Fnn), fN_1, fN_2). +2. Assert: Due to validation, the type of valtype_u1 is Fnn. +3. Let Fnn be valtype_u1. +4. Let fN_1 be val__u3. +5. Let fN_2 be val__u5. +6. If (relop__u0 is EQ), then: + a. Return $feq_($size(Fnn), fN_1, fN_2). +7. If (relop__u0 is NE), then: + a. Return $fne_($size(Fnn), fN_1, fN_2). +8. If (relop__u0 is LT), then: + a. Return $flt_($size(Fnn), fN_1, fN_2). +9. If (relop__u0 is GT), then: + a. Return $fgt_($size(Fnn), fN_1, fN_2). +10. If (relop__u0 is LE), then: + a. Return $fle_($size(Fnn), fN_1, fN_2). +11. Assert: Due to validation, (relop__u0 is GE). +12. Return $fge_($size(Fnn), fN_1, fN_2). cvtop__ valtype_u0 valtype_u1 cvtop_u2 val__u4 -1. If ((valtype_u0 is I32) and (valtype_u1 is I64)), then: - a. Let iN be val__u4. - b. If cvtop_u2 is of the case EXTEND, then: - 1) Let (EXTEND sx) be cvtop_u2. - 2) Return [$extend__(32, 64, sx, iN)]. -2. If ((valtype_u0 is I64) and ((valtype_u1 is I32) and (cvtop_u2 is WRAP))), then: - a. Let iN be val__u4. - b. Return [$wrap__(64, 32, iN)]. -3. If the type of valtype_u0 is Fnn, then: +1. If cvtop_u2 is of the case EXTEND, then: + a. Let (EXTEND sx) be cvtop_u2. + b. Let iN be val__u4. + c. If ((valtype_u0 is I32) and (valtype_u1 is I64)), then: + 1) Return [$extend__(32, 64, sx, iN)]. +2. Let iN be val__u4. +3. If ((valtype_u0 is I64) and ((valtype_u1 is I32) and (cvtop_u2 is WRAP))), then: + a. Return [$wrap__(64, 32, iN)]. +4. If the type of valtype_u0 is Fnn, then: a. Let Fnn be valtype_u0. b. If the type of valtype_u1 is Inn, then: 1) Let Inn be valtype_u1. - 2) Let fN be val__u4. - 3) If cvtop_u2 is of the case TRUNC, then: + 2) If cvtop_u2 is of the case TRUNC, then: a) Let (TRUNC sx) be cvtop_u2. - b) Return $list_(val_((Inn : Inn <: valtype)), $trunc__($size(Fnn), $size(Inn), sx, fN)). -4. If ((valtype_u0 is F32) and ((valtype_u1 is F64) and (cvtop_u2 is PROMOTE))), then: - a. Let fN be val__u4. - b. Return $promote__(32, 64, fN). -5. If ((valtype_u0 is F64) and ((valtype_u1 is F32) and (cvtop_u2 is DEMOTE))), then: - a. Let fN be val__u4. - b. Return $demote__(64, 32, fN). -6. If the type of valtype_u1 is Fnn, then: - a. Let Fnn be valtype_u1. - b. If the type of valtype_u0 is Inn, then: - 1) Let Inn be valtype_u0. - 2) Let iN be val__u4. - 3) If cvtop_u2 is of the case CONVERT, then: + b) Let fN be val__u4. + c) Return $list_(val_((Inn : Inn <: valtype)), $trunc__($size(Fnn), $size(Inn), sx, fN)). +5. Let fN be val__u4. +6. If ((valtype_u0 is F32) and ((valtype_u1 is F64) and (cvtop_u2 is PROMOTE))), then: + a. Return $promote__(32, 64, fN). +7. If ((valtype_u0 is F64) and ((valtype_u1 is F32) and (cvtop_u2 is DEMOTE))), then: + a. Return $demote__(64, 32, fN). +8. If the type of valtype_u0 is Inn, then: + a. Let Inn be valtype_u0. + b. If the type of valtype_u1 is Fnn, then: + 1) Let Fnn be valtype_u1. + 2) If cvtop_u2 is of the case CONVERT, then: a) Let (CONVERT sx) be cvtop_u2. b) Return [$convert__($size(Inn), $size(Fnn), sx, iN)]. -7. Assert: Due to validation, (cvtop_u2 is REINTERPRET). -8. If the type of valtype_u1 is Fnn, then: - a. Let Fnn be valtype_u1. - b. If the type of valtype_u0 is Inn, then: - 1) Let Inn be valtype_u0. - 2) Let iN be val__u4. - 3) If ($size(Inn) is $size(Fnn)), then: + 3) If ((cvtop_u2 is REINTERPRET) and ($size(Inn) is $size(Fnn))), then: a) Return [$reinterpret__(Inn, Fnn, iN)]. 9. Assert: Due to validation, the type of valtype_u0 is Fnn. 10. Let Fnn be valtype_u0. 11. Assert: Due to validation, the type of valtype_u1 is Inn. 12. Let Inn be valtype_u1. -13. Let fN be val__u4. +13. Assert: Due to validation, (cvtop_u2 is REINTERPRET). 14. Assert: Due to validation, ($size(Inn) is $size(Fnn)). 15. Return [$reinterpret__(Fnn, Inn, fN)]. @@ -4038,20 +3759,20 @@ instexport fa* ga* ta* ma* (EXPORT name externidx_u0) 6. Return { NAME: name; ADDR: (MEM ma*[x]); }. allocmodule module externaddr* val* -1. Let fa_ex* be $funcs(externaddr*). -2. Let ga_ex* be $globals(externaddr*). -3. Let ma_ex* be $mems(externaddr*). -4. Let ta_ex* be $tables(externaddr*). -5. Assert: Due to validation, module is of the case MODULE. -6. Let (MODULE type_0* import* func^n_func global_1^n_global table_2^n_table mem_3^n_mem elem* data* start? export*) be module. -7. Assert: Due to validation, mem_3 is of the case MEMORY^n_mem. -8. Let (MEMORY memtype)^n_mem be mem_3^n_mem. -9. Assert: Due to validation, table_2 is of the case TABLE^n_table. -10. Let (TABLE tabletype)^n_table be table_2^n_table. -11. Assert: Due to validation, global_1 is of the case GLOBAL^n_global. -12. Let (GLOBAL globaltype expr_1)^n_global be global_1^n_global. -13. Assert: Due to validation, type_0 is of the case TYPE*. -14. Let (TYPE ft)* be type_0*. +1. Assert: Due to validation, module is of the case MODULE. +2. Let (MODULE type_0* import* func^n_func global_1^n_global table_2^n_table mem_3^n_mem elem* data* start? export*) be module. +3. Assert: Due to validation, mem_3 is of the case MEMORY^n_mem. +4. Let (MEMORY memtype)^n_mem be mem_3^n_mem. +5. Assert: Due to validation, table_2 is of the case TABLE^n_table. +6. Let (TABLE tabletype)^n_table be table_2^n_table. +7. Assert: Due to validation, global_1 is of the case GLOBAL^n_global. +8. Let (GLOBAL globaltype expr_1)^n_global be global_1^n_global. +9. Assert: Due to validation, type_0 is of the case TYPE*. +10. Let (TYPE ft)* be type_0*. +11. Let fa_ex* be $funcs(externaddr*). +12. Let ga_ex* be $globals(externaddr*). +13. Let ma_ex* be $mems(externaddr*). +14. Let ta_ex* be $tables(externaddr*). 15. Let fa* be (|s.FUNCS| + i_func)^(i_func t_2^n); MODULE: mm; CODE: func; } be $funcinst(z)[a]. -4. Assert: Due to validation, there are at least k values on the top of the stack. -5. Pop the values val^k from the stack. -6. Assert: Due to validation, func is of the case FUNC. -7. Let (FUNC x local_0* instr*) be func. -8. Assert: Due to validation, local_0 is of the case LOCAL*. -9. Let (LOCAL t)* be local_0*. +4. Assert: Due to validation, func is of the case FUNC. +5. Let (FUNC x local_0* instr*) be func. +6. Assert: Due to validation, local_0 is of the case LOCAL*. +7. Let (LOCAL t)* be local_0*. +8. Assert: Due to validation, there are at least k values on the top of the stack. +9. Pop the values val^k from the stack. 10. Let f be { LOCALS: val^k :: $default_(t)*; MODULE: mm; }. 11. Push the evaluation context (FRAME_ n { f }) to the stack. 12. Enter instr* with label (LABEL_ n { [] }). @@ -11139,277 +10606,184 @@ invsigned_ N i 2. Return j. unop_ numtype_u1 unop__u0 num__u3 -1. If ((unop__u0 is CLZ) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN be num__u3. - c. Return [$iclz_($sizenn(Inn), iN)]. -2. If ((unop__u0 is CTZ) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN be num__u3. - c. Return [$ictz_($sizenn(Inn), iN)]. -3. If ((unop__u0 is POPCNT) and the type of numtype_u1 is Inn), then: +1. If the type of numtype_u1 is Inn, then: a. Let Inn be numtype_u1. b. Let iN be num__u3. - c. Return [$ipopcnt_($sizenn(Inn), iN)]. -4. If the type of numtype_u1 is Inn, then: - a. Let Inn be numtype_u1. - b. Assert: Due to validation, unop__u0 is of the case EXTEND. - c. Let (EXTEND M) be unop__u0. - d. Let iN be num__u3. - e. Return [$extend__(M, $sizenn(Inn), S, $wrap__($sizenn(Inn), M, iN))]. -5. If ((unop__u0 is ABS) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $fabs_($sizenn(Fnn), fN). -6. If ((unop__u0 is NEG) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $fneg_($sizenn(Fnn), fN). -7. If ((unop__u0 is SQRT) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $fsqrt_($sizenn(Fnn), fN). -8. If ((unop__u0 is CEIL) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $fceil_($sizenn(Fnn), fN). -9. If ((unop__u0 is FLOOR) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $ffloor_($sizenn(Fnn), fN). -10. If ((unop__u0 is TRUNC) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $ftrunc_($sizenn(Fnn), fN). + c. If (unop__u0 is CLZ), then: + 1) Return [$iclz_($sizenn(Inn), iN)]. + d. If (unop__u0 is CTZ), then: + 1) Return [$ictz_($sizenn(Inn), iN)]. + e. If (unop__u0 is POPCNT), then: + 1) Return [$ipopcnt_($sizenn(Inn), iN)]. + f. Assert: Due to validation, unop__u0 is of the case EXTEND. + g. Let (EXTEND M) be unop__u0. + h. Return [$extend__(M, $sizenn(Inn), S, $wrap__($sizenn(Inn), M, iN))]. +2. Assert: Due to validation, the type of numtype_u1 is Fnn. +3. Let Fnn be numtype_u1. +4. Let fN be num__u3. +5. If (unop__u0 is ABS), then: + a. Return $fabs_($sizenn(Fnn), fN). +6. If (unop__u0 is NEG), then: + a. Return $fneg_($sizenn(Fnn), fN). +7. If (unop__u0 is SQRT), then: + a. Return $fsqrt_($sizenn(Fnn), fN). +8. If (unop__u0 is CEIL), then: + a. Return $fceil_($sizenn(Fnn), fN). +9. If (unop__u0 is FLOOR), then: + a. Return $ffloor_($sizenn(Fnn), fN). +10. If (unop__u0 is TRUNC), then: + a. Return $ftrunc_($sizenn(Fnn), fN). 11. Assert: Due to validation, (unop__u0 is NEAREST). -12. Assert: Due to validation, the type of numtype_u1 is Fnn. -13. Let Fnn be numtype_u1. -14. Let fN be num__u3. -15. Return $fnearest_($sizenn(Fnn), fN). +12. Return $fnearest_($sizenn(Fnn), fN). binop_ numtype_u1 binop__u0 num__u3 num__u5 -1. If ((binop__u0 is ADD) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$iadd_($sizenn(Inn), iN_1, iN_2)]. -2. If ((binop__u0 is SUB) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$isub_($sizenn(Inn), iN_1, iN_2)]. -3. If ((binop__u0 is MUL) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$imul_($sizenn(Inn), iN_1, iN_2)]. -4. If the type of numtype_u1 is Inn, then: +1. If the type of numtype_u1 is Inn, then: a. Let Inn be numtype_u1. b. Let iN_1 be num__u3. c. Let iN_2 be num__u5. - d. If binop__u0 is of the case DIV, then: + d. If (binop__u0 is ADD), then: + 1) Return [$iadd_($sizenn(Inn), iN_1, iN_2)]. + e. If (binop__u0 is SUB), then: + 1) Return [$isub_($sizenn(Inn), iN_1, iN_2)]. + f. If (binop__u0 is MUL), then: + 1) Return [$imul_($sizenn(Inn), iN_1, iN_2)]. + g. If binop__u0 is of the case DIV, then: 1) Let (DIV sx) be binop__u0. 2) Return $list_(num_((Inn : Inn <: numtype)), $idiv_($sizenn(Inn), sx, iN_1, iN_2)). - e. If binop__u0 is of the case REM, then: + h. If binop__u0 is of the case REM, then: 1) Let (REM sx) be binop__u0. 2) Return $list_(num_((Inn : Inn <: numtype)), $irem_($sizenn(Inn), sx, iN_1, iN_2)). -5. If ((binop__u0 is AND) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$iand_($sizenn(Inn), iN_1, iN_2)]. -6. If ((binop__u0 is OR) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$ior_($sizenn(Inn), iN_1, iN_2)]. -7. If ((binop__u0 is XOR) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$ixor_($sizenn(Inn), iN_1, iN_2)]. -8. If ((binop__u0 is SHL) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$ishl_($sizenn(Inn), iN_1, iN_2)]. -9. If the type of numtype_u1 is Inn, then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. If binop__u0 is of the case SHR, then: + i. If (binop__u0 is AND), then: + 1) Return [$iand_($sizenn(Inn), iN_1, iN_2)]. + j. If (binop__u0 is OR), then: + 1) Return [$ior_($sizenn(Inn), iN_1, iN_2)]. + k. If (binop__u0 is XOR), then: + 1) Return [$ixor_($sizenn(Inn), iN_1, iN_2)]. + l. If (binop__u0 is SHL), then: + 1) Return [$ishl_($sizenn(Inn), iN_1, iN_2)]. + m. If binop__u0 is of the case SHR, then: 1) Let (SHR sx) be binop__u0. 2) Return [$ishr_($sizenn(Inn), sx, iN_1, iN_2)]. -10. If ((binop__u0 is ROTL) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$irotl_($sizenn(Inn), iN_1, iN_2)]. -11. If ((binop__u0 is ROTR) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$irotr_($sizenn(Inn), iN_1, iN_2)]. -12. If ((binop__u0 is ADD) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fadd_($sizenn(Fnn), fN_1, fN_2). -13. If ((binop__u0 is SUB) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fsub_($sizenn(Fnn), fN_1, fN_2). -14. If ((binop__u0 is MUL) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fmul_($sizenn(Fnn), fN_1, fN_2). -15. If ((binop__u0 is DIV) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fdiv_($sizenn(Fnn), fN_1, fN_2). -16. If ((binop__u0 is MIN) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fmin_($sizenn(Fnn), fN_1, fN_2). -17. If ((binop__u0 is MAX) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fmax_($sizenn(Fnn), fN_1, fN_2). -18. Assert: Due to validation, (binop__u0 is COPYSIGN). -19. Assert: Due to validation, the type of numtype_u1 is Fnn. -20. Let Fnn be numtype_u1. -21. Let fN_1 be num__u3. -22. Let fN_2 be num__u5. -23. Return $fcopysign_($sizenn(Fnn), fN_1, fN_2). + n. If (binop__u0 is ROTL), then: + 1) Return [$irotl_($sizenn(Inn), iN_1, iN_2)]. + o. If (binop__u0 is ROTR), then: + 1) Return [$irotr_($sizenn(Inn), iN_1, iN_2)]. +2. Assert: Due to validation, the type of numtype_u1 is Fnn. +3. Let Fnn be numtype_u1. +4. Let fN_1 be num__u3. +5. Let fN_2 be num__u5. +6. If (binop__u0 is ADD), then: + a. Return $fadd_($sizenn(Fnn), fN_1, fN_2). +7. If (binop__u0 is SUB), then: + a. Return $fsub_($sizenn(Fnn), fN_1, fN_2). +8. If (binop__u0 is MUL), then: + a. Return $fmul_($sizenn(Fnn), fN_1, fN_2). +9. If (binop__u0 is DIV), then: + a. Return $fdiv_($sizenn(Fnn), fN_1, fN_2). +10. If (binop__u0 is MIN), then: + a. Return $fmin_($sizenn(Fnn), fN_1, fN_2). +11. If (binop__u0 is MAX), then: + a. Return $fmax_($sizenn(Fnn), fN_1, fN_2). +12. Assert: Due to validation, (binop__u0 is COPYSIGN). +13. Return $fcopysign_($sizenn(Fnn), fN_1, fN_2). testop_ Inn EQZ iN 1. Return $ieqz_($sizenn(Inn), iN). relop_ numtype_u1 relop__u0 num__u3 num__u5 -1. If ((relop__u0 is EQ) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return $ieq_($sizenn(Inn), iN_1, iN_2). -2. If ((relop__u0 is NE) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return $ine_($sizenn(Inn), iN_1, iN_2). -3. If the type of numtype_u1 is Inn, then: +1. If the type of numtype_u1 is Inn, then: a. Let Inn be numtype_u1. b. Let iN_1 be num__u3. c. Let iN_2 be num__u5. - d. If relop__u0 is of the case LT, then: + d. If (relop__u0 is EQ), then: + 1) Return $ieq_($sizenn(Inn), iN_1, iN_2). + e. If (relop__u0 is NE), then: + 1) Return $ine_($sizenn(Inn), iN_1, iN_2). + f. If relop__u0 is of the case LT, then: 1) Let (LT sx) be relop__u0. 2) Return $ilt_($sizenn(Inn), sx, iN_1, iN_2). - e. If relop__u0 is of the case GT, then: + g. If relop__u0 is of the case GT, then: 1) Let (GT sx) be relop__u0. 2) Return $igt_($sizenn(Inn), sx, iN_1, iN_2). - f. If relop__u0 is of the case LE, then: + h. If relop__u0 is of the case LE, then: 1) Let (LE sx) be relop__u0. 2) Return $ile_($sizenn(Inn), sx, iN_1, iN_2). - g. If relop__u0 is of the case GE, then: + i. If relop__u0 is of the case GE, then: 1) Let (GE sx) be relop__u0. 2) Return $ige_($sizenn(Inn), sx, iN_1, iN_2). -4. If ((relop__u0 is EQ) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $feq_($sizenn(Fnn), fN_1, fN_2). -5. If ((relop__u0 is NE) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fne_($sizenn(Fnn), fN_1, fN_2). -6. If ((relop__u0 is LT) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $flt_($sizenn(Fnn), fN_1, fN_2). -7. If ((relop__u0 is GT) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fgt_($sizenn(Fnn), fN_1, fN_2). -8. If ((relop__u0 is LE) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fle_($sizenn(Fnn), fN_1, fN_2). -9. Assert: Due to validation, (relop__u0 is GE). -10. Assert: Due to validation, the type of numtype_u1 is Fnn. -11. Let Fnn be numtype_u1. -12. Let fN_1 be num__u3. -13. Let fN_2 be num__u5. -14. Return $fge_($sizenn(Fnn), fN_1, fN_2). +2. Assert: Due to validation, the type of numtype_u1 is Fnn. +3. Let Fnn be numtype_u1. +4. Let fN_1 be num__u3. +5. Let fN_2 be num__u5. +6. If (relop__u0 is EQ), then: + a. Return $feq_($sizenn(Fnn), fN_1, fN_2). +7. If (relop__u0 is NE), then: + a. Return $fne_($sizenn(Fnn), fN_1, fN_2). +8. If (relop__u0 is LT), then: + a. Return $flt_($sizenn(Fnn), fN_1, fN_2). +9. If (relop__u0 is GT), then: + a. Return $fgt_($sizenn(Fnn), fN_1, fN_2). +10. If (relop__u0 is LE), then: + a. Return $fle_($sizenn(Fnn), fN_1, fN_2). +11. Assert: Due to validation, (relop__u0 is GE). +12. Return $fge_($sizenn(Fnn), fN_1, fN_2). cvtop__ numtype_u1 numtype_u4 cvtop_u0 num__u3 1. If the type of numtype_u1 is Inn, then: a. Let Inn_1 be numtype_u1. b. If the type of numtype_u4 is Inn, then: 1) Let Inn_2 be numtype_u4. - 2) Let iN_1 be num__u3. - 3) If cvtop_u0 is of the case EXTEND, then: + 2) If cvtop_u0 is of the case EXTEND, then: a) Let (EXTEND sx) be cvtop_u0. - b) Return [$extend__($sizenn1(Inn_1), $sizenn2(Inn_2), sx, iN_1)]. -2. If ((cvtop_u0 is WRAP) and the type of numtype_u1 is Inn), then: - a. Let Inn_1 be numtype_u1. - b. If the type of numtype_u4 is Inn, then: - 1) Let Inn_2 be numtype_u4. - 2) Let iN_1 be num__u3. - 3) Return [$wrap__($sizenn1(Inn_1), $sizenn2(Inn_2), iN_1)]. -3. If the type of numtype_u1 is Fnn, then: + b) Let iN_1 be num__u3. + c) Return [$extend__($sizenn1(Inn_1), $sizenn2(Inn_2), sx, iN_1)]. + 3) Let iN_1 be num__u3. + 4) If (cvtop_u0 is WRAP), then: + a) Return [$wrap__($sizenn1(Inn_1), $sizenn2(Inn_2), iN_1)]. +2. If the type of numtype_u1 is Fnn, then: a. Let Fnn_1 be numtype_u1. b. If the type of numtype_u4 is Inn, then: 1) Let Inn_2 be numtype_u4. - 2) Let fN_1 be num__u3. - 3) If cvtop_u0 is of the case TRUNC, then: + 2) If cvtop_u0 is of the case TRUNC, then: a) Let (TRUNC sx) be cvtop_u0. - b) Return $list_(num_((Inn_2 : Inn <: numtype)), $trunc__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, fN_1)). - 4) If cvtop_u0 is of the case TRUNC_SAT, then: + b) Let fN_1 be num__u3. + c) Return $list_(num_((Inn_2 : Inn <: numtype)), $trunc__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, fN_1)). + 3) If cvtop_u0 is of the case TRUNC_SAT, then: a) Let (TRUNC_SAT sx) be cvtop_u0. - b) Return $list_(num_((Inn_2 : Inn <: numtype)), $trunc_sat__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, fN_1)). -4. If the type of numtype_u4 is Fnn, then: - a. Let Fnn_2 be numtype_u4. - b. If the type of numtype_u1 is Inn, then: - 1) Let Inn_1 be numtype_u1. - 2) Let iN_1 be num__u3. - 3) If cvtop_u0 is of the case CONVERT, then: + b) Let fN_1 be num__u3. + c) Return $list_(num_((Inn_2 : Inn <: numtype)), $trunc_sat__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, fN_1)). +3. If the type of numtype_u1 is Inn, then: + a. Let Inn_1 be numtype_u1. + b. If the type of numtype_u4 is Fnn, then: + 1) Let Fnn_2 be numtype_u4. + 2) If cvtop_u0 is of the case CONVERT, then: a) Let (CONVERT sx) be cvtop_u0. - b) Return [$convert__($sizenn1(Inn_1), $sizenn2(Fnn_2), sx, iN_1)]. -5. If ((cvtop_u0 is PROMOTE) and the type of numtype_u1 is Fnn), then: + b) Let iN_1 be num__u3. + c) Return [$convert__($sizenn1(Inn_1), $sizenn2(Fnn_2), sx, iN_1)]. +4. If the type of numtype_u1 is Fnn, then: a. Let Fnn_1 be numtype_u1. b. If the type of numtype_u4 is Fnn, then: 1) Let Fnn_2 be numtype_u4. 2) Let fN_1 be num__u3. - 3) Return $promote__($sizenn1(Fnn_1), $sizenn2(Fnn_2), fN_1). -6. If ((cvtop_u0 is DEMOTE) and the type of numtype_u1 is Fnn), then: - a. Let Fnn_1 be numtype_u1. + 3) If (cvtop_u0 is PROMOTE), then: + a) Return $promote__($sizenn1(Fnn_1), $sizenn2(Fnn_2), fN_1). + 4) If (cvtop_u0 is DEMOTE), then: + a) Return $demote__($sizenn1(Fnn_1), $sizenn2(Fnn_2), fN_1). +5. If the type of numtype_u1 is Inn, then: + a. Let Inn_1 be numtype_u1. b. If the type of numtype_u4 is Fnn, then: 1) Let Fnn_2 be numtype_u4. - 2) Let fN_1 be num__u3. - 3) Return $demote__($sizenn1(Fnn_1), $sizenn2(Fnn_2), fN_1). -7. Assert: Due to validation, (cvtop_u0 is REINTERPRET). -8. If the type of numtype_u4 is Fnn, then: - a. Let Fnn_2 be numtype_u4. - b. If the type of numtype_u1 is Inn, then: - 1) Let Inn_1 be numtype_u1. 2) Let iN_1 be num__u3. - 3) If ($size(Inn_1) is $size(Fnn_2)), then: + 3) If ((cvtop_u0 is REINTERPRET) and ($size(Inn_1) is $size(Fnn_2))), then: a) Return [$reinterpret__(Inn_1, Fnn_2, iN_1)]. -9. Assert: Due to validation, the type of numtype_u1 is Fnn. -10. Let Fnn_1 be numtype_u1. -11. Assert: Due to validation, the type of numtype_u4 is Inn. -12. Let Inn_2 be numtype_u4. -13. Let fN_1 be num__u3. -14. Assert: Due to validation, ($size(Fnn_1) is $size(Inn_2)). -15. Return [$reinterpret__(Fnn_1, Inn_2, fN_1)]. +6. Assert: Due to validation, the type of numtype_u1 is Fnn. +7. Let Fnn_1 be numtype_u1. +8. Assert: Due to validation, the type of numtype_u4 is Inn. +9. Let Inn_2 be numtype_u4. +10. Let fN_1 be num__u3. +11. Assert: Due to validation, (cvtop_u0 is REINTERPRET). +12. Assert: Due to validation, ($size(Fnn_1) is $size(Inn_2)). +13. Return [$reinterpret__(Fnn_1, Inn_2, fN_1)]. invibytes_ N b* 1. Let n be $ibytes__1^-1(N, b*). @@ -11456,322 +10830,288 @@ vvbinop_ V128 vvbinop_u0 v128_1 v128_2 4. Assert: Due to validation, (vvbinop_u0 is XOR). 5. Return $ixor_($size(V128), v128_1, v128_2). -vvternop_ V128 BITSELECT v128_1 v128_2 v128_3 -1. Return $ibitselect_($size(V128), v128_1, v128_2, v128_3). - -vunop_ (lanetype_u1 X M) vunop__u0 v128_1 -1. If ((vunop__u0 is ABS) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Let lane_1* be $lanes_((Jnn X M), v128_1). - c. Let v128 be $invlanes_((Jnn X M), $iabs_($lsizenn(Jnn), lane_1)*). - d. Return [v128]. -2. If ((vunop__u0 is NEG) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Let lane_1* be $lanes_((Jnn X M), v128_1). - c. Let v128 be $invlanes_((Jnn X M), $ineg_($lsizenn(Jnn), lane_1)*). - d. Return [v128]. -3. If ((vunop__u0 is POPCNT) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Let lane_1* be $lanes_((Jnn X M), v128_1). - c. Let v128 be $invlanes_((Jnn X M), $ipopcnt_($lsizenn(Jnn), lane_1)*). - d. Return [v128]. -4. If ((vunop__u0 is ABS) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fabs_($sizenn(Fnn), lane_1)*). - d. Let v128* be $invlanes_((Fnn X M), lane*)*. - e. Return v128*. -5. If ((vunop__u0 is NEG) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fneg_($sizenn(Fnn), lane_1)*). - d. Let v128* be $invlanes_((Fnn X M), lane*)*. - e. Return v128*. -6. If ((vunop__u0 is SQRT) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fsqrt_($sizenn(Fnn), lane_1)*). - d. Let v128* be $invlanes_((Fnn X M), lane*)*. - e. Return v128*. -7. If ((vunop__u0 is CEIL) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fceil_($sizenn(Fnn), lane_1)*). - d. Let v128* be $invlanes_((Fnn X M), lane*)*. - e. Return v128*. -8. If ((vunop__u0 is FLOOR) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $ffloor_($sizenn(Fnn), lane_1)*). - d. Let v128* be $invlanes_((Fnn X M), lane*)*. - e. Return v128*. -9. If ((vunop__u0 is TRUNC) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $ftrunc_($sizenn(Fnn), lane_1)*). - d. Let v128* be $invlanes_((Fnn X M), lane*)*. - e. Return v128*. +vvternop_ V128 BITSELECT v128_1 v128_2 v128_3 +1. Return $ibitselect_($size(V128), v128_1, v128_2, v128_3). + +vunop_ (lanetype_u1 X M) vunop__u0 v128_1 +1. If the type of lanetype_u1 is Jnn, then: + a. Let Jnn be lanetype_u1. + b. If (vunop__u0 is ABS), then: + 1) Let lane_1* be $lanes_((Jnn X M), v128_1). + 2) Let v128 be $invlanes_((Jnn X M), $iabs_($lsizenn(Jnn), lane_1)*). + 3) Return [v128]. + c. If (vunop__u0 is NEG), then: + 1) Let lane_1* be $lanes_((Jnn X M), v128_1). + 2) Let v128 be $invlanes_((Jnn X M), $ineg_($lsizenn(Jnn), lane_1)*). + 3) Return [v128]. + d. If (vunop__u0 is POPCNT), then: + 1) Let lane_1* be $lanes_((Jnn X M), v128_1). + 2) Let v128 be $invlanes_((Jnn X M), $ipopcnt_($lsizenn(Jnn), lane_1)*). + 3) Return [v128]. +2. Assert: Due to validation, the type of lanetype_u1 is Fnn. +3. Let Fnn be lanetype_u1. +4. If (vunop__u0 is ABS), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fabs_($sizenn(Fnn), lane_1)*). + c. Let v128* be $invlanes_((Fnn X M), lane*)*. + d. Return v128*. +5. If (vunop__u0 is NEG), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fneg_($sizenn(Fnn), lane_1)*). + c. Let v128* be $invlanes_((Fnn X M), lane*)*. + d. Return v128*. +6. If (vunop__u0 is SQRT), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fsqrt_($sizenn(Fnn), lane_1)*). + c. Let v128* be $invlanes_((Fnn X M), lane*)*. + d. Return v128*. +7. If (vunop__u0 is CEIL), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fceil_($sizenn(Fnn), lane_1)*). + c. Let v128* be $invlanes_((Fnn X M), lane*)*. + d. Return v128*. +8. If (vunop__u0 is FLOOR), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $ffloor_($sizenn(Fnn), lane_1)*). + c. Let v128* be $invlanes_((Fnn X M), lane*)*. + d. Return v128*. +9. If (vunop__u0 is TRUNC), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $ftrunc_($sizenn(Fnn), lane_1)*). + c. Let v128* be $invlanes_((Fnn X M), lane*)*. + d. Return v128*. 10. Assert: Due to validation, (vunop__u0 is NEAREST). -11. Assert: Due to validation, the type of lanetype_u1 is Fnn. -12. Let Fnn be lanetype_u1. -13. Let lane_1* be $lanes_((Fnn X M), v128_1). -14. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fnearest_($sizenn(Fnn), lane_1)*). -15. Let v128* be $invlanes_((Fnn X M), lane*)*. -16. Return v128*. +11. Let lane_1* be $lanes_((Fnn X M), v128_1). +12. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fnearest_($sizenn(Fnn), lane_1)*). +13. Let v128* be $invlanes_((Fnn X M), lane*)*. +14. Return v128*. vbinop_ (lanetype_u1 X M) vbinop__u0 v128_1 v128_2 -1. If ((vbinop__u0 is ADD) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Let lane_1* be $lanes_((Jnn X M), v128_1). - c. Let lane_2* be $lanes_((Jnn X M), v128_2). - d. Let v128 be $invlanes_((Jnn X M), $iadd_($lsizenn(Jnn), lane_1, lane_2)*). - e. Return [v128]. -2. If ((vbinop__u0 is SUB) and the type of lanetype_u1 is Jnn), then: +1. If the type of lanetype_u1 is Jnn, then: a. Let Jnn be lanetype_u1. - b. Let lane_1* be $lanes_((Jnn X M), v128_1). - c. Let lane_2* be $lanes_((Jnn X M), v128_2). - d. Let v128 be $invlanes_((Jnn X M), $isub_($lsizenn(Jnn), lane_1, lane_2)*). - e. Return [v128]. -3. If the type of lanetype_u1 is Jnn, then: - a. Let Jnn be lanetype_u1. - b. If vbinop__u0 is of the case MIN, then: + b. If (vbinop__u0 is ADD), then: + 1) Let lane_1* be $lanes_((Jnn X M), v128_1). + 2) Let lane_2* be $lanes_((Jnn X M), v128_2). + 3) Let v128 be $invlanes_((Jnn X M), $iadd_($lsizenn(Jnn), lane_1, lane_2)*). + 4) Return [v128]. + c. If (vbinop__u0 is SUB), then: + 1) Let lane_1* be $lanes_((Jnn X M), v128_1). + 2) Let lane_2* be $lanes_((Jnn X M), v128_2). + 3) Let v128 be $invlanes_((Jnn X M), $isub_($lsizenn(Jnn), lane_1, lane_2)*). + 4) Return [v128]. + d. If vbinop__u0 is of the case MIN, then: 1) Let (MIN sx) be vbinop__u0. 2) Let lane_1* be $lanes_((Jnn X M), v128_1). 3) Let lane_2* be $lanes_((Jnn X M), v128_2). 4) Let v128 be $invlanes_((Jnn X M), $imin_($lsizenn(Jnn), sx, lane_1, lane_2)*). 5) Return [v128]. - c. If vbinop__u0 is of the case MAX, then: + e. If vbinop__u0 is of the case MAX, then: 1) Let (MAX sx) be vbinop__u0. 2) Let lane_1* be $lanes_((Jnn X M), v128_1). 3) Let lane_2* be $lanes_((Jnn X M), v128_2). 4) Let v128 be $invlanes_((Jnn X M), $imax_($lsizenn(Jnn), sx, lane_1, lane_2)*). 5) Return [v128]. - d. If vbinop__u0 is of the case ADD_SAT, then: + f. If vbinop__u0 is of the case ADD_SAT, then: 1) Let (ADD_SAT sx) be vbinop__u0. 2) Let lane_1* be $lanes_((Jnn X M), v128_1). 3) Let lane_2* be $lanes_((Jnn X M), v128_2). 4) Let v128 be $invlanes_((Jnn X M), $iadd_sat_($lsizenn(Jnn), sx, lane_1, lane_2)*). 5) Return [v128]. - e. If vbinop__u0 is of the case SUB_SAT, then: + g. If vbinop__u0 is of the case SUB_SAT, then: 1) Let (SUB_SAT sx) be vbinop__u0. 2) Let lane_1* be $lanes_((Jnn X M), v128_1). 3) Let lane_2* be $lanes_((Jnn X M), v128_2). 4) Let v128 be $invlanes_((Jnn X M), $isub_sat_($lsizenn(Jnn), sx, lane_1, lane_2)*). 5) Return [v128]. -4. If ((vbinop__u0 is MUL) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Let lane_1* be $lanes_((Jnn X M), v128_1). - c. Let lane_2* be $lanes_((Jnn X M), v128_2). - d. Let v128 be $invlanes_((Jnn X M), $imul_($lsizenn(Jnn), lane_1, lane_2)*). - e. Return [v128]. -5. If ((vbinop__u0 is (AVGRU)) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Let lane_1* be $lanes_((Jnn X M), v128_1). - c. Let lane_2* be $lanes_((Jnn X M), v128_2). - d. Let v128 be $invlanes_((Jnn X M), $iavgr_($lsizenn(Jnn), U, lane_1, lane_2)*). - e. Return [v128]. -6. If ((vbinop__u0 is (Q15MULR_SATS)) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Let lane_1* be $lanes_((Jnn X M), v128_1). - c. Let lane_2* be $lanes_((Jnn X M), v128_2). - d. Let v128 be $invlanes_((Jnn X M), $iq15mulr_sat_($lsizenn(Jnn), S, lane_1, lane_2)*). - e. Return [v128]. -7. If ((vbinop__u0 is ADD) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fadd_($sizenn(Fnn), lane_1, lane_2)*). - e. Let v128* be $invlanes_((Fnn X M), lane*)*. - f. Return v128*. -8. If ((vbinop__u0 is SUB) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fsub_($sizenn(Fnn), lane_1, lane_2)*). - e. Let v128* be $invlanes_((Fnn X M), lane*)*. - f. Return v128*. -9. If ((vbinop__u0 is MUL) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fmul_($sizenn(Fnn), lane_1, lane_2)*). - e. Let v128* be $invlanes_((Fnn X M), lane*)*. - f. Return v128*. -10. If ((vbinop__u0 is DIV) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fdiv_($sizenn(Fnn), lane_1, lane_2)*). - e. Let v128* be $invlanes_((Fnn X M), lane*)*. - f. Return v128*. -11. If ((vbinop__u0 is MIN) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fmin_($sizenn(Fnn), lane_1, lane_2)*). - e. Let v128* be $invlanes_((Fnn X M), lane*)*. - f. Return v128*. -12. If ((vbinop__u0 is MAX) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fmax_($sizenn(Fnn), lane_1, lane_2)*). - e. Let v128* be $invlanes_((Fnn X M), lane*)*. - f. Return v128*. -13. If ((vbinop__u0 is PMIN) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fpmin_($sizenn(Fnn), lane_1, lane_2)*). - e. Let v128* be $invlanes_((Fnn X M), lane*)*. - f. Return v128*. -14. Assert: Due to validation, (vbinop__u0 is PMAX). -15. Assert: Due to validation, the type of lanetype_u1 is Fnn. -16. Let Fnn be lanetype_u1. -17. Let lane_1* be $lanes_((Fnn X M), v128_1). -18. Let lane_2* be $lanes_((Fnn X M), v128_2). -19. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fpmax_($sizenn(Fnn), lane_1, lane_2)*). -20. Let v128* be $invlanes_((Fnn X M), lane*)*. -21. Return v128*. + h. If (vbinop__u0 is MUL), then: + 1) Let lane_1* be $lanes_((Jnn X M), v128_1). + 2) Let lane_2* be $lanes_((Jnn X M), v128_2). + 3) Let v128 be $invlanes_((Jnn X M), $imul_($lsizenn(Jnn), lane_1, lane_2)*). + 4) Return [v128]. + i. If (vbinop__u0 is (AVGRU)), then: + 1) Let lane_1* be $lanes_((Jnn X M), v128_1). + 2) Let lane_2* be $lanes_((Jnn X M), v128_2). + 3) Let v128 be $invlanes_((Jnn X M), $iavgr_($lsizenn(Jnn), U, lane_1, lane_2)*). + 4) Return [v128]. + j. If (vbinop__u0 is (Q15MULR_SATS)), then: + 1) Let lane_1* be $lanes_((Jnn X M), v128_1). + 2) Let lane_2* be $lanes_((Jnn X M), v128_2). + 3) Let v128 be $invlanes_((Jnn X M), $iq15mulr_sat_($lsizenn(Jnn), S, lane_1, lane_2)*). + 4) Return [v128]. +2. Assert: Due to validation, the type of lanetype_u1 is Fnn. +3. Let Fnn be lanetype_u1. +4. If (vbinop__u0 is ADD), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fadd_($sizenn(Fnn), lane_1, lane_2)*). + d. Let v128* be $invlanes_((Fnn X M), lane*)*. + e. Return v128*. +5. If (vbinop__u0 is SUB), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fsub_($sizenn(Fnn), lane_1, lane_2)*). + d. Let v128* be $invlanes_((Fnn X M), lane*)*. + e. Return v128*. +6. If (vbinop__u0 is MUL), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fmul_($sizenn(Fnn), lane_1, lane_2)*). + d. Let v128* be $invlanes_((Fnn X M), lane*)*. + e. Return v128*. +7. If (vbinop__u0 is DIV), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fdiv_($sizenn(Fnn), lane_1, lane_2)*). + d. Let v128* be $invlanes_((Fnn X M), lane*)*. + e. Return v128*. +8. If (vbinop__u0 is MIN), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fmin_($sizenn(Fnn), lane_1, lane_2)*). + d. Let v128* be $invlanes_((Fnn X M), lane*)*. + e. Return v128*. +9. If (vbinop__u0 is MAX), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fmax_($sizenn(Fnn), lane_1, lane_2)*). + d. Let v128* be $invlanes_((Fnn X M), lane*)*. + e. Return v128*. +10. If (vbinop__u0 is PMIN), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fpmin_($sizenn(Fnn), lane_1, lane_2)*). + d. Let v128* be $invlanes_((Fnn X M), lane*)*. + e. Return v128*. +11. Assert: Due to validation, (vbinop__u0 is PMAX). +12. Let lane_1* be $lanes_((Fnn X M), v128_1). +13. Let lane_2* be $lanes_((Fnn X M), v128_2). +14. Let lane** be $setproduct_(lane_((Fnn : Fnn <: lanetype)), $fpmax_($sizenn(Fnn), lane_1, lane_2)*). +15. Let v128* be $invlanes_((Fnn X M), lane*)*. +16. Return v128*. vrelop_ (lanetype_u1 X M) vrelop__u0 v128_1 v128_2 -1. If ((vrelop__u0 is EQ) and the type of lanetype_u1 is Jnn), then: +1. If the type of lanetype_u1 is Jnn, then: a. Let Jnn be lanetype_u1. - b. Let lane_1* be $lanes_((Jnn X M), v128_1). - c. Let lane_2* be $lanes_((Jnn X M), v128_2). - d. Let lane_3* be $extend__(1, $lsizenn(Jnn), S, $ieq_($lsizenn(Jnn), lane_1, lane_2))*. - e. Let v128 be $invlanes_((Jnn X M), lane_3*). - f. Return v128. -2. If ((vrelop__u0 is NE) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Let lane_1* be $lanes_((Jnn X M), v128_1). - c. Let lane_2* be $lanes_((Jnn X M), v128_2). - d. Let lane_3* be $extend__(1, $lsizenn(Jnn), S, $ine_($lsizenn(Jnn), lane_1, lane_2))*. - e. Let v128 be $invlanes_((Jnn X M), lane_3*). - f. Return v128. -3. If the type of lanetype_u1 is Jnn, then: - a. Let Jnn be lanetype_u1. - b. If vrelop__u0 is of the case LT, then: + b. If (vrelop__u0 is EQ), then: + 1) Let lane_1* be $lanes_((Jnn X M), v128_1). + 2) Let lane_2* be $lanes_((Jnn X M), v128_2). + 3) Let lane_3* be $extend__(1, $lsizenn(Jnn), S, $ieq_($lsizenn(Jnn), lane_1, lane_2))*. + 4) Let v128 be $invlanes_((Jnn X M), lane_3*). + 5) Return v128. + c. If (vrelop__u0 is NE), then: + 1) Let lane_1* be $lanes_((Jnn X M), v128_1). + 2) Let lane_2* be $lanes_((Jnn X M), v128_2). + 3) Let lane_3* be $extend__(1, $lsizenn(Jnn), S, $ine_($lsizenn(Jnn), lane_1, lane_2))*. + 4) Let v128 be $invlanes_((Jnn X M), lane_3*). + 5) Return v128. + d. If vrelop__u0 is of the case LT, then: 1) Let (LT sx) be vrelop__u0. 2) Let lane_1* be $lanes_((Jnn X M), v128_1). 3) Let lane_2* be $lanes_((Jnn X M), v128_2). 4) Let lane_3* be $extend__(1, $lsizenn(Jnn), S, $ilt_($lsizenn(Jnn), sx, lane_1, lane_2))*. 5) Let v128 be $invlanes_((Jnn X M), lane_3*). 6) Return v128. - c. If vrelop__u0 is of the case GT, then: + e. If vrelop__u0 is of the case GT, then: 1) Let (GT sx) be vrelop__u0. 2) Let lane_1* be $lanes_((Jnn X M), v128_1). 3) Let lane_2* be $lanes_((Jnn X M), v128_2). 4) Let lane_3* be $extend__(1, $lsizenn(Jnn), S, $igt_($lsizenn(Jnn), sx, lane_1, lane_2))*. 5) Let v128 be $invlanes_((Jnn X M), lane_3*). 6) Return v128. - d. If vrelop__u0 is of the case LE, then: + f. If vrelop__u0 is of the case LE, then: 1) Let (LE sx) be vrelop__u0. 2) Let lane_1* be $lanes_((Jnn X M), v128_1). 3) Let lane_2* be $lanes_((Jnn X M), v128_2). 4) Let lane_3* be $extend__(1, $lsizenn(Jnn), S, $ile_($lsizenn(Jnn), sx, lane_1, lane_2))*. 5) Let v128 be $invlanes_((Jnn X M), lane_3*). 6) Return v128. - e. If vrelop__u0 is of the case GE, then: + g. If vrelop__u0 is of the case GE, then: 1) Let (GE sx) be vrelop__u0. 2) Let lane_1* be $lanes_((Jnn X M), v128_1). 3) Let lane_2* be $lanes_((Jnn X M), v128_2). 4) Let lane_3* be $extend__(1, $lsizenn(Jnn), S, $ige_($lsizenn(Jnn), sx, lane_1, lane_2))*. 5) Let v128 be $invlanes_((Jnn X M), lane_3*). 6) Return v128. -4. If ((vrelop__u0 is EQ) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let Inn be $isize^-1($size(Fnn)). - e. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $feq_($sizenn(Fnn), lane_1, lane_2))*. - f. Let v128 be $invlanes_((Inn X M), lane_3*). - g. Return v128. -5. If ((vrelop__u0 is NE) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let Inn be $isize^-1($size(Fnn)). - e. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $fne_($sizenn(Fnn), lane_1, lane_2))*. - f. Let v128 be $invlanes_((Inn X M), lane_3*). - g. Return v128. -6. If ((vrelop__u0 is LT) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let Inn be $isize^-1($size(Fnn)). - e. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $flt_($sizenn(Fnn), lane_1, lane_2))*. - f. Let v128 be $invlanes_((Inn X M), lane_3*). - g. Return v128. -7. If ((vrelop__u0 is GT) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let Inn be $isize^-1($size(Fnn)). - e. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $fgt_($sizenn(Fnn), lane_1, lane_2))*. - f. Let v128 be $invlanes_((Inn X M), lane_3*). - g. Return v128. -8. If ((vrelop__u0 is LE) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Let lane_1* be $lanes_((Fnn X M), v128_1). - c. Let lane_2* be $lanes_((Fnn X M), v128_2). - d. Let Inn be $isize^-1($size(Fnn)). - e. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $fle_($sizenn(Fnn), lane_1, lane_2))*. - f. Let v128 be $invlanes_((Inn X M), lane_3*). - g. Return v128. +2. Assert: Due to validation, the type of lanetype_u1 is Fnn. +3. Let Fnn be lanetype_u1. +4. If (vrelop__u0 is EQ), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let Inn be $isize^-1($size(Fnn)). + d. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $feq_($sizenn(Fnn), lane_1, lane_2))*. + e. Let v128 be $invlanes_((Inn X M), lane_3*). + f. Return v128. +5. If (vrelop__u0 is NE), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let Inn be $isize^-1($size(Fnn)). + d. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $fne_($sizenn(Fnn), lane_1, lane_2))*. + e. Let v128 be $invlanes_((Inn X M), lane_3*). + f. Return v128. +6. If (vrelop__u0 is LT), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let Inn be $isize^-1($size(Fnn)). + d. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $flt_($sizenn(Fnn), lane_1, lane_2))*. + e. Let v128 be $invlanes_((Inn X M), lane_3*). + f. Return v128. +7. If (vrelop__u0 is GT), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let Inn be $isize^-1($size(Fnn)). + d. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $fgt_($sizenn(Fnn), lane_1, lane_2))*. + e. Let v128 be $invlanes_((Inn X M), lane_3*). + f. Return v128. +8. If (vrelop__u0 is LE), then: + a. Let lane_1* be $lanes_((Fnn X M), v128_1). + b. Let lane_2* be $lanes_((Fnn X M), v128_2). + c. Let Inn be $isize^-1($size(Fnn)). + d. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $fle_($sizenn(Fnn), lane_1, lane_2))*. + e. Let v128 be $invlanes_((Inn X M), lane_3*). + f. Return v128. 9. Assert: Due to validation, (vrelop__u0 is GE). -10. Assert: Due to validation, the type of lanetype_u1 is Fnn. -11. Let Fnn be lanetype_u1. -12. Let lane_1* be $lanes_((Fnn X M), v128_1). -13. Let lane_2* be $lanes_((Fnn X M), v128_2). -14. Let Inn be $isize^-1($size(Fnn)). -15. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $fge_($sizenn(Fnn), lane_1, lane_2))*. -16. Let v128 be $invlanes_((Inn X M), lane_3*). -17. Return v128. +10. Let lane_1* be $lanes_((Fnn X M), v128_1). +11. Let lane_2* be $lanes_((Fnn X M), v128_2). +12. Let Inn be $isize^-1($size(Fnn)). +13. Let lane_3* be $extend__(1, $sizenn(Fnn), S, $fge_($sizenn(Fnn), lane_1, lane_2))*. +14. Let v128 be $invlanes_((Inn X M), lane_3*). +15. Return v128. vcvtop__ (lanetype_u2 X M_1) (lanetype_u0 X M_2) vcvtop_u1 lane__u4 1. If the type of lanetype_u2 is Jnn, then: a. Let Jnn_1 be lanetype_u2. b. If the type of lanetype_u0 is Jnn, then: 1) Let Jnn_2 be lanetype_u0. - 2) Let iN_1 be lane__u4. - 3) If vcvtop_u1 is of the case EXTEND, then: + 2) If vcvtop_u1 is of the case EXTEND, then: a) Let (EXTEND sx) be vcvtop_u1. - b) Let iN_2 be $extend__($lsizenn1(Jnn_1), $lsizenn2(Jnn_2), sx, iN_1). - c) Return [iN_2]. -2. If the type of lanetype_u0 is Fnn, then: - a. Let Fnn_2 be lanetype_u0. - b. If the type of lanetype_u2 is Jnn, then: - 1) Let Jnn_1 be lanetype_u2. - 2) Let iN_1 be lane__u4. - 3) If vcvtop_u1 is of the case CONVERT, then: - a) Let (CONVERT sx) be vcvtop_u1. - b) Let fN_2 be $convert__($lsizenn1(Jnn_1), $lsizenn2(Fnn_2), sx, iN_1). - c) Return [fN_2]. -3. If the type of lanetype_u2 is Fnn, then: - a. Let Fnn_1 be lanetype_u2. - b. If the type of lanetype_u0 is Inn, then: - 1) Let Inn_2 be lanetype_u0. - 2) Let fN_1 be lane__u4. - 3) If vcvtop_u1 is of the case TRUNC_SAT, then: - a) Let (TRUNC_SAT sx) be vcvtop_u1. - b) Let iN_2? be $trunc_sat__($lsizenn1(Fnn_1), $lsizenn2(Inn_2), sx, fN_1). - c) Return $list_(lane_((Inn_2 : Inn <: lanetype)), iN_2?). -4. If ((vcvtop_u1 is DEMOTE) and the type of lanetype_u2 is Fnn), then: - a. Let Fnn_1 be lanetype_u2. - b. If the type of lanetype_u0 is Fnn, then: + b) Let iN_1 be lane__u4. + c) Let iN_2 be $extend__($lsizenn1(Jnn_1), $lsizenn2(Jnn_2), sx, iN_1). + d) Return [iN_2]. + c. If the type of lanetype_u0 is Fnn, then: 1) Let Fnn_2 be lanetype_u0. + 2) If vcvtop_u1 is of the case CONVERT, then: + a) Let (CONVERT sx) be vcvtop_u1. + b) Let iN_1 be lane__u4. + c) Let fN_2 be $convert__($lsizenn1(Jnn_1), $lsizenn2(Fnn_2), sx, iN_1). + d) Return [fN_2]. +2. Assert: Due to validation, the type of lanetype_u2 is Fnn. +3. Let Fnn_1 be lanetype_u2. +4. If the type of lanetype_u0 is Inn, then: + a. Let Inn_2 be lanetype_u0. + b. If vcvtop_u1 is of the case TRUNC_SAT, then: + 1) Let (TRUNC_SAT sx) be vcvtop_u1. 2) Let fN_1 be lane__u4. - 3) Let fN_2* be $demote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1). - 4) Return fN_2*. -5. Assert: Due to validation, (vcvtop_u1 is PROMOTE). -6. Assert: Due to validation, the type of lanetype_u2 is Fnn. -7. Let Fnn_1 be lanetype_u2. -8. Assert: Due to validation, the type of lanetype_u0 is Fnn. -9. Let Fnn_2 be lanetype_u0. -10. Let fN_1 be lane__u4. -11. Let fN_2* be $promote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1). -12. Return fN_2*. + 3) Let iN_2? be $trunc_sat__($lsizenn1(Fnn_1), $lsizenn2(Inn_2), sx, fN_1). + 4) Return $list_(lane_((Inn_2 : Inn <: lanetype)), iN_2?). +5. Assert: Due to validation, the type of lanetype_u0 is Fnn. +6. Let Fnn_2 be lanetype_u0. +7. Let fN_1 be lane__u4. +8. If (vcvtop_u1 is DEMOTE), then: + a. Let fN_2* be $demote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1). + b. Return fN_2*. +9. Assert: Due to validation, (vcvtop_u1 is PROMOTE). +10. Let fN_2* be $promote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1). +11. Return fN_2*. vextunop__ (Inn_1 X M_1) (Inn_2 X M_2) (EXTADD_PAIRWISE sx) c_1 1. Let ci* be $lanes_((Inn_2 X M_2), c_1). @@ -12127,24 +11467,24 @@ instexport fa* ga* ta* ma* (EXPORT name externidx_u0) 6. Return { NAME: name; ADDR: (MEM ma*[x]); }. allocmodule module externaddr* val* ref** -1. Let fa_ex* be $funcs(externaddr*). -2. Let ga_ex* be $globals(externaddr*). -3. Let ma_ex* be $mems(externaddr*). -4. Let ta_ex* be $tables(externaddr*). -5. Assert: Due to validation, module is of the case MODULE. -6. Let (MODULE type_0* import* func^n_func global_1^n_global table_2^n_table mem_3^n_mem elem_4^n_elem data_5^n_data start? export*) be module. -7. Assert: Due to validation, data_5 is of the case DATA^n_data. -8. Let (DATA byte* datamode)^n_data be data_5^n_data. -9. Assert: Due to validation, elem_4 is of the case ELEM^n_elem. -10. Let (ELEM rt expr_2* elemmode)^n_elem be elem_4^n_elem. -11. Assert: Due to validation, mem_3 is of the case MEMORY^n_mem. -12. Let (MEMORY memtype)^n_mem be mem_3^n_mem. -13. Assert: Due to validation, table_2 is of the case TABLE^n_table. -14. Let (TABLE tabletype)^n_table be table_2^n_table. -15. Assert: Due to validation, global_1 is of the case GLOBAL^n_global. -16. Let (GLOBAL globaltype expr_1)^n_global be global_1^n_global. -17. Assert: Due to validation, type_0 is of the case TYPE*. -18. Let (TYPE ft)* be type_0*. +1. Assert: Due to validation, module is of the case MODULE. +2. Let (MODULE type_0* import* func^n_func global_1^n_global table_2^n_table mem_3^n_mem elem_4^n_elem data_5^n_data start? export*) be module. +3. Assert: Due to validation, data_5 is of the case DATA^n_data. +4. Let (DATA byte* datamode)^n_data be data_5^n_data. +5. Assert: Due to validation, elem_4 is of the case ELEM^n_elem. +6. Let (ELEM rt expr_2* elemmode)^n_elem be elem_4^n_elem. +7. Assert: Due to validation, mem_3 is of the case MEMORY^n_mem. +8. Let (MEMORY memtype)^n_mem be mem_3^n_mem. +9. Assert: Due to validation, table_2 is of the case TABLE^n_table. +10. Let (TABLE tabletype)^n_table be table_2^n_table. +11. Assert: Due to validation, global_1 is of the case GLOBAL^n_global. +12. Let (GLOBAL globaltype expr_1)^n_global be global_1^n_global. +13. Assert: Due to validation, type_0 is of the case TYPE*. +14. Let (TYPE ft)* be type_0*. +15. Let fa_ex* be $funcs(externaddr*). +16. Let ga_ex* be $globals(externaddr*). +17. Let ma_ex* be $mems(externaddr*). +18. Let ta_ex* be $tables(externaddr*). 19. Let fa* be (|s.FUNCS| + i_func)^(i_func valtype_1) be functype_0. -7. Assert: Due to validation, (valtype_1 is []). +3. Assert: Due to validation, $expanddt($tag(z, x).TYPE) is of the case FUNC. +4. Let (FUNC functype_0) be $expanddt($tag(z, x).TYPE). +5. Let (t^n -> valtype_1) be functype_0. +6. Assert: Due to validation, (valtype_1 is []). +7. Let a be |$exninst(z)|. 8. Assert: Due to validation, there are at least n values on the top of the stack. 9. Pop the values val^n from the stack. 10. Let exn be { TAG: $tagaddr(z)[x]; FIELDS: val^n; }. @@ -24710,10 +23787,10 @@ Step/throw x Step/struct.new x 1. Let z be the current state. -2. Let a be |$structinst(z)|. -3. Assert: Due to validation, $expanddt($type(z, x)) is of the case STRUCT. -4. Let (STRUCT fieldtype_0^n) be $expanddt($type(z, x)). -5. Let (mut, zt)^n be fieldtype_0^n. +2. Assert: Due to validation, $expanddt($type(z, x)) is of the case STRUCT. +3. Let (STRUCT fieldtype_0^n) be $expanddt($type(z, x)). +4. Let (mut, zt)^n be fieldtype_0^n. +5. Let a be |$structinst(z)|. 6. Assert: Due to validation, there are at least n values on the top of the stack. 7. Pop the values val^n from the stack. 8. Let si be { TYPE: $type(z, x); FIELDS: $packfield_(zt, val)^n; }. @@ -24738,12 +23815,12 @@ Step/struct.set x i Step/array.new_fixed x n 1. Let z be the current state. -2. Assert: Due to validation, there are at least n values on the top of the stack. -3. Pop the values val^n from the stack. -4. Let a be |$arrayinst(z)|. -5. Assert: Due to validation, $expanddt($type(z, x)) is of the case ARRAY. -6. Let (ARRAY arraytype_0) be $expanddt($type(z, x)). -7. Let (mut, zt) be arraytype_0. +2. Assert: Due to validation, $expanddt($type(z, x)) is of the case ARRAY. +3. Let (ARRAY arraytype_0) be $expanddt($type(z, x)). +4. Let (mut, zt) be arraytype_0. +5. Let a be |$arrayinst(z)|. +6. Assert: Due to validation, there are at least n values on the top of the stack. +7. Pop the values val^n from the stack. 8. Let ai be { TYPE: $type(z, x); FIELDS: $packfield_(zt, val)^n; }. 9. Push the value (REF.ARRAY_ADDR a) to the stack. 10. Perform $add_arrayinst(z, [ai]). @@ -26015,277 +25092,184 @@ invsigned_ N i 2. Return j. unop_ numtype_u1 unop__u0 num__u3 -1. If ((unop__u0 is CLZ) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN be num__u3. - c. Return [$iclz_($sizenn(Inn), iN)]. -2. If ((unop__u0 is CTZ) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN be num__u3. - c. Return [$ictz_($sizenn(Inn), iN)]. -3. If ((unop__u0 is POPCNT) and the type of numtype_u1 is Inn), then: +1. If the type of numtype_u1 is Inn, then: a. Let Inn be numtype_u1. b. Let iN be num__u3. - c. Return [$ipopcnt_($sizenn(Inn), iN)]. -4. If the type of numtype_u1 is Inn, then: - a. Let Inn be numtype_u1. - b. Assert: Due to validation, unop__u0 is of the case EXTEND. - c. Let (EXTEND M) be unop__u0. - d. Let iN be num__u3. - e. Return [$extend__(M, $sizenn(Inn), S, $wrap__($sizenn(Inn), M, iN))]. -5. If ((unop__u0 is ABS) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $fabs_($sizenn(Fnn), fN). -6. If ((unop__u0 is NEG) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $fneg_($sizenn(Fnn), fN). -7. If ((unop__u0 is SQRT) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $fsqrt_($sizenn(Fnn), fN). -8. If ((unop__u0 is CEIL) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $fceil_($sizenn(Fnn), fN). -9. If ((unop__u0 is FLOOR) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $ffloor_($sizenn(Fnn), fN). -10. If ((unop__u0 is TRUNC) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN be num__u3. - c. Return $ftrunc_($sizenn(Fnn), fN). + c. If (unop__u0 is CLZ), then: + 1) Return [$iclz_($sizenn(Inn), iN)]. + d. If (unop__u0 is CTZ), then: + 1) Return [$ictz_($sizenn(Inn), iN)]. + e. If (unop__u0 is POPCNT), then: + 1) Return [$ipopcnt_($sizenn(Inn), iN)]. + f. Assert: Due to validation, unop__u0 is of the case EXTEND. + g. Let (EXTEND M) be unop__u0. + h. Return [$extend__(M, $sizenn(Inn), S, $wrap__($sizenn(Inn), M, iN))]. +2. Assert: Due to validation, the type of numtype_u1 is Fnn. +3. Let Fnn be numtype_u1. +4. Let fN be num__u3. +5. If (unop__u0 is ABS), then: + a. Return $fabs_($sizenn(Fnn), fN). +6. If (unop__u0 is NEG), then: + a. Return $fneg_($sizenn(Fnn), fN). +7. If (unop__u0 is SQRT), then: + a. Return $fsqrt_($sizenn(Fnn), fN). +8. If (unop__u0 is CEIL), then: + a. Return $fceil_($sizenn(Fnn), fN). +9. If (unop__u0 is FLOOR), then: + a. Return $ffloor_($sizenn(Fnn), fN). +10. If (unop__u0 is TRUNC), then: + a. Return $ftrunc_($sizenn(Fnn), fN). 11. Assert: Due to validation, (unop__u0 is NEAREST). -12. Assert: Due to validation, the type of numtype_u1 is Fnn. -13. Let Fnn be numtype_u1. -14. Let fN be num__u3. -15. Return $fnearest_($sizenn(Fnn), fN). +12. Return $fnearest_($sizenn(Fnn), fN). binop_ numtype_u1 binop__u0 num__u3 num__u5 -1. If ((binop__u0 is ADD) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$iadd_($sizenn(Inn), iN_1, iN_2)]. -2. If ((binop__u0 is SUB) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$isub_($sizenn(Inn), iN_1, iN_2)]. -3. If ((binop__u0 is MUL) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$imul_($sizenn(Inn), iN_1, iN_2)]. -4. If the type of numtype_u1 is Inn, then: +1. If the type of numtype_u1 is Inn, then: a. Let Inn be numtype_u1. b. Let iN_1 be num__u3. c. Let iN_2 be num__u5. - d. If binop__u0 is of the case DIV, then: + d. If (binop__u0 is ADD), then: + 1) Return [$iadd_($sizenn(Inn), iN_1, iN_2)]. + e. If (binop__u0 is SUB), then: + 1) Return [$isub_($sizenn(Inn), iN_1, iN_2)]. + f. If (binop__u0 is MUL), then: + 1) Return [$imul_($sizenn(Inn), iN_1, iN_2)]. + g. If binop__u0 is of the case DIV, then: 1) Let (DIV sx) be binop__u0. 2) Return $list_(num_((Inn : Inn <: numtype)), $idiv_($sizenn(Inn), sx, iN_1, iN_2)). - e. If binop__u0 is of the case REM, then: + h. If binop__u0 is of the case REM, then: 1) Let (REM sx) be binop__u0. 2) Return $list_(num_((Inn : Inn <: numtype)), $irem_($sizenn(Inn), sx, iN_1, iN_2)). -5. If ((binop__u0 is AND) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$iand_($sizenn(Inn), iN_1, iN_2)]. -6. If ((binop__u0 is OR) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$ior_($sizenn(Inn), iN_1, iN_2)]. -7. If ((binop__u0 is XOR) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$ixor_($sizenn(Inn), iN_1, iN_2)]. -8. If ((binop__u0 is SHL) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$ishl_($sizenn(Inn), iN_1, iN_2)]. -9. If the type of numtype_u1 is Inn, then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. If binop__u0 is of the case SHR, then: + i. If (binop__u0 is AND), then: + 1) Return [$iand_($sizenn(Inn), iN_1, iN_2)]. + j. If (binop__u0 is OR), then: + 1) Return [$ior_($sizenn(Inn), iN_1, iN_2)]. + k. If (binop__u0 is XOR), then: + 1) Return [$ixor_($sizenn(Inn), iN_1, iN_2)]. + l. If (binop__u0 is SHL), then: + 1) Return [$ishl_($sizenn(Inn), iN_1, iN_2)]. + m. If binop__u0 is of the case SHR, then: 1) Let (SHR sx) be binop__u0. 2) Return [$ishr_($sizenn(Inn), sx, iN_1, iN_2)]. -10. If ((binop__u0 is ROTL) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$irotl_($sizenn(Inn), iN_1, iN_2)]. -11. If ((binop__u0 is ROTR) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return [$irotr_($sizenn(Inn), iN_1, iN_2)]. -12. If ((binop__u0 is ADD) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fadd_($sizenn(Fnn), fN_1, fN_2). -13. If ((binop__u0 is SUB) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fsub_($sizenn(Fnn), fN_1, fN_2). -14. If ((binop__u0 is MUL) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fmul_($sizenn(Fnn), fN_1, fN_2). -15. If ((binop__u0 is DIV) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fdiv_($sizenn(Fnn), fN_1, fN_2). -16. If ((binop__u0 is MIN) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fmin_($sizenn(Fnn), fN_1, fN_2). -17. If ((binop__u0 is MAX) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fmax_($sizenn(Fnn), fN_1, fN_2). -18. Assert: Due to validation, (binop__u0 is COPYSIGN). -19. Assert: Due to validation, the type of numtype_u1 is Fnn. -20. Let Fnn be numtype_u1. -21. Let fN_1 be num__u3. -22. Let fN_2 be num__u5. -23. Return $fcopysign_($sizenn(Fnn), fN_1, fN_2). + n. If (binop__u0 is ROTL), then: + 1) Return [$irotl_($sizenn(Inn), iN_1, iN_2)]. + o. If (binop__u0 is ROTR), then: + 1) Return [$irotr_($sizenn(Inn), iN_1, iN_2)]. +2. Assert: Due to validation, the type of numtype_u1 is Fnn. +3. Let Fnn be numtype_u1. +4. Let fN_1 be num__u3. +5. Let fN_2 be num__u5. +6. If (binop__u0 is ADD), then: + a. Return $fadd_($sizenn(Fnn), fN_1, fN_2). +7. If (binop__u0 is SUB), then: + a. Return $fsub_($sizenn(Fnn), fN_1, fN_2). +8. If (binop__u0 is MUL), then: + a. Return $fmul_($sizenn(Fnn), fN_1, fN_2). +9. If (binop__u0 is DIV), then: + a. Return $fdiv_($sizenn(Fnn), fN_1, fN_2). +10. If (binop__u0 is MIN), then: + a. Return $fmin_($sizenn(Fnn), fN_1, fN_2). +11. If (binop__u0 is MAX), then: + a. Return $fmax_($sizenn(Fnn), fN_1, fN_2). +12. Assert: Due to validation, (binop__u0 is COPYSIGN). +13. Return $fcopysign_($sizenn(Fnn), fN_1, fN_2). testop_ Inn EQZ iN 1. Return $ieqz_($sizenn(Inn), iN). relop_ numtype_u1 relop__u0 num__u3 num__u5 -1. If ((relop__u0 is EQ) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return $ieq_($sizenn(Inn), iN_1, iN_2). -2. If ((relop__u0 is NE) and the type of numtype_u1 is Inn), then: - a. Let Inn be numtype_u1. - b. Let iN_1 be num__u3. - c. Let iN_2 be num__u5. - d. Return $ine_($sizenn(Inn), iN_1, iN_2). -3. If the type of numtype_u1 is Inn, then: +1. If the type of numtype_u1 is Inn, then: a. Let Inn be numtype_u1. b. Let iN_1 be num__u3. c. Let iN_2 be num__u5. - d. If relop__u0 is of the case LT, then: + d. If (relop__u0 is EQ), then: + 1) Return $ieq_($sizenn(Inn), iN_1, iN_2). + e. If (relop__u0 is NE), then: + 1) Return $ine_($sizenn(Inn), iN_1, iN_2). + f. If relop__u0 is of the case LT, then: 1) Let (LT sx) be relop__u0. 2) Return $ilt_($sizenn(Inn), sx, iN_1, iN_2). - e. If relop__u0 is of the case GT, then: + g. If relop__u0 is of the case GT, then: 1) Let (GT sx) be relop__u0. 2) Return $igt_($sizenn(Inn), sx, iN_1, iN_2). - f. If relop__u0 is of the case LE, then: + h. If relop__u0 is of the case LE, then: 1) Let (LE sx) be relop__u0. 2) Return $ile_($sizenn(Inn), sx, iN_1, iN_2). - g. If relop__u0 is of the case GE, then: + i. If relop__u0 is of the case GE, then: 1) Let (GE sx) be relop__u0. 2) Return $ige_($sizenn(Inn), sx, iN_1, iN_2). -4. If ((relop__u0 is EQ) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $feq_($sizenn(Fnn), fN_1, fN_2). -5. If ((relop__u0 is NE) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fne_($sizenn(Fnn), fN_1, fN_2). -6. If ((relop__u0 is LT) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $flt_($sizenn(Fnn), fN_1, fN_2). -7. If ((relop__u0 is GT) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fgt_($sizenn(Fnn), fN_1, fN_2). -8. If ((relop__u0 is LE) and the type of numtype_u1 is Fnn), then: - a. Let Fnn be numtype_u1. - b. Let fN_1 be num__u3. - c. Let fN_2 be num__u5. - d. Return $fle_($sizenn(Fnn), fN_1, fN_2). -9. Assert: Due to validation, (relop__u0 is GE). -10. Assert: Due to validation, the type of numtype_u1 is Fnn. -11. Let Fnn be numtype_u1. -12. Let fN_1 be num__u3. -13. Let fN_2 be num__u5. -14. Return $fge_($sizenn(Fnn), fN_1, fN_2). +2. Assert: Due to validation, the type of numtype_u1 is Fnn. +3. Let Fnn be numtype_u1. +4. Let fN_1 be num__u3. +5. Let fN_2 be num__u5. +6. If (relop__u0 is EQ), then: + a. Return $feq_($sizenn(Fnn), fN_1, fN_2). +7. If (relop__u0 is NE), then: + a. Return $fne_($sizenn(Fnn), fN_1, fN_2). +8. If (relop__u0 is LT), then: + a. Return $flt_($sizenn(Fnn), fN_1, fN_2). +9. If (relop__u0 is GT), then: + a. Return $fgt_($sizenn(Fnn), fN_1, fN_2). +10. If (relop__u0 is LE), then: + a. Return $fle_($sizenn(Fnn), fN_1, fN_2). +11. Assert: Due to validation, (relop__u0 is GE). +12. Return $fge_($sizenn(Fnn), fN_1, fN_2). cvtop__ numtype_u1 numtype_u4 cvtop___u0 num__u3 1. If the type of numtype_u1 is Inn, then: a. Let Inn_1 be numtype_u1. b. If the type of numtype_u4 is Inn, then: 1) Let Inn_2 be numtype_u4. - 2) Let iN_1 be num__u3. - 3) If cvtop___u0 is of the case EXTEND, then: + 2) If cvtop___u0 is of the case EXTEND, then: a) Let (EXTEND sx) be cvtop___u0. - b) Return [$extend__($sizenn1(Inn_1), $sizenn2(Inn_2), sx, iN_1)]. -2. If ((cvtop___u0 is WRAP) and the type of numtype_u1 is Inn), then: - a. Let Inn_1 be numtype_u1. - b. If the type of numtype_u4 is Inn, then: - 1) Let Inn_2 be numtype_u4. - 2) Let iN_1 be num__u3. - 3) Return [$wrap__($sizenn1(Inn_1), $sizenn2(Inn_2), iN_1)]. -3. If the type of numtype_u1 is Fnn, then: + b) Let iN_1 be num__u3. + c) Return [$extend__($sizenn1(Inn_1), $sizenn2(Inn_2), sx, iN_1)]. + 3) Let iN_1 be num__u3. + 4) If (cvtop___u0 is WRAP), then: + a) Return [$wrap__($sizenn1(Inn_1), $sizenn2(Inn_2), iN_1)]. +2. If the type of numtype_u1 is Fnn, then: a. Let Fnn_1 be numtype_u1. b. If the type of numtype_u4 is Inn, then: 1) Let Inn_2 be numtype_u4. - 2) Let fN_1 be num__u3. - 3) If cvtop___u0 is of the case TRUNC, then: + 2) If cvtop___u0 is of the case TRUNC, then: a) Let (TRUNC sx) be cvtop___u0. - b) Return $list_(num_((Inn_2 : Inn <: numtype)), $trunc__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, fN_1)). - 4) If cvtop___u0 is of the case TRUNC_SAT, then: + b) Let fN_1 be num__u3. + c) Return $list_(num_((Inn_2 : Inn <: numtype)), $trunc__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, fN_1)). + 3) If cvtop___u0 is of the case TRUNC_SAT, then: a) Let (TRUNC_SAT sx) be cvtop___u0. - b) Return $list_(num_((Inn_2 : Inn <: numtype)), $trunc_sat__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, fN_1)). -4. If the type of numtype_u4 is Fnn, then: - a. Let Fnn_2 be numtype_u4. - b. If the type of numtype_u1 is Inn, then: - 1) Let Inn_1 be numtype_u1. - 2) Let iN_1 be num__u3. - 3) If cvtop___u0 is of the case CONVERT, then: + b) Let fN_1 be num__u3. + c) Return $list_(num_((Inn_2 : Inn <: numtype)), $trunc_sat__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, fN_1)). +3. If the type of numtype_u1 is Inn, then: + a. Let Inn_1 be numtype_u1. + b. If the type of numtype_u4 is Fnn, then: + 1) Let Fnn_2 be numtype_u4. + 2) If cvtop___u0 is of the case CONVERT, then: a) Let (CONVERT sx) be cvtop___u0. - b) Return [$convert__($sizenn1(Inn_1), $sizenn2(Fnn_2), sx, iN_1)]. -5. If ((cvtop___u0 is PROMOTE) and the type of numtype_u1 is Fnn), then: + b) Let iN_1 be num__u3. + c) Return [$convert__($sizenn1(Inn_1), $sizenn2(Fnn_2), sx, iN_1)]. +4. If the type of numtype_u1 is Fnn, then: a. Let Fnn_1 be numtype_u1. b. If the type of numtype_u4 is Fnn, then: 1) Let Fnn_2 be numtype_u4. 2) Let fN_1 be num__u3. - 3) Return $promote__($sizenn1(Fnn_1), $sizenn2(Fnn_2), fN_1). -6. If ((cvtop___u0 is DEMOTE) and the type of numtype_u1 is Fnn), then: - a. Let Fnn_1 be numtype_u1. + 3) If (cvtop___u0 is PROMOTE), then: + a) Return $promote__($sizenn1(Fnn_1), $sizenn2(Fnn_2), fN_1). + 4) If (cvtop___u0 is DEMOTE), then: + a) Return $demote__($sizenn1(Fnn_1), $sizenn2(Fnn_2), fN_1). +5. If the type of numtype_u1 is Inn, then: + a. Let Inn_1 be numtype_u1. b. If the type of numtype_u4 is Fnn, then: 1) Let Fnn_2 be numtype_u4. - 2) Let fN_1 be num__u3. - 3) Return $demote__($sizenn1(Fnn_1), $sizenn2(Fnn_2), fN_1). -7. Assert: Due to validation, (cvtop___u0 is REINTERPRET). -8. If the type of numtype_u4 is Fnn, then: - a. Let Fnn_2 be numtype_u4. - b. If the type of numtype_u1 is Inn, then: - 1) Let Inn_1 be numtype_u1. 2) Let iN_1 be num__u3. - 3) If ($size(Inn_1) is $size(Fnn_2)), then: + 3) If ((cvtop___u0 is REINTERPRET) and ($size(Inn_1) is $size(Fnn_2))), then: a) Return [$reinterpret__(Inn_1, Fnn_2, iN_1)]. -9. Assert: Due to validation, the type of numtype_u1 is Fnn. -10. Let Fnn_1 be numtype_u1. -11. Assert: Due to validation, the type of numtype_u4 is Inn. -12. Let Inn_2 be numtype_u4. -13. Let fN_1 be num__u3. -14. Assert: Due to validation, ($size(Fnn_1) is $size(Inn_2)). -15. Return [$reinterpret__(Fnn_1, Inn_2, fN_1)]. +6. Assert: Due to validation, the type of numtype_u1 is Fnn. +7. Let Fnn_1 be numtype_u1. +8. Assert: Due to validation, the type of numtype_u4 is Inn. +9. Let Inn_2 be numtype_u4. +10. Let fN_1 be num__u3. +11. Assert: Due to validation, (cvtop___u0 is REINTERPRET). +12. Assert: Due to validation, ($size(Fnn_1) is $size(Inn_2)). +13. Return [$reinterpret__(Fnn_1, Inn_2, fN_1)]. invibytes_ N b* 1. Let n be $ibytes__1^-1(N, b*). @@ -26328,13 +25312,14 @@ invlanes_ sh c* 2. Return vc. half__ (lanetype_u1 X M_1) (lanetype_u2 X M_2) half___u0 i j -1. If ((half___u0 is LOW) and (the type of lanetype_u1 is Jnn and the type of lanetype_u2 is Jnn)), then: - a. Return i. -2. If ((half___u0 is HIGH) and (the type of lanetype_u1 is Jnn and the type of lanetype_u2 is Jnn)), then: - a. Return j. +1. If (the type of lanetype_u1 is Jnn and the type of lanetype_u2 is Jnn), then: + a. If (half___u0 is LOW), then: + 1) Return i. + b. If (half___u0 is HIGH), then: + 1) Return j. +2. Assert: Due to validation, the type of lanetype_u2 is Fnn. 3. Assert: Due to validation, (half___u0 is LOW). -4. Assert: Due to validation, the type of lanetype_u2 is Fnn. -5. Return i. +4. Return i. vvunop_ V128 NOT v128 1. Return [$inot_($vsize(V128), v128)]. @@ -26363,37 +25348,30 @@ ivunop_ (Jnn X M) $f_ vN_1 3. Return [$invlanes_((Jnn X M), c*)]. vunop_ (lanetype_u1 X M) vunop__u0 vN_1 -1. If ((vunop__u0 is ABS) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Return $ivunop_((Jnn X M), $iabs_, vN_1). -2. If ((vunop__u0 is NEG) and the type of lanetype_u1 is Jnn), then: +1. If the type of lanetype_u1 is Jnn, then: a. Let Jnn be lanetype_u1. - b. Return $ivunop_((Jnn X M), $ineg_, vN_1). -3. If ((vunop__u0 is POPCNT) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Return $ivunop_((Jnn X M), $ipopcnt_, vN_1). -4. If ((vunop__u0 is ABS) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvunop_((Fnn X M), $fabs_, vN_1). -5. If ((vunop__u0 is NEG) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvunop_((Fnn X M), $fneg_, vN_1). -6. If ((vunop__u0 is SQRT) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvunop_((Fnn X M), $fsqrt_, vN_1). -7. If ((vunop__u0 is CEIL) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvunop_((Fnn X M), $fceil_, vN_1). -8. If ((vunop__u0 is FLOOR) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvunop_((Fnn X M), $ffloor_, vN_1). -9. If ((vunop__u0 is TRUNC) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvunop_((Fnn X M), $ftrunc_, vN_1). + b. If (vunop__u0 is ABS), then: + 1) Return $ivunop_((Jnn X M), $iabs_, vN_1). + c. If (vunop__u0 is NEG), then: + 1) Return $ivunop_((Jnn X M), $ineg_, vN_1). + d. If (vunop__u0 is POPCNT), then: + 1) Return $ivunop_((Jnn X M), $ipopcnt_, vN_1). +2. Assert: Due to validation, the type of lanetype_u1 is Fnn. +3. Let Fnn be lanetype_u1. +4. If (vunop__u0 is ABS), then: + a. Return $fvunop_((Fnn X M), $fabs_, vN_1). +5. If (vunop__u0 is NEG), then: + a. Return $fvunop_((Fnn X M), $fneg_, vN_1). +6. If (vunop__u0 is SQRT), then: + a. Return $fvunop_((Fnn X M), $fsqrt_, vN_1). +7. If (vunop__u0 is CEIL), then: + a. Return $fvunop_((Fnn X M), $fceil_, vN_1). +8. If (vunop__u0 is FLOOR), then: + a. Return $fvunop_((Fnn X M), $ffloor_, vN_1). +9. If (vunop__u0 is TRUNC), then: + a. Return $fvunop_((Fnn X M), $ftrunc_, vN_1). 10. Assert: Due to validation, (vunop__u0 is NEAREST). -11. Assert: Due to validation, the type of lanetype_u1 is Fnn. -12. Let Fnn be lanetype_u1. -13. Return $fvunop_((Fnn X M), $fnearest_, vN_1). +11. Return $fvunop_((Fnn X M), $fnearest_, vN_1). fvbinop_ (Fnn X M) $f_ vN_1 vN_2 1. Let c_1* be $lanes_((Fnn X M), vN_1). @@ -26414,60 +25392,48 @@ ivbinopsx_ (Jnn X M) $f_ sx vN_1 vN_2 4. Return [$invlanes_((Jnn X M), c*)]. vbinop_ (lanetype_u1 X M) vbinop__u0 vN_1 vN_2 -1. If ((vbinop__u0 is ADD) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Return $ivbinop_((Jnn X M), $iadd_, vN_1, vN_2). -2. If ((vbinop__u0 is SUB) and the type of lanetype_u1 is Jnn), then: +1. If the type of lanetype_u1 is Jnn, then: a. Let Jnn be lanetype_u1. - b. Return $ivbinop_((Jnn X M), $isub_, vN_1, vN_2). -3. If ((vbinop__u0 is MUL) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Return $ivbinop_((Jnn X M), $imul_, vN_1, vN_2). -4. If the type of lanetype_u1 is Jnn, then: - a. Let Jnn be lanetype_u1. - b. If vbinop__u0 is of the case ADD_SAT, then: + b. If (vbinop__u0 is ADD), then: + 1) Return $ivbinop_((Jnn X M), $iadd_, vN_1, vN_2). + c. If (vbinop__u0 is SUB), then: + 1) Return $ivbinop_((Jnn X M), $isub_, vN_1, vN_2). + d. If (vbinop__u0 is MUL), then: + 1) Return $ivbinop_((Jnn X M), $imul_, vN_1, vN_2). + e. If vbinop__u0 is of the case ADD_SAT, then: 1) Let (ADD_SAT sx) be vbinop__u0. 2) Return $ivbinopsx_((Jnn X M), $iadd_sat_, sx, vN_1, vN_2). - c. If vbinop__u0 is of the case SUB_SAT, then: + f. If vbinop__u0 is of the case SUB_SAT, then: 1) Let (SUB_SAT sx) be vbinop__u0. 2) Return $ivbinopsx_((Jnn X M), $isub_sat_, sx, vN_1, vN_2). - d. If vbinop__u0 is of the case MIN, then: + g. If vbinop__u0 is of the case MIN, then: 1) Let (MIN sx) be vbinop__u0. 2) Return $ivbinopsx_((Jnn X M), $imin_, sx, vN_1, vN_2). - e. If vbinop__u0 is of the case MAX, then: + h. If vbinop__u0 is of the case MAX, then: 1) Let (MAX sx) be vbinop__u0. 2) Return $ivbinopsx_((Jnn X M), $imax_, sx, vN_1, vN_2). -5. If ((vbinop__u0 is (AVGRU)) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Return $ivbinopsx_((Jnn X M), $iavgr_, U, vN_1, vN_2). -6. If ((vbinop__u0 is (Q15MULR_SATS)) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Return $ivbinopsx_((Jnn X M), $iq15mulr_sat_, S, vN_1, vN_2). -7. If ((vbinop__u0 is ADD) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvbinop_((Fnn X M), $fadd_, vN_1, vN_2). -8. If ((vbinop__u0 is SUB) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvbinop_((Fnn X M), $fsub_, vN_1, vN_2). -9. If ((vbinop__u0 is MUL) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvbinop_((Fnn X M), $fmul_, vN_1, vN_2). -10. If ((vbinop__u0 is DIV) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvbinop_((Fnn X M), $fdiv_, vN_1, vN_2). -11. If ((vbinop__u0 is MIN) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvbinop_((Fnn X M), $fmin_, vN_1, vN_2). -12. If ((vbinop__u0 is MAX) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvbinop_((Fnn X M), $fmax_, vN_1, vN_2). -13. If ((vbinop__u0 is PMIN) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvbinop_((Fnn X M), $fpmin_, vN_1, vN_2). -14. Assert: Due to validation, (vbinop__u0 is PMAX). -15. Assert: Due to validation, the type of lanetype_u1 is Fnn. -16. Let Fnn be lanetype_u1. -17. Return $fvbinop_((Fnn X M), $fpmax_, vN_1, vN_2). + i. If (vbinop__u0 is (AVGRU)), then: + 1) Return $ivbinopsx_((Jnn X M), $iavgr_, U, vN_1, vN_2). + j. If (vbinop__u0 is (Q15MULR_SATS)), then: + 1) Return $ivbinopsx_((Jnn X M), $iq15mulr_sat_, S, vN_1, vN_2). +2. Assert: Due to validation, the type of lanetype_u1 is Fnn. +3. Let Fnn be lanetype_u1. +4. If (vbinop__u0 is ADD), then: + a. Return $fvbinop_((Fnn X M), $fadd_, vN_1, vN_2). +5. If (vbinop__u0 is SUB), then: + a. Return $fvbinop_((Fnn X M), $fsub_, vN_1, vN_2). +6. If (vbinop__u0 is MUL), then: + a. Return $fvbinop_((Fnn X M), $fmul_, vN_1, vN_2). +7. If (vbinop__u0 is DIV), then: + a. Return $fvbinop_((Fnn X M), $fdiv_, vN_1, vN_2). +8. If (vbinop__u0 is MIN), then: + a. Return $fvbinop_((Fnn X M), $fmin_, vN_1, vN_2). +9. If (vbinop__u0 is MAX), then: + a. Return $fvbinop_((Fnn X M), $fmax_, vN_1, vN_2). +10. If (vbinop__u0 is PMIN), then: + a. Return $fvbinop_((Fnn X M), $fpmin_, vN_1, vN_2). +11. Assert: Due to validation, (vbinop__u0 is PMAX). +12. Return $fvbinop_((Fnn X M), $fpmax_, vN_1, vN_2). fvrelop_ (Fnn X M) $f_ vN_1 vN_2 1. Let c_1* be $lanes_((Fnn X M), vN_1). @@ -26490,89 +25456,74 @@ ivrelopsx_ (Jnn X M) $f_ sx vN_1 vN_2 4. Return $invlanes_((Jnn X M), c*). vrelop_ (lanetype_u1 X M) vrelop__u0 vN_1 vN_2 -1. If ((vrelop__u0 is EQ) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Return $ivrelop_((Jnn X M), $ieq_, vN_1, vN_2). -2. If ((vrelop__u0 is NE) and the type of lanetype_u1 is Jnn), then: - a. Let Jnn be lanetype_u1. - b. Return $ivrelop_((Jnn X M), $ine_, vN_1, vN_2). -3. If the type of lanetype_u1 is Jnn, then: +1. If the type of lanetype_u1 is Jnn, then: a. Let Jnn be lanetype_u1. - b. If vrelop__u0 is of the case LT, then: + b. If (vrelop__u0 is EQ), then: + 1) Return $ivrelop_((Jnn X M), $ieq_, vN_1, vN_2). + c. If (vrelop__u0 is NE), then: + 1) Return $ivrelop_((Jnn X M), $ine_, vN_1, vN_2). + d. If vrelop__u0 is of the case LT, then: 1) Let (LT sx) be vrelop__u0. 2) Return $ivrelopsx_((Jnn X M), $ilt_, sx, vN_1, vN_2). - c. If vrelop__u0 is of the case GT, then: + e. If vrelop__u0 is of the case GT, then: 1) Let (GT sx) be vrelop__u0. 2) Return $ivrelopsx_((Jnn X M), $igt_, sx, vN_1, vN_2). - d. If vrelop__u0 is of the case LE, then: + f. If vrelop__u0 is of the case LE, then: 1) Let (LE sx) be vrelop__u0. 2) Return $ivrelopsx_((Jnn X M), $ile_, sx, vN_1, vN_2). - e. If vrelop__u0 is of the case GE, then: + g. If vrelop__u0 is of the case GE, then: 1) Let (GE sx) be vrelop__u0. 2) Return $ivrelopsx_((Jnn X M), $ige_, sx, vN_1, vN_2). -4. If ((vrelop__u0 is EQ) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvrelop_((Fnn X M), $feq_, vN_1, vN_2). -5. If ((vrelop__u0 is NE) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvrelop_((Fnn X M), $fne_, vN_1, vN_2). -6. If ((vrelop__u0 is LT) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvrelop_((Fnn X M), $flt_, vN_1, vN_2). -7. If ((vrelop__u0 is GT) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvrelop_((Fnn X M), $fgt_, vN_1, vN_2). -8. If ((vrelop__u0 is LE) and the type of lanetype_u1 is Fnn), then: - a. Let Fnn be lanetype_u1. - b. Return $fvrelop_((Fnn X M), $fle_, vN_1, vN_2). +2. Assert: Due to validation, the type of lanetype_u1 is Fnn. +3. Let Fnn be lanetype_u1. +4. If (vrelop__u0 is EQ), then: + a. Return $fvrelop_((Fnn X M), $feq_, vN_1, vN_2). +5. If (vrelop__u0 is NE), then: + a. Return $fvrelop_((Fnn X M), $fne_, vN_1, vN_2). +6. If (vrelop__u0 is LT), then: + a. Return $fvrelop_((Fnn X M), $flt_, vN_1, vN_2). +7. If (vrelop__u0 is GT), then: + a. Return $fvrelop_((Fnn X M), $fgt_, vN_1, vN_2). +8. If (vrelop__u0 is LE), then: + a. Return $fvrelop_((Fnn X M), $fle_, vN_1, vN_2). 9. Assert: Due to validation, (vrelop__u0 is GE). -10. Assert: Due to validation, the type of lanetype_u1 is Fnn. -11. Let Fnn be lanetype_u1. -12. Return $fvrelop_((Fnn X M), $fge_, vN_1, vN_2). +10. Return $fvrelop_((Fnn X M), $fge_, vN_1, vN_2). vcvtop__ (lanetype_u3 X M_1) (lanetype_u0 X M_2) vcvtop___u2 lane__u5 1. If the type of lanetype_u3 is Jnn, then: a. Let Jnn_1 be lanetype_u3. b. If the type of lanetype_u0 is Jnn, then: 1) Let Jnn_2 be lanetype_u0. - 2) Let iN_1 be lane__u5. - 3) If vcvtop___u2 is of the case EXTEND, then: + 2) If vcvtop___u2 is of the case EXTEND, then: a) Let (EXTEND sx) be vcvtop___u2. - b) Let iN_2 be $extend__($lsizenn1(Jnn_1), $lsizenn2(Jnn_2), sx, iN_1). - c) Return [iN_2]. -2. If the type of lanetype_u0 is Fnn, then: - a. Let Fnn_2 be lanetype_u0. - b. If the type of lanetype_u3 is Jnn, then: - 1) Let Jnn_1 be lanetype_u3. - 2) Let iN_1 be lane__u5. - 3) If vcvtop___u2 is of the case CONVERT, then: - a) Let (CONVERT sx) be vcvtop___u2. - b) Let fN_2 be $convert__($lsizenn1(Jnn_1), $lsizenn2(Fnn_2), sx, iN_1). - c) Return [fN_2]. -3. If the type of lanetype_u3 is Fnn, then: - a. Let Fnn_1 be lanetype_u3. - b. If the type of lanetype_u0 is Inn, then: - 1) Let Inn_2 be lanetype_u0. - 2) Let fN_1 be lane__u5. - 3) If vcvtop___u2 is of the case TRUNC_SAT, then: - a) Let (TRUNC_SAT sx) be vcvtop___u2. - b) Let iN_2? be $trunc_sat__($lsizenn1(Fnn_1), $lsizenn2(Inn_2), sx, fN_1). - c) Return $list_(lane_((Inn_2 : Inn <: lanetype)), iN_2?). -4. If ((vcvtop___u2 is DEMOTE) and the type of lanetype_u3 is Fnn), then: - a. Let Fnn_1 be lanetype_u3. - b. If the type of lanetype_u0 is Fnn, then: + b) Let iN_1 be lane__u5. + c) Let iN_2 be $extend__($lsizenn1(Jnn_1), $lsizenn2(Jnn_2), sx, iN_1). + d) Return [iN_2]. + c. If the type of lanetype_u0 is Fnn, then: 1) Let Fnn_2 be lanetype_u0. + 2) If vcvtop___u2 is of the case CONVERT, then: + a) Let (CONVERT sx) be vcvtop___u2. + b) Let iN_1 be lane__u5. + c) Let fN_2 be $convert__($lsizenn1(Jnn_1), $lsizenn2(Fnn_2), sx, iN_1). + d) Return [fN_2]. +2. Assert: Due to validation, the type of lanetype_u3 is Fnn. +3. Let Fnn_1 be lanetype_u3. +4. If the type of lanetype_u0 is Inn, then: + a. Let Inn_2 be lanetype_u0. + b. If vcvtop___u2 is of the case TRUNC_SAT, then: + 1) Let (TRUNC_SAT sx) be vcvtop___u2. 2) Let fN_1 be lane__u5. - 3) Let fN_2* be $demote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1). - 4) Return fN_2*. -5. Assert: Due to validation, (vcvtop___u2 is PROMOTE). -6. Assert: Due to validation, the type of lanetype_u3 is Fnn. -7. Let Fnn_1 be lanetype_u3. -8. Assert: Due to validation, the type of lanetype_u0 is Fnn. -9. Let Fnn_2 be lanetype_u0. -10. Let fN_1 be lane__u5. -11. Let fN_2* be $promote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1). -12. Return fN_2*. + 3) Let iN_2? be $trunc_sat__($lsizenn1(Fnn_1), $lsizenn2(Inn_2), sx, fN_1). + 4) Return $list_(lane_((Inn_2 : Inn <: lanetype)), iN_2?). +5. Assert: Due to validation, the type of lanetype_u0 is Fnn. +6. Let Fnn_2 be lanetype_u0. +7. Let fN_1 be lane__u5. +8. If (vcvtop___u2 is DEMOTE), then: + a. Let fN_2* be $demote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1). + b. Return fN_2*. +9. Assert: Due to validation, (vcvtop___u2 is PROMOTE). +10. Let fN_2* be $promote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1). +11. Return fN_2*. vextunop__ (Jnn_1 X M_1) (Jnn_2 X M_2) (EXTADD_PAIRWISE sx) c_1 1. Let ci* be $lanes_((Jnn_1 X M_1), c_1). @@ -26639,28 +25590,27 @@ default_ valtype_u0 8. Return ?(). packfield_ storagetype_u0 val_u1 -1. Let val be val_u1. -2. If the type of storagetype_u0 is valtype, then: - a. Return val. -3. Assert: Due to validation, val_u1 is of the case CONST. -4. Let (numtype_0.CONST i) be val_u1. -5. Assert: Due to validation, (numtype_0 is I32). -6. Assert: Due to validation, the type of storagetype_u0 is packtype. -7. Let packtype be storagetype_u0. -8. Return (PACK packtype $wrap__(32, $psize(packtype), i)). +1. If the type of storagetype_u0 is valtype, then: + a. Let val be val_u1. + b. Return val. +2. Assert: Due to validation, the type of storagetype_u0 is packtype. +3. Let packtype be storagetype_u0. +4. Assert: Due to validation, val_u1 is of the case CONST. +5. Let (numtype_0.CONST i) be val_u1. +6. Assert: Due to validation, (numtype_0 is I32). +7. Return (PACK packtype $wrap__(32, $psize(packtype), i)). unpackfield_ storagetype_u0 sx_u1? fieldval_u2 -1. If sx_u1? is not defined, then: - a. Assert: Due to validation, the type of fieldval_u2 is val. - b. Let val be fieldval_u2. - c. Assert: Due to validation, the type of storagetype_u0 is valtype. - d. Return val. -2. Else: - a. Let ?(sx) be sx_u1?. - b. Assert: Due to validation, fieldval_u2 is of the case PACK. - c. Let (PACK packtype i) be fieldval_u2. - d. Assert: Due to validation, (storagetype_u0 is packtype). - e. Return (I32.CONST $extend__($psize(packtype), 32, sx, i)). +1. If (the type of storagetype_u0 is valtype and the type of fieldval_u2 is val), then: + a. Let val be fieldval_u2. + b. If sx_u1? is not defined, then: + 1) Return val. +2. Assert: Due to validation, fieldval_u2 is of the case PACK. +3. Let (PACK packtype i) be fieldval_u2. +4. Assert: Due to validation, sx_u1? is defined. +5. Let ?(sx) be sx_u1?. +6. Assert: Due to validation, (storagetype_u0 is packtype). +7. Return (I32.CONST $extend__($psize(packtype), 32, sx, i)). funcsxa externaddr_u0* 1. If (externaddr_u0* is []), then: @@ -27014,13 +25964,13 @@ allocexports moduleinst export* 1. Return $allocexport(moduleinst, export)*. allocmodule module externaddr* val_G* ref_T* ref_E** -1. Let fa_I* be $funcsxa(externaddr*). -2. Let ga_I* be $globalsxa(externaddr*). -3. Let aa_I* be $tagsxa(externaddr*). -4. Let ma_I* be $memsxa(externaddr*). -5. Let ta_I* be $tablesxa(externaddr*). -6. Assert: Due to validation, module is of the case MODULE. -7. Let (MODULE type* import* func* global* table* mem* tag* elem* data* start? export*) be module. +1. Assert: Due to validation, module is of the case MODULE. +2. Let (MODULE type* import* func* global* table* mem* tag* elem* data* start? export*) be module. +3. Let fa_I* be $funcsxa(externaddr*). +4. Let ga_I* be $globalsxa(externaddr*). +5. Let aa_I* be $tagsxa(externaddr*). +6. Let ma_I* be $memsxa(externaddr*). +7. Let ta_I* be $tablesxa(externaddr*). 8. Let fa* be (|s.FUNCS| + i_F)^(i_F<|func*|). 9. Let ga* be (|s.GLOBALS| + i_G)^(i_G<|global*|). 10. Let ta* be (|s.TABLES| + i_T)^(i_T<|table*|). @@ -27085,8 +26035,8 @@ evalglobals z globaltype_u0* expr_u1* 4. Let [expr] :: expr'* be expr_u1*. 5. Assert: Due to validation, (|globaltype_u0*| ≥ 1). 6. Let [gt] :: gt'* be globaltype_u0*. -7. Let [val] be $eval_expr(expr). -8. Let f be z. +7. Let f be z. +8. Let [val] be $eval_expr(expr). 9. Let a be $allocglobal(gt, val). 10. Append a to the f.MODULE.GLOBALS. 11. Let val'* be $evalglobals(z, gt'*, expr'*). @@ -27131,10 +26081,10 @@ instantiate z module externaddr* 35. Return f.MODULE. invoke funcaddr val* -1. Let f be { LOCALS: []; MODULE: { TYPES: []; FUNCS: []; GLOBALS: []; TABLES: []; MEMS: []; TAGS: []; ELEMS: []; DATAS: []; EXPORTS: []; }; }. -2. Assert: Due to validation, $expanddt(s.FUNCS[funcaddr].TYPE) is of the case FUNC. -3. Let (FUNC functype_0) be $expanddt(s.FUNCS[funcaddr].TYPE). -4. Let (t_1* -> t_2*) be functype_0. +1. Assert: Due to validation, $expanddt(s.FUNCS[funcaddr].TYPE) is of the case FUNC. +2. Let (FUNC functype_0) be $expanddt(s.FUNCS[funcaddr].TYPE). +3. Let (t_1* -> t_2*) be functype_0. +4. Let f be { LOCALS: []; MODULE: { TYPES: []; FUNCS: []; GLOBALS: []; TABLES: []; MEMS: []; TAGS: []; ELEMS: []; DATAS: []; EXPORTS: []; }; }. 5. Assert: Due to validation, $Val_type(val, t_1)*. 6. Let k be |t_2*|. 7. Push the evaluation context (FRAME_ k { f }) to the stack.