Commit 7fbf7e27 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Implement hash-consing of big_ints. This allows us to know the set of all...

Implement hash-consing of big_ints. This allows us to know the set of all big_ints constants that are used
by a program and to serialize them as string (fix a compatibility issue with js_of_ocaml).
This could also lead to some optimizations when computing expensive big_ints.
parent e719abe3
......@@ -171,7 +171,7 @@ DIRS := $(DIRS_DEPEND) $(OCAMLIFACE)
# Objects to build
OBJECTS = \
driver/cduce_config.cmo misc/stats.cmo misc/custom.cmo misc/encodings.cmo \
driver/cduce_config.cmo misc/stats.cmo misc/custom.cmo misc/hBig_int.cmo misc/encodings.cmo \
misc/upool.cmo misc/pretty.cmo misc/ns.cmo misc/imap.cmo misc/html.cmo misc/utils.cmo \
\
types/compunit.cmo types/sortedList.cmo types/ident.cmo types/var.cmo types/bool.cmo \
......
......@@ -4,6 +4,8 @@ misc/stats.cmo : misc/stats.cmi
misc/stats.cmx : misc/stats.cmi
misc/custom.cmo :
misc/custom.cmx :
misc/hBig_int.cmo : misc/hBig_int.cmi
misc/hBig_int.cmx : misc/hBig_int.cmi
misc/encodings.cmo : misc/custom.cmo misc/encodings.cmi
misc/encodings.cmx : misc/custom.cmx misc/encodings.cmi
misc/upool.cmo : misc/custom.cmo misc/upool.cmi
......@@ -32,8 +34,8 @@ types/var.cmx : misc/utils.cmx types/sortedList.cmx types/ident.cmx \
misc/custom.cmx types/var.cmi
types/bool.cmo : types/var.cmi misc/custom.cmo types/bool.cmi
types/bool.cmx : types/var.cmx misc/custom.cmx types/bool.cmi
types/intervals.cmo : types/intervals.cmi
types/intervals.cmx : types/intervals.cmi
types/intervals.cmo : misc/hBig_int.cmi types/intervals.cmi
types/intervals.cmx : misc/hBig_int.cmx types/intervals.cmi
types/chars.cmo : misc/custom.cmo types/chars.cmi
types/chars.cmx : misc/custom.cmx types/chars.cmi
types/atoms.cmo : misc/upool.cmi types/sortedList.cmi misc/ns.cmi \
......@@ -366,6 +368,7 @@ runtime/cduce_js.cmx : runtime/value.cmx runtime/print_xml.cmx misc/ns.cmx \
runtime/load_xml.cmx runtime/cduce_js.cmi
driver/cduce_config.cmi :
misc/stats.cmi :
misc/hBig_int.cmi : misc/custom.cmo
misc/encodings.cmi : misc/custom.cmo
misc/upool.cmi : misc/custom.cmo
misc/pretty.cmi :
......
......@@ -47,7 +47,7 @@ let mk name descr typing compile code ext_info depends =
status = `Unevaluated;
}
let magic = "CDUCE:compunit:00007"
let magic = "CDUCE:compunit:00008"
let has_obj n =
let base = U.to_string n ^ ".cdo" in
......@@ -120,9 +120,10 @@ let compile_save verbose name src out =
let c = compile verbose name src in
set_hash c;
let pools = Value.extract_all () in
let ints = Intervals.V.extract () in
let oc = open_out_bin out in
output_string oc magic;
Marshal.to_channel oc (pools,c) [Marshal.Compat_32];
Marshal.to_channel oc (pools,c, ints) [Marshal.Compat_32];
let digest = Digest.file out in
Marshal.to_channel oc digest [Marshal.Compat_32];
close_out oc
......@@ -149,9 +150,10 @@ let rec real_load src =
let s = String.copy magic in
really_input ic s 0 (String.length s);
if s <> magic then raise (InvalidObject src);
let pools,c = Marshal.from_channel ic in
let pools, c, ints = Marshal.from_channel ic in
let digest = Marshal.from_channel ic in
c.digest <- Some digest;
Intervals.V.intract ints;
Value.intract_all pools;
close_in ic;
c
......
(* Hash-consed big int that can be serialized without resorting to serializing custom-block.
works around a bug in js_of_ocaml that does not support deserializing nat
*)
open Big_int
type pool = { mutable ints : big_int array;
mutable next : int }
let pool = { ints = [| |] ;
next = 0 }
type ext_pool = string array * int * int
let extract () =
let arr = Array.sub pool.ints 0 pool.next in
(Array.map (string_of_big_int) arr,
pool.next,
Array.length pool.ints)
let get i = Array.unsafe_get pool.ints i
let set i v =
if i == pool.next then
begin
let len = Array.length pool.ints in
if i >= len then begin
let arr = Array.make (2 * len + 1) zero_big_int in
Array.blit pool.ints 0 arr 0 len;
pool.ints <- arr;
end;
Array.unsafe_set pool.ints i v
end
else
if i < pool.next then Array.unsafe_set pool.ints i v
else assert false
let hash_nat x = Nat.nth_digit_nat x 0
let hash_bigint (sign,nat) = (sign * 17 + hash_nat nat) land 0x3fffffff
module HBI = Hashtbl.Make(struct
type t = big_int
let hash v = hash_bigint (Obj.magic v)
let equal = eq_big_int
end)
let hbi = HBI.create 17
let intract (sa, next, len) =
let arr = Array.make len zero_big_int in
Array.iteri (fun i s ->
let bi = big_int_of_string s in
Array.unsafe_set arr i bi;
HBI.add hbi bi i
) sa;
pool.ints <- arr;
pool.next <- next
let cons bi =
try
HBI.find hbi bi
with
Not_found ->
let i = pool.next in
set i bi;
HBI.add hbi bi i;
pool.next <- pool.next + 1;
if pool.next land 0x3fffffff != pool.next then
failwith "Internal error, hBig_int.ml,l50 : counter overflow";
i
type t = int
let print ppf i = Format.fprintf ppf "%s" (string_of_big_int (get i))
let dump = print
let compare i j = compare_big_int (get i) (get j)
let hash i = hash_bigint (Obj.magic (get i))
let equal i j = eq_big_int (get i) (get j)
let check _ = ()
let from_int i = cons (big_int_of_int i)
let from_bigint i = cons i
let mk s = cons (big_int_of_string s)
let to_string i = string_of_big_int (get i)
let get_int i = int_of_big_int (get i)
let get_bigint i = get i
let is_int i = is_int_big_int (get i)
let add i j = cons (add_big_int (get i) (get j))
let mult i j = cons (mult_big_int (get i) (get j))
let sub i j = cons (sub_big_int (get i) (get j))
let div i j = cons (div_big_int (get i) (get j))
let modulo i j = cons (mod_big_int (get i) (get j))
let succ i = cons (succ_big_int (get i))
let pred i = cons (pred_big_int (get i))
let negat i = cons (sub_big_int zero_big_int (get i))
let lt i j = lt_big_int (get i) (get j)
let le i j = le_big_int (get i) (get j)
let gt i j = gt_big_int (get i) (get j)
let ge i j = ge_big_int (get i) (get j)
let max i j = cons (max_big_int (get i) (get j))
let min i j = cons (min_big_int (get i) (get j))
let zero = cons (zero_big_int)
let one = cons (unit_big_int)
let () = for i = 2 to 255 do
ignore (cons (big_int_of_int i))
done
let minus_one = negat one
let is_zero i = i == 0 (* invariant, zero_big_int is the first hash-consed big_int *)
let sign i = sign_big_int (get i)
let from_int32 i = cons (big_int_of_string (Int32.to_string i))
let from_int64 i = cons (big_int_of_string (Int64.to_string i))
let to_int32 i = Int32.of_string (to_string i)
let to_int64 i = Int64.of_string (to_string i)
include Custom.T
val print : Format.formatter -> t -> unit
val mk: string -> t
val from_int: int -> t
val from_bigint: Big_int.big_int -> t
val to_string: t -> string
val is_int: t -> bool
val get_int: t -> int
val get_bigint: t -> Big_int.big_int
val is_zero: t -> bool
val add: t -> t -> t
val mult: t -> t -> t
val sub: t -> t -> t
val div: t -> t -> t
val modulo: t -> t -> t
val succ: t -> t
val pred: t -> t
val negat: t -> t
val lt: t -> t -> bool
val le: t -> t -> bool
val gt: t -> t -> bool
val ge: t -> t -> bool
val max: t -> t -> t
val min: t -> t -> t
val zero : t
val one : t
val minus_one : t
val sign : t -> int
val from_int32: Int32.t -> t
val from_int64: Int64.t -> t
val to_int32: t -> Int32.t
val to_int64: t -> Int64.t
type ext_pool
val extract : unit -> ext_pool
val intract : ext_pool -> unit
open Big_int
module V = struct
(* Hack to compute hash value for bigints *)
(*
(* Hack to compute hash value for bigints *)
let hash_nat x = Nat.nth_digit_nat x 0
let hash_bigint (sign,nat) = (sign * 17 + hash_nat nat) land 0x3fffffff
......@@ -44,12 +45,14 @@ let from_int32 i = mk (Int32.to_string i)
let from_int64 i = mk (Int64.to_string i)
let to_int32 i = Int32.of_string (to_string i)
let to_int64 i = Int64.of_string (to_string i)
*)
include HBig_int
end
type interval =
| Bounded of big_int * big_int
| Left of big_int
| Right of big_int
| Bounded of HBig_int.t * HBig_int.t
| Left of HBig_int.t
| Right of HBig_int.t
| Any
type t = interval list
......@@ -95,14 +98,14 @@ let rec equal l1 l2 =
(l1 == l2) ||
match (l1,l2) with
| (Bounded (a1,b1) :: l1, Bounded (a2,b2) :: l2) ->
(eq_big_int a1 a2) &&
(eq_big_int b1 b2) &&
(HBig_int.equal a1 a2) &&
(HBig_int.equal b1 b2) &&
(equal l1 l2)
| (Left b1 :: l1, Left b2 :: l2) ->
(eq_big_int b1 b2) &&
(HBig_int.equal b1 b2) &&
(equal l1 l2)
| (Right a1 :: l1, Right a2 :: l2) ->
(eq_big_int a1 a2) &&
(HBig_int.equal a1 a2) &&
(equal l1 l2)
| (Any :: _, Any :: _) -> true
| ([], []) -> true
......@@ -128,7 +131,7 @@ type elem = V.t
let full = any
let bounded a b =
if le_big_int a b then [Bounded (a,b)] else empty
if HBig_int.le a b then [Bounded (a,b)] else empty
let left a = [Left a]
let right a = [Right a]
......@@ -138,11 +141,11 @@ let atom a = bounded a a
let rec iadd_left l b = match l with
| [] -> [Left b]
| (Bounded (a1,_) | Right a1) :: _
when (lt_big_int b (pred_big_int a1)) ->
when HBig_int.(lt b (pred a1)) ->
Left b :: l
| Bounded (_,b1) :: l' ->
iadd_left l' (max_big_int b b1)
| Left b1 :: _ when le_big_int b b1-> l
iadd_left l' (HBig_int.max b b1)
| Left b1 :: _ when HBig_int.le b b1-> l
| Left _ :: l' ->
iadd_left l' b
| _ -> any
......@@ -151,25 +154,25 @@ let rec iadd_bounded l a b = match l with
| [] ->
[Bounded (a,b)]
| (Bounded (a1,_) | Right a1) :: _
when (lt_big_int b (pred_big_int a1)) ->
when (HBig_int.lt b (HBig_int.pred a1)) ->
Bounded (a,b) :: l
| ((Bounded (_,b1) | Left b1) as i') :: l'
when (lt_big_int (succ_big_int b1) a) ->
when (HBig_int.lt (HBig_int.succ b1) a) ->
i'::(iadd_bounded l' a b)
| Bounded (a1,b1) :: l' ->
iadd_bounded l' (min_big_int a a1) (max_big_int b b1)
iadd_bounded l' (HBig_int.min a a1) (HBig_int.max b b1)
| Left b1 :: l' ->
iadd_left l' (max_big_int b b1)
| Right a1 :: _ -> [Right (min_big_int a a1)]
iadd_left l' (HBig_int.max b b1)
| Right a1 :: _ -> [Right (HBig_int.min a a1)]
| Any :: _ -> any
let rec iadd_right l a = match l with
| [] -> [Right a]
| ((Bounded (_,b1) | Left b1) as i') :: l'
when (lt_big_int (succ_big_int b1) a) ->
when (HBig_int.lt (HBig_int.succ b1) a) ->
i'::(iadd_right l' a)
| (Bounded (a1,_) | Right a1) :: _ ->
[Right (min_big_int a a1)]
[Right (HBig_int.min a a1)]
| _ -> any
let iadd l = function
......@@ -181,17 +184,17 @@ let iadd l = function
let rec neg' start l = match l with
| [] -> [Right start]
| Bounded (a,b) :: l' ->
Bounded (start, pred_big_int a) :: (neg' (succ_big_int b) l')
Bounded (start, HBig_int.pred a) :: (neg' (HBig_int.succ b) l')
| Right a :: l' ->
[Bounded (start, pred_big_int a)]
[Bounded (start, HBig_int.pred a)]
| _ -> assert false
let neg = function
| Any :: _ -> []
| [] -> any
| Left b :: l -> neg' (succ_big_int b) l
| Right a :: _ -> [Left (pred_big_int a)]
| Bounded (a,b) :: l -> Left (pred_big_int a) :: neg' (succ_big_int b) l
| Left b :: l -> neg' (HBig_int.succ b) l
| Right a :: _ -> [Left (HBig_int.pred a)]
| Bounded (a,b) :: l -> Left (HBig_int.pred a) :: neg' (HBig_int.succ b) l
let cup i1 i2 =
List.fold_left iadd i1 i2
......@@ -210,36 +213,36 @@ let rec disjoint a b =
| Any::_,_ | _,Any::_ -> false
| Left _::_, Left _::_ -> false
| Right _::_, Right _::_ -> false
| Left x :: a, Bounded (y,_) :: _ -> (lt_big_int x y) && (disjoint a b)
| Bounded (y,_) :: _, Left x :: b -> (lt_big_int x y) && (disjoint a b)
| Left x :: _, Right y :: _ -> lt_big_int x y
| Right y :: _, Left x :: _ -> lt_big_int x y
| Right y :: _, Bounded (_,x) :: _ -> lt_big_int x y
| Bounded (_,x) :: _, Right y :: _ -> lt_big_int x y
| Left x :: a, Bounded (y,_) :: _ -> (HBig_int.lt x y) && (disjoint a b)
| Bounded (y,_) :: _, Left x :: b -> (HBig_int.lt x y) && (disjoint a b)
| Left x :: _, Right y :: _ -> HBig_int.lt x y
| Right y :: _, Left x :: _ -> HBig_int.lt x y
| Right y :: _, Bounded (_,x) :: _ -> HBig_int.lt x y
| Bounded (_,x) :: _, Right y :: _ -> HBig_int.lt x y
| Bounded (xa,ya) :: a', Bounded (xb,yb) :: b' ->
let c = compare_big_int xa xb in
let c = HBig_int.compare xa xb in
if c = 0 then false
else
if c < 0 then (lt_big_int ya xb) && (disjoint a' b)
else (lt_big_int yb xa) && (disjoint a b')
if c < 0 then (HBig_int.lt ya xb) && (disjoint a' b)
else (HBig_int.lt yb xa) && (disjoint a b')
(* TODO: can optimize this to stop running through the list earlier *)
let contains n =
List.exists (function
| Any -> true
| Left b -> le_big_int n b
| Right a -> le_big_int a n
| Bounded (a,b) -> (le_big_int a n) && (le_big_int n b)
| Left b -> HBig_int.le n b
| Right a -> HBig_int.le a n
| Bounded (a,b) -> (HBig_int.le a n) && (HBig_int.le n b)
)
let sample = function
| (Left x | Right x | Bounded (x,_)) :: _ -> x
| Any :: _ -> zero_big_int
| Any :: _ -> HBig_int.zero
| [] -> raise Not_found
let single = function
| [ Bounded (x,y) ] when eq_big_int x y -> x
| [ Bounded (x,y) ] when HBig_int.equal x y -> x
| [] -> raise Not_found
| _ -> raise Exit
......@@ -250,22 +253,22 @@ let print l =
Format.fprintf ppf "Int"
| Left b ->
Format.fprintf ppf "*--%s"
(string_of_big_int b)
(HBig_int.to_string b)
| Right a ->
Format.fprintf ppf "%s--*"
(string_of_big_int a)
| Bounded (a,b) when eq_big_int a b ->
(HBig_int.to_string a)
| Bounded (a,b) when HBig_int.equal a b ->
Format.fprintf ppf "%s"
(string_of_big_int a)
(HBig_int.to_string a)
| Bounded (a,b) ->
Format.fprintf ppf "%s--%s"
(string_of_big_int a)
(string_of_big_int b)
(HBig_int.to_string a)
(HBig_int.to_string b)
)
l
let ( + ) = add_big_int
let ( * ) = mult_big_int
let ( + ) = HBig_int.add
let ( * ) = HBig_int.mult
let is_bounded l =
List.for_all (function Left _ | Any -> false | _ -> true) l,
......@@ -296,9 +299,9 @@ let add l1 l2 =
let negat =
List.rev_map
(function
| Bounded (i,j) -> Bounded (minus_big_int j, minus_big_int i)
| Left i -> Right (minus_big_int i)
| Right j -> Left (minus_big_int j)
| Bounded (i,j) -> Bounded (HBig_int.negat j, HBig_int.negat i)
| Left i -> Right (HBig_int.negat i)
| Right j -> Left (HBig_int.negat j)
| Any -> Any
)
......@@ -313,7 +316,7 @@ let ( * ) x y =
| PlusInf,MinusInf | MinusInf,PlusInf -> MinusInf
| Int x, Int y -> Int (x * y)
| i,(Int x as ix) | (Int x as ix), i ->
(match i, sign_big_int x with
(match i, HBig_int.sign x with
| PlusInf,1 | MinusInf,-1 -> PlusInf
| PlusInf,-1 | MinusInf,1 -> MinusInf
| _ -> ix)
......@@ -322,13 +325,13 @@ let min a b =
match (a,b) with
| MinusInf,_ | _,PlusInf -> a
| PlusInf,_ | _,MinusInf -> b
| Int x, Int y -> if le_big_int x y then a else b
| Int x, Int y -> if HBig_int.le x y then a else b
let max a b =
match (a,b) with
| MinusInf,_ | _,PlusInf -> b
| PlusInf,_ | _,MinusInf -> a
| Int x, Int y -> if le_big_int x y then b else a
| Int x, Int y -> if HBig_int.le x y then b else a
let max4 a b c d = max a (max b (max c d))
let min4 a b c d = min a (min b (min c d))
......
module V : sig
include Custom.T
val print : Format.formatter -> t -> unit
val mk: string -> t
val from_int: int -> t
val from_bigint: Big_int.big_int -> t
val to_string: t -> string
val is_int: t -> bool
val get_int: t -> int
val get_bigint: t -> Big_int.big_int
val is_zero: t -> bool
val add: t -> t -> t
val mult: t -> t -> t
val sub: t -> t -> t
val div: t -> t -> t
val modulo: t -> t -> t
val succ: t -> t
val pred: t -> t
val negat: t -> t
val lt: t -> t -> bool
val gt: t -> t -> bool
val zero : t
val one : t
val minus_one : t
val from_int32: Int32.t -> t
val from_int64: Int64.t -> t
val to_int32: t -> Int32.t
val to_int64: t -> Int64.t
end
include module type of HBig_int
end
include Bool.S with type elem = V.t
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment