From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- clib/int.ml | 239 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 239 insertions(+) create mode 100644 clib/int.ml (limited to 'clib/int.ml') diff --git a/clib/int.ml b/clib/int.ml new file mode 100644 index 00000000..3ae836ae --- /dev/null +++ b/clib/int.ml @@ -0,0 +1,239 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* int -> bool = "%eq" + +external compare : int -> int -> int = "caml_int_compare" + +let hash i = i land 0x3FFFFFFF + +module Self = +struct + type t = int + let compare = compare +end + +module Set = Set.Make(Self) +module Map = +struct + include CMap.Make(Self) + + type 'a map = 'a CMap.Make(Self).t + + type 'a _map = + | MEmpty + | MNode of 'a map * int * 'a * 'a map * int + + let map_prj : 'a map -> 'a _map = Obj.magic + + let rec find i s = match map_prj s with + | MEmpty -> raise Not_found + | MNode (l, k, v, r, h) -> + if i < k then find i l + else if i = k then v + else find i r +end + +module List = struct + let mem = List.memq + let assoc = List.assq + let mem_assoc = List.mem_assq + let remove_assoc = List.remove_assq +end + +let min (i : int) j = if i < j then i else j + +(** Utility function *) +let rec next from upto = + if from < upto then next (2 * from + 1) upto + else from + + +module PArray = +struct + + type 'a t = 'a data ref + and 'a data = + | Root of 'a option array + | DSet of int * 'a option * 'a t + + let empty n = ref (Root (Array.make n None)) + + let rec rerootk t k = match !t with + | Root _ -> k () + | DSet (i, v, t') -> + let next () = match !t' with + | Root a as n -> + let v' = Array.unsafe_get a i in + let () = Array.unsafe_set a i v in + let () = t := n in + let () = t' := DSet (i, v', t) in + k () + | DSet _ -> assert false + in + rerootk t' next + + let reroot t = rerootk t (fun () -> ()) + + let get t i = + let () = assert (0 <= i) in + match !t with + | Root a -> + if Array.length a <= i then None + else Array.unsafe_get a i + | DSet _ -> + let () = reroot t in + match !t with + | Root a -> + if Array.length a <= i then None + else Array.unsafe_get a i + | DSet _ -> assert false + + let set t i v = + let () = assert (0 <= i) in + let () = reroot t in + match !t with + | DSet _ -> assert false + | Root a as n -> + let len = Array.length a in + if i < len then + let old = Array.unsafe_get a i in + if old == v then t + else + let () = Array.unsafe_set a i v in + let res = ref n in + let () = t := DSet (i, old, res) in + res + else match v with + | None -> t (** Nothing to do! *) + | Some _ -> (** we must resize *) + let nlen = next len (succ i) in + let nlen = min nlen Sys.max_array_length in + let () = assert (i < nlen) in + let a' = Array.make nlen None in + let () = Array.blit a 0 a' 0 len in + let () = Array.unsafe_set a' i v in + let res = ref (Root a') in + let () = t := DSet (i, None, res) in + res + +end + +module PMap = +struct + + type key = int + + (** Invariants: + + 1. an empty map is always [Empty]. + 2. the set of the [Map] constructor remembers the present keys. + *) + type 'a t = Empty | Map of Set.t * 'a PArray.t + + let empty = Empty + + let is_empty = function + | Empty -> true + | Map _ -> false + + let singleton k x = + let len = next 19 (k + 1) in + let len = min Sys.max_array_length len in + let v = PArray.empty len in + let v = PArray.set v k (Some x) in + let s = Set.singleton k in + Map (s, v) + + let add k x = function + | Empty -> singleton k x + | Map (s, v) -> + let s = match PArray.get v k with + | None -> Set.add k s + | Some _ -> s + in + let v = PArray.set v k (Some x) in + Map (s, v) + + let remove k = function + | Empty -> Empty + | Map (s, v) -> + let s = Set.remove k s in + if Set.is_empty s then Empty + else + let v = PArray.set v k None in + Map (s, v) + + let mem k = function + | Empty -> false + | Map (_, v) -> + match PArray.get v k with + | None -> false + | Some _ -> true + + let find k = function + | Empty -> raise Not_found + | Map (_, v) -> + match PArray.get v k with + | None -> raise Not_found + | Some x -> x + + let iter f = function + | Empty -> () + | Map (s, v) -> + let iter k = match PArray.get v k with + | None -> () + | Some x -> f k x + in + Set.iter iter s + + let fold f m accu = match m with + | Empty -> accu + | Map (s, v) -> + let fold k accu = match PArray.get v k with + | None -> accu + | Some x -> f k x accu + in + Set.fold fold s accu + + let exists f m = match m with + | Empty -> false + | Map (s, v) -> + let exists k = match PArray.get v k with + | None -> false + | Some x -> f k x + in + Set.exists exists s + + let for_all f m = match m with + | Empty -> true + | Map (s, v) -> + let for_all k = match PArray.get v k with + | None -> true + | Some x -> f k x + in + Set.for_all for_all s + + let cast = function + | Empty -> Map.empty + | Map (s, v) -> + let bind k = match PArray.get v k with + | None -> assert false + | Some x -> x + in + Map.bind bind s + + let domain = function + | Empty -> Set.empty + | Map (s, _) -> s + +end -- cgit v1.2.3