Commit 056a7875 authored by Andrei Paskevich's avatar Andrei Paskevich

minor

parent c0b33ea3
......@@ -12,10 +12,9 @@
(***********************************************************************)
(* This file originates from the OCaml v 3.12 Standard Library.
It was extended and modified for the needs of the Why3 project
by François Bobot and Andrei Paskevich. It is distributed under
the terms of its initial license, which is provided in file
OCAML-LICENSE. *)
It was extended and modified for the needs of the Why3 project.
It is distributed under the terms of its initial license, which
is provided in the file OCAML-LICENSE. *)
module type S =
sig
......@@ -48,7 +47,6 @@ module type S =
val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
(** Added into why stdlib version *)
val is_num_elt : int -> 'a t -> bool
val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
......@@ -69,17 +67,18 @@ module type S =
val mapi_filter: (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapi_fold:
(key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
val mapi_filter_fold:
(key -> 'a -> 'acc -> 'acc * 'b option) -> 'a t -> 'acc -> 'acc * 'b t
val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
val fold2_inter: (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
val fold2_union:
(key -> 'a option -> 'b option -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
val translate : (key -> key) -> 'a t -> 'a t
val mapi_filter_fold:
(key -> 'a -> 'acc -> 'acc * 'b option) -> 'a t -> 'acc -> 'acc * 'b t
val add_new : exn -> key -> 'a -> 'a t -> 'a t
val keys: 'a t -> key list
val values: 'a t -> 'a list
val of_list : (key * 'a) list -> 'a t
val is_num_elt : int -> 'a t -> bool
type 'a enumeration
val val_enum : 'a enumeration -> (key * 'a) option
val start_enum : 'a t -> 'a enumeration
......
......@@ -16,21 +16,21 @@
It is distributed under the terms of its initial license, which
is provided in the file OCAML-LICENSE. *)
(** Association tables over ordered types.
(** Association tables over ordered types.
This module implements applicative association tables, also known as
finite maps or dictionaries, given a total ordering function
over the keys.
All operations over maps are purely applicative (no side-effects).
The implementation uses balanced binary trees, and therefore searching
and insertion take time logarithmic in the size of the map.
*)
This module implements applicative association tables, also known as
finite maps or dictionaries, given a total ordering function
over the keys.
All operations over maps are purely applicative (no side-effects).
The implementation uses balanced binary trees, and therefore searching
and insertion take time logarithmic in the size of the map.
*)
(** Input signature of the functor {!Extmap.Make}. *)
module type OrderedType = Map.OrderedType
(** Input signature of the functor {!Extmap.Make}. *)
module type OrderedType = Map.OrderedType
(** Output signature of the functor {!Extmap.Make}. *)
module type S =
(** Output signature of the functor {!Extmap.Make}. *)
module type S =
sig
type key
(** The type of the map keys. *)
......@@ -155,9 +155,6 @@
(** @Added in Why3 *)
val is_num_elt : int -> 'a t -> bool
(** check if the map has the given number of elements *)
val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
(** [change f x m] returns a map containing the same bindings as
[m], except the binding of [x] in [m] is changed from [y] to
......@@ -236,6 +233,10 @@
(key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
(** fold and map at the same time *)
val mapi_filter_fold:
(key -> 'a -> 'acc -> 'acc * 'b option) -> 'a t -> 'acc -> 'acc * 'b t
(** Same as {!Extmap.S.mapi_fold}, but may remove bindings. *)
val fold_left: ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
(** same as {!fold} but in the order of {!List.fold_left} *)
......@@ -251,10 +252,6 @@
function [f]. [f] must be strictly monotone on the key of [m].
Otherwise it raises invalid_arg *)
val mapi_filter_fold:
(key -> 'a -> 'acc -> 'acc * 'b option) -> 'a t -> 'acc -> 'acc * 'b t
(** Same as {!Extmap.S.mapi_fold}, but may remove bindings. *)
val add_new : exn -> key -> 'a -> 'a t -> 'a t
(** [add_new e x v m] binds [x] to [v] in [m] if [x] is not bound,
and raises [e] otherwise. *)
......@@ -274,6 +271,9 @@
val of_list: (key * 'a) list -> 'a t
(** construct a map from a pair of bindings *)
val is_num_elt : int -> 'a t -> bool
(** check if the map has the given number of elements *)
type 'a enumeration
(** enumeration: zipper style *)
......@@ -296,6 +296,6 @@
greater or equal to the given key *)
end
module Make (Ord : OrderedType) : S with type key = Ord.t
(** Functor building an implementation of the map structure
given a totally ordered type. *)
module Make (Ord : OrderedType) : S with type key = Ord.t
(** Functor building an implementation of the map structure
given a totally ordered type. *)
......@@ -40,8 +40,9 @@ module type S = sig
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val fold_left: ('b -> elt -> 'b) -> 'b -> t -> 'b
val fold2: (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
val translate : (elt -> elt) -> t -> t
val add_new : exn -> elt -> t -> t
val is_num_elt : int -> t -> bool
......@@ -83,11 +84,12 @@ module MakeOfMap (M: Extmap.S) = struct
let union = M.set_union
let inter = M.set_inter
let diff = M.set_diff
let fold2 f s t acc = M.fold2_union (fun k _ _ acc -> f k acc) s t acc
let fold_left f acc s = M.fold_left (fun acc k () -> f acc k) acc s
let fold2_inter f s t acc = M.fold2_inter (fun k _ _ acc -> f k acc) s t acc
let fold2_union f s t acc = M.fold2_union (fun k _ _ acc -> f k acc) s t acc
let translate = M.translate
let add_new e x s = M.add_new e x () s
let is_num_elt n m = M.is_num_elt n m
let fold_left f acc s = M.fold_left (fun acc k () -> f acc k) acc s
let of_list l = List.fold_left (fun acc a -> add a acc) empty l
end
......
......@@ -9,11 +9,13 @@
(* *)
(********************************************************************)
(** Input signature of the functor {!Extset.Make}. *)
module type OrderedType = Set.OrderedType
(** This module extends the standard OCaml Set module. *)
(** Output signature of the functor {!Extset.Make}. *)
module type S =
(** Input signature of the functor {!Extset.Make}. *)
module type OrderedType = Set.OrderedType
(** Output signature of the functor {!Extset.Make}. *)
module type S =
sig
module M : Extmap.S
(** The module of association tables over [elt]. *)
......@@ -132,11 +134,16 @@
val diff : t -> t -> t
(** [diff f s1 s2] computes the difference of two sets *)
val fold_left: ('b -> elt -> 'b) -> 'b -> t -> 'b
val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
(** same as {!fold} but in the order of {!List.fold_left} *)
val fold2: (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
(** [fold2 f s1 s2 a] computes [(f eN ... (f e1 a) ...)],
val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
(** [fold2_inter f s1 s2 a] computes [(f eN ... (f e1 a) ...)],
where [e1 ... eN] are the elements of [inter s1 s2]
in increasing order. *)
val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
(** [fold2_union f s1 s2 a] computes [(f eN ... (f e1 a) ...)],
where [e1 ... eN] are the elements of [union s1 s2]
in increasing order. *)
......@@ -156,10 +163,10 @@
(** construct a set from a list of elements *)
end
module MakeOfMap (M : Extmap.S) : S with module M = M
(** Functor building an implementation of the set structure
given a totally ordered type. *)
module MakeOfMap (M : Extmap.S) : S with module M = M
(** Functor building an implementation of the set structure
given a totally ordered type. *)
module Make (Ord : OrderedType) : S with type M.key = Ord.t
(** Functor building an implementation of the set structure
given a totally ordered type. *)
module Make (Ord : OrderedType) : S with type M.key = Ord.t
(** Functor building an implementation of the set structure
given a totally ordered type. *)
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