unique BigInt module for Ocamlnum/Zarith compatibility

Makefile.in

@@ -108,7 +108,7 @@ LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
 
 LIB_UTIL = config util opt lists strings extmap extset exthtbl weakhtbl \
 	   hashcons stdlib exn_printer pp debug loc print_tree \
-	   cmdline warning sysutil rc plugin number pqueue
+	   cmdline warning sysutil rc plugin bigInt number pqueue
 
 LIB_CORE = ident ty term pattern decl theory \
 	   task pretty dterm env trans printer

src/util/bigInt.ml

+
+open Big_int
+
+type t = big_int
+let compare = compare_big_int
+
+let zero = zero_big_int
+let of_int = big_int_of_int
+
+let succ = succ_big_int
+let pred = pred_big_int
+
+let add_int = add_int_big_int
+let mul_int = mult_int_big_int
+
+let add = add_big_int
+let sub = sub_big_int
+let mul = mult_big_int
+let minus = minus_big_int
+
+let sign = sign_big_int
+
+let eq = eq_big_int
+let lt = lt_big_int
+let gt = gt_big_int
+let le = le_big_int
+let ge = ge_big_int
+
+
+let euclidean_div_mod = quomod_big_int
+
+let euclidean_div x y = fst (euclidean_div_mod x y)
+
+let euclidean_mod x y = snd (euclidean_div_mod x y)
+
+let computer_div_mod x y =
+  let q,r = quomod_big_int x y in
+  (* we have x = q*y + r with 0 <= r < |y| *)
+  if sign x < 0 then
+    if sign y < 0 
+    then (pred q, add r y)
+    else (succ q, sub r y)
+  else (q,r)
+
+let computer_div x y = fst (computer_div_mod x y)
+
+let computer_mod x y = snd (computer_div_mod x y)
+
+let min = min_big_int
+let max = max_big_int
+
+let pow_int_pos = power_int_positive_int
+
+let to_string = string_of_big_int
+let of_string = big_int_of_string

src/util/bigInt.mli

+
+
+type t
+
+val compare : t -> t -> int
+
+(** constants *)
+val zero : t
+val of_int : int -> t
+
+(** basic operations *)
+val succ : t -> t
+val pred : t -> t
+val add_int : int -> t -> t
+val mul_int : int -> t -> t
+val add : t -> t -> t
+val sub : t -> t -> t
+val mul : t -> t -> t
+val minus : t -> t
+val sign : t -> int
+
+(** comparisons *)
+val eq : t -> t -> bool
+val lt : t -> t -> bool
+val gt : t -> t -> bool
+val le : t -> t -> bool
+val ge : t -> t -> bool
+
+(** Division and modulo operators with the convention 
+that modulo is always non-negative.
+
+It implies that division rounds down when divisor is positive, and
+rounds up when divisor is negative.
+*)
+val euclidean_div_mod : t -> t -> t * t
+val euclidean_div : t -> t -> t 
+val euclidean_mod : t -> t -> t 
+
+(** "computer" division, i.e division rounds towards zero, and thus [mod
+    x y] has the same sign as x
+*)
+val computer_div_mod : t -> t -> t * t
+val computer_div : t -> t -> t 
+val computer_mod : t -> t -> t 
+
+(** min and max *)
+val min : t -> t -> t
+val max : t -> t -> t
+
+(** power of small integers. Second arg must be non-negative *)
+val pow_int_pos : int -> int -> t
+
+(** conversion with strings *)
+val of_string : string -> t
+val to_string : t -> string

src/util/bigInt_ocamlnum.ml

