Library DigraphInterface

Require Import FMaps.
Require Import Directed_edges.
Require Import FMapAVL.
Require Import MapFacts.
Require Import Labels.

Module Type Directed_Graph (Vertex : OrderedType) (Lab : Labels).

Import Lab.

Module VertexMap := FMapAVL.Make Vertex.
Module Export VMapFacts := MyMapFacts VertexMap.
Module Import Edge := Directed_Edge Vertex.
Module EdgeMap := FMapAVL.Make Edge.
Module Import EMapFacts := MyMapFacts EdgeMap.

Parameter t : Type.
Parameter V : t -> VertexMap.t (option NodeLabel).
Parameter vertex_label : Vertex.t -> t -> option (option NodeLabel).
Parameter E : t -> EdgeMap.t (option EdgeLabel).
Parameter edge_label : Edge.t -> t -> option (option EdgeLabel).
Parameter successors : Vertex.t -> t -> VertexMap.t (option EdgeLabel).
Parameter predecessors : Vertex.t -> t -> VertexMap.t (option EdgeLabel).
Parameter link : t -> Vertex.t -> Vertex.t -> option (option EdgeLabel).

Parameter vertex_label_spec : forall v g,
vertex_label v g = VertexMap.find v (V g).

Parameter edge_label_spec : forall e g,
edge_label e g = EdgeMap.find e (E g).

Parameter In_graph_vertex : Vertex.t -> t -> Prop.
Parameter In_graph_labeled_vertex : Vertex.t -> t -> option NodeLabel -> Prop.
Parameter In_graph_edge : Edge.t -> t -> Prop.
Parameter In_graph_labeled_edge : Edge.t -> t -> option EdgeLabel -> Prop.

Parameter In_graph_vertex_spec : forall v g,
In_graph_vertex v g <-> VertexMap.In v (V g).

Parameter In_graph_labeled_vertex_spec : forall v g l,
In_graph_labeled_vertex v g l <-> VertexMap.MapsTo v l (V g).

Add Morphism In_graph_vertex : In_graph_vertex_m.
Add Morphism In_graph_labeled_vertex : In_graph_labeled_vertex_m.

Parameter In_graph_edge_spec : forall e g,
In_graph_edge e g <-> EdgeMap.In e (E g).

Opaque Edge.t.

Parameter In_graph_labeled_edge_spec : forall e g l,
In_graph_labeled_edge e g l <-> EdgeMap.MapsTo e l (E g).

Add Morphism In_graph_edge : In_graph_edge_m.
Add Morphism In_graph_labeled_edge : In_graph_labeled_edge_m.

Parameter link_edge_equiv : forall v1 v2 g l,
link g v1 v2 = Some l <-> In_graph_labeled_edge (v1,v2) g l.

Parameter mapsto_edge_equiv_succ : forall v1 v2 g l,
VertexMap.MapsTo v2 l (successors v1 g) <-> In_graph_labeled_edge (v1,v2) g l.

Parameter mapsto_edge_equiv_pred : forall v1 v2 g l,
VertexMap.MapsTo v1 l (predecessors v2 g) <-> In_graph_labeled_edge (v1,v2) g l.


Parameter In_graph_edge_in_ext : forall e g,
In_graph_edge e g -> In_graph_vertex (fst_end e) g /\
                                   In_graph_vertex (snd_end e) g.

Parameter fold_edges : forall (A : Type), (t -> Edge.t -> (option EdgeLabel) -> A -> A) -> t -> A -> A.
Parameter fold_vertices : forall (A : Type), (t -> Vertex.t -> (option NodeLabel) -> A -> A) -> t -> A -> A.
Parameter fold_succ : forall (A : Type), (t -> Vertex.t -> Vertex.t -> (option EdgeLabel) -> A -> A) -> Vertex.t -> t -> A -> A.
Parameter fold_pred : forall (A : Type), (t -> Vertex.t -> Vertex.t -> (option EdgeLabel) -> A -> A) -> Vertex.t -> t -> A -> A.
Parameter fold_succ_ne : forall (A : Type), (t -> Vertex.t -> Vertex.t -> (option EdgeLabel) -> A -> A) -> Vertex.t -> t -> A -> A.
Parameter fold_pred_ne : forall (A : Type), (t -> Vertex.t -> Vertex.t -> (option EdgeLabel) -> A -> A) -> Vertex.t -> t -> A -> A.

Implicit Arguments fold_edges [A].
Implicit Arguments fold_vertices [A].
Implicit Arguments fold_succ [A].
Implicit Arguments fold_pred [A].
Implicit Arguments fold_succ_ne [A].
Implicit Arguments fold_pred_ne [A].

Parameter fold_vertices_spec : forall (A : Type) f g (a : A),
fold_vertices f g a = VertexMap.fold (f g) (V g) a.

Parameter fold_edges_spec : forall (A : Type) f g (a : A),
fold_edges f g a = EdgeMap.fold (f g) (E g) a.

Parameter fold_succ_spec : forall (A : Type) f v g (a : A),
fold_succ f v g a = VertexMap.fold (f g v) (successors v g) a.

Parameter fold_pred_spec : forall (A : Type) f v g (a : A),
fold_pred f v g a = VertexMap.fold (f g v) (predecessors v g) a.

Parameter fold_succ_ne_spec : forall (A : Type) f v g (a : A),
fold_succ_ne f v g a = VertexMap.fold (f g v) (VertexMap.remove v (successors v g)) a.

Parameter fold_pred_ne_spec : forall (A : Type) f v g (a : A),
fold_pred_ne f v g a = VertexMap.fold (f g v) (VertexMap.remove v (predecessors v g)) a.

End Directed_Graph.