diff options
Diffstat (limited to 'src/finite_map.ml')
| -rw-r--r-- | src/finite_map.ml | 216 |
1 files changed, 0 insertions, 216 deletions
diff --git a/src/finite_map.ml b/src/finite_map.ml deleted file mode 100644 index 444e3790..00000000 --- a/src/finite_map.ml +++ /dev/null @@ -1,216 +0,0 @@ -(**************************************************************************) -(* Sail *) -(* *) -(* Copyright (c) 2013-2017 *) -(* Kathyrn Gray *) -(* Shaked Flur *) -(* Stephen Kell *) -(* Gabriel Kerneis *) -(* Robert Norton-Wright *) -(* Christopher Pulte *) -(* Peter Sewell *) -(* Alasdair Armstrong *) -(* Brian Campbell *) -(* Thomas Bauereiss *) -(* Anthony Fox *) -(* Jon French *) -(* Dominic Mulligan *) -(* Stephen Kell *) -(* Mark Wassell *) -(* *) -(* All rights reserved. *) -(* *) -(* This software was developed by the University of Cambridge Computer *) -(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) -(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) -(* *) -(* Redistribution and use in source and binary forms, with or without *) -(* modification, are permitted provided that the following conditions *) -(* are met: *) -(* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) -(* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in *) -(* the documentation and/or other materials provided with the *) -(* distribution. *) -(* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) -(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) -(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) -(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) -(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) -(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) -(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) -(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) -(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) -(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) -(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) -(* SUCH DAMAGE. *) -(**************************************************************************) - - -(**************************************************************************) -(* Lem *) -(* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) -(* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) -(* *) -(* *) -(* Redistribution and use in source and binary forms, with or without *) -(* modification, are permitted provided that the following conditions *) -(* are met: *) -(* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) -(* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) -(* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) -(**************************************************************************) - - -(** finite map library *) - -module type Fmap = sig - type k - module S : Set.S with type elt = k - type 'a t - val empty : 'a t - val is_empty : 'a t -> bool - val from_list : (k * 'a) list -> 'a t - val to_list : 'a t -> (k * 'a) list - val from_list2 : k list -> 'a list -> 'a t - val insert : 'a t -> (k * 'a) -> 'a t - (* Keys from the right argument replace those from the left *) - val union : 'a t -> 'a t -> 'a t - (* Function merges the stored value when a key is in the right and the left map *) - val union_merge : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t - val intersect : 'a t -> 'a t -> 'a t - (* Function merges the stored values for shared keys *) - val intersect_merge : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t - val big_union : 'a t list -> 'a t - val big_union_merge : ('a -> 'a -> 'a) -> 'a t list -> 'a t - val difference : 'a t -> 'a t -> 'a t - val merge : (k -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t - val apply : 'a t -> k -> 'a option - val in_dom : k -> 'a t -> bool - val map : (k -> 'a -> 'b) -> 'a t -> 'b t - val domains_overlap : 'a t -> 'b t -> k option - val domains_disjoint : 'a t list -> bool - val iter : (k -> 'a -> unit) -> 'a t -> unit - val fold : ('b -> k -> 'a -> 'b) -> 'b -> 'a t -> 'b - val remove : 'a t -> k -> 'a t - val pp_map : (Format.formatter -> k -> unit) -> - (Format.formatter -> 'a -> unit) -> - Format.formatter -> - 'a t -> - unit - val domain : 'a t -> S.t -end - -module Fmap_map(Key : Set.OrderedType) : Fmap - with type k = Key.t and module S = Set.Make(Key) = struct - - type k = Key.t - module S = Set.Make(Key) - - module M = Map.Make(Key) - module D = Util.Duplicate(S) - - type 'a t = 'a M.t - let empty = M.empty - let is_empty m = M.is_empty m - let from_list l = List.fold_left (fun m (k,v) -> M.add k v m) M.empty l - let from_list2 l1 l2 = List.fold_left2 (fun m k v -> M.add k v m) M.empty l1 l2 - let insert m (k,v) = M.add k v m - let union m1 m2 = - M.merge (fun k v1 v2 -> match v2 with | None -> v1 | Some _ -> v2) m1 m2 - let union_merge f m1 m2 = - M.merge (fun k v1 v2 -> - match v1,v2 with - | None,None -> None - | None,Some v | Some v,None -> Some v - | Some v1, Some v2 -> Some (f v1 v2)) m1 m2 - let merge f m1 m2 = M.merge f m1 m2 - let apply m k = - try - Some(M.find k m) - with - | Not_found -> None - let in_dom k m = M.mem k m - let map f m = M.mapi f m - let rec domains_overlap m1 m2 = - M.fold - (fun k _ res -> - if M.mem k m1 then - Some(k) - else - res) - m2 - None - let iter f m = M.iter f m - let fold f m base = M.fold (fun k v res -> f res k v) base m - let difference m1 m2 = - M.fold (fun k v res -> - if (M.mem k m2) - then res - else M.add k v res) m1 M.empty - let intersect m1 m2 = - M.fold (fun k v res -> - if (M.mem k m2) - then M.add k v res - else res) m1 M.empty - let intersect_merge f m1 m2 = - M.fold (fun k v res -> - match (apply m2 k) with - | None -> res - | Some v2 -> M.add k (f v v2) res) m1 M.empty - let to_list m = M.fold (fun k v res -> (k,v)::res) m [] - let remove m k = M.remove k m - let pp_map pp_key pp_val ppf m = - let l = M.fold (fun k v l -> (k,v)::l) m [] in - Format.fprintf ppf "@[%a@]" - (Pp.lst "@\n" - (fun ppf (k,v) -> - Format.fprintf ppf "@[<2>%a@ |->@ %a@]" - pp_key k - pp_val v)) - l - let big_union l = List.fold_left union empty l - let big_union_merge f l = List.fold_left (union_merge f) empty l - let domains_disjoint maps = - match D.duplicates (List.concat (List.map (fun m -> List.map fst (M.bindings m)) maps)) with - | D.No_dups _ -> true - | D.Has_dups _ -> false - - let domain m = - M.fold (fun k _ s -> S.add k s) m S.empty -end - |