diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-02-28 09:41:13 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-02-28 09:41:13 +0000 |
commit | 7a09bbe8d18abb376104e1399fc84ce911d8897d (patch) | |
tree | fd4b26554df3e532bf8ccf9be2df522fd3295b37 /src/bourdoncle/ptset.mli | |
parent | 71669aaba76f65ff9ac99a99f4559fdfcbf3446d (diff) | |
download | vericert-7a09bbe8d18abb376104e1399fc84ce911d8897d.tar.gz vericert-7a09bbe8d18abb376104e1399fc84ce911d8897d.zip |
Add ptsets.ml library from CompCert for Bourdoncle
Diffstat (limited to 'src/bourdoncle/ptset.mli')
-rw-r--r-- | src/bourdoncle/ptset.mli | 125 |
1 files changed, 125 insertions, 0 deletions
diff --git a/src/bourdoncle/ptset.mli b/src/bourdoncle/ptset.mli new file mode 100644 index 0000000..88319ea --- /dev/null +++ b/src/bourdoncle/ptset.mli @@ -0,0 +1,125 @@ +(* + * Copyright (C) 2008 Jean-Christophe Filliatre + * Copyright (C) 2008, 2009 Laurent Hubert (CNRS) + * + * This software is free software; you can redistribute it and/or + * modify it under the terms of the GNU Lesser General Public License + * version 2.1, with the special exception on linking described in file + * LICENSE. + + * This software is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + *) + +(** Sets of integers implemented as Patricia trees. + + This implementation follows Chris Okasaki and Andrew Gill's paper + {e Fast Mergeable Integer Maps}. + + Patricia trees provide faster operations than standard library's + module [Set], and especially very fast [union], [subset], [inter] + and [diff] operations. *) + +(** The idea behind Patricia trees is to build a {e trie} on the + binary digits of the elements, and to compact the representation + by branching only one the relevant bits (i.e. the ones for which + there is at least on element in each subtree). We implement here + {e little-endian} Patricia trees: bits are processed from + least-significant to most-significant. The trie is implemented by + the following type [t]. [Empty] stands for the empty trie, and + [Leaf k] for the singleton [k]. (Note that [k] is the actual + element.) [Branch (m,p,l,r)] represents a branching, where [p] is + the prefix (from the root of the trie) and [m] is the branching + bit (a power of 2). [l] and [r] contain the subsets for which the + branching bit is respectively 0 and 1. Invariant: the trees [l] + and [r] are not empty. *) + +(** The docuemntation is given for function that differs from [Set.S + with type elt = int]. *) + +module type S = sig + type t + + type elt = int + + val empty : t + + val is_empty : t -> bool + + val mem : int -> t -> bool + + val add : int -> t -> t + + val singleton : int -> t + + val remove : int -> t -> t + + val union : t -> t -> t + + val subset : t -> t -> bool + + val inter : t -> t -> t + + val diff : t -> t -> t + + val equal : t -> t -> bool + + val compare : t -> t -> int + + val elements : t -> int list + + val choose : t -> int + + val cardinal : t -> int + + val iter : (int -> unit) -> t -> unit + + val fold : (int -> 'a -> 'a) -> t -> 'a -> 'a + + val for_all : (int -> bool) -> t -> bool + + val exists : (int -> bool) -> t -> bool + + val filter : (int -> bool) -> t -> t + + val partition : (int -> bool) -> t -> t * t + + val split : int -> t -> t * bool * t + + (** Warning: [min_elt] and [max_elt] are linear w.r.t. the size of the + set. In other words, [min_elt t] is barely more efficient than [fold + min t (choose t)]. *) + + val min_elt : t -> int + val max_elt : t -> int + + (** Additional functions not appearing in the signature [Set.S] from + ocaml standard library. *) + + (** [intersect u v] determines if sets [u] and [v] have a non-empty + intersection. *) + + val intersect : t -> t -> bool + + (** [choose_and_remove t] is equivalent (but more efficient) to + [(fun t -> let i = choose t in (i,remove i t)) t] + @author Laurent Hubert*) + val choose_and_remove : t -> int*t + +end + +include S + +(** Big-endian Patricia trees *) + +module Big : S + +(** Big-endian Patricia trees with non-negative elements. Changes: + - [add] and [singleton] raise [Invalid_arg] if a negative element is given + - [mem] is slightly faster (the Patricia tree is now a search tree) + - [min_elt] and [max_elt] are now O(log(N)) + - [elements] returns a list with elements in ascending order + *) + +module BigPos : S |