+
+open Big_int
+
+type t = big_int
+let compare = compare_big_int
+
+let zero = zero_big_int
+let of_int = big_int_of_int
+
+let succ = succ_big_int
+let pred = pred_big_int
+
+let add_int = add_int_big_int
+let mul_int = mult_int_big_int
+
+let add = add_big_int
+let sub = sub_big_int
+let mul = mult_big_int
+let minus = minus_big_int
+
+let sign = sign_big_int
+
+let eq = eq_big_int
+let lt = lt_big_int
+let gt = gt_big_int
+let le = le_big_int
+let ge = ge_big_int
+
+
+let euclidean_div_mod = quomod_big_int
+
+let euclidean_div x y = fst (euclidean_div_mod x y)
+
+let euclidean_mod x y = snd (euclidean_div_mod x y)
+
+let computer_div_mod x y =
+  let q,r = quomod_big_int x y in
+  (* we have x = q*y + r with 0 <= r < |y| *)
+  if sign x < 0 then
+    if sign y < 0 
+    then (pred q, add r y)
+    else (succ q, sub r y)
+  else (q,r)
+
+let computer_div x y = fst (computer_div_mod x y)
+
+let computer_mod x y = snd (computer_div_mod x y)
+
+let min = min_big_int
+let max = max_big_int
+
+let pow_int_pos = power_int_positive_int
+
+let to_string = string_of_big_int
+let of_string = big_int_of_string

src/util/bigInt_zarith.ml

+
+type t = Z.t
+let compare = compare_big_int
+
+let zero = zero_big_int
+let of_int = big_int_of_int
+
+let succ = succ_big_int
+let pred = pred_big_int
+
+let add_int = add_int_big_int
+let mul_int = mult_int_big_int
+
+let add = add_big_int
+let sub = sub_big_int
+let mul = mult_big_int
+let minus = minus_big_int
+
+let sign = sign_big_int
+
+let eq = eq_big_int
+let lt = lt_big_int
+let gt = gt_big_int
+let le = le_big_int
+let ge = ge_big_int
+
+
+let euclidean_div_mod = quomod_big_int
+
+let euclidean_div x y = fst (euclidean_div_mod x y)
+
+let euclidean_mod x y = snd (euclidean_div_mod x y)
+
+let computer_div_mod x y =
+  let q,r = quomod_big_int x y in
+  (* we have x = q*y + r with 0 <= r < |y| *)
+  if sign x < 0 then
+    if sign y < 0 
+    then (pred q, add r y)
+    else (succ q, sub r y)
+  else (q,r)
+
+let computer_div x y = fst (computer_div_mod x y)
+
+let computer_mod x y = snd (computer_div_mod x y)
+
+let min = min_big_int
+let max = max_big_int
+
+let pow_int_pos = power_int_positive_int
+
+let to_string = string_of_big_int
+let of_string = big_int_of_string

src/util/number.ml

@@ -10,7 +10,6 @@
 (********************************************************************)
 
 open Format
-open Big_int
 
 (** Construction *)
 
@@ -77,6 +76,7 @@ let real_const_hex i f e =
 
 (** Printing *)
 
+
 let compute_any radix s =
   let n = String.length s in
   let rec compute acc i =
@@ -89,9 +89,9 @@ let compute_any radix s =
         | 'a'..'z' as c -> 10 + Char.code c - Char.code 'a'
         | _ -> assert false in
       assert (v < radix);
-      compute (add_int_big_int v (mult_int_big_int radix acc)) (i + 1)
+      compute (BigInt.add_int v (BigInt.mul_int radix acc)) (i + 1)
     end in
-  (compute zero_big_int 0)
+  (compute BigInt.zero 0)
 
 let compute_int c =
   match c with
@@ -101,10 +101,10 @@ let compute_int c =
   | IConstBin s -> compute_any 2 s
 
 let any_to_dec radix s =
-  string_of_big_int (compute_any radix s)
+  BigInt.to_string (compute_any radix s)
 
 let power2 n =
-  string_of_big_int (power_int_positive_int 2 n)
+  BigInt.to_string (BigInt.pow_int_pos 2 n)
 
 type integer_format =
   (string -> unit, Format.formatter, unit) format
@@ -154,7 +154,7 @@ let force_support support do_it v =
   | Number_default -> assert false
   | Number_custom f -> do_it f v
 
-let simplify_max_int = big_int_of_string "2147483646"
+let simplify_max_int = BigInt.of_string "2147483646"
 
 let remove_minus e =
   if e.[0] = '-' then
@@ -165,7 +165,7 @@ let print_dec_int support fmt i =
   let fallback i =
     force_support support.def_int_support (fprintf fmt) i in
   if not support.long_int_support &&
