Bigger integers

dune-project

@@ -52,7 +52,8 @@
   ocaml-lsp-server
   qcheck
   qcheck-alcotest
-  ppx_deriving_qcheck))
+  ppx_deriving_qcheck
+  bignum))
 
 ; After upgrading to opam 2.2 use with-dev https://opam.ocaml.org/blog/opam-2-2-0/
 

src/haz3lcore/dynamics/Builtins.re

@@ -53,8 +53,6 @@
     let nan = Float(Float.nan) |> fresh;
     let epsilon_float = Float(epsilon_float) |> fresh;
     let pi = Float(Float.pi) |> fresh;
-    let max_int = Int(Int.max_int) |> fresh;
-    let min_int = Int(Int.min_int) |> fresh;
 
     [@warning "-8"]
     // let-unbox guarantees that the tuple will have length 2
@@ -88,7 +86,7 @@
 
     let string_of_int = d => {
       let-unbox n = (Int, d);
-      Some(fresh(String(string_of_int(n))));
+      Some(fresh(String(Bigint.to_string(n))));
     };
 
     let string_of_float = d => {
@@ -103,17 +101,17 @@
 
     let int_of_float = d => {
       let-unbox f = (Float, d);
-      Some(fresh(Int(int_of_float(f))));
+      Some(fresh(Int(Bigint.of_float(f))));
     };
 
     let float_of_int = d => {
       let-unbox n = (Int, d);
-      Some(fresh(Float(float_of_int(n))));
+      Some(fresh(Float(Bigint.to_float(n))));
     };
 
     let abs = d => {
       let-unbox n = (Int, d);
-      Some(fresh(Int(abs(n))));
+      Some(fresh(Int(Bigint.abs(n))));
     };
 
     let float_op = (fn, d) => {
@@ -154,7 +152,7 @@
     };
 
     let int_of_string =
-      of_string(int_of_string_opt, n => Int(n) |> DHExp.fresh);
+      of_string(Bigint.of_string_opt, n => Int(n) |> DHExp.fresh);
     let float_of_string =
       of_string(float_of_string_opt, f => Float(f) |> DHExp.fresh);
     let bool_of_string =
@@ -164,7 +162,7 @@
       binary((d1, d2) => {
         let-unbox m = (Int, d1);
         let-unbox n = (Int, d2);
-        if (n == 0) {
+        if (n == Bigint.zero) {
           Some(
             fresh(
               DynamicErrorHole(
@@ -174,20 +172,20 @@
             ),
           );
         } else {
-          Some(fresh(Int(m mod n)));
+          Some(fresh(Int(Bigint.rem(m, n))));
         };
       });
 
     let string_length = d => {
       let-unbox s = (String, d);
-      Some(fresh(Int(String.length(s))));
+      Some(fresh(Int(String.length(s) |> Bigint.of_int)));
     };
 
     let string_compare =
       binary((d1, d2) => {
         let-unbox s1 = (String, d1);
         let-unbox s2 = (String, d2);
-        Some(fresh(Int(String.compare(s1, s2))));
+        Some(fresh(Int(String.compare(s1, s2) |> Bigint.of_int)));
       });
 
     let string_trim = d => {
@@ -212,8 +210,8 @@
     let string_sub = name =>
       ternary((d1, d2, d3) => {
         let-unbox s = (String, d1);
-        let-unbox idx = (Int, d2);
-        let-unbox len = (Int, d3);
+        let-unbox idx = (OCamlInt, d2);
+        let-unbox len = (OCamlInt, d3);
         try(Some(fresh(String(String.sub(s, idx, len))))) {
         | _ =>
           let d' = BuiltinFun(name) |> DHExp.fresh;
@@ -243,8 +241,6 @@
     |> const("nan", Float, nan)
     |> const("epsilon_float", Float, epsilon_float)
     |> const("pi", Float, pi)
-    |> const("max_int", Int, max_int)
-    |> const("min_int", Int, min_int)
     |> fn("is_finite", Float, Bool, is_finite)
     |> fn("is_infinite", Float, Bool, is_infinite)
     |> fn("is_nan", Float, Bool, is_nan)

src/haz3lcore/dynamics/EvaluatorError.re

@@ -19,6 +19,7 @@
   | InvalidBoxedTuple(DHExp.t)
   | InvalidBuiltin(string)
   | BadBuiltinAp(string, list(DHExp.t))
-  | InvalidProjection(int);
+  | InvalidProjection(int)
+  | IntegerTooBig(Bigint.t);
 
 exception Exception(t);

src/haz3lcore/dynamics/Transition.re

@@ -477,7 +477,7 @@
         );
       let-unbox n = (Int, d1');
       Step({
-        expr: Int(- n) |> fresh,
+        expr: Int(Bigint.neg(n)) |> fresh,
         state_update,
         kind: UnOp(Int(Minus)),
         is_value: true,
@@ -545,39 +545,41 @@
         );
       let-unbox n1 = (Int, d1');
       let-unbox n2 = (Int, d2');
-      Step({
-        expr:
-          (
-            switch (op) {
-            | Plus => Int(n1 + n2)
-            | Minus => Int(n1 - n2)
-            | Power when n2 < 0 =>
-              DynamicErrorHole(
-                BinOp(Int(op), d1', d2') |> rewrap,
-                NegativeExponent,
-              )
-            | Power => Int(IntUtil.ipow(n1, n2))
-            | Times => Int(n1 * n2)
-            | Divide when n2 == 0 =>
-              DynamicErrorHole(
-                BinOp(Int(op), d1', d2') |> rewrap,
-                DivideByZero,
-              )
-            | Divide => Int(n1 / n2)
-            | LessThan => Bool(n1 < n2)
-            | LessThanOrEqual => Bool(n1 <= n2)
-            | GreaterThan => Bool(n1 > n2)
-            | GreaterThanOrEqual => Bool(n1 >= n2)
-            | Equals => Bool(n1 == n2)
-            | NotEquals => Bool(n1 != n2)
-            }
-          )
-          |> fresh,
-        state_update,
-        kind: BinIntOp(op),
-        // False so that InvalidOperations are caught and made indet by the next step
-        is_value: false,
-      });
+      Bigint.(
+        Step({
+          expr:
+            (
+              switch (op) {
+              | Plus => Int(n1 + n2)
+              | Minus => Int(n1 - n2)
+              | Power when n2 < zero =>
+                DynamicErrorHole(
+                  BinOp(Int(op), d1', d2') |> rewrap,
+                  NegativeExponent,
+                )
+              | Power => Int(Bigint.pow(n1, n2))
+              | Times => Int(n1 * n2)
+              | Divide when n2 == zero =>
+                DynamicErrorHole(
+                  BinOp(Int(op), d1', d2') |> rewrap,
+                  DivideByZero,
+                )
+              | Divide => Int(n1 / n2)
+              | LessThan => Bool(n1 < n2)
+              | LessThanOrEqual => Bool(n1 <= n2)
+              | GreaterThan => Bool(n1 > n2)
+              | GreaterThanOrEqual => Bool(n1 >= n2)
+              | Equals => Bool(n1 == n2)
+              | NotEquals => Bool(n1 != n2)
+              }
+            )
+            |> fresh,
+          state_update,
+          kind: BinIntOp(op),
+          // False so that InvalidOperations are caught and made indet by the next step
+          is_value: false,
+        })
+      );
     | BinOp(Float(op), d1, d2) =>
       let. _ =
         otherwise(env, (d1, d2) => BinOp(Float(op), d1, d2) |> rewrap)

src/haz3lcore/dynamics/Unboxing.re

@@ -27,7 +27,8 @@
   | DeferredAp(DHExp.t, list(DHExp.t));
 
 type unbox_request('a) =
-  | Int: unbox_request(int)
+  | Int: unbox_request(Bigint.t)
+  | OCamlInt: unbox_request(int) // For builtins that require OCaml ints
   | Float: unbox_request(float)
   | Bool: unbox_request(bool)
   | String: unbox_request(string)
@@ -103,6 +104,13 @@
     | (String, String(s)) => Matches(s)
     | (Label, Label(s)) => Matches(s)
 
+    /* Can only unbox an OCaml int if it's small enough */
+    | (OCamlInt, Int(i)) =>
+      switch (Bigint.to_int(i)) {
+      | Some(i) => Matches(i)
+      | None => raise(EvaluatorError.Exception(IntegerTooBig(i)))
+      }
+
     /* Lists can be either lists or list casts */
     | (List, ListLit(l)) => Matches(l)
     | (ListLit(n), ListLit(l)) when ListUtil.is_length(n, l) => Matches(l)
@@ -246,6 +254,7 @@
       | TupLabel(_) =>
         raise(EvaluatorError.Exception(InvalidBoxedTupLabel(expr)))
       | Bool => raise(EvaluatorError.Exception(InvalidBoxedBoolLit(expr)))
+      | OCamlInt
       | Int => raise(EvaluatorError.Exception(InvalidBoxedIntLit(expr)))
       | Float => raise(EvaluatorError.Exception(InvalidBoxedFloatLit(expr)))
       | String =>

src/haz3lcore/lang/term/Grammar.re

@@ -35,7 +35,7 @@ and exp_term('a) =
   | Deferral(deferral_position_t)
   | Undefined
   | Bool(bool)
-  | Int(int)
+  | Int(Bigint.t)
   | Float(float)
   | String(string)
   | ListLit(list(exp_t('a)))
@@ -75,7 +75,7 @@ and pat_term('a) =
   | EmptyHole
   | MultiHole(list(any_t('a)))
   | Wild
-  | Int(int)
+  | Int(Bigint.t)
   | Float(float)
   | Bool(bool)
   | String(string)

src/haz3lcore/pretty/ExpToSegment.re

@@ -724,7 +724,8 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
     p_just([Grout({id, shape: Convex})]);
   | Undefined => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, "undefined")
   | Bool(b) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Bool.to_string(b))
-  | Int(n) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Int.to_string(n))
+  | Int(n) =>
+    text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Bigint.to_string(n))
   // TODO: do floats print right?
   | Float(f) =>
     text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Printf.sprintf("%f", f))
@@ -1069,7 +1070,8 @@ and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
     p_just([Grout({id, shape: Convex})]);
   | Wild => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, "_")
   | Var(v) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, v)
-  | Int(n) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, Int.to_string(n))
+  | Int(n) =>
+    text_to_pretty(pat |> Pat.rep_id, Sort.Pat, Bigint.to_string(n))
   | Float(f) =>
     text_to_pretty(pat |> Pat.rep_id, Sort.Pat, Printf.sprintf("%f", f))
   | Bool(b) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, Bool.to_string(b))

src/haz3lcore/statics/Coverage.re

@@ -13,7 +13,7 @@
   type t =
     | Truth
     | Hole
-    | Int(int)
+    | Int(Bigint.t)
     | Float(float)
     | String(string)
     | Ap(Constructor.t, option(t))
@@ -54,7 +54,7 @@
 
   // Ctrs for primitive types
   // Names here should not be anotherwise valid sum type constructor names.
-  let of_int = n => mk(string_of_int(n), 0);
+  let of_int = n => mk(Bigint.to_string(n), 0);
   let of_float = x => mk(string_of_float(x), 0);
   let of_string = s => mk("\"" ++ s, 0); // don't need closing quote, just need to distinguish from others
   let tuple_ctr: int => t = n => mk("tuple", n);
@@ -114,8 +114,8 @@
       )
     | Bool => Finite(Map.of_list([(true_ctr, []), (false_ctr, [])]))
     | Unknown(_) => Unknown
-    | Int // technically int and float are finite, but ya know
-    | Float
+    | Int
+    | Float // technically float is finite, but ya know
     | String
     | Arrow(_)
     | Forall(_)
@@ -188,7 +188,7 @@
   };
 
   type seen = {
-    seen_ints: IntSet.t,
+    seen_ints: BigintSet.t,
     seen_floats: FloatSet.t,
     seen_strings: StringSet.t,
     seen_ctrs: Ctr.Set.t,
@@ -199,7 +199,7 @@
   };
 
   let init_seen = {
-    seen_ints: IntSet.empty,
+    seen_ints: BigintSet.empty,
     seen_floats: FloatSet.empty,
     seen_strings: StringSet.empty,
     seen_ctrs: Ctr.Set.empty,
@@ -224,10 +224,10 @@
         | [] => seen
         | [Int(n), ..._] => {
             ...seen,
-            seen_ints: IntSet.add(n, seen.seen_ints),
+            seen_ints: BigintSet.add(n, seen.seen_ints),
             first_col_redundant_rows:
               add_redundant_row_if(
-                IntSet.mem(n, seen.seen_ints) || seen.seen_truth,
+                BigintSet.mem(n, seen.seen_ints) || seen.seen_truth,
                 row.idx,
                 seen.first_col_redundant_rows,
               ),

src/haz3lcore/statics/MakeTerm.re

@@ -206,7 +206,7 @@ and exp_term: unsorted => (Exp.term, list(Id.t)) = {
       | ([t], []) when Form.is_empty_list(t) => ret(ListLit([]))
       | ([t], []) when Form.is_bool(t) => ret(Bool(bool_of_string(t)))
       | ([t], []) when Form.is_undefined(t) => ret(Undefined)
-      | ([t], []) when Form.is_int(t) => ret(Int(int_of_string(t)))
+      | ([t], []) when Form.is_int(t) => ret(Int(Bigint.of_string(t)))
       | ([t], []) when Form.is_string(t) =>
         ret(String(Form.strip_quotes(t)))
       | ([t], []) when Form.is_float(t) => ret(Float(float_of_string(t)))
@@ -432,7 +432,7 @@ and pat_term: unsorted => (Pat.term, list(Id.t)) = {
         | ([t], []) when Form.is_empty_list(t) => ListLit([])
         | ([t], []) when Form.is_bool(t) => Bool(bool_of_string(t))
         | ([t], []) when Form.is_float(t) => Float(float_of_string(t))
-        | ([t], []) when Form.is_int(t) => Int(int_of_string(t))
+        | ([t], []) when Form.is_int(t) => Int(Bigint.of_string(t))
         | ([t], []) when Form.is_string(t) => String(Form.strip_quotes(t))
         | ([t], []) when Form.is_var(t) => Var(t)
         | ([t], []) when Form.is_wild(t) => Wild

src/haz3lmenhir/AST.re

@@ -109,7 +109,7 @@ type pat =
   | CastPat(pat, typ, typ)
   | EmptyHolePat
   | WildPat
-  | IntPat(int)
+  | IntPat(Bigint.t)
   | FloatPat(
       [@equal (a, b) => Printf.(sprintf("%f", a) == sprintf("%f", b))] float,
     )
@@ -138,7 +138,7 @@ type deferral_pos =
 
 [@deriving (show({with_path: false}), sexp, eq)]
 type exp =
-  | Int(int)
+  | Int(Bigint.t)
   | Float
       // This equality condition is used to say that two floats are equal if they are equal in the ExpToSegment serialization
       (
@@ -305,7 +305,7 @@ let rec gen_exp_sized = (n: int): QCheck.Gen.t(exp) =>
   QCheck.Gen.(
     let leaf =
       oneof([
-        map(x => Int(x), small_int),
+        map(x => Int(x |> Bigint.of_int), small_int),
         map(x => String(x), gen_string_literal),
         map(x => Float(x), QCheck.pos_float.gen), // Floats are positive because we use UnOp minus
         map(x => Var(x), gen_ident),
@@ -568,7 +568,7 @@ and gen_pat_sized: int => QCheck.Gen.t(pat) =
             oneof([
               return(WildPat),
               return(EmptyHolePat),
-              map(x => IntPat(x), small_int),
+              map(x => IntPat(Bigint.of_int(x)), small_int),
               map(x => FloatPat(x), QCheck.pos_float.gen),
               map(x => VarPat(x), gen_ident),
               map(x => StringPat(x), gen_string_literal),