aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/dag.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/dag.mli')
-rw-r--r--lib/dag.mli38
1 files changed, 38 insertions, 0 deletions
diff --git a/lib/dag.mli b/lib/dag.mli
new file mode 100644
index 000000000..791d82db1
--- /dev/null
+++ b/lib/dag.mli
@@ -0,0 +1,38 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+module type S = sig
+
+ type cluster_id
+ val string_of_cluster_id : cluster_id -> string
+
+ type node
+ type ('edge,'info) t
+
+ val empty : ('e,'i) t
+
+ val add_edge : ('e,'i) t -> node -> 'e -> node -> ('e,'i) t
+ (* raise Not_found if the node is not there *)
+ val from_node : ('e,'i) t -> node -> (node * 'e) list
+ val mem : ('e,'i) t -> node -> bool
+
+ val iter : ('e,'i) t ->
+ (node -> cluster_id option -> 'i option ->
+ (node * 'e) list -> unit) -> unit
+
+ val create_cluster : ('e,'i) t -> node list -> ('e,'i) t
+ val cluster_of : ('e,'i) t -> node -> cluster_id option
+
+ val get_info : ('e,'i) t -> node -> 'i option
+ val set_info : ('e,'i) t -> node -> 'i -> ('e,'i) t
+ val clear_info : ('e,'i) t -> node -> ('e,'i) t
+
+end
+
+module Make(OT : Map.OrderedType) : S with type node = OT.t
+