Merge pull request #75 from Wasm-DSL/zarith

Unbounded nats

.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

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

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

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 *)

spectec/src/al/dune

@@ -1,5 +1,5 @@
 (library
   (name al)
-  (libraries util)
+  (libraries util zarith)
   (modules ast al_util print walk free eq)
 )

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 ("

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 =