aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/dag.ml
blob: d0515d3ff1940c7839305afbe8e2856fbbd7fa59 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

module type S = sig

  module Cluster :
  sig
    type 'd t
    val equal : 'd t -> 'd t -> bool
    val compare : 'd t -> 'd t -> int
    val to_string : 'd t -> string
    val data : 'd t -> 'd
  end

  type node
  module NodeSet : Set.S with type elt = node

  type ('edge,'info,'cdata) t

  val empty : ('e,'i,'d) t

  val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t
  val from_node : ('e,'i,'d) t -> node -> (node * 'e) list
  val mem : ('e,'i,'d) t -> node -> bool
  val del_edge : ('e,'i,'d) t -> node -> node -> ('e,'i,'d) t
  val del_nodes : ('e,'i,'d) t -> NodeSet.t  -> ('e,'i,'d) t
  val all_nodes : ('e,'i,'d) t -> NodeSet.t

  val iter : ('e,'i,'d) t ->
    (node -> 'd Cluster.t option -> 'i option ->
      (node * 'e) list -> unit) -> unit

  val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
  val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option
  val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t

  val get_info : ('e,'i,'d) t -> node -> 'i option
  val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t
  val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t

end

module Make(OT : Map.OrderedType) = struct

module Cluster =
struct
  type 'd t = 'd * int
  let equal (_,i1) (_,i2) = Int.equal i1 i2
  let compare (_,i1) (_,i2) = Int.compare i1 i2
  let to_string (_,i) = string_of_int i
  let data (d,_) = d
end

type node = OT.t

module NodeMap = CMap.Make(OT)
module NodeSet = Set.Make(OT)

type ('edge,'info,'data) t = {
  graph : (node * 'edge) list NodeMap.t;
  clusters : 'data Cluster.t NodeMap.t;
  infos : 'info NodeMap.t;
}

let empty = {
  graph = NodeMap.empty;
  clusters = NodeMap.empty;
  infos = NodeMap.empty;
}

let mem { graph } id = NodeMap.mem id graph

let add_edge dag from trans dest = { dag with
  graph =
    try NodeMap.modify from (fun _ arcs -> (dest, trans) :: arcs) dag.graph
    with Not_found -> NodeMap.add from [dest, trans] dag.graph }

let from_node { graph } id = NodeMap.find id graph

let del_edge dag id tgt = { dag with
  graph =
    try
      let modify _ arcs =
        let filter (d, _) = OT.compare d tgt <> 0 in
        List.filter filter arcs
      in
      NodeMap.modify id modify dag.graph
    with Not_found -> dag.graph }

let del_nodes dag s = {
  infos = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.infos;
  clusters = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.clusters;
  graph = NodeMap.filter (fun n l ->
      let drop = NodeSet.mem n s in
      if not drop then
        assert(List.for_all (fun (n',_) -> not(NodeSet.mem n' s)) l);
      not drop)
    dag.graph }

let clid = ref 1
let create_cluster dag l data =
  incr clid;
  { dag with clusters =
     List.fold_right (fun x clusters ->
       NodeMap.add x (data, !clid) clusters) l dag.clusters }

let cluster_of dag id =
  try Some (NodeMap.find id dag.clusters)
  with Not_found -> None

let del_cluster dag c =
  { dag with clusters =
     NodeMap.filter (fun _ c' -> not (Cluster.equal c' c)) dag.clusters }

let get_info dag id =
  try Some (NodeMap.find id dag.infos)
  with Not_found -> None

let set_info dag id info = { dag with infos = NodeMap.add id info dag.infos }

let clear_info dag id = { dag with infos = NodeMap.remove id dag.infos }

let iter dag f =
  NodeMap.iter (fun k v -> f k (cluster_of dag k) (get_info dag k) v) dag.graph

let all_nodes dag = NodeMap.domain dag.graph

end