liquid-fixpoint-0.1.0.0: external/ocamlgraph/src/sig.mli
(**************************************************************************)
(* *)
(* Ocamlgraph: a generic graph library for OCaml *)
(* Copyright (C) 2004-2007 *)
(* Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(* $Id: sig.mli,v 1.21 2006-05-12 14:07:16 filliatr Exp $ *)
(** Signatures for graph implementations *)
(** {2 Signatures for graph implementations} *)
(** Interface for vertices *)
module type VERTEX = sig
(** Vertices are [COMPARABLE] *)
type t
val compare : t -> t -> int
val hash : t -> int
val equal : t -> t -> bool
(** Vertices are labeled. *)
type label
val create : label -> t
val label : t -> label
end
(** Interface for edges *)
module type EDGE = sig
(** Edges are [ORDERED]. *)
type t
val compare : t -> t -> int
(** Edges are directed. *)
type vertex
val src : t -> vertex
val dst : t -> vertex
(** Edges are labeled. *)
type label
val create : vertex -> label -> vertex -> t
(** [create v1 l v2] creates an edge from [v1] to [v2] with label [l] *)
val label : t -> label
end
(** Common interface for all graph implementations *)
module type G = sig
(** {2 Graph structure} *)
(** Abstract type of graphs *)
type t
(** Vertices have type [V.t] and are labeled with type [V.label]
(note that an implementation may identify the vertex with its
label) *)
module V : VERTEX
type vertex = V.t
(** Edges have type [E.t] and are labeled with type [E.label].
[src] (resp. [dst]) returns the origin (resp. the destination) of a
given edge. *)
module E : EDGE with type vertex = vertex
type edge = E.t
(** Is this an implementation of directed graphs? *)
val is_directed : bool
(** {2 Size functions} *)
val is_empty : t -> bool
val nb_vertex : t -> int
val nb_edges : t -> int
(** Degree of a vertex *)
val out_degree : t -> vertex -> int
(** [out_degree g v] returns the out-degree of [v] in [g].
@raise Invalid_argument if [v] is not in [g]. *)
val in_degree : t -> vertex -> int
(** [in_degree g v] returns the in-degree of [v] in [g].
@raise Invalid_argument if [v] is not in [g]. *)
(** {2 Membership functions} *)
val mem_vertex : t -> vertex -> bool
val mem_edge : t -> vertex -> vertex -> bool
val mem_edge_e : t -> edge -> bool
val find_edge : t -> vertex -> vertex -> edge
(** [find_edge g v1 v2] returns the edge from [v1] to [v2] if it exists.
The behaviour is unspecified if [g] has several edges from [v1] to [v2].
@raise Not_found if no such edge exists. *)
(** {2 Successors and predecessors} *)
val succ : t -> vertex -> vertex list
(** [succ g v] returns the successors of [v] in [g].
@raise Invalid_argument if [v] is not in [g]. *)
val pred : t -> vertex -> vertex list
(** [pred g v] returns the predecessors of [v] in [g].
@raise Invalid_argument if [v] is not in [g]. *)
(** Labeled edges going from/to a vertex *)
val succ_e : t -> vertex -> edge list
(** [succ_e g v] returns the edges going from [v] in [g].
@raise Invalid_argument if [v] is not in [g]. *)
val pred_e : t -> vertex -> edge list
(** [pred_e g v] returns the edges going to [v] in [g].
@raise Invalid_argument if [v] is not in [g]. *)
(** {2 Graph iterators} *)
(** iter/fold on all vertices/edges of a graph *)
val iter_vertex : (vertex -> unit) -> t -> unit
val iter_edges : (vertex -> vertex -> unit) -> t -> unit
val fold_vertex : (vertex -> 'a -> 'a) -> t -> 'a -> 'a
val fold_edges : (vertex -> vertex -> 'a -> 'a) -> t -> 'a -> 'a
(** map iterator on vertex *)
val map_vertex : (vertex -> vertex) -> t -> t
(** iter/fold on all labeled edges of a graph *)
val iter_edges_e : (edge -> unit) -> t -> unit
val fold_edges_e : (edge -> 'a -> 'a) -> t -> 'a -> 'a
(** {2 Vertex iterators}
Each iterator [iterator f v g] iters [f] to the successors/predecessors
of [v] in the graph [g] and raises [Invalid_argument] if [v] is not in
[g]. *)
(** iter/fold on all successors/predecessors of a vertex. *)
val iter_succ : (vertex -> unit) -> t -> vertex -> unit
val iter_pred : (vertex -> unit) -> t -> vertex -> unit
val fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
val fold_pred : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
(** iter/fold on all edges going from/to a vertex. *)
val iter_succ_e : (edge -> unit) -> t -> vertex -> unit
val fold_succ_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
val iter_pred_e : (edge -> unit) -> t -> vertex -> unit
val fold_pred_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
end
(** Persistent (i.e. immutable) implementation *)
module type P = sig
include G
val empty : t
(** The empty graph. *)
val add_vertex : t -> vertex -> t
(** [add_vertex g v] adds the vertex [v] from the graph [g].
Just return [g] if [v] is already in [g]. *)
val remove_vertex : t -> vertex -> t
(** [remove g v] removes the vertex [v] from the graph [g]
(and all the edges going from [v] in [g]).
Just return [g] if [v] is not in [g]. *)
val add_edge : t -> vertex -> vertex -> t
(** [add_edge g v1 v2] adds an edge from the vertex [v1] to the vertex [v2]
in the graph [g].
Add also [v1] (resp. [v2]) in [g] if [v1] (resp. [v2]) is not in [g].
Just return [g] if this edge is already in [g]. *)
val add_edge_e : t -> edge -> t
(** [add_edge_e g e] adds the edge [e] in the graph [g].
Add also [E.src e] (resp. [E.dst e]) in [g] if [E.src e] (resp. [E.dst
e]) is not in [g].
Just return [g] if [e] is already in [g]. *)
val remove_edge : t -> vertex -> vertex -> t
(** [remove_edge g v1 v2] removes the edge going from [v1] to [v2] from the
graph [g]. If the graph is labelled, all the edges going from [v1] to
[v2] are removed from [g].
Just return [g] if this edge is not in [g].
@raise Invalid_argument if [v1] or [v2] are not in [g]. *)
val remove_edge_e : t -> edge -> t
(** [remove_edge_e g e] removes the edge [e] from the graph [g].
Just return [g] if [e] is not in [g].
@raise Invalid_argument if [E.src e] or [E.dst e] are not in [g]. *)
end
(** Imperative (i.e. mutable) implementation *)
module type I = sig
include G
val create : ?size:int -> unit -> t
(** [create ()] returns an empty graph. Optionally, a size can be
given, which should be on the order of the expected number of
vertices that will be in the graph (for hash tables-based
implementations). The graph grows as needed, so [size] is
just an initial guess. *)
val copy : t -> t
(** [copy g] returns a copy of [g]. Vertices and edges (and eventually
marks, see module [Mark]) are duplicated. *)
val add_vertex : t -> vertex -> unit
(** [add_vertex g v] adds the vertex [v] from the graph [g].
Do nothing if [v] is already in [g]. *)
val remove_vertex : t -> vertex -> unit
(** [remove g v] removes the vertex [v] from the graph [g]
(and all the edges going from [v] in [g]).
Do nothing if [v] is not in [g]. *)
val add_edge : t -> vertex -> vertex -> unit
(** [add_edge g v1 v2] adds an edge from the vertex [v1] to the vertex [v2]
in the graph [g].
Add also [v1] (resp. [v2]) in [g] if [v1] (resp. [v2]) is not in [g].
Do nothing if this edge is already in [g]. *)
val add_edge_e : t -> edge -> unit
(** [add_edge_e g e] adds the edge [e] in the graph [g].
Add also [E.src e] (resp. [E.dst e]) in [g] if [E.src e] (resp. [E.dst
e]) is not in [g].
Do nothing if [e] is already in [g]. *)
val remove_edge : t -> vertex -> vertex -> unit
(** [remove_edge g v1 v2] removes the edge going from [v1] to [v2] from the
graph [g]. If the graph is labelled, all the edges going from [v1] to
[v2] are removed from [g].
Do nothing if this edge is not in [g].
@raise Invalid_argument if [v1] or [v2] are not in [g]. *)
val remove_edge_e : t -> edge -> unit
(** [remove_edge_e g e] removes the edge [e] from the graph [g].
Do nothing if [e] is not in [g].
@raise Invalid_argument if [E.src e] or [E.dst e] are not in [g]. *)
end
(** Imperative implementation with marks *)
module type MARK = sig
type graph
type vertex
val clear : graph -> unit
(** [clear g] sets all the marks to 0 for all the vertices of [g]. *)
val get : vertex -> int
val set : vertex -> int -> unit
end
module type IM = sig
include I
module Mark : MARK with type graph = t and type vertex = vertex
end
(** {2 Signature for ordered and hashable types} *)
module type ANY_TYPE = sig type t end
module type ORDERED_TYPE = sig type t val compare : t -> t -> int end
module type ORDERED_TYPE_DFT = sig include ORDERED_TYPE val default : t end
module type HASHABLE = sig
type t
val hash : t -> int
val equal : t -> t -> bool
end
(** Comparable = Ordered + Hashable *)
module type COMPARABLE = sig
type t
val compare : t -> t -> int
val hash : t -> int
val equal : t -> t -> bool
end