Merge remote-tracking branch 'origin/asl_flow2' into sail2

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
-