-     (compare_big_int (big_int_of_string i) simplify_max_int > 0) then
+     (BigInt.compare (BigInt.of_string i) simplify_max_int > 0) then
     fallback i
   else
     check_support support.dec_int_support (Some "%s") (fprintf fmt)

src/util/number.mli

@@ -38,7 +38,7 @@ val int_const_bin : string -> integer_constant
     InvalidConstantLiteral(base,s) is raised if [s] contains invalid
     characters for the given base. *)
 
-val compute_int : integer_constant -> Big_int.big_int
+val compute_int : integer_constant -> BigInt.t
 
 val real_const_dec : string -> string -> string option -> real_constant
 val real_const_hex : string -> string -> string option -> real_constant

src/whyml/mlw_interp.ml

@@ -23,13 +23,11 @@ open Mlw_ty
 open Mlw_ty.T
 open Mlw_expr
 
-module Nummap =
-  Map.Make(struct type t = Big_int.big_int
-                  let compare = Big_int.compare_big_int end)
+module Nummap = Map.Make(BigInt)
 
 type value =
   | Vapp of lsymbol * value list
-  | Vnum of Big_int.big_int
+  | Vnum of BigInt.t
   | Vbool of bool
   | Vvoid
   | Vreg of region
@@ -52,7 +50,7 @@ let array_cons_ls = ref ps_equ
 let rec print_value fmt v =
   match v with
   | Vnum n ->
-    fprintf fmt "%s" (Big_int.string_of_big_int n)
+    fprintf fmt "%s" (BigInt.to_string n)
   | Vbool b ->
     fprintf fmt "%b" b
   | Vvoid ->
@@ -62,21 +60,21 @@ let rec print_value fmt v =
     fprintf fmt "@[[def=%a" print_value def;
     Nummap.iter
       (fun i v ->
-        fprintf fmt ",@ %s -> %a" (Big_int.string_of_big_int i) print_value v)
+        fprintf fmt ",@ %s -> %a" (BigInt.to_string i) print_value v)
       m;
     fprintf fmt "]@]"
   | Vapp(ls,[Vnum len;Vmap(def,m)]) when ls_equal ls !array_cons_ls ->
     fprintf fmt "@[[";
-    let i = ref Big_int.zero_big_int in
-    while Big_int.lt_big_int !i len do
+    let i = ref BigInt.zero in
+    while BigInt.lt !i len do
       let v =
         try Nummap.find !i m
         with Not_found -> def
       in
-      if Big_int.gt_big_int !i Big_int.zero_big_int
+      if BigInt.gt !i BigInt.zero
       then fprintf fmt ",@ ";
       fprintf fmt "%a" print_value v;
-      i := Big_int.succ_big_int !i
+      i := BigInt.succ !i
     done;
     fprintf fmt "]@]"
   | Vapp(ls,vl) ->
@@ -229,22 +227,6 @@ let rec matching env (t:value) p =
 
 (* builtin symbols *)
 
-let computer_div_mod_big_int x y =
-  let q,r = Big_int.quomod_big_int x y in
-  (* we have x = q*y + r with 0 <= r < |y| *)
-  if Big_int.sign_big_int x < 0 then
-    if Big_int.sign_big_int y < 0 then
-      (Big_int.pred_big_int q, Big_int.add_big_int r y)
-    else
-      (Big_int.succ_big_int q, Big_int.sub_big_int r y)
-  else (q,r)
-
-let computer_div_big_int x y =
-  fst (computer_div_mod_big_int x y)
-
-let computer_mod_big_int x y =
-  snd (computer_div_mod_big_int x y)
-
 let builtins = Hls.create 17
 
 let ls_minus = ref ps_equ (* temporary *)
@@ -301,7 +283,7 @@ let must_be_true b =
 
 let rec value_equality v1 v2 =
   match (v1,v2) with
-    | Vnum i1, Vnum i2 -> Big_int.eq_big_int i1 i2
+    | Vnum i1, Vnum i2 -> BigInt.eq i1 i2
     | Vbool b1, Vbool b2 -> b1 == b2
     | Vapp(ls1,vl1), Vapp(ls2,vl2) ->
       must_be_true (ls_equal ls1 ls2 && List.for_all2 value_equality vl1 vl2)
