Skip to content

GitLab

Commit fa6e437d authored by Michele Alberti's avatar Michele Alberti
Browse files

[kernel][stdlib] Remove FCSet and move basic signature to Hptset module.

parent 374a32b8
Hide whitespace changes
Inline Side-by-side
.Makefile.lint
View file @ fa6e437d
......@@ -147,8 +147,6 @@ 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/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
......
Makefile
View file @ fa6e437d
......@@ -440,7 +440,6 @@ CMO += $(VERY_FIRST_CMO)
LIB_CMO =\
src/libraries/stdlib/transitioning \
src/libraries/stdlib/FCSet \
src/libraries/stdlib/FCHashtbl \
src/libraries/stdlib/extlib \
src/libraries/datatype/unmarshal \
......
headers/header_spec.txt
View file @ fa6e437d
......@@ -632,8 +632,6 @@ 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
......
src/kernel_services/abstract_interp/abstract_interp.ml
View file @ fa6e437d
......@@ -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
......
src/kernel_services/abstract_interp/abstract_interp.mli
View file @ fa6e437d
......@@ -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
......
src/kernel_services/abstract_interp/float_sig.mli
View file @ fa6e437d
......@@ -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
......
src/kernel_services/abstract_interp/int_set.ml
View file @ fa6e437d
......@@ -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
......
src/kernel_services/abstract_interp/lattice_type.mli
View file @ fa6e437d
......@@ -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
......
src/kernel_services/ast_queries/logic_typing.ml
View file @ fa6e437d
......@@ -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 =
......
src/libraries/datatype/datatype.ml
View file @ fa6e437d
......@@ -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))
(Stdlib.Set.Make(D))
(D)
(struct let module_name = Info.module_name ^ ".Set" end)
......
src/libraries/datatype/datatype.mli
View file @ fa6e437d
......@@ -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
......
src/libraries/stdlib/FCHashtbl.ml
View file @ fa6e437d
......@@ -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
......
src/libraries/stdlib/FCSet.ml deleted 100644 → 0
View file @ 374a32b8
(*****************************************************************************)
(* *)
(* 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 Set.S
val nearest_elt_le: elt -> t -> elt
val nearest_elt_ge: elt -> t -> elt
end
module Make(Ord: Set.OrderedType) =
struct
include Set.Make(Ord)
let nearest_elt_le x =
find_last (fun y -> y <= x)
let nearest_elt_ge x =
find_first (fun y -> y >= x)
end
(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
src/libraries/stdlib/FCSet.mli deleted 100644 → 0
View file @ 374a32b8
(*****************************************************************************)
(* *)
(* 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 Set.S
(* 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:
*)
src/libraries/utils/hptset.ml
View file @ fa6e437d
......@@ -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
......
src/libraries/utils/hptset.mli
View file @ fa6e437d
......@@ -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
......
src/plugins/gui/project_manager.ml
View file @ fa6e437d
......@@ -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
......
src/plugins/loop_analysis/region_analysis_sig.ml
View file @ fa6e437d
......@@ -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
......
src/plugins/metrics/metrics_base.ml
View file @ fa6e437d
......@@ -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 *)
......
src/plugins/metrics/metrics_base.mli
View file @ fa6e437d
......@@ -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
;;
......
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