extracted/untrusted/setMap.ml

   1 (* Pasted from Pottier's PP compiler *)
   2
   3 (* This signature defines a few operations over maps of keys to
   4    nonempty sets of items. Keys and items can have distinct types,
   5    hence the name [Heterogeneous].
   6
   7    These maps can be used to represent directed bipartite graphs whose
   8    source vertices are keys and whose target vertices are items. Each
   9    key is mapped to the set of its successors. *)
  10
  11 module type Heterogeneous = sig
  12
  13   (* These are the types of keys, items, and sets of items. *)
  14
  15   type key
  16   type item
  17   type itemset
  18
  19   (* This is the type of maps of keys to sets of items. *)
  20
  21   type t
  22
  23   (* [find x m] is the item set associated with key [x] in map [m], if
  24      such an association is defined; it is the empty set otherwise. *)
  25
  26   val find: key -> t -> itemset
  27
  28   (* [add x is m] extends [m] with a binding of [x] to the item set
  29      [is], if [is] is nonempty. If [is] is empty, it removes [x] from
  30      [m]. *)
  31
  32   val add: key -> itemset -> t -> t
  33
  34   (* [update x f m] is [add x (f (find x m)) m]. *)
  35
  36   val update: key -> (itemset -> itemset) -> t -> t
  37
  38   (* [mkedge x i m] extends [m] with a binding of [x] to the union of
  39      the set [m x] and the singleton [i], where [m x] is taken to be
  40      empty if undefined. In terms of graphs, [mkedge x i m] extends
  41      the graph [m] with an edge of [x] to [i]. *)
  42
  43   val mkedge: key -> item -> t -> t
  44
  45   (* [rmedge x i m] extends [m] with a binding of [x] to the
  46      difference of the set [m x] and the singleton [i], where the
  47      binding is considered undefined if that difference is empty.  In
  48      terms of graphs, [rmedge x i m] removes an edge of [x] to [i]
  49      to the graph [m]. *)
  50
  51   val rmedge: key -> item -> t -> t
  52
  53   (* [iter] and [fold] iterate over all edges in the graph. *)
  54
  55   val iter: (key * item -> unit) -> t -> unit
  56   val fold: (key * item -> 'a -> 'a) -> t -> 'a -> 'a
  57
  58   (* [pick m p] returns an arbitrary edge that satisfies predicate
  59      [p], if the graph contains one. *)
  60
  61   val pick: t -> (key * item -> bool) -> (key * item) option
  62
  63 end
  64
  65 (* This functor offers an implementation of [Heterogeneous] out of
  66    standard implementations of sets and maps. *)
  67
  68 module MakeHetero
  69     (Set : sig
  70       type elt
  71       type t
  72       val empty: t
  73       val is_empty: t -> bool
  74       val add: elt -> t -> t
  75       val remove: elt -> t -> t
  76       val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
  77     end)
  78     (Map : sig
  79       type key
  80       type 'a t
  81       val add: key -> 'a -> 'a t -> 'a t
  82       val find: key -> 'a t -> 'a
  83       val remove: key -> 'a t -> 'a t
  84       val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
  85     end)
  86 = struct
  87
  88   type key = Map.key
  89   type item = Set.elt
  90   type itemset = Set.t
  91   type t = Set.t Map.t
  92
  93   let find x m =
  94     try
  95       Map.find x m
  96     with Not_found ->
  97       Set.empty
  98
  99   let add x is m =
 100     if Set.is_empty is then
 101       Map.remove x m
 102     else
 103       Map.add x is m
 104
 105   let update x f m =
 106     add x (f (find x m)) m
 107
 108   let mkedge x i m =
 109     update x (Set.add i) m
 110
 111   let rmedge x i m =
 112     update x (Set.remove i) m
 113
 114   let fold f m accu =
 115     Map.fold (fun source targets accu ->
 116       Set.fold (fun target accu ->
 117         f (source, target) accu
 118       ) targets accu
 119     ) m accu
 120
 121   let iter f m =
 122     fold (fun edge () -> f edge) m ()
 123
 124   exception Picked of (key * item)
 125
 126   let pick m p =
 127     try
 128       iter (fun edge ->
 129         if p edge then
 130           raise (Picked edge)
 131       ) m;
 132       None
 133     with Picked edge ->
 134       Some edge
 135
 136 end
 137
 138 (* This signature defines a few common operations over maps of keys
 139    to sets of keys -- that is, keys and items have the same type,
 140    hence the name [Homogeneous].
 141
 142    These maps can be used to represent general directed graphs. *)
 143
 144 module type Homogeneous = sig
 145
 146   include Heterogeneous (* [key] and [item] intended to be equal *)
 147
 148   (* [mkbiedge x1 x2 m] is [mkedge x1 x2 (mkedge x2 x1 m)]. *)
 149
 150   val mkbiedge: key -> key -> t -> t
 151
 152   (* [rmbiedge x1 x2 m] is [rmedge x1 x2 (rmedge x2 x1 m)]. *)
 153
 154   val rmbiedge: key -> key -> t -> t
 155
 156   (* [reverse m] is the reverse of graph [m]. *)
 157
 158   val reverse: t -> t
 159
 160   (* [restrict m] is the graph obtained by keeping only the vertices
 161      that satisfy predicate [p]. *)
 162
 163   val restrict: (key -> bool) -> t -> t
 164
 165 end
 166
 167 module MakeHomo
 168     (Set : sig
 169       type elt
 170       type t
 171       val empty: t
 172       val is_empty: t -> bool
 173       val add: elt -> t -> t
 174       val remove: elt -> t -> t
 175       val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
 176       val filter: (elt -> bool) -> t -> t
 177     end)
 178     (Map : sig
 179       type key = Set.elt
 180       type 'a t
 181       val empty: 'a t
 182       val add: key -> 'a -> 'a t -> 'a t
 183       val find: key -> 'a t -> 'a
 184       val remove: key -> 'a t -> 'a t
 185       val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
 186     end)
 187 = struct
 188
 189   include MakeHetero(Set)(Map)
 190
 191   let symmetric transform x1 x2 m =
 192     transform x1 x2 (transform x2 x1 m)
 193
 194   let mkbiedge =
 195     symmetric mkedge
 196
 197   let rmbiedge =
 198     symmetric rmedge
 199
 200   let reverse m =
 201     Map.fold (fun source targets predecessors ->
 202       Set.fold (fun target predecessors ->
 203
 204         (* We have a direct edge from [source] to [target]. Thus, we
 205            record the existence of a reverse edge from [target] to
 206            [source]. *)
 207
 208         mkedge target source predecessors
 209
 210       ) targets predecessors
 211     ) m Map.empty
 212
 213   let restrict p m =
 214     Map.fold (fun source targets m ->
 215       if p source then
 216         let targets = Set.filter p targets in
 217         if Set.is_empty targets then
 218           m
 219         else
 220           Map.add source targets m
 221       else
 222         m
 223     ) m Map.empty
 224
 225 end
 226