@@ -422,26 +404,26 @@ let built_in_theories =
       "False", None, eval_false ;
     ] ;
     ["int"],"Int", [],
-    [ "infix +", None, eval_int_op Big_int.add_big_int;
-      "infix -", None, eval_int_op Big_int.sub_big_int;
-      "infix *", None, eval_int_op Big_int.mult_big_int;
-      "prefix -", Some ls_minus, eval_int_uop Big_int.minus_big_int;
-      "infix <", None, eval_int_rel Big_int.lt_big_int;
-      "infix <=", None, eval_int_rel Big_int.le_big_int;
-      "infix >", None, eval_int_rel Big_int.gt_big_int;
-      "infix >=", None, eval_int_rel Big_int.ge_big_int;
+    [ "infix +", None, eval_int_op BigInt.add;
+      "infix -", None, eval_int_op BigInt.sub;
+      "infix *", None, eval_int_op BigInt.mul;
+      "prefix -", Some ls_minus, eval_int_uop BigInt.minus;
+      "infix <", None, eval_int_rel BigInt.lt;
+      "infix <=", None, eval_int_rel BigInt.le;
+      "infix >", None, eval_int_rel BigInt.gt;
+      "infix >=", None, eval_int_rel BigInt.ge;
     ] ;
     ["int"],"MinMax", [],
-    [ "min", None, eval_int_op Big_int.min_big_int;
-      "max", None, eval_int_op Big_int.max_big_int;
+    [ "min", None, eval_int_op BigInt.min;
+      "max", None, eval_int_op BigInt.max;
     ] ;
     ["int"],"ComputerDivision", [],
-    [ "div", None, eval_int_op computer_div_big_int;
-      "mod", None, eval_int_op computer_mod_big_int;
+    [ "div", None, eval_int_op BigInt.computer_div;
+      "mod", None, eval_int_op BigInt.computer_mod;
     ] ;
     ["int"],"EuclideanDivision", [],
-    [ "div", None, eval_int_op Big_int.div_big_int;
-      "mod", None, eval_int_op Big_int.mod_big_int;
+    [ "div", None, eval_int_op BigInt.euclidean_div;
+      "mod", None, eval_int_op BigInt.euclidean_mod;
     ] ;
     ["map"],"Map", ["map", builtin_map_type],
     [ "const", Some ls_map_const, eval_map_const;
@@ -566,7 +548,7 @@ let rec any_value_of_type env ty =
   | Ty.Tyvar _ -> assert false
   | Ty.Tyapp(ts,_) when Ty.ts_equal ts Ty.ts_int ->
     let n = Random.int 199 - 99 in
-    Vnum (Big_int.big_int_of_int n)
+    Vnum (BigInt.of_int n)
   | Ty.Tyapp(ts,_) when Ty.ts_equal ts Ty.ts_real ->
     Vvoid (* FIXME *)
   | Ty.Tyapp(ts,_) when Ty.ts_equal ts Ty.ts_bool ->
@@ -1148,12 +1130,12 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
         let a = big_int_of_value (get_pvs env (*s*) pvs1) in
         let b = big_int_of_value (get_pvs env (*s*) pvs2) in
         let le,suc = match dir with
-          | To -> Big_int.le_big_int, Big_int.succ_big_int
-          | DownTo -> Big_int.ge_big_int, Big_int.pred_big_int
+          | To -> BigInt.le, BigInt.succ
+          | DownTo -> BigInt.ge, BigInt.pred
         in
         let rec iter i s =
           Debug.dprintf debug "[interp] for loop with index = %s@."
-            (Big_int.string_of_big_int i);
+            (BigInt.to_string i);
           if le i b then
             let env' = bind_vs pvs.pv_vs (Vnum i) env in
             match eval_expr env' s e1 with
@@ -1297,9 +1279,6 @@ and exec_app env s ps args (*spec*) ity_result =
 
 
 
-(*
-let default_fixme = Vnum (Big_int.big_int_of_string "424242")
-*)
 
 let eval_global_expr env mkm tkm _writes e =
 (*