From fa1f2f48298e560ffb3310bb3d8a3615c1465e1f Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 15 Feb 2024 23:01:16 +0100 Subject: [PATCH 1/2] Use bigints for representing nats --- spectec/README.md | 7 +- spectec/src/al/al_util.ml | 12 +- spectec/src/al/ast.ml | 4 +- spectec/src/al/dune | 2 +- spectec/src/al/print.ml | 8 +- spectec/src/backend-interpreter/builtin.ml | 10 +- spectec/src/backend-interpreter/construct.ml | 367 +++++++++--------- .../src/backend-interpreter/interpreter.ml | 49 +-- spectec/src/backend-interpreter/manual.ml | 10 +- spectec/src/backend-interpreter/numerics.ml | 274 ++++++------- spectec/src/backend-latex/render.ml | 36 +- spectec/src/backend-prose/render.ml | 5 +- spectec/src/el/ast.ml | 4 +- spectec/src/el/dune | 2 +- spectec/src/el/print.ml | 12 +- spectec/src/frontend/elab.ml | 2 +- spectec/src/frontend/lexer.mll | 19 +- spectec/src/frontend/parser.mly | 4 +- spectec/src/il/ast.ml | 2 +- spectec/src/il/dune | 2 +- spectec/src/il/print.ml | 2 +- spectec/src/il2al/translate.ml | 6 +- spectec/src/il2al/transpile.ml | 28 +- 23 files changed, 432 insertions(+), 435 deletions(-) diff --git a/spectec/README.md b/spectec/README.md index aa3968befc..bfcf23c204 100644 --- a/spectec/README.md +++ b/spectec/README.md @@ -135,7 +135,7 @@ Lowering from EL into IL infers additional information and makes it explicit in ### Prerequisites -You will need `ocaml` installed with `dune`, `menhir`, and `mdx` using `opam`. +You will need `ocaml` installed with `dune`, `menhir`, `mdx`, and the `zarith` library using `opam`. * Install `opam` version 2.0.5 or higher. ``` @@ -146,12 +146,11 @@ You will need `ocaml` installed with `dune`, `menhir`, and `mdx` using `opam`. * Set `ocaml` as version 5.0.0 or higher. ``` $ opam switch create 5.0.0 - $ opam install dune menhir mdx ``` -* Install `dune` version 3.11.0, `menhir` version 20230608, and `mdx` version 2.3.1 via `opam` (default versions) +* Install `dune` version 3.11.0, `menhir` version 20230608, `mdx` version 2.3.1, and `zarith` version 1.12, via `opam` (default versions) ``` - $ opam install dune menhir mdx + $ opam install dune menhir mdx zarith ``` ### Building the Project diff --git a/spectec/src/al/al_util.ml b/spectec/src/al/al_util.ml index 129c08a58c..1f81173632 100644 --- a/spectec/src/al/al_util.ml +++ b/spectec/src/al/al_util.ml @@ -80,7 +80,7 @@ let sliceP ?(at = no) (e1, e2) = SliceP (e1, e2) |> mk_path at let dotP ?(at = no) kwd = DotP kwd |> mk_path at let numV i = NumV i -let numV_of_int i = Int64.of_int i |> numV +let numV_of_int i = Z.of_int i |> numV let boolV b = BoolV b let vecV vec = VecV vec let strV r = StrV r @@ -90,8 +90,8 @@ let tupV vl = TupV vl let nullary s = CaseV (String.uppercase_ascii s, []) let listV a = ListV (ref a) let listV_of_list l = Array.of_list l |> listV -let zero = numV 0L -let one = numV 1L +let zero = numV Z.zero +let one = numV Z.one let empty_list = listV [||] let singleton v = listV [|v|] @@ -167,10 +167,10 @@ let get_body = function let unwrap_textv: value -> string = function | TextV str -> str | v -> fail "text" v -let unwrap_numv: value -> int64 = function - | NumV i64 -> i64 +let unwrap_numv: value -> Z.t = function + | NumV i -> i | v -> fail "int64" v -let unwrap_numv_to_int (v: value): int = unwrap_numv v |> Int64.to_int +let unwrap_numv_to_int (v: value): int = unwrap_numv v |> Z.to_int let unwrap_boolv: value -> bool = function | BoolV b -> b | v -> fail "boolean" v diff --git a/spectec/src/al/ast.ml b/spectec/src/al/ast.ml index a831bb49ea..c2e434d0b6 100644 --- a/spectec/src/al/ast.ml +++ b/spectec/src/al/ast.ml @@ -22,7 +22,7 @@ type ('a, 'b) record = ('a * 'b ref) list and store = (kwd', value) record and value = - | NumV of int64 (* number *) + | NumV of Z.t (* number *) | BoolV of bool (* boolean *) | VecV of vec128 (* vector *) | TextV of string (* string *) @@ -76,7 +76,7 @@ type iter = and expr = expr' phrase and expr' = | VarE of id (* varid *) - | NumE of int64 (* number *) + | NumE of Z.t (* number *) | BoolE of bool (* boolean *) | UnE of unop * expr (* unop expr *) | BinE of binop * expr * expr (* expr binop expr *) diff --git a/spectec/src/al/dune b/spectec/src/al/dune index 1560696e87..e7dd440785 100644 --- a/spectec/src/al/dune +++ b/spectec/src/al/dune @@ -1,5 +1,5 @@ (library (name al) - (libraries util) + (libraries util zarith) (modules ast al_util print walk free eq) ) diff --git a/spectec/src/al/print.ml b/spectec/src/al/print.ml index 80b3d4ed16..8677e42ad1 100644 --- a/spectec/src/al/print.ml +++ b/spectec/src/al/print.ml @@ -54,7 +54,7 @@ and string_of_value = function | FrameV _ -> "FrameV" | StoreV _ -> "StoreV" | ListV lv -> "[" ^ string_of_values ", " (Array.to_list !lv) ^ "]" - | NumV n -> Printf.sprintf "0x%LX" n + | NumV n -> "0x" ^ Z.format "%X" n | BoolV b -> string_of_bool b | VecV v -> "VecV (" ^ String.concat " " (List.init 4 (fun i -> Int32.to_string (Bytes.get_int32_le (Bytes.of_string v) (i*4)))) ^ ")" | TextV s -> s @@ -116,7 +116,7 @@ and string_of_record_expr r = and string_of_expr expr = match expr.it with - | NumE i -> Int64.to_string i + | NumE i -> Z.to_string i | BoolE b -> string_of_bool b | UnE (NotOp, { it = IsCaseOfE (e, kwd); _ }) -> sprintf "%s is not of the case %s" (string_of_expr e) (string_of_kwd kwd) @@ -346,7 +346,7 @@ let rec structured_string_of_value = function | StoreV _ -> "StoreV" | ListV _ -> "ListV" | BoolV b -> "BoolV (" ^ string_of_bool b ^ ")" - | NumV n -> "NumV (" ^ Int64.to_string n ^ ")" + | NumV n -> "NumV (" ^ Z.to_string n ^ ")" | VecV v -> "VecV (" ^ String.concat " " (List.init 4 (fun i -> Int32.to_string (Bytes.get_int32_le (Bytes.of_string v) (i*4)))) ^ ")" | TextV s -> "TextV (" ^ s ^ ")" | TupV vl -> "TupV (" ^ structured_string_of_values vl ^ ")" @@ -378,7 +378,7 @@ and structured_string_of_record_expr r = and structured_string_of_expr expr = match expr.it with - | NumE i -> Int64.to_string i + | NumE i -> Z.to_string i | BoolE b -> string_of_bool b | UnE (op, e) -> "UnE (" diff --git a/spectec/src/backend-interpreter/builtin.ml b/spectec/src/backend-interpreter/builtin.ml index f132a2ecda..085233243f 100644 --- a/spectec/src/backend-interpreter/builtin.ml +++ b/spectec/src/backend-interpreter/builtin.ml @@ -25,7 +25,7 @@ let builtin () = CaseV ("DEF", [ CaseV ("REC", [ [| CaseV ("SUBD", [none "FINAL"; listV [||]; ftype]) |] |> listV - ]); numV 0L + ]); numV Z.zero ]) in name, StrV [ "TYPE", ref (if !Construct.version = 3 then dt else arrow); @@ -70,14 +70,14 @@ let builtin () = let tables = [ "table", listV nulls - |> create_tableinst (TupV [ TupV [ numV 10L; numV 20L ]; nullary "FUNCREF" ]); + |> create_tableinst (TupV [ TupV [ numV (Z.of_int 10); numV (Z.of_int 20) ]; nullary "FUNCREF" ]); ] in (* Builtin memories *) - let zeros = numV 0L |> Array.make 0x10000 in + let zeros = numV Z.zero |> Array.make 0x10000 in let memories = [ "memory", listV zeros - |> create_meminst (CaseV ("I8", [ TupV [ numV 1L; numV 2L ] ])); + |> create_meminst (CaseV ("I8", [ TupV [ numV Z.one; numV (Z.of_int 2) ] ])); ] in let append kind (name, inst) extern = @@ -86,7 +86,7 @@ let builtin () = let addr = match Record.find kind (get_store ()) with - | ListV a -> Array.length !a |> Int64.of_int + | ListV a -> Array.length !a |> Z.of_int | _ -> failwith "Unreachable" in let new_extern = diff --git a/spectec/src/backend-interpreter/construct.ml b/spectec/src/backend-interpreter/construct.ml index 6f58c66476..9fae346714 100644 --- a/spectec/src/backend-interpreter/construct.ml +++ b/spectec/src/backend-interpreter/construct.ml @@ -37,9 +37,12 @@ let al_to_phrase (f: value -> 'a) (v: value): 'a phrase = f v @@ no_region (* Destruct minor *) -let al_to_int64: value -> int64 = unwrap_numv -let al_to_int (v: value): int = al_to_int64 v |> Int64.to_int -let al_to_int32 (v: value): int32 = al_to_int64 v |> Int64.to_int32 +let al_to_intN signed unsigned z = if z < Z.zero then signed z else unsigned z + +let al_to_z: value -> Z.t = unwrap_numv +let al_to_int (v: value): int = al_to_z v |> Z.to_int +let al_to_int32 (v: value): int32 = al_to_z v |> al_to_intN Z.to_int32 Z.to_int32_unsigned +let al_to_int64 (v: value): int64 = al_to_z v |> al_to_intN Z.to_int64 Z.to_int64_unsigned let al_to_float32 (v: value): F32.t = al_to_int32 v |> F32.of_bits let al_to_float64 (v: value): F64.t = al_to_int64 v |> F64.of_bits let al_to_idx: value -> idx = al_to_phrase al_to_int32 @@ -366,18 +369,25 @@ let al_to_cvtop: value list -> cvtop = function (* Vector operator *) +let two = Z.of_int 2 +let four = Z.of_int 4 +let eight = Z.of_int 8 +let sixteen = Z.of_int 16 +let thirtytwo = Z.of_int 32 +let sixtyfour = Z.of_int 64 + let al_to_extension : value -> Pack.extension = function | CaseV ("S", []) -> Pack.SX | CaseV ("U", []) -> Pack.ZX | v -> fail "extension" v let al_to_vop f1 f2 = function - | [ TupV [ CaseV ("I8", []); NumV 16L ]; CaseV ("_VI", [vop]) ] -> V128 (V128.I8x16 (f1 vop)) - | [ TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("_VI", [vop]) ] -> V128 (V128.I16x8 (f1 vop)) - | [ TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("_VI", [vop]) ] -> V128 (V128.I32x4 (f1 vop)) - | [ TupV [ CaseV ("I64", []); NumV 2L ]; CaseV ("_VI", [vop]) ] -> V128 (V128.I64x2 (f1 vop)) - | [ TupV [ CaseV ("F32", []); NumV 4L ]; CaseV ("_VF", [vop]) ] -> V128 (V128.F32x4 (f2 vop)) - | [ TupV [ CaseV ("F64", []); NumV 2L ]; CaseV ("_VF", [vop]) ] -> V128 (V128.F64x2 (f2 vop)) + | [ TupV [ CaseV ("I8", []); NumV z ]; CaseV ("_VI", [vop]) ] when z = sixteen -> V128 (V128.I8x16 (f1 vop)) + | [ TupV [ CaseV ("I16", []); NumV z ]; CaseV ("_VI", [vop]) ] when z = eight -> V128 (V128.I16x8 (f1 vop)) + | [ TupV [ CaseV ("I32", []); NumV z ]; CaseV ("_VI", [vop]) ] when z = four -> V128 (V128.I32x4 (f1 vop)) + | [ TupV [ CaseV ("I64", []); NumV z ]; CaseV ("_VI", [vop]) ] when z = two -> V128 (V128.I64x2 (f1 vop)) + | [ TupV [ CaseV ("F32", []); NumV z ]; CaseV ("_VF", [vop]) ] when z = four -> V128 (V128.F32x4 (f2 vop)) + | [ TupV [ CaseV ("F64", []); NumV z ]; CaseV ("_VF", [vop]) ] when z = two -> V128 (V128.F64x2 (f2 vop)) | l -> fail_list "vop" l let al_to_vvop f = function @@ -385,17 +395,17 @@ let al_to_vvop f = function | l -> fail_list "vvop" l let al_to_vtestop : value list -> vec_testop = function - | [ TupV [ CaseV ("I8", []); NumV 16L ] ] -> V128 (V128.I8x16 (V128Op.AllTrue)) - | [ TupV [ CaseV ("I16", []); NumV 8L ] ] -> V128 (V128.I16x8 (V128Op.AllTrue)) - | [ TupV [ CaseV ("I32", []); NumV 4L ] ] -> V128 (V128.I32x4 (V128Op.AllTrue)) - | [ TupV [ CaseV ("I64", []); NumV 2L ] ] -> V128 (V128.I64x2 (V128Op.AllTrue)) + | [ TupV [ CaseV ("I8", []); NumV z ] ] when z = sixteen -> V128 (V128.I8x16 (V128Op.AllTrue)) + | [ TupV [ CaseV ("I16", []); NumV z ] ] when z = eight -> V128 (V128.I16x8 (V128Op.AllTrue)) + | [ TupV [ CaseV ("I32", []); NumV z ] ] when z = four -> V128 (V128.I32x4 (V128Op.AllTrue)) + | [ TupV [ CaseV ("I64", []); NumV z ] ] when z = two -> V128 (V128.I64x2 (V128Op.AllTrue)) | l -> fail_list "vtestop" l let al_to_vbitmaskop : value list -> vec_bitmaskop = function - | [ TupV [ CaseV ("I8", []); NumV 16L ] ] -> V128 (V128.I8x16 (V128Op.Bitmask)) - | [ TupV [ CaseV ("I16", []); NumV 8L ] ] -> V128 (V128.I16x8 (V128Op.Bitmask)) - | [ TupV [ CaseV ("I32", []); NumV 4L ] ] -> V128 (V128.I32x4 (V128Op.Bitmask)) - | [ TupV [ CaseV ("I64", []); NumV 2L ] ] -> V128 (V128.I64x2 (V128Op.Bitmask)) + | [ TupV [ CaseV ("I8", []); NumV z ] ] when z = sixteen -> V128 (V128.I8x16 (V128Op.Bitmask)) + | [ TupV [ CaseV ("I16", []); NumV z ] ] when z = eight -> V128 (V128.I16x8 (V128Op.Bitmask)) + | [ TupV [ CaseV ("I32", []); NumV z ] ] when z = four -> V128 (V128.I32x4 (V128Op.Bitmask)) + | [ TupV [ CaseV ("I64", []); NumV z ] ] when z = two -> V128 (V128.I64x2 (V128Op.Bitmask)) | l -> fail_list "vbitmaskop" l let al_to_int_vrelop : value -> V128Op.irelop = function @@ -476,25 +486,25 @@ let al_to_float_vbinop : value -> V128Op.fbinop = function let al_to_vbinop : value list -> vec_binop = al_to_vop al_to_int_vbinop al_to_float_vbinop let al_to_special_vbinop = function - | CaseV ("VSWIZZLE", [ TupV [ CaseV ("I8", []); NumV 16L ]; ]) -> V128 (V128.I8x16 (V128Op.Swizzle)) - | CaseV ("VSHUFFLE", [ TupV [ CaseV ("I8", []); NumV 16L ]; l ]) -> V128 (V128.I8x16 (V128Op.Shuffle (al_to_list al_to_int l))) - | CaseV ("VNARROW", [ TupV [ CaseV ("I8", []); NumV 16L ]; TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("S", []) ]) -> V128 (V128.I8x16 (V128Op.NarrowS)) - | CaseV ("VNARROW", [ TupV [ CaseV ("I16", []); NumV 8L ]; TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("S", []) ]) -> V128 (V128.I16x8 (V128Op.NarrowS)) - | CaseV ("VNARROW", [ TupV [ CaseV ("I8", []); NumV 16L ]; TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("U", []) ]) -> V128 (V128.I8x16 (V128Op.NarrowU)) - | CaseV ("VNARROW", [ TupV [ CaseV ("I16", []); NumV 8L]; TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("U", []) ]) -> V128 (V128.I16x8 (V128Op.NarrowU)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("HIGH", []); TupV [ CaseV ("I8", []); NumV 16L ]; CaseV ("S", []) ]) -> V128 (V128.I16x8 (V128Op.ExtMulHighS)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("HIGH", []); TupV [ CaseV ("I8", []); NumV 16L ]; CaseV ("U", []) ]) -> V128 (V128.I16x8 (V128Op.ExtMulHighU)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("LOW", []); TupV [ CaseV ("I8", []); NumV 16L ]; CaseV ("S", []) ]) -> V128 (V128.I16x8 (V128Op.ExtMulLowS)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("LOW", []); TupV [ CaseV ("I8", []); NumV 16L ]; CaseV ("U", []) ] ) -> V128 (V128.I16x8 (V128Op.ExtMulLowU)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("HIGH", []); TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("S", []) ]) -> V128 (V128.I32x4 (V128Op.ExtMulHighS)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("HIGH", []); TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("U", []) ]) -> V128 (V128.I32x4 (V128Op.ExtMulHighU)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("LOW", []); TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("S", []) ]) -> V128 (V128.I32x4 (V128Op.ExtMulLowS)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("LOW", []); TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("U", []) ] ) -> V128 (V128.I32x4 (V128Op.ExtMulLowU)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I64", []); NumV 2L ]; CaseV ("HIGH", []); TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("S", []) ]) -> V128 (V128.I64x2 (V128Op.ExtMulHighS)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I64", []); NumV 2L ]; CaseV ("HIGH", []); TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("U", []) ]) -> V128 (V128.I64x2 (V128Op.ExtMulHighU)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I64", []); NumV 2L ]; CaseV ("LOW", []); TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("S", []) ]) -> V128 (V128.I64x2 (V128Op.ExtMulLowS)) - | CaseV ("VEXTMUL", [ TupV [ CaseV ("I64", []); NumV 2L ]; CaseV ("LOW", []); TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("U", []) ] ) -> V128 (V128.I64x2 (V128Op.ExtMulLowU)) - | CaseV ("VDOT", [ TupV [ CaseV ("I32", []); NumV 4L]; TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("S", []) ]) -> V128 (V128.I32x4 (V128Op.DotS)) + | CaseV ("VSWIZZLE", [ TupV [ CaseV ("I8", []); NumV z ]; ]) when z = sixteen -> V128 (V128.I8x16 (V128Op.Swizzle)) + | CaseV ("VSHUFFLE", [ TupV [ CaseV ("I8", []); NumV z ]; l ]) when z = sixteen -> V128 (V128.I8x16 (V128Op.Shuffle (al_to_list al_to_int l))) + | CaseV ("VNARROW", [ TupV [ CaseV ("I8", []); NumV z1 ]; TupV [ CaseV ("I16", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = sixteen && z2 = eight -> V128 (V128.I8x16 (V128Op.NarrowS)) + | CaseV ("VNARROW", [ TupV [ CaseV ("I16", []); NumV z1 ]; TupV [ CaseV ("I32", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = eight && z2 = four -> V128 (V128.I16x8 (V128Op.NarrowS)) + | CaseV ("VNARROW", [ TupV [ CaseV ("I8", []); NumV z1 ]; TupV [ CaseV ("I16", []); NumV z2 ]; CaseV ("U", []) ]) when z1 = sixteen && z2 = eight -> V128 (V128.I8x16 (V128Op.NarrowU)) + | CaseV ("VNARROW", [ TupV [ CaseV ("I16", []); NumV z1 ]; TupV [ CaseV ("I32", []); NumV z2 ]; CaseV ("U", []) ]) when z1 = eight && z2 = four -> V128 (V128.I16x8 (V128Op.NarrowU)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I16", []); NumV z1 ]; CaseV ("HIGH", []); TupV [ CaseV ("I8", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = eight && z2 = sixteen -> V128 (V128.I16x8 (V128Op.ExtMulHighS)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I16", []); NumV z1 ]; CaseV ("HIGH", []); TupV [ CaseV ("I8", []); NumV z2 ]; CaseV ("U", []) ]) when z1 = eight && z2 = sixteen -> V128 (V128.I16x8 (V128Op.ExtMulHighU)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I16", []); NumV z1 ]; CaseV ("LOW", []); TupV [ CaseV ("I8", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = eight && z2 = sixteen -> V128 (V128.I16x8 (V128Op.ExtMulLowS)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I16", []); NumV z1 ]; CaseV ("LOW", []); TupV [ CaseV ("I8", []); NumV z2 ]; CaseV ("U", []) ] ) when z1 = eight && z2 = sixteen -> V128 (V128.I16x8 (V128Op.ExtMulLowU)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I32", []); NumV z1 ]; CaseV ("HIGH", []); TupV [ CaseV ("I16", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = four && z2 = eight -> V128 (V128.I32x4 (V128Op.ExtMulHighS)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I32", []); NumV z1 ]; CaseV ("HIGH", []); TupV [ CaseV ("I16", []); NumV z2 ]; CaseV ("U", []) ]) when z1 = four && z2 = eight -> V128 (V128.I32x4 (V128Op.ExtMulHighU)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I32", []); NumV z1 ]; CaseV ("LOW", []); TupV [ CaseV ("I16", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = four && z2 = eight -> V128 (V128.I32x4 (V128Op.ExtMulLowS)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I32", []); NumV z1 ]; CaseV ("LOW", []); TupV [ CaseV ("I16", []); NumV z2 ]; CaseV ("U", []) ] ) when z1 = four && z2 = eight -> V128 (V128.I32x4 (V128Op.ExtMulLowU)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I64", []); NumV z1 ]; CaseV ("HIGH", []); TupV [ CaseV ("I32", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = two && z2 = four -> V128 (V128.I64x2 (V128Op.ExtMulHighS)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I64", []); NumV z1 ]; CaseV ("HIGH", []); TupV [ CaseV ("I32", []); NumV z2 ]; CaseV ("U", []) ]) when z1 = two && z2 = four -> V128 (V128.I64x2 (V128Op.ExtMulHighU)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I64", []); NumV z1 ]; CaseV ("LOW", []); TupV [ CaseV ("I32", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = two && z2 = four -> V128 (V128.I64x2 (V128Op.ExtMulLowS)) + | CaseV ("VEXTMUL", [ TupV [ CaseV ("I64", []); NumV z1 ]; CaseV ("LOW", []); TupV [ CaseV ("I32", []); NumV z2 ]; CaseV ("U", []) ] ) when z1 = two && z2 = four -> V128 (V128.I64x2 (V128Op.ExtMulLowU)) + | CaseV ("VDOT", [ TupV [ CaseV ("I32", []); NumV z1 ]; TupV [ CaseV ("I16", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = four && z2 = eight -> V128 (V128.I32x4 (V128Op.DotS)) | v -> fail "special vbinop" v let al_to_int_vcvtop : value list -> V128Op.icvtop = function @@ -510,10 +520,10 @@ let al_to_int_vcvtop : value list -> V128Op.icvtop = function ) | "TRUNC_SAT" -> ( match sh, ext with - | TupV [ CaseV ("F32", []); NumV 4L ], Some (CaseV ("S", [])) -> V128Op.TruncSatSF32x4 - | TupV [ CaseV ("F32", []); NumV 4L ], Some (CaseV ("U", [])) -> V128Op.TruncSatUF32x4 - | TupV [ CaseV ("F64", []); NumV 2L ], Some (CaseV ("S", [])) -> V128Op.TruncSatSZeroF64x2 - | TupV [ CaseV ("F64", []); NumV 2L ], Some (CaseV ("U", [])) -> V128Op.TruncSatUZeroF64x2 + | TupV [ CaseV ("F32", []); NumV z ], Some (CaseV ("S", [])) when z = four -> V128Op.TruncSatSF32x4 + | TupV [ CaseV ("F32", []); NumV z ], Some (CaseV ("U", [])) when z = four -> V128Op.TruncSatUF32x4 + | TupV [ CaseV ("F64", []); NumV z ], Some (CaseV ("S", [])) when z = two -> V128Op.TruncSatSZeroF64x2 + | TupV [ CaseV ("F64", []); NumV z ], Some (CaseV ("U", [])) when z = two -> V128Op.TruncSatUZeroF64x2 | _ -> fail_list "integer vcvtop" l ) | _ -> fail_list "integer vcvtop" l @@ -536,19 +546,19 @@ let al_to_float_vcvtop : value list -> V128Op.fcvtop = function | l -> fail_list "float vcvtop" l let al_to_vcvtop : value list -> vec_cvtop = function - | TupV [ CaseV ("I8", []); NumV 16L ] :: op -> V128 (V128.I8x16 (al_to_int_vcvtop op)) - | TupV [ CaseV ("I16", []); NumV 8L ] :: op -> V128 (V128.I16x8 (al_to_int_vcvtop op)) - | TupV [ CaseV ("I32", []); NumV 4L ] :: op -> V128 (V128.I32x4 (al_to_int_vcvtop op)) - | TupV [ CaseV ("I64", []); NumV 2L ] :: op -> V128 (V128.I64x2 (al_to_int_vcvtop op)) - | TupV [ CaseV ("F32", []); NumV 4L ] :: op -> V128 (V128.F32x4 (al_to_float_vcvtop op)) - | TupV [ CaseV ("F64", []); NumV 2L ] :: op -> V128 (V128.F64x2 (al_to_float_vcvtop op)) + | TupV [ CaseV ("I8", []); NumV z ] :: op when z = sixteen -> V128 (V128.I8x16 (al_to_int_vcvtop op)) + | TupV [ CaseV ("I16", []); NumV z ] :: op when z = eight -> V128 (V128.I16x8 (al_to_int_vcvtop op)) + | TupV [ CaseV ("I32", []); NumV z ] :: op when z = four -> V128 (V128.I32x4 (al_to_int_vcvtop op)) + | TupV [ CaseV ("I64", []); NumV z ] :: op when z = two -> V128 (V128.I64x2 (al_to_int_vcvtop op)) + | TupV [ CaseV ("F32", []); NumV z ] :: op when z = four -> V128 (V128.F32x4 (al_to_float_vcvtop op)) + | TupV [ CaseV ("F64", []); NumV z ] :: op when z = two -> V128 (V128.F64x2 (al_to_float_vcvtop op)) | l -> fail_list "vcvtop" l let al_to_special_vcvtop = function - | CaseV ("VEXTADD_PAIRWISE", [ TupV [ CaseV ("I16", []); NumV 8L]; TupV [ CaseV ("I8", []); NumV 16L ]; CaseV ("S", []) ]) -> V128 (V128.I16x8 (V128Op.ExtAddPairwiseS)) - | CaseV ("VEXTADD_PAIRWISE", [ TupV [ CaseV ("I16", []); NumV 8L]; TupV [ CaseV ("I8", []); NumV 16L ]; CaseV ("U", []) ]) -> V128 (V128.I16x8 (V128Op.ExtAddPairwiseU)) - | CaseV ("VEXTADD_PAIRWISE", [ TupV [ CaseV ("I32", []); NumV 4L]; TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("S", []) ]) -> V128 (V128.I32x4 (V128Op.ExtAddPairwiseS)) - | CaseV ("VEXTADD_PAIRWISE", [ TupV [ CaseV ("I32", []); NumV 4L]; TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("U", []) ]) -> V128 (V128.I32x4 (V128Op.ExtAddPairwiseU)) + | CaseV ("VEXTADD_PAIRWISE", [ TupV [ CaseV ("I16", []); NumV z1]; TupV [ CaseV ("I8", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = eight && z2 = sixteen -> V128 (V128.I16x8 (V128Op.ExtAddPairwiseS)) + | CaseV ("VEXTADD_PAIRWISE", [ TupV [ CaseV ("I16", []); NumV z1]; TupV [ CaseV ("I8", []); NumV z2 ]; CaseV ("U", []) ]) when z1 = eight && z2 = sixteen -> V128 (V128.I16x8 (V128Op.ExtAddPairwiseU)) + | CaseV ("VEXTADD_PAIRWISE", [ TupV [ CaseV ("I32", []); NumV z1]; TupV [ CaseV ("I16", []); NumV z2 ]; CaseV ("S", []) ]) when z1 = four && z2 = eight -> V128 (V128.I32x4 (V128Op.ExtAddPairwiseS)) + | CaseV ("VEXTADD_PAIRWISE", [ TupV [ CaseV ("I32", []); NumV z1]; TupV [ CaseV ("I16", []); NumV z2 ]; CaseV ("U", []) ]) when z1 = four && z2 = eight -> V128 (V128.I32x4 (V128Op.ExtAddPairwiseU)) | v -> fail "special vcvtop" v let al_to_int_vshiftop : value -> V128Op.ishiftop = function @@ -583,43 +593,43 @@ let al_to_vvternop' : value -> V128Op.vternop = function let al_to_vvternop : value list -> vec_vternop = al_to_vvop al_to_vvternop' let al_to_vsplatop : value list -> vec_splatop = function - | [ TupV [ CaseV ("I8", []); NumV 16L ] ] -> V128 (V128.I8x16 Splat) - | [ TupV [ CaseV ("I16", []); NumV 8L ] ] -> V128 (V128.I16x8 Splat) - | [ TupV [ CaseV ("I32", []); NumV 4L ] ] -> V128 (V128.I32x4 Splat) - | [ TupV [ CaseV ("I64", []); NumV 2L ] ] -> V128 (V128.I64x2 Splat) - | [ TupV [ CaseV ("F32", []); NumV 4L ] ] -> V128 (V128.F32x4 Splat) - | [ TupV [ CaseV ("F64", []); NumV 2L ] ] -> V128 (V128.F64x2 Splat) + | [ TupV [ CaseV ("I8", []); NumV z ] ] when z = sixteen -> V128 (V128.I8x16 Splat) + | [ TupV [ CaseV ("I16", []); NumV z ] ] when z = eight -> V128 (V128.I16x8 Splat) + | [ TupV [ CaseV ("I32", []); NumV z ] ] when z = four -> V128 (V128.I32x4 Splat) + | [ TupV [ CaseV ("I64", []); NumV z ] ] when z = two -> V128 (V128.I64x2 Splat) + | [ TupV [ CaseV ("F32", []); NumV z ] ] when z = four -> V128 (V128.F32x4 Splat) + | [ TupV [ CaseV ("F64", []); NumV z ] ] when z = two -> V128 (V128.F64x2 Splat) | vl -> fail_list "vsplatop" vl let al_to_vextractop : value list -> vec_extractop = function - | [ TupV [ CaseV ("I8", []); NumV 16L ]; OptV (Some ext); n ] -> + | [ TupV [ CaseV ("I8", []); NumV z ]; OptV (Some ext); n ] when z = sixteen -> V128 (V128.I8x16 (Extract (al_to_int n, al_to_extension ext))) - | [ TupV [ CaseV ("I16", []); NumV 8L ]; OptV (Some ext); n ] -> + | [ TupV [ CaseV ("I16", []); NumV z ]; OptV (Some ext); n ] when z = eight -> V128 (V128.I16x8 (Extract (al_to_int n, al_to_extension ext))) - | [ TupV [ CaseV ("I32", []); NumV 4L ]; OptV None; n ] -> + | [ TupV [ CaseV ("I32", []); NumV z ]; OptV None; n ] when z = four -> V128 (V128.I32x4 (Extract (al_to_int n, ()))) - | [ TupV [ CaseV ("I64", []); NumV 2L ]; OptV None; n ] -> + | [ TupV [ CaseV ("I64", []); NumV z ]; OptV None; n ] when z = two -> V128 (V128.I64x2 (Extract (al_to_int n, ()))) - | [ TupV [ CaseV ("F32", []); NumV 4L ]; OptV None; n ] -> + | [ TupV [ CaseV ("F32", []); NumV z ]; OptV None; n ] when z = four -> V128 (V128.F32x4 (Extract (al_to_int n, ()))) - | [ TupV [ CaseV ("F64", []); NumV 2L ]; OptV None; n ] -> + | [ TupV [ CaseV ("F64", []); NumV z ]; OptV None; n ] when z = two -> V128 (V128.F64x2 (Extract (al_to_int n, ()))) | vl -> fail_list "vextractop" vl let al_to_vreplaceop : value list -> vec_replaceop = function - | [ TupV [ CaseV ("I8", []); NumV 16L ]; n ] -> V128 (V128.I8x16 (Replace (al_to_int n))) - | [ TupV [ CaseV ("I16", []); NumV 8L ]; n ] -> V128 (V128.I16x8 (Replace (al_to_int n))) - | [ TupV [ CaseV ("I32", []); NumV 4L ]; n ] -> V128 (V128.I32x4 (Replace (al_to_int n))) - | [ TupV [ CaseV ("I64", []); NumV 2L ]; n ] -> V128 (V128.I64x2 (Replace (al_to_int n))) - | [ TupV [ CaseV ("F32", []); NumV 4L ]; n ] -> V128 (V128.F32x4 (Replace (al_to_int n))) - | [ TupV [ CaseV ("F64", []); NumV 2L ]; n ] -> V128 (V128.F64x2 (Replace (al_to_int n))) + | [ TupV [ CaseV ("I8", []); NumV z ]; n ] when z = sixteen -> V128 (V128.I8x16 (Replace (al_to_int n))) + | [ TupV [ CaseV ("I16", []); NumV z ]; n ] when z = eight -> V128 (V128.I16x8 (Replace (al_to_int n))) + | [ TupV [ CaseV ("I32", []); NumV z ]; n ] when z = four -> V128 (V128.I32x4 (Replace (al_to_int n))) + | [ TupV [ CaseV ("I64", []); NumV z ]; n ] when z = two -> V128 (V128.I64x2 (Replace (al_to_int n))) + | [ TupV [ CaseV ("F32", []); NumV z ]; n ] when z = four -> V128 (V128.F32x4 (Replace (al_to_int n))) + | [ TupV [ CaseV ("F64", []); NumV z ]; n ] when z = two -> V128 (V128.F64x2 (Replace (al_to_int n))) | vl -> fail_list "vreplaceop" vl let al_to_pack_size : value -> Pack.pack_size = function - | NumV 8L -> Pack.Pack8 - | NumV 16L -> Pack.Pack16 - | NumV 32L -> Pack.Pack32 - | NumV 64L -> Pack.Pack64 + | NumV z when z = eight -> Pack.Pack8 + | NumV z when z = sixteen -> Pack.Pack16 + | NumV z when z = thirtytwo -> Pack.Pack32 + | NumV z when z = sixtyfour -> Pack.Pack64 | v -> fail "pack_size" v let al_to_extension: value -> Pack.extension = function @@ -628,7 +638,7 @@ let al_to_extension: value -> Pack.extension = function | v -> fail "extension" v let al_to_memop (f: value -> 'p) : value list -> (num_type, 'p) memop = function - | [ nt; p; NumV 0L; StrV str ] -> + | [ nt; p; NumV z; StrV str ] when z = Z.zero -> { ty = al_to_num_type nt; align = Record.find "ALIGN" str |> al_to_int; @@ -651,7 +661,7 @@ let al_to_vmemop (f: value -> 'p): value list -> (vec_type, 'p) memop = function ty = V128T; align = Record.find "ALIGN" str |> al_to_int; offset = Record.find "OFFSET" str |> al_to_int32; - pack = f (numV 0L); + pack = f (numV Z.zero); } | [ p; StrV str ] -> { @@ -663,9 +673,9 @@ let al_to_vmemop (f: value -> 'p): value list -> (vec_type, 'p) memop = function | v -> fail_list "vmemop" v let al_to_pack_shape = function - | TupV [NumV 8L; NumV 8L] -> Pack.Pack8x8 - | TupV [NumV 16L; NumV 4L] -> Pack.Pack16x4 - | TupV [NumV 32L; NumV 2L] -> Pack.Pack32x2 + | TupV [NumV z1; NumV z2] when z1 = eight && z2 = eight -> Pack.Pack8x8 + | TupV [NumV z1; NumV z2] when z1 = sixteen && z2 = four -> Pack.Pack16x4 + | TupV [NumV z1; NumV z2] when z1 = thirtytwo && z2 = two -> Pack.Pack32x2 | v -> fail "pack shape" v let pack_shape_to_pack_size = function @@ -770,11 +780,11 @@ and al_to_instr': value -> Ast.instr' = function | CaseV ("VLOAD_LANE", vlaneop) -> VecLoadLane (al_to_vlaneop vlaneop) | CaseV ("VSTORE", vstoreop) -> VecStore (al_to_vstoreop vstoreop) | CaseV ("VSTORE_LANE", vlaneop) -> VecStoreLane (al_to_vlaneop vlaneop) - | CaseV ("MEMORY.SIZE", [ NumV 0L ]) -> MemorySize - | CaseV ("MEMORY.GROW", [ NumV 0L ]) -> MemoryGrow - | CaseV ("MEMORY.FILL", [ NumV 0L ]) -> MemoryFill - | CaseV ("MEMORY.COPY", [ NumV 0L; NumV 0L ]) -> MemoryCopy - | CaseV ("MEMORY.INIT", [ NumV 0L; idx ]) -> MemoryInit (al_to_idx idx) + | CaseV ("MEMORY.SIZE", [ NumV z ]) when z = Z.zero -> MemorySize + | CaseV ("MEMORY.GROW", [ NumV z ]) when z = Z.zero -> MemoryGrow + | CaseV ("MEMORY.FILL", [ NumV z ]) when z = Z.zero -> MemoryFill + | CaseV ("MEMORY.COPY", [ NumV z1; NumV z2 ]) when z1 = Z.zero && z2 = Z.zero -> MemoryCopy + | CaseV ("MEMORY.INIT", [ NumV z; idx ]) when z = Z.zero -> MemoryInit (al_to_idx idx) | CaseV ("DATA.DROP", [ idx ]) -> DataDrop (al_to_idx idx) | CaseV ("REF.AS_NON_NULL", []) -> RefAsNonNull | CaseV ("REF.TEST", [ rt ]) -> RefTest (al_to_ref_type rt) @@ -945,17 +955,20 @@ let al_of_opt f opt = Option.map f opt |> optV (* Construct minor *) -let al_of_int64 i64 = numV i64 -let al_of_int i = Int64.of_int i |> al_of_int64 +let al_of_z z = numV z +let al_of_int i = Z.of_int i |> al_of_z let al_of_int8 i8 = (* NOTE: int8 is considered to be unsigned *) - Int64.of_int32 i8 |> Int64.logand 0x0000_0000_0000_00ffL |> al_of_int64 + Z.of_int32 Int32.(logand i8 0x0000_00ffl) |> al_of_z let al_of_int16 i16 = (* NOTE: int32 is considered to be unsigned *) - Int64.of_int32 i16 |> Int64.logand 0x0000_0000_0000_ffffL |> al_of_int64 + Z.of_int32 Int32.(logand i16 0x0000_ffffl) |> al_of_z let al_of_int32 i32 = (* NOTE: int32 is considered to be unsigned *) - Int64.of_int32 i32 |> Int64.logand 0x0000_0000_ffff_ffffL |> al_of_int64 + Z.of_int32_unsigned i32 |> al_of_z +let al_of_int64 i64 = + (* NOTE: int32 is considered to be unsigned *) + Z.of_int64_unsigned i64 |> al_of_z let al_of_float32 f32 = F32.to_bits f32 |> al_of_int32 let al_of_float64 f64 = F64.to_bits f64 |> al_of_int64 let al_of_vector vec = V128.to_bits vec |> vecV @@ -1232,12 +1245,12 @@ let al_of_extension = function let al_of_vop f1 f2 = function | V128 vop -> ( match vop with - | V128.I8x16 op -> [ TupV [ nullary "I8"; numV 16L ]; f1 op ] - | V128.I16x8 op -> [ TupV [ nullary "I16"; numV 8L ]; f1 op ] - | V128.I32x4 op -> [ TupV [ nullary "I32"; numV 4L ]; f1 op ] - | V128.I64x2 op -> [ TupV [ nullary "I64"; numV 2L ]; f1 op ] - | V128.F32x4 op -> [ TupV [ nullary "F32"; numV 4L ]; f2 op ] - | V128.F64x2 op -> [ TupV [ nullary "F64"; numV 2L ]; f2 op ] + | V128.I8x16 op -> [ TupV [ nullary "I8"; numV sixteen ]; f1 op ] + | V128.I16x8 op -> [ TupV [ nullary "I16"; numV eight ]; f1 op ] + | V128.I32x4 op -> [ TupV [ nullary "I32"; numV four ]; f1 op ] + | V128.I64x2 op -> [ TupV [ nullary "I64"; numV two ]; f1 op ] + | V128.F32x4 op -> [ TupV [ nullary "F32"; numV four ]; f2 op ] + | V128.F64x2 op -> [ TupV [ nullary "F64"; numV two ]; f2 op ] ) let al_of_viop f1: @@ -1245,20 +1258,20 @@ let al_of_viop f1: function | V128 vop -> ( match vop with - | V128.I8x16 op -> [ TupV [ nullary "I8"; numV 16L ]; f1 op ] - | V128.I16x8 op -> [ TupV [ nullary "I16"; numV 8L ]; f1 op ] - | V128.I32x4 op -> [ TupV [ nullary "I32"; numV 4L ]; f1 op ] - | V128.I64x2 op -> [ TupV [ nullary "I64"; numV 2L ]; f1 op ] + | V128.I8x16 op -> [ TupV [ nullary "I8"; numV sixteen ]; f1 op ] + | V128.I16x8 op -> [ TupV [ nullary "I16"; numV eight ]; f1 op ] + | V128.I32x4 op -> [ TupV [ nullary "I32"; numV four ]; f1 op ] + | V128.I64x2 op -> [ TupV [ nullary "I64"; numV two ]; f1 op ] | _ -> . ) let al_of_vtestop = function | V128 vop -> ( match vop with - | V128.I8x16 _ -> [ TupV [ nullary "I8"; numV 16L ] ] - | V128.I16x8 _ -> [ TupV [ nullary "I16"; numV 8L ] ] - | V128.I32x4 _ -> [ TupV [ nullary "I32"; numV 4L ] ] - | V128.I64x2 _ -> [ TupV [ nullary "I64"; numV 2L ] ] + | V128.I8x16 _ -> [ TupV [ nullary "I8"; numV sixteen ] ] + | V128.I16x8 _ -> [ TupV [ nullary "I16"; numV eight ] ] + | V128.I32x4 _ -> [ TupV [ nullary "I32"; numV four ] ] + | V128.I64x2 _ -> [ TupV [ nullary "I64"; numV two ] ] | _ -> failwith "Invalid shape" ) @@ -1329,34 +1342,34 @@ let al_of_float_vbinop : V128Op.fbinop -> value = function let al_of_vbinop = function | V128 vop -> ( match vop with - | V128.I8x16 op -> Option.map (fun v -> [ TupV [ nullary "I8"; numV 16L ]; v ]) (al_of_int_vbinop op) - | V128.I16x8 op -> Option.map (fun v -> [ TupV [ nullary "I16"; numV 8L ]; v ]) (al_of_int_vbinop op) - | V128.I32x4 op -> Option.map (fun v -> [ TupV [ nullary "I32"; numV 4L ]; v ]) (al_of_int_vbinop op) - | V128.I64x2 op -> Option.map (fun v -> [ TupV [ nullary "I64"; numV 2L ]; v ]) (al_of_int_vbinop op) - | V128.F32x4 op -> Some ([ TupV [ nullary "F32"; numV 4L ]; al_of_float_vbinop op ]) - | V128.F64x2 op -> Some ([ TupV [ nullary "F64"; numV 2L ]; al_of_float_vbinop op ]) + | V128.I8x16 op -> Option.map (fun v -> [ TupV [ nullary "I8"; numV sixteen ]; v ]) (al_of_int_vbinop op) + | V128.I16x8 op -> Option.map (fun v -> [ TupV [ nullary "I16"; numV eight ]; v ]) (al_of_int_vbinop op) + | V128.I32x4 op -> Option.map (fun v -> [ TupV [ nullary "I32"; numV four ]; v ]) (al_of_int_vbinop op) + | V128.I64x2 op -> Option.map (fun v -> [ TupV [ nullary "I64"; numV two ]; v ]) (al_of_int_vbinop op) + | V128.F32x4 op -> Some ([ TupV [ nullary "F32"; numV four ]; al_of_float_vbinop op ]) + | V128.F64x2 op -> Some ([ TupV [ nullary "F64"; numV two ]; al_of_float_vbinop op ]) ) let al_of_special_vbinop = function - | V128 (V128.I8x16 (V128Op.Swizzle)) -> CaseV ("VSWIZZLE", [ TupV [ nullary "I8"; numV 16L ]; ]) - | V128 (V128.I8x16 (V128Op.Shuffle l)) -> CaseV ("VSHUFFLE", [ TupV [ nullary "I8"; numV 16L ]; al_of_list al_of_int l ]) - | V128 (V128.I8x16 (V128Op.NarrowS)) -> CaseV ("VNARROW", [ TupV [ nullary "I8"; numV 16L ]; TupV [ nullary "I16"; numV 8L ]; al_of_extension Pack.SX ]) - | V128 (V128.I16x8 (V128Op.NarrowS)) -> CaseV ("VNARROW", [ TupV [ nullary "I16"; numV 8L ]; TupV [ nullary "I32"; numV 4L ]; al_of_extension Pack.SX ]) - | V128 (V128.I8x16 (V128Op.NarrowU)) -> CaseV ("VNARROW", [ TupV [ nullary "I8"; numV 16L ]; TupV [ nullary "I16"; numV 8L ]; al_of_extension Pack.ZX ]) - | V128 (V128.I16x8 (V128Op.NarrowU)) -> CaseV ("VNARROW", [ TupV [ nullary "I16"; numV 8L]; TupV [ nullary "I32"; numV 4L ]; al_of_extension Pack.ZX ]) - | V128 (V128.I16x8 (V128Op.ExtMulHighS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I16"; numV 8L ]; nullary "HIGH"; TupV [ nullary "I8"; numV 16L ]; al_of_extension Pack.SX ]) - | V128 (V128.I16x8 (V128Op.ExtMulHighU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I16"; numV 8L ]; nullary "HIGH"; TupV [ nullary "I8"; numV 16L ]; al_of_extension Pack.ZX ]) - | V128 (V128.I16x8 (V128Op.ExtMulLowS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I16"; numV 8L ]; nullary "LOW"; TupV [ nullary "I8"; numV 16L ]; al_of_extension Pack.SX ]) - | V128 (V128.I16x8 (V128Op.ExtMulLowU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I16"; numV 8L ]; nullary "LOW"; TupV [ nullary "I8"; numV 16L ]; al_of_extension Pack.ZX ] ) - | V128 (V128.I32x4 (V128Op.ExtMulHighS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I32"; numV 4L ]; nullary "HIGH"; TupV [ nullary "I16"; numV 8L ]; al_of_extension Pack.SX ]) - | V128 (V128.I32x4 (V128Op.ExtMulHighU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I32"; numV 4L ]; nullary "HIGH"; TupV [ nullary "I16"; numV 8L ]; al_of_extension Pack.ZX ]) - | V128 (V128.I32x4 (V128Op.ExtMulLowS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I32"; numV 4L ]; nullary "LOW"; TupV [ nullary "I16"; numV 8L ]; al_of_extension Pack.SX ]) - | V128 (V128.I32x4 (V128Op.ExtMulLowU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I32"; numV 4L ]; nullary "LOW"; TupV [ nullary "I16"; numV 8L ]; al_of_extension Pack.ZX ] ) - | V128 (V128.I64x2 (V128Op.ExtMulHighS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I64"; numV 2L ]; nullary "HIGH"; TupV [ nullary "I32"; numV 4L ]; al_of_extension Pack.SX ]) - | V128 (V128.I64x2 (V128Op.ExtMulHighU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I64"; numV 2L ]; nullary "HIGH"; TupV [ nullary "I32"; numV 4L ]; al_of_extension Pack.ZX ]) - | V128 (V128.I64x2 (V128Op.ExtMulLowS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I64"; numV 2L ]; nullary "LOW"; TupV [ nullary "I32"; numV 4L ]; al_of_extension Pack.SX ]) - | V128 (V128.I64x2 (V128Op.ExtMulLowU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I64"; numV 2L ]; nullary "LOW"; TupV [ nullary "I32"; numV 4L ]; al_of_extension Pack.ZX ] ) - | V128 (V128.I32x4 (V128Op.DotS)) -> CaseV ("VDOT", [ TupV [ nullary "I32"; numV 4L]; TupV [ nullary "I16"; numV 8L ]; al_of_extension Pack.SX ]) + | V128 (V128.I8x16 (V128Op.Swizzle)) -> CaseV ("VSWIZZLE", [ TupV [ nullary "I8"; numV sixteen ]; ]) + | V128 (V128.I8x16 (V128Op.Shuffle l)) -> CaseV ("VSHUFFLE", [ TupV [ nullary "I8"; numV sixteen ]; al_of_list al_of_int l ]) + | V128 (V128.I8x16 (V128Op.NarrowS)) -> CaseV ("VNARROW", [ TupV [ nullary "I8"; numV sixteen ]; TupV [ nullary "I16"; numV eight ]; al_of_extension Pack.SX ]) + | V128 (V128.I16x8 (V128Op.NarrowS)) -> CaseV ("VNARROW", [ TupV [ nullary "I16"; numV eight ]; TupV [ nullary "I32"; numV four ]; al_of_extension Pack.SX ]) + | V128 (V128.I8x16 (V128Op.NarrowU)) -> CaseV ("VNARROW", [ TupV [ nullary "I8"; numV sixteen ]; TupV [ nullary "I16"; numV eight ]; al_of_extension Pack.ZX ]) + | V128 (V128.I16x8 (V128Op.NarrowU)) -> CaseV ("VNARROW", [ TupV [ nullary "I16"; numV eight]; TupV [ nullary "I32"; numV four ]; al_of_extension Pack.ZX ]) + | V128 (V128.I16x8 (V128Op.ExtMulHighS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I16"; numV eight ]; nullary "HIGH"; TupV [ nullary "I8"; numV sixteen ]; al_of_extension Pack.SX ]) + | V128 (V128.I16x8 (V128Op.ExtMulHighU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I16"; numV eight ]; nullary "HIGH"; TupV [ nullary "I8"; numV sixteen ]; al_of_extension Pack.ZX ]) + | V128 (V128.I16x8 (V128Op.ExtMulLowS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I16"; numV eight ]; nullary "LOW"; TupV [ nullary "I8"; numV sixteen ]; al_of_extension Pack.SX ]) + | V128 (V128.I16x8 (V128Op.ExtMulLowU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I16"; numV eight ]; nullary "LOW"; TupV [ nullary "I8"; numV sixteen ]; al_of_extension Pack.ZX ] ) + | V128 (V128.I32x4 (V128Op.ExtMulHighS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I32"; numV four ]; nullary "HIGH"; TupV [ nullary "I16"; numV eight ]; al_of_extension Pack.SX ]) + | V128 (V128.I32x4 (V128Op.ExtMulHighU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I32"; numV four ]; nullary "HIGH"; TupV [ nullary "I16"; numV eight ]; al_of_extension Pack.ZX ]) + | V128 (V128.I32x4 (V128Op.ExtMulLowS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I32"; numV four ]; nullary "LOW"; TupV [ nullary "I16"; numV eight ]; al_of_extension Pack.SX ]) + | V128 (V128.I32x4 (V128Op.ExtMulLowU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I32"; numV four ]; nullary "LOW"; TupV [ nullary "I16"; numV eight ]; al_of_extension Pack.ZX ] ) + | V128 (V128.I64x2 (V128Op.ExtMulHighS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I64"; numV two ]; nullary "HIGH"; TupV [ nullary "I32"; numV four ]; al_of_extension Pack.SX ]) + | V128 (V128.I64x2 (V128Op.ExtMulHighU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I64"; numV two ]; nullary "HIGH"; TupV [ nullary "I32"; numV four ]; al_of_extension Pack.ZX ]) + | V128 (V128.I64x2 (V128Op.ExtMulLowS)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I64"; numV two ]; nullary "LOW"; TupV [ nullary "I32"; numV four ]; al_of_extension Pack.SX ]) + | V128 (V128.I64x2 (V128Op.ExtMulLowU)) -> CaseV ("VEXTMUL", [ TupV [ nullary "I64"; numV two ]; nullary "LOW"; TupV [ nullary "I32"; numV four ]; al_of_extension Pack.ZX ] ) + | V128 (V128.I32x4 (V128Op.DotS)) -> CaseV ("VDOT", [ TupV [ nullary "I32"; numV four]; TupV [ nullary "I16"; numV eight ]; al_of_extension Pack.SX ]) | _ -> failwith "invalid special vbinop" let al_of_int_vcvtop = function @@ -1364,22 +1377,22 @@ let al_of_int_vcvtop = function | V128Op.ExtendLowU -> Some (nullary "EXTEND", Some (nullary "LOW"), None, Some (nullary "U"), None) | V128Op.ExtendHighS -> Some (nullary "EXTEND", Some (nullary "HIGH"), None, Some (nullary "S"), None) | V128Op.ExtendHighU -> Some (nullary "EXTEND", Some (nullary "HIGH"), None, Some (nullary "U"), None) - | V128Op.TruncSatSF32x4 -> Some (nullary "TRUNC_SAT", None, Some (TupV [ nullary "F32"; numV 4L ]), Some (nullary "S"), None) - | V128Op.TruncSatUF32x4 -> Some (nullary "TRUNC_SAT", None, Some (TupV [ nullary "F32"; numV 4L ]), Some (nullary "U"), None) - | V128Op.TruncSatSZeroF64x2 -> Some (nullary "TRUNC_SAT", None, Some (TupV [ nullary "F64"; numV 2L ]), Some (nullary "S"), Some (tupV [])) - | V128Op.TruncSatUZeroF64x2 -> Some (nullary "TRUNC_SAT", None, Some (TupV [ nullary "F64"; numV 2L ]), Some (nullary "U"), Some (tupV [])) + | V128Op.TruncSatSF32x4 -> Some (nullary "TRUNC_SAT", None, Some (TupV [ nullary "F32"; numV four ]), Some (nullary "S"), None) + | V128Op.TruncSatUF32x4 -> Some (nullary "TRUNC_SAT", None, Some (TupV [ nullary "F32"; numV four ]), Some (nullary "U"), None) + | V128Op.TruncSatSZeroF64x2 -> Some (nullary "TRUNC_SAT", None, Some (TupV [ nullary "F64"; numV two ]), Some (nullary "S"), Some (tupV [])) + | V128Op.TruncSatUZeroF64x2 -> Some (nullary "TRUNC_SAT", None, Some (TupV [ nullary "F64"; numV two ]), Some (nullary "U"), Some (tupV [])) | _ -> None let al_of_float32_vcvtop = function - | V128Op.DemoteZeroF64x2 -> Some (nullary "DEMOTE", None, Some (TupV [ nullary "F64"; numV 2L ]), None, Some (tupV [])) - | V128Op.ConvertSI32x4 -> Some (nullary "CONVERT", None, Some (TupV [ nullary "I32"; numV 4L ]), Some (nullary "S"), None) - | V128Op.ConvertUI32x4 -> Some (nullary "CONVERT", None, Some (TupV [ nullary "I32"; numV 4L ]), Some (nullary "U"), None) + | V128Op.DemoteZeroF64x2 -> Some (nullary "DEMOTE", None, Some (TupV [ nullary "F64"; numV two ]), None, Some (tupV [])) + | V128Op.ConvertSI32x4 -> Some (nullary "CONVERT", None, Some (TupV [ nullary "I32"; numV four ]), Some (nullary "S"), None) + | V128Op.ConvertUI32x4 -> Some (nullary "CONVERT", None, Some (TupV [ nullary "I32"; numV four ]), Some (nullary "U"), None) | _ -> None let al_of_float64_vcvtop = function - | V128Op.PromoteLowF32x4 -> Some (nullary "PROMOTE", Some (nullary "LOW"), Some (TupV [ nullary "F32"; numV 4L ]), None, None) - | V128Op.ConvertSI32x4 -> Some (nullary "CONVERT", Some (nullary "LOW"), Some (TupV [ nullary "I32"; numV 4L ]), Some (nullary "S"), None) - | V128Op.ConvertUI32x4 -> Some (nullary "CONVERT", Some (nullary "LOW"), Some (TupV [ nullary "I32"; numV 4L ]), Some (nullary "U"), None) + | V128Op.PromoteLowF32x4 -> Some (nullary "PROMOTE", Some (nullary "LOW"), Some (TupV [ nullary "F32"; numV four ]), None, None) + | V128Op.ConvertSI32x4 -> Some (nullary "CONVERT", Some (nullary "LOW"), Some (TupV [ nullary "I32"; numV four ]), Some (nullary "S"), None) + | V128Op.ConvertUI32x4 -> Some (nullary "CONVERT", Some (nullary "LOW"), Some (TupV [ nullary "I32"; numV four ]), Some (nullary "U"), None) | _ -> None let al_of_vcvtop = function @@ -1390,39 +1403,39 @@ let al_of_vcvtop = function let sh = match to_ with Some sh -> sh | None -> ( match half with | Some _ -> failwith "invalid vcvtop" - | None -> TupV [ nullary "I8"; numV 16L ] + | None -> TupV [ nullary "I8"; numV sixteen ] ) in - [ TupV [ nullary "I8"; numV 16L ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] + [ TupV [ nullary "I8"; numV sixteen ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] ) (al_of_int_vcvtop op) ) | V128.I16x8 op -> ( Option.map (fun (op', half, to_, ext, zero) -> let sh = match to_ with Some sh -> sh | None -> ( match half with - | Some _ -> TupV [ nullary "I8"; numV 16L ] - | None -> TupV [ nullary "I16"; numV 8L ] + | Some _ -> TupV [ nullary "I8"; numV sixteen ] + | None -> TupV [ nullary "I16"; numV eight ] ) in - [ TupV [ nullary "I16"; numV 8L ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] + [ TupV [ nullary "I16"; numV eight ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] ) (al_of_int_vcvtop op) ) | V128.I32x4 op -> ( Option.map (fun (op', half, to_, ext, zero) -> let sh = match to_ with Some sh -> sh | None -> ( match half with - | Some _ -> TupV [ nullary "I16"; numV 8L ] - | None -> TupV [ nullary "I32"; numV 4L ] + | Some _ -> TupV [ nullary "I16"; numV eight ] + | None -> TupV [ nullary "I32"; numV four ] ) in - [ TupV [ nullary "I32"; numV 4L ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] + [ TupV [ nullary "I32"; numV four ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] ) (al_of_int_vcvtop op) ) | V128.I64x2 op -> ( Option.map (fun (op', half, to_, ext, zero) -> let sh = match to_ with Some sh -> sh | None -> ( match half with - | Some _ -> TupV [ nullary "I32"; numV 4L ] - | None -> TupV [ nullary "I64"; numV 2L ] + | Some _ -> TupV [ nullary "I32"; numV four ] + | None -> TupV [ nullary "I64"; numV two ] ) in - [ TupV [ nullary "I64"; numV 2L ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] + [ TupV [ nullary "I64"; numV two ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] ) (al_of_int_vcvtop op) ) | V128.F32x4 op -> ( @@ -1430,29 +1443,29 @@ let al_of_vcvtop = function let sh = match to_ with Some sh -> sh | None -> ( match half with | Some _ -> failwith "invalid vcvtop" - | None -> TupV [ nullary "F32"; numV 4L ] + | None -> TupV [ nullary "F32"; numV four ] ) in - [ TupV [ nullary "F32"; numV 4L ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] + [ TupV [ nullary "F32"; numV four ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] ) (al_of_float32_vcvtop op) ) | V128.F64x2 op -> ( Option.map (fun (op', half, to_, ext, zero) -> let sh = match to_ with Some sh -> sh | None -> ( match half with - | Some _ -> TupV [ nullary "F32"; numV 4L ] - | None -> TupV [ nullary "F64"; numV 2L ] + | Some _ -> TupV [ nullary "F32"; numV four ] + | None -> TupV [ nullary "F64"; numV two ] ) in - [ TupV [ nullary "F64"; numV 2L ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] + [ TupV [ nullary "F64"; numV two ]; op'; optV half; sh; optV ext; CaseV ("ZERO", [OptV zero]) ] ) (al_of_float64_vcvtop op) ) ) let al_of_special_vcvtop = function - | V128 (V128.I16x8 (V128Op.ExtAddPairwiseS)) -> CaseV ("VEXTADD_PAIRWISE", [ TupV [ nullary "I16"; numV 8L]; TupV [ nullary "I8"; numV 16L ]; al_of_extension Pack.SX ]) - | V128 (V128.I16x8 (V128Op.ExtAddPairwiseU)) -> CaseV ("VEXTADD_PAIRWISE", [ TupV [ nullary "I16"; numV 8L]; TupV [ nullary "I8"; numV 16L ]; al_of_extension Pack.ZX ]) - | V128 (V128.I32x4 (V128Op.ExtAddPairwiseS)) -> CaseV ("VEXTADD_PAIRWISE", [ TupV [ nullary "I32"; numV 4L]; TupV [ nullary "I16"; numV 8L ]; al_of_extension Pack.SX ]) - | V128 (V128.I32x4 (V128Op.ExtAddPairwiseU)) -> CaseV ("VEXTADD_PAIRWISE", [ TupV [ nullary "I32"; numV 4L]; TupV [ nullary "I16"; numV 8L ]; al_of_extension Pack.ZX ]) + | V128 (V128.I16x8 (V128Op.ExtAddPairwiseS)) -> CaseV ("VEXTADD_PAIRWISE", [ TupV [ nullary "I16"; numV eight]; TupV [ nullary "I8"; numV sixteen ]; al_of_extension Pack.SX ]) + | V128 (V128.I16x8 (V128Op.ExtAddPairwiseU)) -> CaseV ("VEXTADD_PAIRWISE", [ TupV [ nullary "I16"; numV eight]; TupV [ nullary "I8"; numV sixteen ]; al_of_extension Pack.ZX ]) + | V128 (V128.I32x4 (V128Op.ExtAddPairwiseS)) -> CaseV ("VEXTADD_PAIRWISE", [ TupV [ nullary "I32"; numV four]; TupV [ nullary "I16"; numV eight ]; al_of_extension Pack.SX ]) + | V128 (V128.I32x4 (V128Op.ExtAddPairwiseU)) -> CaseV ("VEXTADD_PAIRWISE", [ TupV [ nullary "I32"; numV four]; TupV [ nullary "I16"; numV eight ]; al_of_extension Pack.ZX ]) | _ -> failwith "invalid vcvtop" let al_of_int_vshiftop : V128Op.ishiftop -> value = function @@ -1494,12 +1507,12 @@ let al_of_vvternop : vec_vternop -> value list = function let al_of_vsplatop : vec_splatop -> value list = function | V128 vop -> ( match vop with - | V128.I8x16 _ -> [ TupV [ nullary "I8"; numV 16L ] ] - | V128.I16x8 _ -> [ TupV [ nullary "I16"; numV 8L ] ] - | V128.I32x4 _ -> [ TupV [ nullary "I32"; numV 4L ] ] - | V128.I64x2 _ -> [ TupV [ nullary "I64"; numV 2L ] ] - | V128.F32x4 _ -> [ TupV [ nullary "F32"; numV 4L ] ] - | V128.F64x2 _ -> [ TupV [ nullary "F64"; numV 2L ] ] + | V128.I8x16 _ -> [ TupV [ nullary "I8"; numV sixteen ] ] + | V128.I16x8 _ -> [ TupV [ nullary "I16"; numV eight ] ] + | V128.I32x4 _ -> [ TupV [ nullary "I32"; numV four ] ] + | V128.I64x2 _ -> [ TupV [ nullary "I64"; numV two ] ] + | V128.F32x4 _ -> [ TupV [ nullary "F32"; numV four ] ] + | V128.F64x2 _ -> [ TupV [ nullary "F64"; numV two ] ] ) let al_of_vextractop : vec_extractop -> value list = function @@ -1508,40 +1521,40 @@ let al_of_vextractop : vec_extractop -> value list = function | V128.I8x16 vop' -> ( match vop' with | Extract (n, ext) -> - [ TupV [ nullary "I8"; numV 16L ]; optV (Some (al_of_extension ext)); al_of_int n; ] + [ TupV [ nullary "I8"; numV sixteen ]; optV (Some (al_of_extension ext)); al_of_int n; ] ) | V128.I16x8 vop' -> ( match vop' with | Extract (n, ext) -> - [ TupV [ nullary "I16"; numV 8L ]; optV (Some (al_of_extension ext)); al_of_int n; ] + [ TupV [ nullary "I16"; numV eight ]; optV (Some (al_of_extension ext)); al_of_int n; ] ) | V128.I32x4 vop' -> ( match vop' with - | Extract (n, _) -> [ TupV [ nullary "I32"; numV 4L ]; optV None; al_of_int n ] + | Extract (n, _) -> [ TupV [ nullary "I32"; numV four ]; optV None; al_of_int n ] ) | V128.I64x2 vop' -> ( match vop' with - | Extract (n, _) -> [ TupV [ nullary "I64"; numV 2L ]; optV None; al_of_int n ] + | Extract (n, _) -> [ TupV [ nullary "I64"; numV two ]; optV None; al_of_int n ] ) | V128.F32x4 vop' -> ( match vop' with - | Extract (n, _) -> [ TupV [ nullary "F32"; numV 4L ]; optV None; al_of_int n ] + | Extract (n, _) -> [ TupV [ nullary "F32"; numV four ]; optV None; al_of_int n ] ) | V128.F64x2 vop' -> ( match vop' with - | Extract (n, _) -> [ TupV [ nullary "F64"; numV 2L ]; optV None; al_of_int n ] + | Extract (n, _) -> [ TupV [ nullary "F64"; numV two ]; optV None; al_of_int n ] ) ) let al_of_vreplaceop : vec_replaceop -> value list = function | V128 vop -> ( match vop with - | V128.I8x16 (Replace n) -> [ TupV [ nullary "I8"; numV 16L ]; al_of_int n ] - | V128.I16x8 (Replace n) -> [ TupV [ nullary "I16"; numV 8L ]; al_of_int n ] - | V128.I32x4 (Replace n) -> [ TupV [ nullary "I32"; numV 4L ]; al_of_int n ] - | V128.I64x2 (Replace n) -> [ TupV [ nullary "I64"; numV 2L ]; al_of_int n ] - | V128.F32x4 (Replace n) -> [ TupV [ nullary "F32"; numV 4L ]; al_of_int n ] - | V128.F64x2 (Replace n) -> [ TupV [ nullary "F64"; numV 2L ]; al_of_int n ] + | V128.I8x16 (Replace n) -> [ TupV [ nullary "I8"; numV sixteen ]; al_of_int n ] + | V128.I16x8 (Replace n) -> [ TupV [ nullary "I16"; numV eight ]; al_of_int n ] + | V128.I32x4 (Replace n) -> [ TupV [ nullary "I32"; numV four ]; al_of_int n ] + | V128.I64x2 (Replace n) -> [ TupV [ nullary "I64"; numV two ]; al_of_int n ] + | V128.F32x4 (Replace n) -> [ TupV [ nullary "F32"; numV four ]; al_of_int n ] + | V128.F64x2 (Replace n) -> [ TupV [ nullary "F64"; numV two ]; al_of_int n ] ) let al_of_pack_size = function @@ -1551,9 +1564,9 @@ let al_of_pack_size = function | Pack.Pack64 -> al_of_int 64 let al_of_pack_shape = function - | Pack.Pack8x8 -> TupV [NumV 8L; NumV 8L] - | Pack.Pack16x4 -> TupV [NumV 16L; NumV 4L] - | Pack.Pack32x2 -> TupV [NumV 32L; NumV 2L] + | Pack.Pack8x8 -> TupV [NumV eight; NumV eight] + | Pack.Pack16x4 -> TupV [NumV sixteen; NumV four] + | Pack.Pack32x2 -> TupV [NumV thirtytwo; NumV two] let al_of_extension = function | Pack.SX -> nullary "S" diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml index 66051a8d29..9786e5a176 100644 --- a/spectec/src/backend-interpreter/interpreter.ml +++ b/spectec/src/backend-interpreter/interpreter.ml @@ -26,7 +26,7 @@ let fail_on_path msg path = let check_i32_const = function | CaseV ("CONST", [ CaseV ("I32", []); NumV (n) ]) -> - let n' = Int64.logand 0xFFFFFFFFL n in + let n' = Z.logand (Z.of_int64 0xFFFF_FFFFL) n in CaseV ("CONST", [ CaseV ("I32", []); NumV (n') ]) | v -> v let rec is_true = function @@ -34,19 +34,6 @@ let rec is_true = function | ListV a -> Array.for_all is_true !a | _ -> false -let rec int64_exp base exponent = - if exponent = 0L then - 1L - else if exponent = 1L then - base - else - let half_pow = int64_exp base (Int64.div exponent 2L) in - let pow = Int64.mul half_pow half_pow in - if Int64.rem exponent 2L = 0L then - pow - else - Int64.mul base pow - let is_matrix matrix = match matrix with | [] -> true (* Empty matrix is considered a valid matrix *) @@ -166,15 +153,15 @@ and eval_expr expr = (* Value *) | NumE i -> numV i (* Numeric Operation *) - | UnE (MinusOp, inner_e) -> eval_expr inner_e |> al_to_int64 |> Int64.neg |> numV + | UnE (MinusOp, inner_e) -> eval_expr inner_e |> al_to_z |> Z.neg |> numV | UnE (NotOp, e) -> eval_expr e |> al_to_bool |> not |> boolV | BinE (op, e1, e2) -> (match op, eval_expr e1, eval_expr e2 with - | AddOp, NumV i1, NumV i2 -> Int64.add i1 i2 |> numV - | SubOp, NumV i1, NumV i2 -> Int64.sub i1 i2 |> numV - | MulOp, NumV i1, NumV i2 -> Int64.mul i1 i2 |> numV - | DivOp, NumV i1, NumV i2 -> Int64.div i1 i2 |> numV - | ExpOp, NumV i1, NumV i2 -> int64_exp i1 i2 |> numV + | AddOp, NumV i1, NumV i2 -> Z.add i1 i2 |> numV + | SubOp, NumV i1, NumV i2 -> Z.sub i1 i2 |> numV + | MulOp, NumV i1, NumV i2 -> Z.mul i1 i2 |> numV + | DivOp, NumV i1, NumV i2 -> Z.div i1 i2 |> numV + | ExpOp, NumV i1, NumV i2 -> Z.pow i1 (Z.to_int i2) |> numV | AndOp, BoolV b1, BoolV b2 -> boolV (b1 && b2) | OrOp, BoolV b1, BoolV b2 -> boolV (b1 || b2) | ImplOp, BoolV b1, BoolV b2 -> boolV (not b1 || b2) @@ -200,7 +187,7 @@ and eval_expr expr = let a2 = eval_expr e2 |> unwrap_listv_to_array in Array.append a1 a2 |> listV | LenE e -> - eval_expr e |> unwrap_listv_to_array |> Array.length |> I64.of_int_u |> numV + eval_expr e |> unwrap_listv_to_array |> Array.length |> Z.of_int |> numV | StrE r -> r |> Record.map string_of_kwd eval_expr |> strV | AccE (e, p) -> @@ -235,7 +222,7 @@ and eval_expr expr = (match eval_expr e with | LabelV (v, _) -> v | FrameV (Some v, _) -> v - | FrameV _ -> numV 0L + | FrameV _ -> numV Z.zero | _ -> fail_on_expr "Not a context" expr (* Due to AL validation, unreachable *)) | FrameE (e1, e2) -> let v1 = Option.map eval_expr e1 in @@ -301,9 +288,9 @@ and eval_expr expr = | _ -> false in (match eval_expr e with (* valid_tabletype *) - | TupV [ lim; _ ] -> valid_lim 0xffffffffL lim |> boolV + | TupV [ lim; _ ] -> valid_lim (Z.of_int 0xffffffff) lim |> boolV (* valid_memtype *) - | CaseV ("I8", [ lim ]) -> valid_lim 0x10000L lim |> boolV + | CaseV ("I8", [ lim ]) -> valid_lim (Z.of_int 0x10000) lim |> boolV (* valid_other *) | _ -> fail_on_expr "TODO: Currently, we are already validating tabletype and memtype" expr) | HasTypeE (e, s) -> @@ -393,7 +380,7 @@ and assign lhs rhs env = match iter, rhs with | (List | List1), ListV arr -> env, listV [||], Array.to_list !arr | ListN (expr, None), ListV arr -> - let length = Array.length !arr |> Int64.of_int |> numV in + let length = Array.length !arr |> Z.of_int |> numV in assign expr length env, listV [||], Array.to_list !arr | Opt, OptV opt -> env, optV None, Option.to_list opt | ListN (_, Some _), ListV _ -> @@ -433,12 +420,12 @@ and assign lhs rhs env = | BinE (binop, e1, e2), NumV m -> let invop = match binop with - | AddOp -> Int64.sub - | SubOp -> Int64.add - | MulOp -> Int64.unsigned_div - | DivOp -> Int64.mul + | AddOp -> Z.sub + | SubOp -> Z.add + | MulOp -> Z.div + | DivOp -> Z.mul | _ -> failwith "Invalid binop for lhs of assignment" in - let v = eval_expr e2 |> al_to_int64 |> invop m |> numV in + let v = eval_expr e2 |> al_to_z |> invop m |> numV in assign e1 v env | CatE (e1, e2), ListV vs -> assign_split e1 e2 !vs env | StrE r1, StrV r2 when has_same_keys r1 r2 -> @@ -568,7 +555,7 @@ and is_builtin = function and call_builtin name = let local x = - match call_algo "local" [ numV (Int64.of_int x) ] with + match call_algo "local" [ numV (Z.of_int x) ] with | Some v -> v | _ -> failwith "Builtin doesn't return a value" in diff --git a/spectec/src/backend-interpreter/manual.ml b/spectec/src/backend-interpreter/manual.ml index 87f6bfb214..8b8b0a6d13 100644 --- a/spectec/src/backend-interpreter/manual.ml +++ b/spectec/src/backend-interpreter/manual.ml @@ -112,7 +112,7 @@ let group_bytes_by = let n' = varE "n'" in let bytes_ = iterE (varE "byte", ["byte"], List) in - let bytes_left = listE [accE (bytes_, sliceP (numE 0L, n))] in + let bytes_left = listE [accE (bytes_, sliceP (numE Z.zero, n))] in let bytes_right = callE ( "group_bytes_by", @@ -161,7 +161,7 @@ let array_new_data = let unpacknumtype = callE ("unpacknumtype", [zt]) in (* include z or not ??? *) let data = callE ("data", [y]) in - let group_bytes_by = callE ("group_bytes_by", [binE (DivOp, storagesize, numE 8L); bstar]) in + let group_bytes_by = callE ("group_bytes_by", [binE (DivOp, storagesize, numE (Z.of_int 8)); bstar]) in let inverse_of_bytes_ = iterE (callE ("inverse_of_ibytes", [storagesize; gb]), ["gb"], List) in RuleA ( @@ -180,7 +180,7 @@ let array_new_data = ifI ( binE ( GtOp, - binE (AddOp, i, binE (DivOp, binE (MulOp, n, storagesize), numE 8L)), + binE (AddOp, i, binE (DivOp, binE (MulOp, n, storagesize), numE (Z.of_int 8))), lenE (accE (callE ("data", [y]), dotP ("DATA", "datainst"))) ), [ trapI () ], @@ -191,7 +191,7 @@ let array_new_data = bstar, accE ( accE (data, dotP ("DATA", "datainst")), - sliceP (i, binE (DivOp, binE (MulOp, n, storagesize), numE 8L)) + sliceP (i, binE (DivOp, binE (MulOp, n, storagesize), numE (Z.of_int 8))) ) ); letI (gbstar, group_bytes_by); @@ -210,7 +210,7 @@ let return_instrs_of_instantiate config = let store, frame, rhs = config in [ enterI ( - frameE (Some (numE 0L), frame), + frameE (Some (numE Z.zero), frame), listE ([ caseE (("FRAME_", "admininstr"), []) ]), rhs ); returnI (Some (tupE [ store; varE "mm" ])) diff --git a/spectec/src/backend-interpreter/numerics.ml b/spectec/src/backend-interpreter/numerics.ml index 19781e313f..636d49828e 100644 --- a/spectec/src/backend-interpreter/numerics.ml +++ b/spectec/src/backend-interpreter/numerics.ml @@ -6,6 +6,12 @@ open Al_util type numerics = { name : string; f : value list -> value } +let mask32 = Z.of_int32_unsigned (-1l) +let mask64 = Z.of_int64_unsigned (-1L) + +let z_to_int32 z = Z.(to_int32_unsigned (logand mask32 z)) +let z_to_int64 z = Z.(to_int64_unsigned (logand mask64 z)) + let i8_to_i32 i8 = (* NOTE: This operation extends the sign of i8 to i32 *) I32.shr_s (I32.shl i8 24l) 24l @@ -296,14 +302,14 @@ let ext : numerics = name = "ext"; f = (function - | [ NumV 128L; _; CaseV ("U", []); NumV v ] -> VecV (V128.I64x2.of_lanes [ v; 0L ] |> V128.to_bits) (* HARDCODE *) + | [ NumV z; _; CaseV ("U", []); NumV v ] when z = Z.of_int 128 -> VecV (V128.I64x2.of_lanes [ z_to_int64 v; 0L ] |> V128.to_bits) (* HARDCODE *) | [ _; _; CaseV ("U", []); v ] -> v | [ NumV n1; NumV n2; CaseV ("S", []); NumV n3 ] -> - let i1 = Int64.to_int n1 in - let i2 = Int64.to_int n2 in - if Int64.shift_right n3 (i1 - 1) = 0L then NumV n3 else - let mask = Int64.sub (if i2 = 64 then 0L else Int64.shift_left 1L i2) (Int64.shift_left 1L i1) in - NumV (Int64.logor n3 mask) + let i1 = Z.to_int n1 in + let i2 = Z.to_int n2 in + if Z.shift_right n3 (i1 - 1) = Z.zero then NumV n3 else + let mask = Z.sub (if i2 = 64 then Z.zero else Z.shift_left Z.zero i2) (Z.shift_left Z.one i1) in + NumV (Z.logor n3 mask) | _ -> failwith "Invalid argument fot ext" ); } @@ -316,12 +322,12 @@ let ibytes : numerics = (function | [ NumV n; NumV i ] -> let rec decompose n bits = - if n = 0L then + if n = Z.zero then [] else - (Int64.logand bits 255L) :: decompose (Int64.sub n 8L) (Int64.shift_right bits 8) + Z.(bits land of_int 0xff) :: decompose Z.(n - of_int 8) Z.(shift_right bits 8) in - assert (n >= 0L && Int64.rem n 8L = 0L); + assert Z.(n >= Z.zero && rem n (of_int 8) = zero); decompose n i |> List.map numV |> listV_of_list | _ -> failwith "Invalid bytes" ); @@ -332,12 +338,12 @@ let inverse_of_ibytes : numerics = f = (function | [ NumV n; ListV bs ] -> - assert (n = Int64.of_int (Array.length !bs * 8)); + assert (n = Z.of_int (Array.length !bs * 8)); NumV (Array.fold_right (fun b acc -> match b with - | NumV b when 0L <= b && b < 256L -> Int64.add b (Int64.shift_left acc 8) + | NumV b when Z.zero <= b && b < Z.of_int 256 -> Z.add b (Z.shift_left acc 8) | _ -> failwith ("Invalid inverse_of_ibytes: " ^ Print.string_of_value b ^ " is not a valid byte.") - ) !bs 0L) + ) !bs Z.zero) | _ -> failwith "Invalid argument for inverse_of_ibytes." ); } @@ -347,10 +353,10 @@ let ntbytes : numerics = name = "ntbytes"; f = (function - | [ CaseV ("I32", []); n ] -> ibytes.f [ NumV 32L; n ] - | [ CaseV ("I64", []); n ] -> ibytes.f [ NumV 64L; n ] - | [ CaseV ("F32", []); f ] -> ibytes.f [ NumV 32L; f ] (* TODO *) - | [ CaseV ("F64", []); f ] -> ibytes.f [ NumV 64L; f ] (* TODO *) + | [ CaseV ("I32", []); n ] -> ibytes.f [ NumV (Z.of_int 32); n ] + | [ CaseV ("I64", []); n ] -> ibytes.f [ NumV (Z.of_int 64); n ] + | [ CaseV ("F32", []); f ] -> ibytes.f [ NumV (Z.of_int 32); f ] (* TODO *) + | [ CaseV ("F64", []); f ] -> ibytes.f [ NumV (Z.of_int 64); f ] (* TODO *) | _ -> failwith "Invalid ntbytes" ); } @@ -359,10 +365,10 @@ let inverse_of_ntbytes : numerics = name = "inverse_of_ntbytes"; f = (function - | [ CaseV ("I32", []); l ] -> inverse_of_ibytes.f [ NumV 32L; l ] - | [ CaseV ("I64", []); l ] -> inverse_of_ibytes.f [ NumV 64L; l ] - | [ CaseV ("F32", []); l ] -> inverse_of_ibytes.f [ NumV 32L; l ] (* TODO *) - | [ CaseV ("F64", []); l ] -> inverse_of_ibytes.f [ NumV 64L; l ] (* TODO *) + | [ CaseV ("I32", []); l ] -> inverse_of_ibytes.f [ NumV (Z.of_int 32); l ] + | [ CaseV ("I64", []); l ] -> inverse_of_ibytes.f [ NumV (Z.of_int 64); l ] + | [ CaseV ("F32", []); l ] -> inverse_of_ibytes.f [ NumV (Z.of_int 32); l ] (* TODO *) + | [ CaseV ("F64", []); l ] -> inverse_of_ibytes.f [ NumV (Z.of_int 64); l ] (* TODO *) | _ -> failwith "Invalid inverse_of_ntbytes" ); } @@ -373,8 +379,8 @@ let vtbytes : numerics = f = (function | [ CaseV ("V128", []); VecV v ] -> - let v1 = (ibytes.f [ NumV 64L; NumV (Bytes.get_int64_le (Bytes.of_string v) 0) ]) in - let v2 = (ibytes.f [ NumV 64L; NumV (Bytes.get_int64_le (Bytes.of_string v) 8) ]) in + let v1 = (ibytes.f [ NumV (Z.of_int 64); NumV (Z.of_int64 (Bytes.get_int64_le (Bytes.of_string v) 0)) ]) in + let v2 = (ibytes.f [ NumV (Z.of_int 64); NumV (Z.of_int64 (Bytes.get_int64_le (Bytes.of_string v) 8)) ]) in (match v1, v2 with | ListV l1, ListV l2 -> Array.concat [ !l1; !l2] |> listV | _ -> failwith "Invalid vtbytes") @@ -387,11 +393,11 @@ let inverse_of_vtbytes : numerics = f = (function | [ CaseV ("V128", []); ListV l ] -> - let v1 = inverse_of_ibytes.f [ NumV 64L; Array.sub !l 0 8 |> listV ] in - let v2 = inverse_of_ibytes.f [ NumV 64L; Array.sub !l 8 8 |> listV ] in + let v1 = inverse_of_ibytes.f [ NumV (Z.of_int 64); Array.sub !l 0 8 |> listV ] in + let v2 = inverse_of_ibytes.f [ NumV (Z.of_int 64); Array.sub !l 8 8 |> listV ] in (match v1, v2 with - | NumV n1, NumV n2 -> al_of_vector (V128.I64x2.of_lanes [ n1; n2 ]) + | NumV n1, NumV n2 -> al_of_vector (V128.I64x2.of_lanes [ z_to_int64 n1; z_to_int64 n2 ]) | _ -> failwith "Invalid inverse_of_vtbytes") | _ -> failwith "Invalid inverse_of_vtbytes" @@ -403,8 +409,8 @@ let inverse_of_ztbytes : numerics = name = "inverse_of_ztbytes"; f = (function - | [ CaseV ("I8", []); l ] -> inverse_of_ibytes.f [ NumV 8L; l ] - | [ CaseV ("I16", []); l ] -> inverse_of_ibytes.f [ NumV 16L; l ] + | [ CaseV ("I8", []); l ] -> inverse_of_ibytes.f [ NumV (Z.of_int 8); l ] + | [ CaseV ("I16", []); l ] -> inverse_of_ibytes.f [ NumV (Z.of_int 16); l ] | args -> inverse_of_ntbytes.f args ); } @@ -418,8 +424,8 @@ let wrap : numerics = f = (function | [ NumV _m; NumV n; NumV i ] -> - let mask = Int64.sub (Int64.shift_left 1L (Int64.to_int n)) 1L in - NumV (Int64.logand i mask) + let mask = Z.pred (Z.shift_left Z.one (Z.to_int n)) in + NumV (Z.logand i mask) | _ -> failwith "Invalid wrap_" ); } @@ -429,7 +435,7 @@ let inverse_of_signed : numerics = name = "inverse_of_signed"; f = (function - | [ n; i ] -> wrap.f [ NumV 64L; n; i ] + | [ n; i ] -> wrap.f [ NumV (Z.of_int 64); n; i ] | _ -> failwith "Invalid inverse_of_signed" ); } @@ -440,7 +446,7 @@ let ine: numerics = name = "ine"; f = (function - | [ _; VecV v1; VecV v2 ] -> (if v1 = v2 then 0L else 1L) |> numV + | [ _; VecV v1; VecV v2 ] -> (if v1 = v2 then Z.zero else Z.one) |> numV | _ -> failwith "Invaild ine" ); } @@ -453,7 +459,7 @@ let inverse_of_ibits : numerics = (function | [ NumV _; ListV l ] -> let na = Array.map (function | NumV e -> e | _ -> failwith "Invaild inverse_of_ibits") !l in - NumV (Array.fold_right (fun e acc -> Int64.logor e (Int64.shift_left acc 1)) na 0L) + NumV (Array.fold_right (fun e acc -> Z.logor e (Z.shift_left acc 1)) na Z.zero) | _ -> failwith "Invaild inverse_of_ibits" ); } @@ -465,11 +471,11 @@ let ilt: numerics = f = (function | [ CaseV ("S", []); NumV t; NumV n1; NumV n2 ] -> - (match t with - | 8L -> I8.lt_s (n1 |> Int64.to_int32 |> i8_to_i32) (n2 |> Int64.to_int32 |> i8_to_i32) |> al_of_bool - | 16L -> I16.lt_s (n1 |> Int64.to_int32 |> i16_to_i32) (n2 |> Int64.to_int32 |> i16_to_i32) |> al_of_bool - | 32L -> I32.lt_s (n1 |> Int64.to_int32) (n2 |> Int64.to_int32) |> al_of_bool - | 64L -> I64.lt_s n1 n2 |> al_of_bool + (match z_to_int64 t with + | 8L -> I8.lt_s (n1 |> z_to_int32 |> i8_to_i32) (n2 |> z_to_int32 |> i8_to_i32) |> al_of_bool + | 16L -> I16.lt_s (n1 |> z_to_int32 |> i16_to_i32) (n2 |> z_to_int32 |> i16_to_i32) |> al_of_bool + | 32L -> I32.lt_s (n1 |> z_to_int32) (n2 |> z_to_int32) |> al_of_bool + | 64L -> I64.lt_s (n1 |> z_to_int64) (n2 |> z_to_int64) |> al_of_bool | _ -> failwith "Invaild ilt" ) | _ -> failwith "Invaild ilt" @@ -508,23 +514,23 @@ let vunop: numerics = (function | [ CaseV ("_VI", [ op ]); TupV [ CaseV (ls, []); NumV (ln) ]; v ] -> ( match ls, ln with - | "I8", 16L -> ( + | "I8", z when z = Z.of_int 16 -> ( match op with | CaseV ("ABS", []) -> wrap_vunop V128.I8x16.abs v | CaseV ("NEG", []) -> wrap_vunop V128.I8x16.neg v | CaseV ("POPCNT", []) -> wrap_vunop V128.I8x16.popcnt v | _ -> failwith ("Invalid viunop: " ^ (Print.string_of_value op))) - | "I16", 8L -> ( + | "I16", z when z = Z.of_int 8 -> ( match op with | CaseV ("ABS", []) -> wrap_vunop V128.I16x8.abs v | CaseV ("NEG", []) -> wrap_vunop V128.I16x8.neg v | _ -> failwith ("Invalid viunop: " ^ (Print.string_of_value op))) - | "I32", 4L -> ( + | "I32", z when z = Z.of_int 4 -> ( match op with | CaseV ("ABS", []) -> wrap_vunop V128.I32x4.abs v | CaseV ("NEG", []) -> wrap_vunop V128.I32x4.neg v | _ -> failwith ("Invalid viunop: " ^ (Print.string_of_value op))) - | "I64", 2L -> ( + | "I64", z when z = Z.of_int 2 -> ( match op with | CaseV ("ABS", []) -> wrap_vunop V128.I64x2.abs v | CaseV ("NEG", []) -> wrap_vunop V128.I64x2.neg v @@ -532,7 +538,7 @@ let vunop: numerics = | _ -> failwith "Invalid type for viunop") | [ CaseV ("_VF", [ op ]); TupV [ CaseV (ls, []); NumV (ln) ]; v ] -> ( match ls, ln with - | "F32", 4L -> ( + | "F32", z when z = Z.of_int 4 -> ( match op with | CaseV ("ABS", []) -> wrap_vunop V128.F32x4.abs v | CaseV ("NEG", []) -> wrap_vunop V128.F32x4.neg v @@ -542,7 +548,7 @@ let vunop: numerics = | CaseV ("TRUNC", []) -> wrap_vunop V128.F32x4.trunc v | CaseV ("NEAREST", []) -> wrap_vunop V128.F32x4.nearest v | _ -> failwith ("Invalid vfunop: " ^ (Print.string_of_value op))) - | "F64", 2L -> ( + | "F64", z when z = Z.of_int 2 -> ( match op with | CaseV ("ABS", []) -> wrap_vunop V128.F64x2.abs v | CaseV ("NEG", []) -> wrap_vunop V128.F64x2.neg v @@ -586,7 +592,7 @@ let vbinop: numerics = (function | [ CaseV ("_VI", [ op ]); TupV [ CaseV (ls, []); NumV (ln) ]; v1; v2 ] -> ( match ls, ln with - | "I8", 16L -> ( + | "I8", z when z = Z.of_int 16 -> ( match op with | CaseV ("ADD", []) -> wrap_vbinop V128.I8x16.add v1 v2 | CaseV ("SUB", []) -> wrap_vbinop V128.I8x16.sub v1 v2 @@ -600,7 +606,7 @@ let vbinop: numerics = | CaseV ("MAX", [CaseV ("U", [])]) -> wrap_vbinop V128.I8x16.max_u v1 v2 | CaseV ("AVGR_U", []) -> wrap_vbinop V128.I8x16.avgr_u v1 v2 | _ -> failwith ("Invalid vibinop: " ^ (Print.string_of_value op))) - | "I16", 8L -> ( + | "I16", z when z = Z.of_int 8 -> ( match op with | CaseV ("ADD", []) -> wrap_vbinop V128.I16x8.add v1 v2 | CaseV ("SUB", []) -> wrap_vbinop V128.I16x8.sub v1 v2 @@ -616,7 +622,7 @@ let vbinop: numerics = | CaseV ("AVGR_U", []) -> wrap_vbinop V128.I16x8.avgr_u v1 v2 | CaseV ("Q15MULR_SAT_S", []) -> wrap_vbinop V128.I16x8.q15mulr_sat_s v1 v2 | _ -> failwith ("Invalid vibinop: " ^ (Print.string_of_value op))) - | "I32", 4L -> ( + | "I32", z when z = Z.of_int 4 -> ( match op with | CaseV ("ADD", []) -> wrap_vbinop V128.I32x4.add v1 v2 | CaseV ("SUB", []) -> wrap_vbinop V128.I32x4.sub v1 v2 @@ -630,7 +636,7 @@ let vbinop: numerics = | CaseV ("MAX", [CaseV ("U", [])]) -> wrap_vbinop V128.I32x4.max_u v1 v2 | CaseV ("MUL", []) -> wrap_vbinop V128.I32x4.mul v1 v2 | _ -> failwith ("Invalid vibinop: " ^ (Print.string_of_value op))) - | "I64", 2L -> ( + | "I64", z when z = Z.of_int 2 -> ( match op with | CaseV ("ADD", []) -> wrap_vbinop V128.I64x2.add v1 v2 | CaseV ("SUB", []) -> wrap_vbinop V128.I64x2.sub v1 v2 @@ -647,7 +653,7 @@ let vbinop: numerics = | _ -> failwith "Invalid type for vibinop") | [ CaseV ("_VF", [ op ]); TupV [ CaseV (ls, []); NumV (ln) ]; v1; v2 ] -> ( match ls, ln with - | "F32", 4L -> ( + | "F32", z when z = Z.of_int 4 -> ( match op with | CaseV ("ADD", []) -> wrap_vbinop V128.F32x4.add v1 v2 | CaseV ("SUB", []) -> wrap_vbinop V128.F32x4.sub v1 v2 @@ -658,7 +664,7 @@ let vbinop: numerics = | CaseV ("PMIN", []) -> wrap_vbinop V128.F32x4.pmin v1 v2 | CaseV ("PMAX", []) -> wrap_vbinop V128.F32x4.pmax v1 v2 | _ -> failwith ("Invalid vfbinop: " ^ (Print.string_of_value op))) - | "F64", 2L -> ( + | "F64", z when z = Z.of_int 2 -> ( match op with | CaseV ("ADD", []) -> wrap_vbinop V128.F64x2.add v1 v2 | CaseV ("SUB", []) -> wrap_vbinop V128.F64x2.sub v1 v2 @@ -683,62 +689,62 @@ let vrelop: numerics = (function | [ CaseV ("_VI", [ op ]); TupV [ CaseV (ls, []); NumV (ln) ]; NumV v1; NumV v2 ] -> ( match ls, ln with - | "I8", 16L -> ( - match op with - | CaseV ("EQ", []) -> wrap_vrelop I8.eq (v1 |> Int64.to_int32 |> i8_to_i32) (v2 |> Int64.to_int32 |> i8_to_i32) - | CaseV ("NE", []) -> wrap_vrelop I8.ne (v1 |> Int64.to_int32 |> i8_to_i32) (v2 |> Int64.to_int32 |> i8_to_i32) - | CaseV ("LTS", []) -> wrap_vrelop I8.lt_s (v1 |> Int64.to_int32 |> i8_to_i32) (v2 |> Int64.to_int32 |> i8_to_i32) - | CaseV ("LTU", []) -> wrap_vrelop I8.lt_u (v1 |> Int64.to_int32 |> i8_to_i32) (v2 |> Int64.to_int32 |> i8_to_i32) - | CaseV ("GTS", []) -> wrap_vrelop I8.gt_s (v1 |> Int64.to_int32 |> i8_to_i32) (v2 |> Int64.to_int32 |> i8_to_i32) - | CaseV ("GTU", []) -> wrap_vrelop I8.gt_u (v1 |> Int64.to_int32 |> i8_to_i32) (v2 |> Int64.to_int32 |> i8_to_i32) - | CaseV ("LES", []) -> wrap_vrelop I8.le_s (v1 |> Int64.to_int32 |> i8_to_i32) (v2 |> Int64.to_int32 |> i8_to_i32) - | CaseV ("LEU", []) -> wrap_vrelop I8.le_u (v1 |> Int64.to_int32 |> i8_to_i32) (v2 |> Int64.to_int32 |> i8_to_i32) - | CaseV ("GES", []) -> wrap_vrelop I8.ge_s (v1 |> Int64.to_int32 |> i8_to_i32) (v2 |> Int64.to_int32 |> i8_to_i32) - | CaseV ("GEU", []) -> wrap_vrelop I8.ge_u (v1 |> Int64.to_int32 |> i8_to_i32) (v2 |> Int64.to_int32 |> i8_to_i32) + | "I8", z when z = Z.of_int 16 -> ( + match op with + | CaseV ("EQ", []) -> wrap_vrelop I8.eq (v1 |> z_to_int32 |> i8_to_i32) (v2 |> z_to_int32 |> i8_to_i32) + | CaseV ("NE", []) -> wrap_vrelop I8.ne (v1 |> z_to_int32 |> i8_to_i32) (v2 |> z_to_int32 |> i8_to_i32) + | CaseV ("LTS", []) -> wrap_vrelop I8.lt_s (v1 |> z_to_int32 |> i8_to_i32) (v2 |> z_to_int32 |> i8_to_i32) + | CaseV ("LTU", []) -> wrap_vrelop I8.lt_u (v1 |> z_to_int32 |> i8_to_i32) (v2 |> z_to_int32 |> i8_to_i32) + | CaseV ("GTS", []) -> wrap_vrelop I8.gt_s (v1 |> z_to_int32 |> i8_to_i32) (v2 |> z_to_int32 |> i8_to_i32) + | CaseV ("GTU", []) -> wrap_vrelop I8.gt_u (v1 |> z_to_int32 |> i8_to_i32) (v2 |> z_to_int32 |> i8_to_i32) + | CaseV ("LES", []) -> wrap_vrelop I8.le_s (v1 |> z_to_int32 |> i8_to_i32) (v2 |> z_to_int32 |> i8_to_i32) + | CaseV ("LEU", []) -> wrap_vrelop I8.le_u (v1 |> z_to_int32 |> i8_to_i32) (v2 |> z_to_int32 |> i8_to_i32) + | CaseV ("GES", []) -> wrap_vrelop I8.ge_s (v1 |> z_to_int32 |> i8_to_i32) (v2 |> z_to_int32 |> i8_to_i32) + | CaseV ("GEU", []) -> wrap_vrelop I8.ge_u (v1 |> z_to_int32 |> i8_to_i32) (v2 |> z_to_int32 |> i8_to_i32) | _ -> failwith ("Invalid virelop: " ^ (Print.string_of_value op))) - | "I16", 8L -> ( - match op with - | CaseV ("EQ", []) -> wrap_vrelop I16.eq (v1 |> Int64.to_int32 |> i16_to_i32) (v2 |> Int64.to_int32 |> i16_to_i32) - | CaseV ("NE", []) -> wrap_vrelop I16.ne (v1 |> Int64.to_int32 |> i16_to_i32) (v2 |> Int64.to_int32 |> i16_to_i32) - | CaseV ("LTS", []) -> wrap_vrelop I16.lt_s (v1 |> Int64.to_int32 |> i16_to_i32) (v2 |> Int64.to_int32 |> i16_to_i32) - | CaseV ("LTU", []) -> wrap_vrelop I16.lt_u (v1 |> Int64.to_int32 |> i16_to_i32) (v2 |> Int64.to_int32 |> i16_to_i32) - | CaseV ("GTS", []) -> wrap_vrelop I16.gt_s (v1 |> Int64.to_int32 |> i16_to_i32) (v2 |> Int64.to_int32 |> i16_to_i32) - | CaseV ("GTU", []) -> wrap_vrelop I16.gt_u (v1 |> Int64.to_int32 |> i16_to_i32) (v2 |> Int64.to_int32 |> i16_to_i32) - | CaseV ("LES", []) -> wrap_vrelop I16.le_s (v1 |> Int64.to_int32 |> i16_to_i32) (v2 |> Int64.to_int32 |> i16_to_i32) - | CaseV ("LEU", []) -> wrap_vrelop I16.le_u (v1 |> Int64.to_int32 |> i16_to_i32) (v2 |> Int64.to_int32 |> i16_to_i32) - | CaseV ("GES", []) -> wrap_vrelop I16.ge_s (v1 |> Int64.to_int32 |> i16_to_i32) (v2 |> Int64.to_int32 |> i16_to_i32) - | CaseV ("GEU", []) -> wrap_vrelop I16.ge_u (v1 |> Int64.to_int32 |> i16_to_i32) (v2 |> Int64.to_int32 |> i16_to_i32) + | "I16", z when z = Z.of_int 8 -> ( + match op with + | CaseV ("EQ", []) -> wrap_vrelop I16.eq (v1 |> z_to_int32 |> i16_to_i32) (v2 |> z_to_int32 |> i16_to_i32) + | CaseV ("NE", []) -> wrap_vrelop I16.ne (v1 |> z_to_int32 |> i16_to_i32) (v2 |> z_to_int32 |> i16_to_i32) + | CaseV ("LTS", []) -> wrap_vrelop I16.lt_s (v1 |> z_to_int32 |> i16_to_i32) (v2 |> z_to_int32 |> i16_to_i32) + | CaseV ("LTU", []) -> wrap_vrelop I16.lt_u (v1 |> z_to_int32 |> i16_to_i32) (v2 |> z_to_int32 |> i16_to_i32) + | CaseV ("GTS", []) -> wrap_vrelop I16.gt_s (v1 |> z_to_int32 |> i16_to_i32) (v2 |> z_to_int32 |> i16_to_i32) + | CaseV ("GTU", []) -> wrap_vrelop I16.gt_u (v1 |> z_to_int32 |> i16_to_i32) (v2 |> z_to_int32 |> i16_to_i32) + | CaseV ("LES", []) -> wrap_vrelop I16.le_s (v1 |> z_to_int32 |> i16_to_i32) (v2 |> z_to_int32 |> i16_to_i32) + | CaseV ("LEU", []) -> wrap_vrelop I16.le_u (v1 |> z_to_int32 |> i16_to_i32) (v2 |> z_to_int32 |> i16_to_i32) + | CaseV ("GES", []) -> wrap_vrelop I16.ge_s (v1 |> z_to_int32 |> i16_to_i32) (v2 |> z_to_int32 |> i16_to_i32) + | CaseV ("GEU", []) -> wrap_vrelop I16.ge_u (v1 |> z_to_int32 |> i16_to_i32) (v2 |> z_to_int32 |> i16_to_i32) | _ -> failwith ("Invalid virelop: " ^ (Print.string_of_value op))) - | "I32", 4L -> ( - match op with - | CaseV ("EQ", []) -> wrap_vrelop I32.eq (v1 |> Int64.to_int32) (v2 |> Int64.to_int32) - | CaseV ("NE", []) -> wrap_vrelop I32.ne (v1 |> Int64.to_int32) (v2 |> Int64.to_int32) - | CaseV ("LTS", []) -> wrap_vrelop I32.lt_s (v1 |> Int64.to_int32) (v2 |> Int64.to_int32) - | CaseV ("LTU", []) -> wrap_vrelop I32.lt_u (v1 |> Int64.to_int32) (v2 |> Int64.to_int32) - | CaseV ("GTS", []) -> wrap_vrelop I32.gt_s (v1 |> Int64.to_int32) (v2 |> Int64.to_int32) - | CaseV ("GTU", []) -> wrap_vrelop I32.gt_u (v1 |> Int64.to_int32) (v2 |> Int64.to_int32) - | CaseV ("LES", []) -> wrap_vrelop I32.le_s (v1 |> Int64.to_int32) (v2 |> Int64.to_int32) - | CaseV ("LEU", []) -> wrap_vrelop I32.le_u (v1 |> Int64.to_int32) (v2 |> Int64.to_int32) - | CaseV ("GES", []) -> wrap_vrelop I32.ge_s (v1 |> Int64.to_int32) (v2 |> Int64.to_int32) - | CaseV ("GEU", []) -> wrap_vrelop I32.ge_u (v1 |> Int64.to_int32) (v2 |> Int64.to_int32) + | "I32", z when z = Z.of_int 4 -> ( + match op with + | CaseV ("EQ", []) -> wrap_vrelop I32.eq (v1 |> z_to_int32) (v2 |> z_to_int32) + | CaseV ("NE", []) -> wrap_vrelop I32.ne (v1 |> z_to_int32) (v2 |> z_to_int32) + | CaseV ("LTS", []) -> wrap_vrelop I32.lt_s (v1 |> z_to_int32) (v2 |> z_to_int32) + | CaseV ("LTU", []) -> wrap_vrelop I32.lt_u (v1 |> z_to_int32) (v2 |> z_to_int32) + | CaseV ("GTS", []) -> wrap_vrelop I32.gt_s (v1 |> z_to_int32) (v2 |> z_to_int32) + | CaseV ("GTU", []) -> wrap_vrelop I32.gt_u (v1 |> z_to_int32) (v2 |> z_to_int32) + | CaseV ("LES", []) -> wrap_vrelop I32.le_s (v1 |> z_to_int32) (v2 |> z_to_int32) + | CaseV ("LEU", []) -> wrap_vrelop I32.le_u (v1 |> z_to_int32) (v2 |> z_to_int32) + | CaseV ("GES", []) -> wrap_vrelop I32.ge_s (v1 |> z_to_int32) (v2 |> z_to_int32) + | CaseV ("GEU", []) -> wrap_vrelop I32.ge_u (v1 |> z_to_int32) (v2 |> z_to_int32) | _ -> failwith ("Invalid virelop: " ^ (Print.string_of_value op))) - | "I64", 2L -> ( - match op with - | CaseV ("EQ", []) -> wrap_vrelop I64.eq v1 v2 - | CaseV ("NE", []) -> wrap_vrelop I64.ne v1 v2 - | CaseV ("LTS", []) -> wrap_vrelop I64.lt_s v1 v2 - | CaseV ("LTU", []) -> wrap_vrelop I64.lt_u v1 v2 - | CaseV ("GTS", []) -> wrap_vrelop I64.gt_s v1 v2 - | CaseV ("GTU", []) -> wrap_vrelop I64.gt_u v1 v2 - | CaseV ("LES", []) -> wrap_vrelop I64.le_s v1 v2 - | CaseV ("LEU", []) -> wrap_vrelop I64.le_u v1 v2 - | CaseV ("GES", []) -> wrap_vrelop I64.ge_s v1 v2 - | CaseV ("GEU", []) -> wrap_vrelop I64.ge_u v1 v2 + | "I64", z when z = Z.of_int 2 -> ( + match op with + | CaseV ("EQ", []) -> wrap_vrelop I64.eq (v1 |> z_to_int64) (v2 |> z_to_int64) + | CaseV ("NE", []) -> wrap_vrelop I64.ne (v1 |> z_to_int64) (v2 |> z_to_int64) + | CaseV ("LTS", []) -> wrap_vrelop I64.lt_s (v1 |> z_to_int64) (v2 |> z_to_int64) + | CaseV ("LTU", []) -> wrap_vrelop I64.lt_u (v1 |> z_to_int64) (v2 |> z_to_int64) + | CaseV ("GTS", []) -> wrap_vrelop I64.gt_s (v1 |> z_to_int64) (v2 |> z_to_int64) + | CaseV ("GTU", []) -> wrap_vrelop I64.gt_u (v1 |> z_to_int64) (v2 |> z_to_int64) + | CaseV ("LES", []) -> wrap_vrelop I64.le_s (v1 |> z_to_int64) (v2 |> z_to_int64) + | CaseV ("LEU", []) -> wrap_vrelop I64.le_u (v1 |> z_to_int64) (v2 |> z_to_int64) + | CaseV ("GES", []) -> wrap_vrelop I64.ge_s (v1 |> z_to_int64) (v2 |> z_to_int64) + | CaseV ("GEU", []) -> wrap_vrelop I64.ge_u (v1 |> z_to_int64) (v2 |> z_to_int64) | _ -> failwith ("Invalid virelop: " ^ (Print.string_of_value op))) | _ -> failwith "Invalid type for virelop") | [ CaseV ("_VF", [ op ]); TupV [ CaseV (ls, []); NumV (ln) ]; v1; v2 ] -> ( match ls, ln with - | "F32", 4L -> ( + | "F32", z when z = Z.of_int 4 -> ( match op with | CaseV ("EQ", []) -> wrap_vrelop F32.eq (al_to_float32 v1) (al_to_float32 v2) | CaseV ("NE", []) -> wrap_vrelop F32.ne (al_to_float32 v1) (al_to_float32 v2) @@ -747,7 +753,7 @@ let vrelop: numerics = | CaseV ("LE", []) -> wrap_vrelop F32.le (al_to_float32 v1) (al_to_float32 v2) | CaseV ("GE", []) -> wrap_vrelop F32.ge (al_to_float32 v1) (al_to_float32 v2) | _ -> failwith ("Invalid vfrelop: " ^ (Print.string_of_value op))) - | "F64", 2L -> ( + | "F64", z when z = Z.of_int 2 -> ( match op with | CaseV ("EQ", []) -> wrap_vrelop F64.eq (al_to_float64 v1) (al_to_float64 v2) | CaseV ("NE", []) -> wrap_vrelop F64.ne (al_to_float64 v1) (al_to_float64 v2) @@ -784,15 +790,15 @@ let narrow : numerics = f = (function | [ NumV _; NumV n; CaseV ("S", []); NumV i ] -> ( - match n with - | 8L -> NumV (i |> Int64.to_int32 |> i16_to_i32 |> I8.saturate_s |> i32_to_i8 |> Int64.of_int32) - | 16L -> NumV (i |> Int64.to_int32 |> I16.saturate_s |> i32_to_i16 |> Int64.of_int32) + match z_to_int64 n with + | 8L -> NumV (i |> z_to_int32 |> i16_to_i32 |> I8.saturate_s |> i32_to_i8 |> Z.of_int32) + | 16L -> NumV (i |> z_to_int32 |> I16.saturate_s |> i32_to_i16 |> Z.of_int32) | _ -> failwith "Invalid narrow" ) | [ NumV _; NumV n; CaseV ("U", []); NumV i ] -> ( - match n with - | 8L -> NumV (i |> Int64.to_int32 |> i16_to_i32 |> I8.saturate_u |> Int64.of_int32) - | 16L -> NumV (i |> Int64.to_int32 |> I16.saturate_u |> i32_to_i16 |> Int64.of_int32) + match z_to_int64 n with + | 8L -> NumV (i |> z_to_int32 |> i16_to_i32 |> I8.saturate_u |> Z.of_int32) + | 16L -> NumV (i |> z_to_int32 |> I16.saturate_u |> i32_to_i16 |> Z.of_int32) | _ -> failwith "Invalid narrow" ) | _ -> failwith "Invalid narrow"); @@ -803,17 +809,17 @@ let lanes : numerics = name = "lanes"; f = (function - | [ TupV [ CaseV ("I8", []); NumV 16L ]; VecV v ] -> + | [ TupV [ CaseV ("I8", []); NumV z ]; VecV v ] when z = Z.of_int 16 -> v |> V128.of_bits |> V128.I8x16.to_lanes |> List.map al_of_int8 |> listV_of_list - | [ TupV [ CaseV ("I16", []); NumV 8L ]; VecV v ] -> + | [ TupV [ CaseV ("I16", []); NumV z ]; VecV v ] when z = Z.of_int 8 -> v |> V128.of_bits |> V128.I16x8.to_lanes |> List.map al_of_int16 |> listV_of_list - | [ TupV [ CaseV ("I32", []); NumV 4L ]; VecV v ] -> + | [ TupV [ CaseV ("I32", []); NumV z ]; VecV v ] when z = Z.of_int 4 -> v |> V128.of_bits |> V128.I32x4.to_lanes |> List.map al_of_int32 |> listV_of_list - | [ TupV [ CaseV ("I64", []); NumV 2L ]; VecV v ] -> + | [ TupV [ CaseV ("I64", []); NumV z ]; VecV v ] when z = Z.of_int 2 -> v |> V128.of_bits |> V128.I64x2.to_lanes |> List.map al_of_int64 |> listV_of_list - | [ TupV [ CaseV ("F32", []); NumV 4L ]; VecV v ] -> + | [ TupV [ CaseV ("F32", []); NumV z ]; VecV v ] when z = Z.of_int 4 -> v |> V128.of_bits |> V128.F32x4.to_lanes |> List.map al_of_float32 |> listV_of_list - | [ TupV [ CaseV ("F64", []); NumV 2L ]; VecV v ] -> + | [ TupV [ CaseV ("F64", []); NumV z ]; VecV v ] when z = Z.of_int 2 -> v |> V128.of_bits |> V128.F64x2.to_lanes |> List.map al_of_float64 |> listV_of_list | _ -> failwith "Invaild lanes" ); @@ -823,12 +829,12 @@ let inverse_of_lanes : numerics = name = "inverse_of_lanes"; f = (function - | [ TupV [ CaseV ("I8", []); NumV 16L ]; ListV lanes; ] -> VecV (List.map al_to_int32 (!lanes |> Array.to_list) |> List.map i8_to_i32 |> V128.I8x16.of_lanes |> V128.to_bits) - | [ TupV [ CaseV ("I16", []); NumV 8L ]; ListV lanes; ] -> VecV (List.map al_to_int32 (!lanes |> Array.to_list) |> List.map i16_to_i32 |> V128.I16x8.of_lanes |> V128.to_bits) - | [ TupV [ CaseV ("I32", []); NumV 4L ]; ListV lanes; ] -> VecV (List.map al_to_int32 (!lanes |> Array.to_list) |> V128.I32x4.of_lanes |> V128.to_bits) - | [ TupV [ CaseV ("I64", []); NumV 2L ]; ListV lanes; ] -> VecV (List.map al_to_int64 (!lanes |> Array.to_list) |> V128.I64x2.of_lanes |> V128.to_bits) - | [ TupV [ CaseV ("F32", []); NumV 4L ]; ListV lanes; ] -> VecV (List.map al_to_float32 (!lanes |> Array.to_list) |> V128.F32x4.of_lanes |> V128.to_bits) - | [ TupV [ CaseV ("F64", []); NumV 2L ]; ListV lanes; ] -> VecV (List.map al_to_float64 (!lanes |> Array.to_list) |> V128.F64x2.of_lanes |> V128.to_bits) + | [ TupV [ CaseV ("I8", []); NumV z ]; ListV lanes; ] when z = Z.of_int 16 -> VecV (List.map al_to_int32 (!lanes |> Array.to_list) |> List.map i8_to_i32 |> V128.I8x16.of_lanes |> V128.to_bits) + | [ TupV [ CaseV ("I16", []); NumV z ]; ListV lanes; ] when z = Z.of_int 8 -> VecV (List.map al_to_int32 (!lanes |> Array.to_list) |> List.map i16_to_i32 |> V128.I16x8.of_lanes |> V128.to_bits) + | [ TupV [ CaseV ("I32", []); NumV z ]; ListV lanes; ] when z = Z.of_int 4 -> VecV (List.map al_to_int32 (!lanes |> Array.to_list) |> V128.I32x4.of_lanes |> V128.to_bits) + | [ TupV [ CaseV ("I64", []); NumV z ]; ListV lanes; ] when z = Z.of_int 2 -> VecV (List.map al_to_int64 (!lanes |> Array.to_list) |> V128.I64x2.of_lanes |> V128.to_bits) + | [ TupV [ CaseV ("F32", []); NumV z ]; ListV lanes; ] when z = Z.of_int 4 -> VecV (List.map al_to_float32 (!lanes |> Array.to_list) |> V128.F32x4.of_lanes |> V128.to_bits) + | [ TupV [ CaseV ("F64", []); NumV z ]; ListV lanes; ] when z = Z.of_int 2 -> VecV (List.map al_to_float64 (!lanes |> Array.to_list) |> V128.F64x2.of_lanes |> V128.to_bits) | _ -> failwith "Invaild inverse_of_lanes" ); } @@ -854,10 +860,10 @@ let iadd : numerics = name = "iadd"; f = (function - | [ NumV 8L; NumV m; NumV n ] -> al_of_int32 (I8.add (Int64.to_int32 m) (Int64.to_int32 n)) - | [ NumV 16L; NumV m; NumV n ] -> al_of_int32 (I16.add (Int64.to_int32 m) (Int64.to_int32 n)) - | [ NumV 32L; NumV m; NumV n ] -> al_of_int32 (I32.add (Int64.to_int32 m) (Int64.to_int32 n)) - | [ NumV 64L; NumV m; NumV n ] -> al_of_int64 (I64.add m n) + | [ NumV z; NumV m; NumV n ] when z = Z.of_int 8 -> al_of_int32 (I8.add (z_to_int32 m) (z_to_int32 n)) + | [ NumV z; NumV m; NumV n ] when z = Z.of_int 16 -> al_of_int32 (I16.add (z_to_int32 m) (z_to_int32 n)) + | [ NumV z; NumV m; NumV n ] when z = Z.of_int 32 -> al_of_int32 (I32.add (z_to_int32 m) (z_to_int32 n)) + | [ NumV z; NumV m; NumV n ] when z = Z.of_int 64 -> al_of_int64 (I64.add (z_to_int64 m) (z_to_int64 n)) | v -> fail_list "Invalid iadd" v ); } @@ -867,10 +873,10 @@ let imul : numerics = name = "imul"; f = (function - | [ NumV 8L; NumV m; NumV n ] -> al_of_int32 (I8.mul (Int64.to_int32 m) (Int64.to_int32 n)) - | [ NumV 16L; NumV m; NumV n ] -> al_of_int32 (I16.mul (Int64.to_int32 m) (Int64.to_int32 n)) - | [ NumV 32L; NumV m; NumV n ] -> al_of_int32 (I32.mul (Int64.to_int32 m) (Int64.to_int32 n)) - | [ NumV 64L; NumV m; NumV n ] -> al_of_int64 (I64.mul m n) + | [ NumV z; NumV m; NumV n ] when z = Z.of_int 8 -> al_of_int32 (I8.mul (z_to_int32 m) (z_to_int32 n)) + | [ NumV z; NumV m; NumV n ] when z = Z.of_int 16 -> al_of_int32 (I16.mul (z_to_int32 m) (z_to_int32 n)) + | [ NumV z; NumV m; NumV n ] when z = Z.of_int 32 -> al_of_int32 (I32.mul (z_to_int32 m) (z_to_int32 n)) + | [ NumV z; NumV m; NumV n ] when z = Z.of_int 64 -> al_of_int64 (I64.mul (z_to_int64 m) (z_to_int64 n)) | v -> fail_list "Invalid imul" v ); } @@ -888,7 +894,7 @@ let vcvtop: numerics = | None -> "" | Some (CaseV (sx, [])) -> sx | _ -> failwith "invalid cvtop" in - match m, n, op, sx with + match z_to_int64 m, z_to_int64 n, op, sx with (* Conversion to I16 *) | 8L, 16L, "EXTEND", "S" -> wrap_i32_cvtop_i32 (fun e -> Int32.logand 0xffffffffl (e |> i8_to_i32)) v | 8L, 16L, "EXTEND", "U" -> wrap_i32_cvtop_i32 (Int32.logand 0xffl) v @@ -924,8 +930,8 @@ let vishiftop: numerics = | [ CaseV ("_VI", [ op ]); CaseV (ls, []); NumV v1; NumV v2] -> ( match ls with | "I8" -> ( - let v1p = v1 |> Int64.to_int32 |> i8_to_i32 in - let v2p = Int64.rem v2 8L |> Int64.to_int32 in + let v1p = v1 |> z_to_int32 |> i8_to_i32 in + let v2p = Z.rem v2 (Z.of_int 8) |> z_to_int32 in match op with | CaseV ("SHL", []) -> I8.shl v1p v2p |> al_of_int32 @@ -934,8 +940,8 @@ let vishiftop: numerics = | _ -> failwith ("Invalid vishiftop: " ^ (Print.string_of_value op)) ) | "I16" -> ( - let v1p = v1 |> Int64.to_int32 |> i16_to_i32 in - let v2p = Int64.rem v2 16L |> Int64.to_int32 in + let v1p = v1 |> z_to_int32 |> i16_to_i32 in + let v2p = Z.rem v2 (Z.of_int 16) |> z_to_int32 in match op with | CaseV ("SHL", []) -> I16.shl v1p v2p |> al_of_int32 @@ -944,8 +950,8 @@ let vishiftop: numerics = | _ -> failwith ("Invalid vishiftop: " ^ (Print.string_of_value op)) ) | "I32" -> ( - let v1p = v1 |> Int64.to_int32 in - let v2p = Int64.rem v2 32L |> Int64.to_int32 in + let v1p = v1 |> z_to_int32 in + let v2p = Z.rem v2 (Z.of_int 32) |> z_to_int32 in match op with | CaseV ("SHL", []) -> I32.shl v1p v2p |> al_of_int32 @@ -954,8 +960,8 @@ let vishiftop: numerics = | _ -> failwith ("Invalid vishiftop: " ^ (Print.string_of_value op)) ) | "I64" -> ( - let v1p = v1 in - let v2p = Int64.rem v2 64L in + let v1p = v1 |> z_to_int64 in + let v2p = Z.rem v2 (Z.of_int 64) |> z_to_int64 in match op with | CaseV ("SHL", []) -> I64.shl v1p v2p |> al_of_int64 diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml index 161d06243e..689dccd61d 100644 --- a/spectec/src/backend-latex/render.ml +++ b/spectec/src/backend-latex/render.ml @@ -562,19 +562,19 @@ and render_exp env e = | VarE (id, args) -> render_apply render_varid render_exp env env.show_syn id args | BoolE b -> render_atom env (Atom (string_of_bool b) $$ e.at % ref "bool") - | NatE (DecOp, n) -> string_of_int n + | NatE (DecOp, n) -> Z.to_string n | NatE (HexOp, n) -> - let fmt : (_, _, _) format = - if n < 0x100 then "%02X" else - if n < 0x10000 then "%04X" else + let fmt = + if n < Z.of_int 0x100 then "%02X" else + if n < Z.of_int 0x10000 then "%04X" else "%X" - in "\\mathtt{0x" ^ Printf.sprintf fmt n ^ "}" + in "\\mathtt{0x" ^ Z.format fmt n ^ "}" | NatE (CharOp, n) -> - let fmt : (_, _, _) format = - if n < 0x100 then "%02X" else - if n < 0x10000 then "%04X" else + let fmt = + if n < Z.of_int 0x100 then "%02X" else + if n < Z.of_int 0x10000 then "%04X" else "%X" - in "\\mathrm{U{+}" ^ Printf.sprintf fmt n ^ "}" + in "\\mathrm{U{+}" ^ Z.format fmt n ^ "}" | TextE t -> "``" ^ t ^ "''" | UnE (op, e2) -> "{" ^ render_unop op ^ render_exp env e2 ^ "}" | BinE (e1, ExpOp, ({it = ParenE (e2, _); _ } | e2)) -> @@ -712,19 +712,19 @@ and render_sym env g = match g.it with | VarG (id, args) -> render_apply render_gramid render_exp_as_sym env env.show_gram id args - | NatG (DecOp, n) -> string_of_int n + | NatG (DecOp, n) -> Z.to_string n | NatG (HexOp, n) -> - let fmt : (_, _, _) format = - if n < 0x100 then "%02X" else - if n < 0x10000 then "%04X" else + let fmt = + if n < Z.of_int 0x100 then "%02X" else + if n < Z.of_int 0x10000 then "%04X" else "%X" - in "\\mathtt{0x" ^ Printf.sprintf fmt n ^ "}" + in "\\mathtt{0x" ^ Z.format fmt n ^ "}" | NatG (CharOp, n) -> - let fmt : (_, _, _) format = - if n < 0x100 then "%02X" else - if n < 0x10000 then "%04X" else + let fmt = + if n < Z.of_int 0x100 then "%02X" else + if n < Z.of_int 0x10000 then "%04X" else "%X" - in "\\mathrm{U{+}" ^ Printf.sprintf fmt n ^ "}" + in "\\mathrm{U{+}" ^ Z.format fmt n ^ "}" | TextG t -> "`" ^ t ^ "'" | EpsG -> "\\epsilon" | SeqG gs -> render_syms "~" env gs diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml index 0e9d48a593..a34fcf7832 100644 --- a/spectec/src/backend-prose/render.ml +++ b/spectec/src/backend-prose/render.ml @@ -91,9 +91,8 @@ and al_to_el_path pl = and al_to_el_expr expr = let exp' = match expr.it with - | Al.Ast.NumE i -> - let ei = Int64.to_int i in - let eli = El.Ast.NatE (El.Ast.DecOp, ei) in + | Al.Ast.NumE i -> + let eli = El.Ast.NatE (El.Ast.DecOp, i) in Some eli | Al.Ast.UnE (op, e) -> let* elop = al_to_el_unop op in diff --git a/spectec/src/el/ast.ml b/spectec/src/el/ast.ml index b9c7d68e36..65307af238 100644 --- a/spectec/src/el/ast.ml +++ b/spectec/src/el/ast.ml @@ -12,7 +12,7 @@ type 'a nl_list = 'a nl_elem list (* Terminals *) -type nat = int +type nat = Z.t type text = string type id = string phrase @@ -172,7 +172,7 @@ and path' = and sym = sym' phrase and sym' = | VarG of id * arg list (* gramid (`(` arg,* `)`)? *) - | NatG of natop * int (* nat *) + | NatG of natop * nat (* nat *) | TextG of string (* `"`text`"` *) | EpsG (* `eps` *) | SeqG of sym nl_list (* sym sym *) diff --git a/spectec/src/el/dune b/spectec/src/el/dune index 59b4f77f10..d0037dfa24 100644 --- a/spectec/src/el/dune +++ b/spectec/src/el/dune @@ -1,5 +1,5 @@ (library (name el) - (libraries util) + (libraries util zarith) (modules ast eq free subst convert print iter) ) diff --git a/spectec/src/el/print.ml b/spectec/src/el/print.ml index 506b66af27..bbaa939e9f 100644 --- a/spectec/src/el/print.ml +++ b/spectec/src/el/print.ml @@ -147,9 +147,9 @@ and string_of_exp e = | VarE (id, args) -> id.it ^ string_of_args args | AtomE atom -> string_of_atom atom | BoolE b -> string_of_bool b - | NatE (DecOp, n) -> string_of_int n - | NatE (HexOp, n) -> Printf.sprintf "0x%X" n - | NatE (CharOp, n) -> Printf.sprintf "U+%X" n + | NatE (DecOp, n) -> Z.to_string n + | NatE (HexOp, n) -> "0x" ^ Z.format "%X" n + | NatE (CharOp, n) -> "U+" ^ Z.format "%X" n | TextE t -> "\"" ^ String.escaped t ^ "\"" | UnE (op, e2) -> string_of_unop op ^ " " ^ string_of_exp e2 | BinE (e1, op, e2) -> @@ -225,9 +225,9 @@ and string_of_prem prem = and string_of_sym g = match g.it with | VarG (id, args) -> id.it ^ string_of_args args - | NatG (DecOp, n) -> string_of_int n - | NatG (HexOp, n) -> Printf.sprintf "0x%X" n - | NatG (CharOp, n) -> Printf.sprintf "U+%X" n + | NatG (DecOp, n) -> Z.to_string n + | NatG (HexOp, n) -> "0x" ^ Z.format "%X" n + | NatG (CharOp, n) -> "U+" ^ Z.format "%X" n | TextG t -> "\"" ^ String.escaped t ^ "\"" | EpsG -> "eps" | SeqG gs -> "{" ^ concat " " (map_filter_nl_list string_of_sym gs) ^ "}" diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml index b55980c992..e59d7be5e3 100644 --- a/spectec/src/frontend/elab.ml +++ b/spectec/src/frontend/elab.ml @@ -721,7 +721,7 @@ and infer_exp' env e : Il.exp' * typ = Il.LenE e1', NumT NatT $ e.at | SizeE id -> let _ = find "grammar" env.syms id in - NatE 0, NumT NatT $ e.at + NatE Z.zero, NumT NatT $ e.at | ParenE (e1, _) -> infer_exp' env e1 | TupE es -> diff --git a/spectec/src/frontend/lexer.mll b/spectec/src/frontend/lexer.mll index bad1e73126..0578eff60b 100644 --- a/spectec/src/frontend/lexer.mll +++ b/spectec/src/frontend/lexer.mll @@ -19,17 +19,10 @@ let error_nest start lexbuf msg = lexbuf.Lexing.lex_start_p <- start; error lexbuf msg -let nat lexbuf s = - try - let n = int_of_string s in - if n >= 0 then n else raise (Failure "") - with Failure _ -> error lexbuf "nat literal out of range" - -let hex lexbuf s = - try - let n = int_of_string s in - if n >= 0 then n else raise (Failure "") - with Failure _ -> error lexbuf "hex literal out of range" +let nat _lexbuf s = Z.of_string s +let hex _lexbuf s = Z.of_string s +let int lexbuf s = + try int_of_string s with Failure _ -> error lexbuf "hex literal out of range" let text _lexbuf s = let b = Buffer.create (String.length s) in @@ -204,10 +197,10 @@ and token = parse | "_|_" { BOT } | "^|^" { TOP } | "%" { HOLE } - | "%"(nat as s) { HOLEN (nat lexbuf s) } + | "%"(nat as s) { HOLEN (int lexbuf s) } | "%%" { MULTIHOLE } | "!%" { SKIP } - | "!%"(nat as s) { SKIPN (nat lexbuf s) } + | "!%"(nat as s) { SKIPN (int lexbuf s) } | "!%%" { MULTISKIP } | "#" { FUSE } diff --git a/spectec/src/frontend/parser.mly b/spectec/src/frontend/parser.mly index f59a4290c2..5269747295 100644 --- a/spectec/src/frontend/parser.mly +++ b/spectec/src/frontend/parser.mly @@ -100,7 +100,7 @@ let is_post_exp e = %token IF OTHERWISE HINT_LPAREN %token EPS INFINITY %token BOOLLIT -%token NATLIT HEXLIT CHARLIT +%token NATLIT HEXLIT CHARLIT %token TEXTLIT %token UPID LOID DOTID UPID_LPAREN LOID_LPAREN %token EOF @@ -202,7 +202,7 @@ gramid_lparen : id_lparen { $1 $ at $sloc } ruleid : ruleid_ { $1 } ruleid_ : | id { $1 } - | NATLIT { Int.to_string $1 } + | NATLIT { Z.to_string $1 } | BOOLLIT { Bool.to_string $1 } | IF { "if" } | VAR { "var" } diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml index f7575d60b3..1cdb654d81 100644 --- a/spectec/src/il/ast.ml +++ b/spectec/src/il/ast.ml @@ -6,7 +6,7 @@ open Util.Source (* Terminals *) -type nat = int +type nat = Z.t type text = string type id = string phrase diff --git a/spectec/src/il/dune b/spectec/src/il/dune index 38b4366dee..52f9eceb6a 100644 --- a/spectec/src/il/dune +++ b/spectec/src/il/dune @@ -1,5 +1,5 @@ (library (name il) - (libraries util) + (libraries util zarith) (modules ast eq free print validation) ) diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml index f97940d15e..14b72ca12f 100644 --- a/spectec/src/il/print.ml +++ b/spectec/src/il/print.ml @@ -148,7 +148,7 @@ and string_of_exp e = match e.it with | VarE id -> id.it | BoolE b -> string_of_bool b - | NatE n -> string_of_int n + | NatE n -> Z.to_string n | TextE t -> "\"" ^ String.escaped t ^ "\"" | UnE (op, e2) -> string_of_unop op ^ " " ^ string_of_exp e2 | BinE (op, e1, e2) -> diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index 9ba83743a7..90114c9c04 100644 --- a/spectec/src/il2al/translate.ml +++ b/spectec/src/il2al/translate.ml @@ -114,7 +114,7 @@ let rec translate_iter = function and translate_expr exp = let at = exp.at in match exp.it with - | Il.NatE n -> numE (Int64.of_int n) ~at:at + | Il.NatE n -> numE n ~at:at | Il.BoolE b -> boolE b ~at:at (* List *) | Il.LenE inner_exp -> lenE (translate_expr inner_exp) ~at:at @@ -507,7 +507,7 @@ let rec translate_letpr lhs rhs targets cont = else [ ifI - ( binE (EqOp, lenE rhs, numE (Int64.of_int (List.length es))), + ( binE (EqOp, lenE rhs, numE (Z.of_int (List.length es))), letI (listE es' ~at:lhs_at, rhs) ~at:at :: translate_bindings bindings, [] ); ] @@ -546,7 +546,7 @@ let rec translate_letpr lhs rhs targets cont = match e.it with | ListE es -> let bindings', es' = extract_non_names es in - Some (numE (Int64.of_int (List.length es))), bindings', listE es' + Some (numE (Z.of_int (List.length es))), bindings', listE es' | IterE (({ it = VarE _; _ } | { it = SubE _; _ }), _, ListN (e', None)) -> Some e', [], e | _ -> diff --git a/spectec/src/il2al/transpile.ml b/spectec/src/il2al/transpile.ml index 313a71c399..0d19896c32 100644 --- a/spectec/src/il2al/transpile.ml +++ b/spectec/src/il2al/transpile.ml @@ -38,13 +38,13 @@ let both_empty cond1 cond2 = let get_list cond = match cond.it with | BinE (EqOp, e, { it = ListE []; _ }) - | BinE (EqOp, { it = ListE []; _ }, e) - | BinE (EqOp, { it = LenE e; _ }, { it = NumE 0L; _ }) - | BinE (EqOp, { it = NumE 0L; _ }, { it = LenE e; _ }) - | BinE (LtOp, { it = LenE e; _ }, { it = NumE 1L; _ }) - | BinE (LeOp, { it = LenE e; _ }, { it = NumE 0L; _ }) - | BinE (GeOp, { it = NumE 0L; _ }, { it = LenE e; _ }) - | BinE (GeOp, { it = NumE 1L; _ }, { it = LenE e; _ }) -> Some e + | BinE (EqOp, { it = ListE []; _ }, e) -> Some e + | BinE (EqOp, { it = LenE e; _ }, { it = NumE z; _ }) + | BinE (EqOp, { it = NumE z; _ }, { it = LenE e; _ }) + | BinE (LeOp, { it = LenE e; _ }, { it = NumE z; _ }) + | BinE (GeOp, { it = NumE z; _ }, { it = LenE e; _ }) when z = Z.zero -> Some e + | BinE (LtOp, { it = LenE e; _ }, { it = NumE z; _ }) + | BinE (GeOp, { it = NumE z; _ }, { it = LenE e; _ }) when z = Z.one -> Some e | _ -> None in match get_list cond1, get_list cond2 with @@ -55,13 +55,13 @@ let both_non_empty cond1 cond2 = let get_list cond = match cond.it with | BinE (NeOp, e, { it = ListE []; _ }) - | BinE (NeOp, { it = ListE []; _ }, e) - | BinE (NeOp, { it = LenE e; _ }, { it = NumE 0L; _ }) - | BinE (NeOp, { it = NumE 0L; _ }, { it = LenE e; _ }) - | BinE (LtOp, { it = NumE 0L; _ }, { it = LenE e; _ }) - | BinE (GtOp, { it = LenE e; _ }, { it = NumE 0L; _ }) - | BinE (LeOp, { it = NumE 1L; _ }, { it = LenE e; _ }) - | BinE (GeOp, { it = LenE e; _ }, { it = NumE 1L; _ }) -> Some e + | BinE (NeOp, { it = ListE []; _ }, e) -> Some e + | BinE (NeOp, { it = LenE e; _ }, { it = NumE z; _ }) + | BinE (NeOp, { it = NumE z; _ }, { it = LenE e; _ }) + | BinE (LtOp, { it = NumE z; _ }, { it = LenE e; _ }) + | BinE (GtOp, { it = LenE e; _ }, { it = NumE z; _ }) when z = Z.zero -> Some e + | BinE (LeOp, { it = NumE z; _ }, { it = LenE e; _ }) + | BinE (GeOp, { it = LenE e; _ }, { it = NumE z; _ }) when z = Z.one-> Some e | _ -> None in match get_list cond1, get_list cond2 with From 7abbfaebb77e4c5eafbd99157fa71b351af5430b Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 16 Feb 2024 07:20:56 +0100 Subject: [PATCH 2/2] Install zarith in CI --- .github/workflows/ci-spectec.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-spectec.yml b/.github/workflows/ci-spectec.yml index 5568044f82..e210ce2cd1 100644 --- a/.github/workflows/ci-spectec.yml +++ b/.github/workflows/ci-spectec.yml @@ -23,7 +23,7 @@ jobs: with: ocaml-compiler: 4.14.x - name: Setup Dune - run: opam install --yes dune menhir mdx + run: opam install --yes dune menhir mdx zarith - name: Setup Latex run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended - name: Setup Sphinx