diff --git a/.Makefile.lint b/.Makefile.lint
index 259a202aa404477813c7df85e7e435de9c5f9870..c09a0269d79008f3c636c3d1c55df785cee4bc6a 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -146,11 +146,7 @@ ML_LINT_KO+=src/libraries/project/state_dependency_graph.mli
ML_LINT_KO+=src/libraries/project/state_selection.ml
ML_LINT_KO+=src/libraries/project/state_selection.mli
ML_LINT_KO+=src/libraries/project/state_topological.mli
-ML_LINT_KO+=src/libraries/stdlib/FCBuffer.ml
-ML_LINT_KO+=src/libraries/stdlib/FCBuffer.mli
ML_LINT_KO+=src/libraries/stdlib/FCHashtbl.mli
-ML_LINT_KO+=src/libraries/stdlib/FCSet.ml
-ML_LINT_KO+=src/libraries/stdlib/FCSet.mli
ML_LINT_KO+=src/libraries/stdlib/extlib.ml
ML_LINT_KO+=src/libraries/stdlib/extlib.mli
ML_LINT_KO+=src/libraries/utils/bag.ml
diff --git a/Makefile b/Makefile
index b9150c0247751961d89bfacf254a7dc188de4c8c..5136dd9a8b93c557310c9baea7309210b55371ed 100644
--- a/Makefile
+++ b/Makefile
@@ -440,8 +440,6 @@ CMO += $(VERY_FIRST_CMO)
LIB_CMO =\
src/libraries/stdlib/transitioning \
- src/libraries/stdlib/FCSet \
- src/libraries/stdlib/FCBuffer \
src/libraries/stdlib/FCHashtbl \
src/libraries/stdlib/extlib \
src/libraries/datatype/unmarshal \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 3e89f12518e8ee6a37d47076c045a8dd2c137848..f93a3797c6f1586aaeaa52de9858856bd5509e5b 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -628,14 +628,8 @@ src/libraries/project/state_selection.ml: CEA_LGPL
src/libraries/project/state_selection.mli: CEA_LGPL
src/libraries/project/state_topological.ml: MODIFIED_OCAMLGRAPH
src/libraries/project/state_topological.mli: MODIFIED_OCAMLGRAPH
-src/libraries/stdlib/FCBuffer.ml: OCAML_STDLIB
-src/libraries/stdlib/FCBuffer.mli: OCAML_STDLIB
src/libraries/stdlib/FCHashtbl.ml: CEA_LGPL
src/libraries/stdlib/FCHashtbl.mli: CEA_LGPL
-src/libraries/stdlib/FCMap.ml: OCAML_STDLIB
-src/libraries/stdlib/FCMap.mli: OCAML_STDLIB
-src/libraries/stdlib/FCSet.ml: OCAML_STDLIB
-src/libraries/stdlib/FCSet.mli: OCAML_STDLIB
src/libraries/stdlib/README.md: .ignore
src/libraries/stdlib/extlib.ml: CEA_LGPL
src/libraries/stdlib/extlib.mli: CEA_LGPL
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 655ce87541875983b1a94f8a057f6633241f54c5..e695b3e086138fe9170814e8953af2e8a6467495 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -71,7 +71,7 @@ end
module Make_Generic_Lattice_Set
(V: Datatype.S)
- (Set: Lattice_type.Set with type elt = V.t)
+ (Set: Lattice_type.Hptset with type elt = V.t)
= struct
type t = Set of Set.t | Top
@@ -232,7 +232,7 @@ end
module Make_Lattice_Set
(V: Datatype.S)
- (Set: Lattice_type.Set with type elt = V.t)
+ (Set: Lattice_type.Hptset with type elt = V.t)
: Lattice_type.Lattice_Set with module O = Set
= struct
module O = Set
diff --git a/src/kernel_services/abstract_interp/abstract_interp.mli b/src/kernel_services/abstract_interp/abstract_interp.mli
index 7a666ccfe69b91161c6523f4c6b9acb78ca60fc2..a177f607b8021f6950aeb9049b1bcde5e1e2ecd6 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.mli
+++ b/src/kernel_services/abstract_interp/abstract_interp.mli
@@ -101,7 +101,7 @@ module Make_Lattice_Base (V : Lattice_Value) : Lattice_Base with type l = V.t
module Make_Lattice_Set
(V : Datatype.S)
- (Set: Lattice_type.Set with type elt = V.t)
+ (Set: Lattice_type.Hptset with type elt = V.t)
: Lattice_type.Lattice_Set with module O = Set
module Make_Hashconsed_Lattice_Set
diff --git a/src/kernel_services/abstract_interp/float_sig.mli b/src/kernel_services/abstract_interp/float_sig.mli
index 50ade7d97dafcc33d3c76ee39747a4e5192e07d4..0f6b76a7b0254c256750451763c5715c5d85cedd 100644
--- a/src/kernel_services/abstract_interp/float_sig.mli
+++ b/src/kernel_services/abstract_interp/float_sig.mli
@@ -32,9 +32,7 @@ type prec = Single | Double | Long_Double | Real
module type Widen_Hints = sig
- include FCSet.S with type elt = Cil_datatype.Logic_real.t
- include Datatype.S with type t:=t
-
+ include module type of Cil_datatype.Logic_real.Set
val default_widen_hints: t
end
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 5ccb3eafff9a23c325c18b0498a21f0e22316cbc..469c299c6869f8b3f99a348a9de90eb360345fa5 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -77,7 +77,7 @@ let inject_periodic ~from ~period ~number =
done;
s
-module O = FCSet.Make (Integer)
+module O = Set.Make (Integer)
let inject_list list =
let o = List.fold_left (fun o r -> O.add r o) O.empty list in
diff --git a/src/kernel_services/abstract_interp/lattice_type.mli b/src/kernel_services/abstract_interp/lattice_type.mli
index 3bcc722d23a98f8633a211d3204fab2056e8c010..90d42d2c82a8f9c91a0c8b3aeedb541bc4688de5 100644
--- a/src/kernel_services/abstract_interp/lattice_type.mli
+++ b/src/kernel_services/abstract_interp/lattice_type.mli
@@ -205,8 +205,8 @@ module type Lattice_Base = sig
val transform: (l -> l -> l) -> t -> t -> t
end
-module type Set = sig
- include FCSet.S_Basic_Compare
+module type Hptset = sig
+ include Hptset.S_Basic_Compare
include Datatype.S with type t := t
end
@@ -214,7 +214,7 @@ end
(see {!Abstract_interp.Make_Lattice_Set} or
{!Abstract_interp.Make_Hashconsed_Lattice_Set}). *)
module type Lattice_Set = sig
- module O: Set
+ module O: Hptset
type t = private Set of O.t | Top
include AI_Lattice_with_cardinal_one
with type t := t
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 4d6d1f1947fb83609de10366967b6033935956e5..08b217e0cc326183800bd3c00694e7c0eb695e18 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3604,7 +3604,7 @@ struct
(* This module is used to sort the list of behaviors in [complete] and
[disjoint] clauses, in order to remove duplicate clauses. *)
module StringListSet =
- FCSet.Make(
+ Set.Make(
struct
type t = string list
let compare s1 s2 =
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index cddbeb78d57ad4635ca5f6bfbe4a70b817cbaabc..a9b4e22ea1c8053c2506b72d19f5b8193f4c41d4 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -289,7 +289,9 @@ module Make(X: Make_input) = struct
end
module type Set = sig
- include FCSet.S
+ include Set.S
+ val nearest_elt_le: elt -> t -> elt
+ val nearest_elt_ge: elt -> t -> elt
include S with type t := t
end
@@ -1342,7 +1344,7 @@ module type Functor_info = sig val module_name: string end
(* OCaml functors are generative *)
module Set
- (S: FCSet.S)(E: S with type t = S.elt)(Info: Functor_info) =
+ (S: Set.S)(E: S with type t = S.elt)(Info: Functor_info) =
struct
let () = check E.equal "equal" E.name Info.module_name
@@ -1409,6 +1411,9 @@ struct
end)
include S
+ let nearest_elt_le x = S.find_last (fun y -> y <= x)
+ let nearest_elt_ge x = S.find_first (fun y -> y >= x)
+
let () = Type.set_ml_name P.ty (Some (Info.module_name ^ ".ty"))
let ty = P.ty
@@ -1671,7 +1676,7 @@ module With_collections(X: S)(Info: Functor_info) = struct
module Set =
Set
- (FCSet.Make(D))
+ (Transitioning.Stdlib.Set.Make(D))
(D)
(struct let module_name = Info.module_name ^ ".Set" end)
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index bf25151f44c53f0cadbf0458289c484871a9f1d7..19f4677cfc880e668466fe398bce46205b5967ed 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -233,7 +233,9 @@ end
(** A standard OCaml set signature extended with datatype operations. *)
module type Set = sig
- include FCSet.S
+ include Set.S
+ val nearest_elt_le: elt -> t -> elt
+ val nearest_elt_ge: elt -> t -> elt
include S with type t := t
end
@@ -634,7 +636,7 @@ val func4:
('a -> 'b -> 'c -> 'd -> 'e) Type.t
module Set
- (S: FCSet.S)(E: S with type t = S.elt)(Info : Functor_info):
+ (S: Set.S)(E: S with type t = S.elt)(Info : Functor_info):
Set with type t = S.t and type elt = E.t
module Map
diff --git a/src/libraries/stdlib/FCBuffer.ml b/src/libraries/stdlib/FCBuffer.ml
deleted file mode 100644
index 0f318b01de4e6b06a20ff1626bee846978bb059b..0000000000000000000000000000000000000000
--- a/src/libraries/stdlib/FCBuffer.ml
+++ /dev/null
@@ -1,255 +0,0 @@
-(*****************************************************************************)
-(* *)
-(* This file was originally part of Objective Caml *)
-(* *)
-(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
-(* *)
-(* Copyright (C) 1996 INRIA *)
-(* INRIA (Institut National de Recherche en Informatique et en *)
-(* Automatique) *)
-(* *)
-(* All rights reserved. *)
-(* *)
-(* This file is distributed under the terms of the GNU Library General *)
-(* Public License version 2, with the special exception on linking *)
-(* described below. See the GNU Library General Public License version *)
-(* 2 for more details (enclosed in the file licenses/LGPLv2). *)
-(* *)
-(* As a special exception to the GNU Library General Public License, *)
-(* you may link, statically or dynamically, a "work that uses the Library" *)
-(* with a publicly distributed version of the Library to *)
-(* produce an executable file containing portions of the Library, and *)
-(* distribute that executable file under terms of your choice, without *)
-(* any of the additional requirements listed in clause 6 of the GNU *)
-(* Library General Public License. *)
-(* By "a publicly distributed version of the Library", *)
-(* we mean either the unmodified Library as *)
-(* distributed by INRIA, or a modified version of the Library that is *)
-(* distributed under the conditions defined in clause 2 of the GNU *)
-(* Library General Public License. This exception does not however *)
-(* invalidate any other reasons why the executable file might be *)
-(* covered by the GNU Library General Public License. *)
-(* *)
-(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
-(* énergies alternatives). *)
-(* *)
-(*****************************************************************************)
-
-(* Extensible buffers *)
-
-type t =
- {mutable buffer : bytes;
- mutable position : int;
- mutable length : int;
- initial_buffer : bytes}
-
-let create n =
- let n = if n < 1 then 1 else n in
- let n = if n > Sys.max_string_length then Sys.max_string_length else n in
- let s = Bytes.create n in
- {buffer = s; position = 0; length = n; initial_buffer = s}
-
-let contents b = Bytes.sub_string b.buffer 0 b.position
-let to_bytes b = Bytes.sub b.buffer 0 b.position
-
-let sub b ofs len =
- if ofs < 0 || len < 0 || ofs > b.position - len
- then invalid_arg "Buffer.sub"
- else Bytes.sub_string b.buffer ofs len
-;;
-
-let sub_bytes b ofs len =
- if ofs < 0 || len < 0 || ofs > b.position - len
- then invalid_arg "Buffer.sub_bytes"
- else Bytes.sub b.buffer ofs len
-;;
-
-let blit src srcoff dst dstoff len =
- if len < 0 || srcoff < 0 || srcoff > src.position - len
- || dstoff < 0 || dstoff > (Bytes.length dst) - len
- then invalid_arg "Buffer.blit"
- else
- Bytes.unsafe_blit src.buffer srcoff dst dstoff len
-;;
-
-(* [calc_size cur_len req_len] computes the new size for a buffer having
- [cur_len] bytes, to ensure that it can contain at least [req_len] bytes.
- Used by [add_*] and [blit_*] functions.
- Raise [Failure] if the new size is too large. *)
-let calc_size cur_len req_len =
- let new_len = ref cur_len in
- while req_len > !new_len do new_len := 2 * !new_len done;
- if !new_len > Sys.max_string_length then begin
- if req_len <= Sys.max_string_length
- then new_len := Sys.max_string_length
- else failwith "Buffer.add: cannot grow buffer"
- end;
- !new_len
-
-(* [resize_aux b len] resizes buffer [b] to ensure it may contain at least
- [len] bytes. *)
-let resize_aux b len =
- let new_len = calc_size b.length len in
- let new_buffer = Bytes.create new_len in
- b.buffer <- new_buffer;
- b.length <- new_len
-
-let resize b len =
- let old_buffer = b.buffer in
- resize_aux b len;
- (* PR#6148: let's keep using [blit] rather than [unsafe_blit] in
- this tricky function that is slow anyway. *)
- Bytes.blit old_buffer 0 b.buffer 0 b.position
-
-let blit_substring_aux src srclen srcoff dst dstoff len =
- if len < 0 || srcoff < 0 || srcoff > srclen - len
- || dstoff < 0 || dstoff > dst.position
- then invalid_arg "Buffer.blit_*/add_*"
- else
- let new_pos = dstoff + len in
- let new_len = calc_size dst.length new_pos in
- if new_len > dst.length then begin
- let old_buffer = dst.buffer in
- resize_aux dst new_len; (* dst points to a new buffer now *)
- Bytes.blit old_buffer 0 dst.buffer 0 dstoff;
- Bytes.blit_string src srcoff dst.buffer dstoff len;
- end
- else Bytes.blit_string src srcoff dst.buffer dstoff len;
- if new_pos > dst.position then dst.position <- new_pos
-;;
-
-let blit_buffer src srcoff dst dstoff len =
- blit_substring_aux (Bytes.unsafe_to_string src.buffer) src.position srcoff dst dstoff len
-
-let blit_substring src srcoff dst dstoff len =
- blit_substring_aux src (String.length src) srcoff dst dstoff len
-
-let blit_subbytes src srcoff dst dstoff len =
- blit_substring_aux (Bytes.unsafe_to_string src) (Bytes.length src) srcoff dst dstoff len
-
-let nth b ofs =
- if ofs < 0 || ofs >= b.position then
- invalid_arg "Buffer.nth"
- else Bytes.unsafe_get b.buffer ofs
-;;
-
-let length b = b.position
-
-let clear b = b.position <- 0
-
-let reset b =
- b.position <- 0; b.buffer <- b.initial_buffer;
- b.length <- Bytes.length b.buffer
-
-let truncate b c =
- if c < 0 then invalid_arg "Buffer.truncate"
- else if b.position > c then b.position <- c
-
-let add_char b c =
- let pos = b.position in
- if pos >= b.length then resize b (pos + 1);
- Bytes.unsafe_set b.buffer pos c;
- b.position <- pos + 1
-
-let add_substring b s offset len =
- if offset < 0 || len < 0 || offset + len > String.length s
- then invalid_arg "Buffer.add_substring/add_subbytes";
- blit_substring_aux s (String.length s) offset b b.position len
-
-let add_subbytes b s offset len =
- add_substring b (Bytes.unsafe_to_string s) offset len
-
-let add_string b s =
- let len = String.length s in
- blit_substring_aux s len 0 b b.position len
-
-let add_bytes b s = add_string b (Bytes.unsafe_to_string s)
-
-let add_buffer b bs =
- add_subbytes b bs.buffer 0 bs.position
-
-(* read up to [len] bytes from [ic] into [b]. *)
-let rec add_channel_rec b ic len =
- if len > 0 then (
- let n = input ic b.buffer b.position len in
- b.position <- b.position + n;
- if n = 0 then raise End_of_file
- else add_channel_rec b ic (len-n) (* n <= len *)
- )
-
-let add_channel b ic len =
- if len < 0 || len > Sys.max_string_length then (* PR#5004 *)
- invalid_arg "Buffer.add_channel";
- if b.position + len > b.length then resize b (b.position + len);
- add_channel_rec b ic len
-
-let output_buffer oc b =
- output oc b.buffer 0 b.position
-
-let closing = function
- | '(' -> ')'
- | '{' -> '}'
- | _ -> assert false;;
-
-(* opening and closing: open and close characters, typically ( and )
- k: balance of opening and closing chars
- s: the string where we are searching
- start: the index where we start the search. *)
-let advance_to_closing opening closing k s start =
- let rec advance k i lim =
- if i >= lim then raise Not_found else
- if s.[i] = opening then advance (k + 1) (i + 1) lim else
- if s.[i] = closing then
- if k = 0 then i else advance (k - 1) (i + 1) lim
- else advance k (i + 1) lim in
- advance k start (String.length s);;
-
-let advance_to_non_alpha s start =
- let rec advance i lim =
- if i >= lim then lim else
- match s.[i] with
- | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> advance (i + 1) lim
- | _ -> i in
- advance start (String.length s);;
-
-(* We are just at the beginning of an ident in s, starting at start. *)
-let find_ident s start lim =
- if start >= lim then raise Not_found else
- match s.[start] with
- (* Parenthesized ident ? *)
- | '(' | '{' as c ->
- let new_start = start + 1 in
- let stop = advance_to_closing c (closing c) 0 s new_start in
- String.sub s new_start (stop - start - 1), stop + 1
- (* Regular ident *)
- | _ ->
- let stop = advance_to_non_alpha s (start + 1) in
- String.sub s start (stop - start), stop;;
-
-(* Substitute $ident, $(ident), or ${ident} in s,
- according to the function mapping f. *)
-let add_substitute b f s =
- let lim = String.length s in
- let rec subst previous i =
- if i < lim then begin
- match s.[i] with
- | '$' as current when previous = '\\' ->
- add_char b current;
- subst ' ' (i + 1)
- | '$' ->
- let j = i + 1 in
- let ident, next_i = find_ident s j lim in
- add_string b (f ident);
- subst ' ' next_i
- | current when previous == '\\' ->
- add_char b '\\';
- add_char b current;
- subst ' ' (i + 1)
- | '\\' as current ->
- subst current (i + 1)
- | current ->
- add_char b current;
- subst current (i + 1)
- end else
- if previous = '\\' then add_char b previous in
- subst ' ' 0;;
diff --git a/src/libraries/stdlib/FCBuffer.mli b/src/libraries/stdlib/FCBuffer.mli
deleted file mode 100644
index c4962e919ef86b3f7948659a722720496a9b1872..0000000000000000000000000000000000000000
--- a/src/libraries/stdlib/FCBuffer.mli
+++ /dev/null
@@ -1,180 +0,0 @@
-(*****************************************************************************)
-(* *)
-(* This file was originally part of Objective Caml *)
-(* *)
-(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
-(* *)
-(* Copyright (C) 1996 INRIA *)
-(* INRIA (Institut National de Recherche en Informatique et en *)
-(* Automatique) *)
-(* *)
-(* All rights reserved. *)
-(* *)
-(* This file is distributed under the terms of the GNU Library General *)
-(* Public License version 2, with the special exception on linking *)
-(* described below. See the GNU Library General Public License version *)
-(* 2 for more details (enclosed in the file licenses/LGPLv2). *)
-(* *)
-(* As a special exception to the GNU Library General Public License, *)
-(* you may link, statically or dynamically, a "work that uses the Library" *)
-(* with a publicly distributed version of the Library to *)
-(* produce an executable file containing portions of the Library, and *)
-(* distribute that executable file under terms of your choice, without *)
-(* any of the additional requirements listed in clause 6 of the GNU *)
-(* Library General Public License. *)
-(* By "a publicly distributed version of the Library", *)
-(* we mean either the unmodified Library as *)
-(* distributed by INRIA, or a modified version of the Library that is *)
-(* distributed under the conditions defined in clause 2 of the GNU *)
-(* Library General Public License. This exception does not however *)
-(* invalidate any other reasons why the executable file might be *)
-(* covered by the GNU Library General Public License. *)
-(* *)
-(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
-(* énergies alternatives). *)
-(* *)
-(*****************************************************************************)
-
-(** Extensible buffers.
-
- This module implements buffers that automatically expand
- as necessary. It provides accumulative concatenation of strings
- in quasi-linear time (instead of quadratic time when strings are
- concatenated pairwise).
-*)
-
-type t
-(** The abstract type of buffers. *)
-
-val create : int -> t
-(** [create n] returns a fresh buffer, initially empty.
- The [n] parameter is the initial size of the internal byte sequence
- that holds the buffer contents. That byte sequence is automatically
- reallocated when more than [n] characters are stored in the buffer,
- but shrinks back to [n] characters when [reset] is called.
- For best performance, [n] should be of the same order of magnitude
- as the number of characters that are expected to be stored in
- the buffer (for instance, 80 for a buffer that holds one output
- line). Nothing bad will happen if the buffer grows beyond that
- limit, however. In doubt, take [n = 16] for instance.
- If [n] is not between 1 and {!Sys.max_string_length}, it will
- be clipped to that interval. *)
-
-val contents : t -> string
-(** Return a copy of the current contents of the buffer.
- The buffer itself is unchanged. *)
-
-val to_bytes : t -> bytes
-(** Return a copy of the current contents of the buffer.
- The buffer itself is unchanged.
- @since 4.02 *)
-
-val sub : t -> int -> int -> string
-(** [Buffer.sub b off len] returns (a copy of) the bytes from the
- current contents of the buffer [b] starting at offset [off] of
- length [len] bytes. May raise [Invalid_argument] if out of bounds
- request. The buffer itself is unaffected. *)
-
-val sub_bytes : t -> int -> int -> bytes
-(** Same as [sub] but return a byte sequence instead of a string.
- @since 4.05 *)
-
-val blit : t -> int -> bytes -> int -> int -> unit
-(** [Buffer.blit src srcoff dst dstoff len] copies [len] characters from
- the current contents of the buffer [src], starting at offset [srcoff]
- to [dst], starting at character [dstoff].
-
- Raise [Invalid_argument] if [srcoff] and [len] do not designate a valid
- range of [src], or if [dstoff] and [len] do not designate a valid
- range of [dst].
- @since 3.11.2
-*)
-
-val blit_buffer : t -> int -> t -> int -> int -> unit
-(** Similar to [blit], but copies to a buffer, and allows the destination
- buffer to grow, that is, [dstoff + len] can be larger than the length of
- [dst]. However, there cannot be any holes, i.e. [dstoff] must be smaller
- than the original length of [dst].
- @since 4.05 *)
-
-val blit_substring : string -> int -> t -> int -> int -> unit
-(** Same as [blit_buffer], but copies from a string to a buffer.
- @since 4.05 *)
-
-val blit_subbytes : bytes -> int -> t -> int -> int -> unit
-(** Same as [blit_buffer], but copies from bytes to a buffer.
- @since 4.05 *)
-
-val nth : t -> int -> char
-(** get the n-th character of the buffer. Raise [Invalid_argument] if
- index out of bounds *)
-
-val length : t -> int
-(** Return the number of characters currently contained in the buffer. *)
-
-val clear : t -> unit
-(** Empty the buffer. *)
-
-val reset : t -> unit
-(** Empty the buffer and deallocate the internal byte sequence holding the
- buffer contents, replacing it with the initial internal byte sequence
- of length [n] that was allocated by {!Buffer.create} [n].
- For long-lived buffers that may have grown a lot, [reset] allows
- faster reclamation of the space used by the buffer. *)
-
-val truncate : t -> int -> unit
-(** [truncate b c] truncates the length of [b] to be no larger than [c].
- Does nothing if the length of [b] is already smaller than or equal [c].
- In particular, it does not change the size of the underlying buffer.
- Raise [Invalid_argument] if [c < 0].
- @since 4.05 *)
-
-val add_char : t -> char -> unit
-(** [add_char b c] appends the character [c] at the end of the buffer [b]. *)
-
-val add_string : t -> string -> unit
-(** [add_string b s] appends the string [s] at the end of the buffer [b]. *)
-
-val add_bytes : t -> bytes -> unit
-(** [add_string b s] appends the string [s] at the end of the buffer [b].
- @since 4.02 *)
-
-val add_substring : t -> string -> int -> int -> unit
-(** [add_substring b s ofs len] takes [len] characters from offset
- [ofs] in string [s] and appends them at the end of the buffer [b]. *)
-
-val add_subbytes : t -> bytes -> int -> int -> unit
-(** [add_substring b s ofs len] takes [len] characters from offset
- [ofs] in byte sequence [s] and appends them at the end of the buffer [b].
- @since 4.02 *)
-
-val add_substitute : t -> (string -> string) -> string -> unit
-(** [add_substitute b f s] appends the string pattern [s] at the end
- of the buffer [b] with substitution.
- The substitution process looks for variables into
- the pattern and substitutes each variable name by its value, as
- obtained by applying the mapping [f] to the variable name. Inside the
- string pattern, a variable name immediately follows a non-escaped
- [$] character and is one of the following:
- - a non empty sequence of alphanumeric or [_] characters,
- - an arbitrary sequence of characters enclosed by a pair of
- matching parentheses or curly brackets.
- An escaped [$] character is a [$] that immediately follows a backslash
- character; it then stands for a plain [$].
- Raise [Not_found] if the closing character of a parenthesized variable
- cannot be found. *)
-
-val add_buffer : t -> t -> unit
-(** [add_buffer b1 b2] appends the current contents of buffer [b2]
- at the end of buffer [b1]. [b2] is not modified. *)
-
-val add_channel : t -> in_channel -> int -> unit
-(** [add_channel b ic n] reads at most [n] characters from the
- input channel [ic] and stores them at the end of buffer [b].
- Raise [End_of_file] if the channel contains fewer than [n]
- characters. In this case the characters are still added to
- the buffer, so as to avoid loss of data. *)
-
-val output_buffer : out_channel -> t -> unit
-(** [output_buffer oc b] writes the current contents of buffer [b]
- on the output channel [oc]. *)
diff --git a/src/libraries/stdlib/FCHashtbl.ml b/src/libraries/stdlib/FCHashtbl.ml
index 00a6463e5da064ec4ad1442978392e5057b8c527..7ee17dd6613813b067ffd62e843c882c1870ad73 100644
--- a/src/libraries/stdlib/FCHashtbl.ml
+++ b/src/libraries/stdlib/FCHashtbl.ml
@@ -70,7 +70,7 @@ module Make(H: Hashtbl.HashedType) : S with type key = H.t = struct
let fold_sorted_by_entry (type value) ~cmp f h acc =
let module Aux = struct type t = (key*value) let compare = cmp end in
- let module S = FCSet.Make(Aux) in
+ let module S = Set.Make(Aux) in
let add k v s = S.add (k,v) s in
let set = fold add h S.empty in
S.fold (fun (k,v) -> f k v) set acc
diff --git a/src/libraries/stdlib/FCSet.ml b/src/libraries/stdlib/FCSet.ml
deleted file mode 100644
index 999ab385bb6d95ec6ce4f6d932476bbee9adabdf..0000000000000000000000000000000000000000
--- a/src/libraries/stdlib/FCSet.ml
+++ /dev/null
@@ -1,473 +0,0 @@
-(*****************************************************************************)
-(* *)
-(* This file was originally part of Objective Caml *)
-(* *)
-(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
-(* *)
-(* Copyright (C) 1996 INRIA *)
-(* INRIA (Institut National de Recherche en Informatique et en *)
-(* Automatique) *)
-(* *)
-(* All rights reserved. *)
-(* *)
-(* This file is distributed under the terms of the GNU Library General *)
-(* Public License version 2, with the special exception on linking *)
-(* described below. See the GNU Library General Public License version *)
-(* 2 for more details (enclosed in the file licenses/LGPLv2). *)
-(* *)
-(* As a special exception to the GNU Library General Public License, *)
-(* you may link, statically or dynamically, a "work that uses the Library" *)
-(* with a publicly distributed version of the Library to *)
-(* produce an executable file containing portions of the Library, and *)
-(* distribute that executable file under terms of your choice, without *)
-(* any of the additional requirements listed in clause 6 of the GNU *)
-(* Library General Public License. *)
-(* By "a publicly distributed version of the Library", *)
-(* we mean either the unmodified Library as *)
-(* distributed by INRIA, or a modified version of the Library that is *)
-(* distributed under the conditions defined in clause 2 of the GNU *)
-(* Library General Public License. This exception does not however *)
-(* invalidate any other reasons why the executable file might be *)
-(* covered by the GNU Library General Public License. *)
-(* *)
-(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
-(* énergies alternatives). *)
-(* *)
-(*****************************************************************************)
-
-module type S_Basic_Compare =
- sig
- type elt
- type t
- val empty: t
- val is_empty: t -> bool
- val mem: elt -> t -> bool
- val add: elt -> t -> t
- val singleton: elt -> t
- val remove: elt -> t -> t
- val union: t -> t -> t
- val inter: t -> t -> t
- val diff: t -> t -> t
- val compare: t -> t -> int
- val equal: t -> t -> bool
- val subset: t -> t -> bool
- val iter: (elt -> unit) -> t -> unit
- val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
- val for_all: (elt -> bool) -> t -> bool
- val exists: (elt -> bool) -> t -> bool
- val filter: (elt -> bool) -> t -> t
- val partition: (elt -> bool) -> t -> t * t
- val cardinal: t -> int
- val elements: t -> elt list
- val choose: t -> elt
- val find: elt -> t -> elt
- val of_list: elt list -> t
- end
-
-module type S =
- sig
- include S_Basic_Compare
- val min_elt: t -> elt
- val max_elt: t -> elt
- val split: elt -> t -> t * bool * t
- val nearest_elt_le: elt -> t -> elt
- val nearest_elt_ge: elt -> t -> elt
- end
-
-module Make(Ord: Set.OrderedType) =
- struct
- type elt = Ord.t
- type t = Empty | Node of t * elt * t * int
-
- (* Sets are represented by balanced binary trees (the heights of the
- children differ by at most 2 *)
-
- let height = function
- Empty -> 0
- | Node(_, _, _, h) -> h
-
- (* Creates a new node with left son l, value v and right son r.
- We must have all elements of l < v < all elements of r.
- l and r must be balanced and | height l - height r | <= 2.
- Inline expansion of height for better speed. *)
-
- let create l v r =
- let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
- let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
- Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))
-
- (* Same as create, but performs one step of rebalancing if necessary.
- Assumes l and r balanced and | height l - height r | <= 3.
- Inline expansion of create for better speed in the most frequent case
- where no rebalancing is required. *)
-
- let bal l v r =
- let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
- let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
- if hl > hr + 2 then begin
- match l with
- Empty -> invalid_arg "Set.bal"
- | Node(ll, lv, lr, _) ->
- if height ll >= height lr then
- create ll lv (create lr v r)
- else begin
- match lr with
- Empty -> invalid_arg "Set.bal"
- | Node(lrl, lrv, lrr, _)->
- create (create ll lv lrl) lrv (create lrr v r)
- end
- end else if hr > hl + 2 then begin
- match r with
- Empty -> invalid_arg "Set.bal"
- | Node(rl, rv, rr, _) ->
- if height rr >= height rl then
- create (create l v rl) rv rr
- else begin
- match rl with
- Empty -> invalid_arg "Set.bal"
- | Node(rll, rlv, rlr, _) ->
- create (create l v rll) rlv (create rlr rv rr)
- end
- end else
- Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))
-
- (* Insertion of one element *)
-
- let rec add x = function
- Empty -> Node(Empty, x, Empty, 1)
- | Node(l, v, r, _) as t ->
- let c = Ord.compare x v in
- if c = 0 then t else
- if c < 0 then bal (add x l) v r else bal l v (add x r)
-
- let singleton x = Node(Empty, x, Empty, 1)
-
- (* Beware: those two functions assume that the added v is *strictly*
- smaller (or bigger) than all the present elements in the tree; it
- does not test for equality with the current min (or max) element.
- Indeed, they are only used during the "join" operation which
- respects this precondition.
- *)
-
- let rec add_min_element v = function
- | Empty -> singleton v
- | Node (l, x, r, _) ->
- bal (add_min_element v l) x r
-
- let rec add_max_element v = function
- | Empty -> singleton v
- | Node (l, x, r, _) ->
- bal l x (add_max_element v r)
-
- (* Same as create and bal, but no assumptions are made on the
- relative heights of l and r. *)
-
- let rec join l v r =
- match (l, r) with
- (Empty, _) -> add_min_element v r
- | (_, Empty) -> add_max_element v l
- | (Node(ll, lv, lr, lh), Node(rl, rv, rr, rh)) ->
- if lh > rh + 2 then bal ll lv (join lr v r) else
- if rh > lh + 2 then bal (join l v rl) rv rr else
- create l v r
-
- (* Smallest and greatest element of a set *)
-
- let rec min_elt = function
- Empty -> raise Not_found
- | Node(Empty, v, _, _) -> v
- | Node(l, _, _, _) -> min_elt l
-
- let rec max_elt = function
- Empty -> raise Not_found
- | Node(_, v, Empty, _) -> v
- | Node(_, _, r, _) -> max_elt r
-
- (* Remove the smallest element of the given set *)
-
- let rec remove_min_elt = function
- Empty -> invalid_arg "Set.remove_min_elt"
- | Node(Empty, _, r, _) -> r
- | Node(l, v, r, _) -> bal (remove_min_elt l) v r
-
- (* Merge two trees l and r into one.
- All elements of l must precede the elements of r.
- Assume | height l - height r | <= 2. *)
-
- let merge t1 t2 =
- match (t1, t2) with
- (Empty, t) -> t
- | (t, Empty) -> t
- | (_, _) -> bal t1 (min_elt t2) (remove_min_elt t2)
-
- (* Merge two trees l and r into one.
- All elements of l must precede the elements of r.
- No assumption on the heights of l and r. *)
-
- let concat t1 t2 =
- match (t1, t2) with
- (Empty, t) -> t
- | (t, Empty) -> t
- | (_, _) -> join t1 (min_elt t2) (remove_min_elt t2)
-
- (* Splitting. split x s returns a triple (l, present, r) where
- - l is the set of elements of s that are < x
- - r is the set of elements of s that are > x
- - present is false if s contains no element equal to x,
- or true if s contains an element equal to x. *)
-
- let rec split x = function
- Empty ->
- (Empty, false, Empty)
- | Node(l, v, r, _) ->
- let c = Ord.compare x v in
- if c = 0 then (l, true, r)
- else if c < 0 then
- let (ll, pres, rl) = split x l in (ll, pres, join rl v r)
- else
- let (lr, pres, rr) = split x r in (join l v lr, pres, rr)
-
- (* Implementation of the set operations *)
-
- let empty = Empty
-
- let is_empty = function Empty -> true | _ -> false
-
- let rec mem x = function
- Empty -> false
- | Node(l, v, r, _) ->
- let c = Ord.compare x v in
- c = 0 || mem x (if c < 0 then l else r)
-
- let rec remove x = function
- Empty -> Empty
- | Node(l, v, r, _) ->
- let c = Ord.compare x v in
- if c = 0 then merge l r else
- if c < 0 then bal (remove x l) v r else bal l v (remove x r)
-
- let rec union s1 s2 =
- match (s1, s2) with
- (Empty, t2) -> t2
- | (t1, Empty) -> t1
- | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
- if h1 >= h2 then
- if h2 = 1 then add v2 s1 else begin
- let (l2, _, r2) = split v1 s2 in
- join (union l1 l2) v1 (union r1 r2)
- end
- else
- if h1 = 1 then add v1 s2 else begin
- let (l1, _, r1) = split v2 s1 in
- join (union l1 l2) v2 (union r1 r2)
- end
-
- let rec inter s1 s2 =
- match (s1, s2) with
- (Empty, _) -> Empty
- | (_, Empty) -> Empty
- | (Node(l1, v1, r1, _), t2) ->
- match split v1 t2 with
- (l2, false, r2) ->
- concat (inter l1 l2) (inter r1 r2)
- | (l2, true, r2) ->
- join (inter l1 l2) v1 (inter r1 r2)
-
- let rec diff s1 s2 =
- match (s1, s2) with
- (Empty, _) -> Empty
- | (t1, Empty) -> t1
- | (Node(l1, v1, r1, _), t2) ->
- match split v1 t2 with
- (l2, false, r2) ->
- join (diff l1 l2) v1 (diff r1 r2)
- | (l2, true, r2) ->
- concat (diff l1 l2) (diff r1 r2)
-
- type enumeration = End | More of elt * t * enumeration
-
- let rec cons_enum s e =
- match s with
- Empty -> e
- | Node(l, v, r, _) -> cons_enum l (More(v, r, e))
-
- let rec compare_aux e1 e2 =
- match (e1, e2) with
- (End, End) -> 0
- | (End, _) -> -1
- | (_, End) -> 1
- | (More(v1, r1, e1), More(v2, r2, e2)) ->
- let c = Ord.compare v1 v2 in
- if c <> 0
- then c
- else compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
-
- let compare s1 s2 =
- compare_aux (cons_enum s1 End) (cons_enum s2 End)
-
- let equal s1 s2 =
- compare s1 s2 = 0
-
- let rec subset s1 s2 =
- match (s1, s2) with
- Empty, _ ->
- true
- | _, Empty ->
- false
- | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) ->
- let c = Ord.compare v1 v2 in
- if c = 0 then
- subset l1 l2 && subset r1 r2
- else if c < 0 then
- subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2
- else
- subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2
-
- let rec iter f = function
- Empty -> ()
- | Node(l, v, r, _) -> iter f l; f v; iter f r
-
- let rec fold f s accu =
- match s with
- Empty -> accu
- | Node(l, v, r, _) -> fold f r (f v (fold f l accu))
-
- let rec for_all p = function
- Empty -> true
- | Node(l, v, r, _) -> p v && for_all p l && for_all p r
-
- let rec exists p = function
- Empty -> false
- | Node(l, v, r, _) -> p v || exists p l || exists p r
-
- let rec filter p = function
- Empty -> Empty
- | Node(l, v, r, _) ->
- (* call [p] in the expected left-to-right order *)
- let l' = filter p l in
- let pv = p v in
- let r' = filter p r in
- if pv then join l' v r' else concat l' r'
-
- let rec partition p = function
- Empty -> (Empty, Empty)
- | Node(l, v, r, _) ->
- (* call [p] in the expected left-to-right order *)
- let (lt, lf) = partition p l in
- let pv = p v in
- let (rt, rf) = partition p r in
- if pv
- then (join lt v rt, concat lf rf)
- else (concat lt rt, join lf v rf)
-
- let rec cardinal = function
- Empty -> 0
- | Node(l, _, r, _) -> cardinal l + 1 + cardinal r
-
- let rec elements_aux accu = function
- Empty -> accu
- | Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l
-
- let elements s =
- elements_aux [] s
-
- let choose = min_elt
-
- let rec find x = function
- Empty -> raise Not_found
- | Node(l, v, r, _) ->
- let c = Ord.compare x v in
- if c = 0 then v
- else find x (if c < 0 then l else r)
-
- (* Auxiliary function for function {!of_list} below *)
- let sort_unique l =
- let l = List.sort Ord.compare l in
- let rec remove_duplicates l =
- match l with
- | [_] | [] -> l
- | e1 :: (e2 :: _ as q) ->
- if Ord.compare e1 e2 = 0 then
- remove_duplicates q
- else
- let q' = remove_duplicates q in
- if q' == q then l else e1 :: q'
- in
- remove_duplicates l
-
- let of_sorted_list l =
- let rec sub n l =
- match n, l with
- | 0, l -> Empty, l
- | 1, x0 :: l -> Node (Empty, x0, Empty, 1), l
- | 2, x0 :: x1 :: l -> Node (Node(Empty, x0, Empty, 1), x1, Empty, 2), l
- | 3, x0 :: x1 :: x2 :: l ->
- Node (Node(Empty, x0, Empty, 1), x1, Node(Empty, x2, Empty, 1), 2), l
- | n, l ->
- let nl = n / 2 in
- let left, l = sub nl l in
- match l with
- | [] -> assert false
- | mid :: l ->
- let right, l = sub (n - nl - 1) l in
- create left mid right, l
- in
- fst (sub (List.length l) l)
-
- let of_list l =
- match l with
- | [] -> empty
- | [x0] -> singleton x0
- | [x0; x1] -> add x1 (singleton x0)
- | [x0; x1; x2] -> add x2 (add x1 (singleton x0))
- | [x0; x1; x2; x3] -> add x3 (add x2 (add x1 (singleton x0)))
- | [x0; x1; x2; x3; x4] -> add x4 (add x3 (add x2 (add x1 (singleton x0))))
- | _ -> of_sorted_list (sort_unique l)
-
- let rec nearest_elt_le x = function
- | Empty ->
- raise Not_found
- | Node(l, v, r, _) ->
- let c = Ord.compare x v in
- if c = 0 then v
- else if c < 0 then
- nearest_elt_le x l
- else
- let rec nearest w x = function
- Empty -> w
- | Node(l, v, r, _) ->
- let c = Ord.compare x v in
- if c = 0 then v
- else if c < 0 then
- nearest w x l
- else
- nearest v x r
- in nearest v x r
-
- let rec nearest_elt_ge x = function
- | Empty ->
- raise Not_found
- | Node(l, v, r, _) ->
- let c = Ord.compare x v in
- if c = 0 then v
- else if c < 0 then
- let rec nearest w x = function
- Empty -> w
- | Node(l, v, r, _) ->
- let c = Ord.compare x v in
- if c = 0 then v
- else if c < 0 then
- nearest v x l
- else
- nearest w x r
- in nearest v x l
- else
- nearest_elt_ge x r
-
- end
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/libraries/stdlib/FCSet.mli b/src/libraries/stdlib/FCSet.mli
deleted file mode 100644
index 30bd963cd1d1aebc318c5f7b659a0301fb420acd..0000000000000000000000000000000000000000
--- a/src/libraries/stdlib/FCSet.mli
+++ /dev/null
@@ -1,202 +0,0 @@
-(*****************************************************************************)
-(* *)
-(* This file was originally part of Objective Caml *)
-(* *)
-(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
-(* *)
-(* Copyright (C) 1996 INRIA *)
-(* INRIA (Institut National de Recherche en Informatique et en *)
-(* Automatique) *)
-(* *)
-(* All rights reserved. *)
-(* *)
-(* This file is distributed under the terms of the GNU Library General *)
-(* Public License version 2, with the special exception on linking *)
-(* described below. See the GNU Library General Public License version *)
-(* 2 for more details (enclosed in the file licenses/LGPLv2). *)
-(* *)
-(* As a special exception to the GNU Library General Public License, *)
-(* you may link, statically or dynamically, a "work that uses the Library" *)
-(* with a publicly distributed version of the Library to *)
-(* produce an executable file containing portions of the Library, and *)
-(* distribute that executable file under terms of your choice, without *)
-(* any of the additional requirements listed in clause 6 of the GNU *)
-(* Library General Public License. *)
-(* By "a publicly distributed version of the Library", *)
-(* we mean either the unmodified Library as *)
-(* distributed by INRIA, or a modified version of the Library that is *)
-(* distributed under the conditions defined in clause 2 of the GNU *)
-(* Library General Public License. This exception does not however *)
-(* invalidate any other reasons why the executable file might be *)
-(* covered by the GNU Library General Public License. *)
-(* *)
-(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
-(* énergies alternatives). *)
-(* *)
-(*****************************************************************************)
-
-(** Sets over ordered types.
-
- This signatures is a partial copy of the signature of OCaml's [Set.S],
- which we extend with new operations. *)
-
-module type S_Basic_Compare =
- sig
- type elt
- (** The type of the set elements. *)
-
- type t
- (** The type of sets. *)
-
- val empty: t
- (** The empty set. *)
-
- val is_empty: t -> bool
- (** Test whether a set is empty or not. *)
-
- val mem: elt -> t -> bool
- (** [mem x s] tests whether [x] belongs to the set [s]. *)
-
- val add: elt -> t -> t
- (** [add x s] returns a set containing all elements of [s],
- plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
-
- val singleton: elt -> t
- (** [singleton x] returns the one-element set containing only [x]. *)
-
- val remove: elt -> t -> t
- (** [remove x s] returns a set containing all elements of [s],
- except [x]. If [x] was not in [s], [s] is returned unchanged. *)
-
- val union: t -> t -> t
- (** Set union. *)
-
- val inter: t -> t -> t
- (** Set intersection. *)
-
- (** Set difference. *)
- val diff: t -> t -> t
-
- val compare: t -> t -> int
- (** Total ordering between sets. Can be used as the ordering function
- for doing sets of sets. *)
-
- val equal: t -> t -> bool
- (** [equal s1 s2] tests whether the sets [s1] and [s2] are
- equal, that is, contain equal elements. *)
-
- val subset: t -> t -> bool
- (** [subset s1 s2] tests whether the set [s1] is a subset of
- the set [s2]. *)
-
- val iter: (elt -> unit) -> t -> unit
- (** [iter f s] applies [f] in turn to all elements of [s].
- The elements of [s] are presented to [f] in increasing order
- with respect to the ordering over the type of the elements. *)
-
- val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
- (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
- where [x1 ... xN] are the elements of [s], in increasing order. *)
-
- val for_all: (elt -> bool) -> t -> bool
- (** [for_all p s] checks if all elements of the set
- satisfy the predicate [p]. *)
-
- val exists: (elt -> bool) -> t -> bool
- (** [exists p s] checks if at least one element of
- the set satisfies the predicate [p]. *)
-
- val filter: (elt -> bool) -> t -> t
- (** [filter p s] returns the set of all elements in [s]
- that satisfy predicate [p]. *)
-
- val partition: (elt -> bool) -> t -> t * t
- (** [partition p s] returns a pair of sets [(s1, s2)], where
- [s1] is the set of all the elements of [s] that satisfy the
- predicate [p], and [s2] is the set of all the elements of
- [s] that do not satisfy [p]. *)
-
- val cardinal: t -> int
- (** Return the number of elements of a set. *)
-
- val elements: t -> elt list
- (** Return the list of all elements of the given set.
- The returned list is sorted in increasing order with respect
- to the ordering [Ord.compare], where [Ord] is the argument
- given to {!Set.Make}. *)
-
- val choose: t -> elt
- (** Return one element of the given set, or raise [Not_found] if
- the set is empty. Which element is chosen is unspecified,
- but equal elements will be chosen for equal sets. *)
-
- val find: elt -> t -> elt
- (** [find x s] returns the element of [s] equal to [x] (according
- to [Ord.compare]), or raise [Not_found] if no such element
- exists.
- @since 4.01.0 *)
-
- val of_list: elt list -> t
- (** [of_list l] creates a set from a list of elements.
- This is usually more efficient than folding [add] over the list,
- except perhaps for lists with many duplicated elements.
- @since 4.02.0 *)
-
- end
-(** Standard operations on sets. This signature does not assume any
- particular property on the [compare] function used to compare elements,
- except that it implements a total order. These are the functions that
- make sense for an usage of [Set] where only the algorithmic complexity is
- interesting to the user. *)
-
-module type S =
- sig
- include S_Basic_Compare
-
- val min_elt: t -> elt
- (** Return the smallest element of the given set
- (with respect to the [Ord.compare] ordering), or raise
- [Not_found] if the set is empty. *)
-
- val max_elt: t -> elt
- (** Same as {min_elt}, but returns the largest element of the
- given set. *)
-
- val split: elt -> t -> t * bool * t
- (** [split x s] returns a triple [(l, present, r)], where
- [l] is the set of elements of [s] that are
- strictly less than [x];
- [r] is the set of elements of [s] that are
- strictly greater than [x];
- [present] is [false] if [s] contains no element equal to [x],
- or [true] if [s] contains an element equal to [x]. *)
-
- (* Frama-C- additions *)
-
- val nearest_elt_le: elt -> t -> elt
- (** [nearest_elt_le v s] returns the largest element of [s] that is
- smaller or equal to [v].
- @raise Not_found if no such element exists. *)
-
- val nearest_elt_ge: elt -> t -> elt
- (** [nearest_elt_ge v s] returns the smallest element of [s] that is
- bigger or equal to [v].
- @raise Not_found if no such element exists. *)
-
- end
-(** Output signature of the functor {!FCSet.Make}.
-
- This signature add functions that assume that the [compare] function between
- elements implements a specific order. In this case, the layout of the
- tree might be interesting to the user.
-*)
-
-module Make (Ord : Set.OrderedType) : S with type elt = Ord.t
-(** Functor building an implementation of the set structure
- given a totally ordered type. *)
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index 8ceacaa401aecdcf0ef65311829266a1c525ecc7..5c42724fd50308e3e4b34b15f29d00b2cff225b6 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -30,6 +30,7 @@ module Stdlib = struct
let min_int = min_int
let max_int = max_int
let flush = flush
+ module Set = Set
module Map = Map
end
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index 5ae8e71271b63319184ac0931bd2775607c5304a..bda303904a08c406c0651743ca67aebd217c7628 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -43,6 +43,7 @@ module Stdlib: sig
val min_int: int
val max_int: int
val flush: out_channel -> unit
+ module Set: module type of Set
module Map: module type of Map
end
diff --git a/src/libraries/utils/hptset.ml b/src/libraries/utils/hptset.ml
index 7624684f2e8c855e3b9873f397cdde077d74aeeb..462bc0947c892610de98a67743b4ae0a443bb0d6 100644
--- a/src/libraries/utils/hptset.ml
+++ b/src/libraries/utils/hptset.ml
@@ -20,9 +20,43 @@
(* *)
(**************************************************************************)
+(** Sets over ordered types.
+
+ This module implements the set data structure.
+ All operations over sets are purely applicative (no side-effects). *)
+
+module type S_Basic_Compare =
+sig
+ type elt
+ type t
+ val empty: t
+ val is_empty: t -> bool
+ val mem: elt -> t -> bool
+ val add: elt -> t -> t
+ val singleton: elt -> t
+ val remove: elt -> t -> t
+ val union: t -> t -> t
+ val inter: t -> t -> t
+ val diff: t -> t -> t
+ val compare: t -> t -> int
+ val equal: t -> t -> bool
+ val subset: t -> t -> bool
+ val iter: (elt -> unit) -> t -> unit
+ val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
+ val for_all: (elt -> bool) -> t -> bool
+ val exists: (elt -> bool) -> t -> bool
+ val filter: (elt -> bool) -> t -> t
+ val partition: (elt -> bool) -> t -> t * t
+ val cardinal: t -> int
+ val elements: t -> elt list
+ val choose: t -> elt
+ val find: elt -> t -> elt
+ val of_list: elt list -> t
+end
+
module type S = sig
include Datatype.S_with_collections
- include FCSet.S_Basic_Compare with type t := t
+ include S_Basic_Compare with type t := t
val contains_single_elt: t -> elt option
val intersects: t -> t -> bool
diff --git a/src/libraries/utils/hptset.mli b/src/libraries/utils/hptset.mli
index e1dc4f1678a4f6a160cb4fa7ed144548bc4b740b..3bca4f3523d6a726d687ed9399a91a29eccc0d54 100644
--- a/src/libraries/utils/hptset.mli
+++ b/src/libraries/utils/hptset.mli
@@ -23,15 +23,43 @@
(** Sets over ordered types.
This module implements the set data structure.
- All operations over sets
- are purely applicative (no side-effects). *)
-
+ All operations over sets are purely applicative (no side-effects). *)
+
+(** Subset of the OCaml Set.S signature. *)
+module type S_Basic_Compare =
+sig
+ type elt
+ type t
+ val empty: t
+ val is_empty: t -> bool
+ val mem: elt -> t -> bool
+ val add: elt -> t -> t
+ val singleton: elt -> t
+ val remove: elt -> t -> t
+ val union: t -> t -> t
+ val inter: t -> t -> t
+ val diff: t -> t -> t
+ val compare: t -> t -> int
+ val equal: t -> t -> bool
+ val subset: t -> t -> bool
+ val iter: (elt -> unit) -> t -> unit
+ val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
+ val for_all: (elt -> bool) -> t -> bool
+ val exists: (elt -> bool) -> t -> bool
+ val filter: (elt -> bool) -> t -> t
+ val partition: (elt -> bool) -> t -> t * t
+ val cardinal: t -> int
+ val elements: t -> elt list
+ val choose: t -> elt
+ val find: elt -> t -> elt
+ val of_list: elt list -> t
+end
(** Output signature of the functor {!Set.Make}. *)
module type S = sig
include Datatype.S_with_collections
- include FCSet.S_Basic_Compare with type t := t
+ include S_Basic_Compare with type t := t
(** The datatype of sets. *)
val contains_single_elt: t -> elt option
diff --git a/src/libraries/utils/rich_text.ml b/src/libraries/utils/rich_text.ml
index cfba39cf308cdc83bd4ac1147c409caf48e75042..0284ae86a418e69c2259457a89b92652d8f1b1d0 100644
--- a/src/libraries/utils/rich_text.ml
+++ b/src/libraries/utils/rich_text.ml
@@ -111,7 +111,7 @@ let tgr_buffer = 3145728 (* elasticity (internal overhead) *)
type buffer = {
mutable formatter : Format.formatter ; (* formatter on self (recursive) *)
- mutable content : FCBuffer.t ;
+ mutable content : Buffer.t ;
mutable revtags : tag list ; (* in reverse order *)
mutable stack : (int * tag list) list ; (* opened tag positions *)
}
@@ -122,52 +122,53 @@ let is_blank = function
let trim_begin buffer =
let rec lookup_fwd text k n =
- if k < n && is_blank (FCBuffer.nth text k) then
+ if k < n && is_blank (Buffer.nth text k) then
lookup_fwd text (succ k) n else k
- in lookup_fwd buffer.content 0 (FCBuffer.length buffer.content)
+ in lookup_fwd buffer.content 0 (Buffer.length buffer.content)
let trim_end buffer =
let rec lookup_bwd text k =
- if k >= 0 && is_blank (FCBuffer.nth text k) then
+ if k >= 0 && is_blank (Buffer.nth text k) then
lookup_bwd text (pred k) else k
- in lookup_bwd buffer.content (pred (FCBuffer.length buffer.content))
+ in lookup_bwd buffer.content (pred (Buffer.length buffer.content))
let shrink buffer =
- if FCBuffer.length buffer.content > min_buffer then
- FCBuffer.reset buffer.content
+ if Buffer.length buffer.content > min_buffer then
+ Buffer.reset buffer.content
let truncate_text buffer size =
- if FCBuffer.length buffer.content > size then
+ if Buffer.length buffer.content > size then
begin
let p = trim_begin buffer in
let q = trim_end buffer in
let n = q+1-p in
- if n <= 0 then shrink buffer else
- if n <= size then
- FCBuffer.blit_buffer buffer.content p buffer.content 0 n
+ if n <= 0 then
+ shrink buffer
+ else if n <= size then
+ Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n
else
begin
let n_left = size / 2 - 3 in
let n_right = size - n_left - 5 in
if p > 0 then
- FCBuffer.blit_buffer buffer.content p buffer.content 0 n_left ;
- FCBuffer.blit_substring "[...]" 0 buffer.content n_left 5 ;
- FCBuffer.blit_buffer
+ Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n_left;
+ Buffer.add_substring buffer.content "[...]" n_left 5 ;
+ Buffer.blit
buffer.content (q-n_right+1)
- buffer.content (n_left + 5)
+ (Buffer.to_bytes buffer.content) (n_left + 5)
n_right ;
- FCBuffer.truncate buffer.content size ;
+ Buffer.truncate buffer.content size ;
end
end
(* All text added shall go through this function *)
let append buffer s k n =
- FCBuffer.add_substring buffer.content s k n ;
- if FCBuffer.length buffer.content > tgr_buffer then
+ Buffer.add_substring buffer.content s k n ;
+ if Buffer.length buffer.content > tgr_buffer then
truncate_text buffer max_buffer
let push_tag buffer _tag =
- let p = FCBuffer.length buffer.content in
+ let p = Buffer.length buffer.content in
buffer.stack <- ( p , buffer.revtags ) :: buffer.stack ;
buffer.revtags <- []
@@ -175,7 +176,7 @@ let pop_tag buffer tag =
match buffer.stack with
| [] -> ()
| (p,tags)::stack ->
- let q = FCBuffer.length buffer.content in
+ let q = Buffer.length buffer.content in
buffer.stack <- stack ;
let children = List.rev buffer.revtags in
buffer.revtags <- { p ; q ; tag ; children } :: tags
@@ -189,7 +190,7 @@ let no_mark _tag = ""
let create ?indent ?margin () =
let buffer = {
formatter = Format.err_formatter ;
- content = FCBuffer.create min_buffer ;
+ content = Buffer.create min_buffer ;
revtags = [] ;
stack = [] ;
} in
@@ -226,13 +227,13 @@ let trim buffer =
p , q
let contents buffer =
- truncate_text buffer max_buffer ; FCBuffer.contents buffer.content
+ truncate_text buffer max_buffer ; Buffer.contents buffer.content
let message buffer =
- ( FCBuffer.contents buffer.content , List.rev buffer.revtags )
+ ( Buffer.contents buffer.content , List.rev buffer.revtags )
-let sub buffer p n = FCBuffer.sub buffer.content p n
-let range buffer p q = FCBuffer.sub buffer.content p (q+1-p)
+let sub buffer p n = Buffer.sub buffer.content p n
+let range buffer p q = Buffer.sub buffer.content p (q+1-p)
let add_char buffer c = Format.pp_print_char buffer.formatter c
let add_string buffer s = Format.pp_print_string buffer.formatter s
diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml
index 890a894f0ddc8c44ae78fae5b1488497220d2b1b..530bd5c8609bbf65666ebd0e1bfb5e42a3185228 100644
--- a/src/plugins/gui/project_manager.ml
+++ b/src/plugins/gui/project_manager.ml
@@ -36,7 +36,7 @@ let projects_list ?(filter=fun _ -> true) () =
is not possible with an hashtbl.
So we use a reference over a set of couple *)
module PrjRadiosSet =
- FCSet.Make
+ Set.Make
(struct
type t = (Project.t * string) * GButton.radio_button * GMenu.menu_item
let compare (p1, _, _) (p2, _, _) = compare_prj p1 p2
diff --git a/src/plugins/loop_analysis/region_analysis_sig.ml b/src/plugins/loop_analysis/region_analysis_sig.ml
index 636b16cfe8314493cebd1c041c5cf14a441bf7cb..df1a00d55ba351f701ec2aa4b30c4ae6d3e8e33a 100644
--- a/src/plugins/loop_analysis/region_analysis_sig.ml
+++ b/src/plugins/loop_analysis/region_analysis_sig.ml
@@ -49,7 +49,7 @@ module type Node = sig
val copy: 'a t -> 'a t (* Shallow copy *)
end
- module Set:FCSet.S with type elt = node
+ module Set : Set.S with type elt = node
(* The graph of nodes. *)
module Graph:sig
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index bc1d8b63d555148f79a53015c0c014716a0a457e..a1375f191c2ab247e514716aff64d1ff391d77ca 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -270,7 +270,7 @@ end
(** Map and sets of varinfos sorted by name (and not by ids) *)
module VInfoMap = Map.Make (VarinfoByName)
-module VInfoSet = FCSet.Make (VarinfoByName)
+module VInfoSet = Set.Make (VarinfoByName)
(** Other pretty-printing and formatting utilities *)
diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli
index c344b1c0ce63106b53b0b89c7ba9ef4af61e7b2b..4ed5101db00030798e18b5e0078c2959ae65536a 100644
--- a/src/plugins/metrics/metrics_base.mli
+++ b/src/plugins/metrics/metrics_base.mli
@@ -97,7 +97,7 @@ end
(** Local varinfo map and set where the comparison function is the
lexicographic one on their respective names. *)
module VInfoMap: Map.S with type key = Cil_types.varinfo
-module VInfoSet: FCSet.S with type elt = Cil_types.varinfo
+module VInfoSet: Set.S with type elt = Cil_types.varinfo
;;
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 8fbfb29d894c58f3eda661b91f9b88524ae29b80..fbb3624e4019237373077cfa3014bb8d72a0f7ed 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -45,7 +45,7 @@ exception Err_Bot of string
(** set of nodes of the graph *)
module BoolNodeSet =
- FCSet.Make(Datatype.Pair(Datatype.Bool)(PdgTypes.Node))
+ Transitioning.Stdlib.Set.Make(Datatype.Pair(Datatype.Bool)(PdgTypes.Node))
let pretty_node ?(key=false) fmt n =
PdgTypes.Node.pretty fmt n;
diff --git a/src/plugins/server/jbuffer.ml b/src/plugins/server/jbuffer.ml
index d354dc8bc22d5c498edde315774d822fb376289b..f3e2136990e8a5e170fee5b8339107490759ee2b 100644
--- a/src/plugins/server/jbuffer.ml
+++ b/src/plugins/server/jbuffer.ml
@@ -23,22 +23,22 @@
type json = Yojson.Basic.t
type buffer = {
- text : FCBuffer.t ;
+ text : Buffer.t ;
mutable rjson : json list ; (* Current op-codes in reverse order *)
mutable stack : ( string * json list ) list ;
mutable fmt : Format.formatter ;
}
let append buffer s k n =
- FCBuffer.add_substring buffer.text s k n
+ Buffer.add_substring buffer.text s k n
let flush buffer () =
let t = buffer.text in
- let n = FCBuffer.length t in
+ let n = Buffer.length t in
if n > 0 then
- let js = `String (FCBuffer.contents t) in
+ let js = `String (Buffer.contents t) in
buffer.rjson <- js :: buffer.rjson ;
- FCBuffer.clear t
+ Buffer.clear t
let push_tag buffer stag =
let tag = Transitioning.Format.string_of_stag stag in
@@ -66,7 +66,7 @@ let mark_close_tag buffer tg = pop_tag buffer tg ; ""
let create ?indent ?margin () =
let buffer = {
fmt = Format.err_formatter ;
- text = FCBuffer.create 80 ; rjson = [] ; stack = []
+ text = Buffer.create 80 ; rjson = [] ; stack = []
} in
let fmt = Format.make_formatter (append buffer) (flush buffer) in
buffer.fmt <- fmt ;
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 9acf448228ae8e33af9c797714522ca1addd52e3..d4410b94fe488ab50342aaba1ab382b28cb84208 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -263,8 +263,8 @@ let call_pred lfun cc es =
module DT = Logic_type_info.Set
module DR = Compinfo.Set
module DS = Datatype.String.Set
-module DF = FCSet.Make(Lang.Fun)
-module DC = FCSet.Make
+module DF = Set.Make(Lang.Fun)
+module DC = Set.Make
(struct
type t = cluster
let compare = cluster_compare
diff --git a/src/plugins/wp/Letify.ml b/src/plugins/wp/Letify.ml
index c9a07102c81863d24f9c908160bd71e5cb828ffc..2e65af7cdff86613c772cdc071731bb6a7cefd30 100644
--- a/src/plugins/wp/Letify.ml
+++ b/src/plugins/wp/Letify.ml
@@ -540,7 +540,7 @@ end
(* --- Substitution Extraction --- *)
(* -------------------------------------------------------------------------- *)
-module XS = FCSet.Make(Var)
+module XS = Set.Make(Var)
let elements xs = Vars.fold XS.add xs XS.empty
let iter f xs = XS.iter f (elements xs)
diff --git a/src/plugins/wp/Warning.ml b/src/plugins/wp/Warning.ml
index 78f631fba1f67276472077221f49df968278ff46..da64b3aac7c03da9e0c437fbab5527583496ad41 100644
--- a/src/plugins/wp/Warning.ml
+++ b/src/plugins/wp/Warning.ml
@@ -54,7 +54,7 @@ end
include SELF
module Map = Map.Make(SELF)
-module Set = FCSet.Make(SELF)
+module Set = Set.Make(SELF)
let severe s = Set.exists (fun w -> w.severe) s
diff --git a/src/plugins/wp/Warning.mli b/src/plugins/wp/Warning.mli
index 0ba5dc048f90d89fbbbef3ecdbb4ca75b563fc4d..270ec44a7d63f889c9a7ccecf4f863d27869cdb9 100644
--- a/src/plugins/wp/Warning.mli
+++ b/src/plugins/wp/Warning.mli
@@ -39,7 +39,7 @@ type t = {
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
-module Set : FCSet.S with type elt = t
+module Set : Set.S with type elt = t
module Map : Map.S with type key = t
val severe : Set.t -> bool
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 565431efa0674528c80781a5fcd6a7c225ca6835..bf42234354bfc24b17cbc91a16e30bf33ba07225 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -104,7 +104,7 @@ struct
module W = Warning.Set
module D = Property.Set
module S = Stmt.Set
- module Eset = FCSet.Make(EFFECT)
+ module Eset = Set.Make(EFFECT)
module Gset = G.Set
module Gmap = G.Map
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index 01e38dc3a82cbd01fefb8719b5a38bc70bc587f7..8ef74ed0a13747c6dfb57c38386ba3fbfde29eb9 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -287,10 +287,10 @@ struct
end
(** Set of edges. *)
-module Eset = FCSet.Make (CFG.E)
+module Eset = Set.Make (CFG.E)
(** Set of nodes. *)
-module Nset = FCSet.Make (CFG.V)
+module Nset = Set.Make (CFG.V)
(** Hashtbl of node *)
module Ntbl = Hashtbl.Make (CFG.V)
diff --git a/src/plugins/wp/cil2cfg.mli b/src/plugins/wp/cil2cfg.mli
index b4745c1b54092f55f775d6e9bc6683fe996e07e8..3ebf1bc8cd4faf3338b2fa6f3b24f34f98df0639 100644
--- a/src/plugins/wp/cil2cfg.mli
+++ b/src/plugins/wp/cil2cfg.mli
@@ -45,7 +45,7 @@ val same_edge : edge -> edge -> bool
val start_edge : t -> edge
(** set of edges *)
-module Eset : FCSet.S with type elt = edge
+module Eset : Set.S with type elt = edge
(** node and edges relations *)
val edge_src : edge -> node
diff --git a/src/plugins/wp/clabels.mli b/src/plugins/wp/clabels.mli
index ae01c6833744dab9ce6999d54f984d6be0f7bdcf..fdc73803faa46518e1bd462698e5568d66559514 100644
--- a/src/plugins/wp/clabels.mli
+++ b/src/plugins/wp/clabels.mli
@@ -37,7 +37,7 @@ val equal : c_label -> c_label -> bool
module T : sig type t = c_label val compare : t -> t -> int end
module LabelMap : Map.S with type key = c_label
-module LabelSet : FCSet.S with type elt = c_label
+module LabelSet : Set.S with type elt = c_label
val pre : c_label
val here : c_label
diff --git a/src/plugins/wp/wpContext.ml b/src/plugins/wp/wpContext.ml
index 98f6832b2a158588a0cbaffc49367d5cf0cdf965..bc8b589d061034e7507a010b764aa8a1774cc4f7 100644
--- a/src/plugins/wp/wpContext.ml
+++ b/src/plugins/wp/wpContext.ml
@@ -204,7 +204,7 @@ struct
module KEY = struct type t = E.key let compare = E.compare end
module MAP = Map.Make(KEY)
- module SET = FCSet.Make(KEY)
+ module SET = Set.Make(KEY)
let demon = ref []
@@ -339,7 +339,7 @@ struct
module KEY = struct type t = E.key let compare = E.compare end
module MAP = Map.Make(KEY)
- module SET = FCSet.Make(KEY)
+ module SET = Set.Make(KEY)
let demon = ref []