1(*
2 *  gr.sig  --  definition of graph interfaces
3 *
4 *  COPYRIGHT (c) 1997 by Martin Erwig.  See COPYRIGHT file for details.
5 *)
6
7(*
8   Hierarchy of Interfaces/Signatures for Directed Graphs
9
10
11             GRAPH_NODE       GRAPH_EXCEPTIONS
12               |                |
13               |                |
14     [UNLAB]_GRAPH_TYPES        |
15               |                |
16               |                |
17               `-------.--------
18                       |
19                       |
20             [UNLAB]_GRAPH = [UNLAB]_STATIC_GRAPH
21                       |
22                       |
23     [UNLAB]_BOUNDED_GRAPH
24
25*)
26
27
28
29(* shared definitions *)
30
31signature GRAPH_NODE =
32sig
33  type node = int
34end
35
36
37signature GRAPH_EXCEPTIONS =
38sig
39  exception Node
40  exception Edge
41  exception NotImplemented
42end
43
44
45
46(* labeled graphs *)
47
48signature GRAPH_TYPES =
49sig
50  include GRAPH_NODE
51  type ('a,'b) graph
52  type 'b out             = ('b * node) list
53  type ('a,'b) adj        = 'a * 'b out
54  type ('a,'b) context    = 'b out * node * 'a * 'b out
55  type ('a,'b) decomp     = ('a,'b) context * ('a,'b) graph
56  type ('a,'b) fwd_decomp = ('a,'b) adj * ('a,'b) graph
57end
58
59
60signature GRAPH =
61sig
62  include GRAPH_EXCEPTIONS
63  include GRAPH_TYPES
64
65  val empty       : ('a,'b) graph
66  val embed       : ('a,'b) context * ('a,'b) graph -> ('a,'b) graph
67  val match       : node * ('a,'b) graph -> ('a,'b) decomp
68  val matchFwd    : node * ('a,'b) graph -> ('a,'b) fwd_decomp
69  val matchAny    : ('a,'b) graph -> ('a,'b) decomp
70  val matchAnyFwd : ('a,'b) graph -> ('a,'b) fwd_decomp
71  (*
72  val matchOrd    : node * ''b list * ''b list * ('a,''b) graph -> ('a,''b) decomp
73  val matchOrdFwd : node * ''b list * ('a,''b) graph -> ('a,''b) fwd_decomp
74  *)
75  val context     : node * ('a,'b) graph -> ('a,'b) context
76  val fwd         : node * ('a,'b) graph -> ('a,'b) adj
77  val bwd         : node * ('a,'b) graph -> ('a,'b) adj
78  val suc         : node * ('a,'b) graph -> node list
79  val pred        : node * ('a,'b) graph -> node list
80  val ufold       : (('a,'b) context * 'c -> 'c) -> 'c -> ('a,'b) graph -> 'c
81  val gfold       : (('a,'b) context -> node list) -> ('a * 'c -> 'd) ->
82                    ('d * 'c -> 'c) -> 'c -> node list -> ('a,'b) graph -> 'c
83  val nodes       : ('a,'b) graph -> node list
84  val labNodes    : ('a,'b) graph -> (node * 'a) list
85  val noNodes     : ('a,'b) graph -> int
86  val isEmpty     : ('a,'b) graph -> bool
87  val newNodes    : int -> ('a,'b) graph -> node list
88  val mkgr        : 'a list * (node * node * 'b) list -> ('a,'b) graph
89  val adj         : ('a,'b) graph -> (node * ('a,'b) adj) list
90end
91
92
93
94(* unlabeled graphs, i.e., without edge lebels *)
95
96signature UNLAB_GRAPH_TYPES =
97sig
98  include GRAPH_NODE
99  type 'a graph
100  type 'a adj        = 'a * node list
101  type 'a context    = node list * node * 'a * node list
102  type 'a decomp     = 'a context * 'a graph
103  type 'a fwd_decomp = 'a adj * 'a graph
104end
105
106
107signature UNLAB_GRAPH =
108sig
109  include UNLAB_GRAPH_TYPES
110  include GRAPH_EXCEPTIONS
111
112  val empty       : 'a graph
113  val embed       : 'a context * 'a graph -> 'a graph
114  val match       : node * 'a graph -> 'a decomp
115  val matchFwd    : node * 'a graph -> 'a fwd_decomp
116  val matchAny    : 'a graph -> 'a decomp
117  val matchAnyFwd : 'a graph -> 'a fwd_decomp
118  val context     : node * 'a graph -> 'a context
119  val fwd         : node * 'a graph -> 'a adj
120  val bwd         : node * 'a graph -> 'a adj
121  val suc         : node * 'a graph -> node list
122  val pred        : node * 'a graph -> node list
123  val ufold       : ('a context * 'b -> 'b) -> 'b -> 'a graph -> 'b
124  val gfold       : ('a context -> node list) -> ('a * 'b -> 'c) ->
125                    ('c * 'b -> 'b) -> 'b -> node list -> 'a graph -> 'b
126  val nodes       : 'a graph -> node list
127  val labNodes    : 'a graph -> (node * 'a) list
128  val noNodes     : 'a graph -> int
129  val isEmpty     : 'a graph -> bool
130  val newNodes    : int -> 'a graph -> node list
131  val mkgr        : 'a list * (node * node) list -> 'a graph
132  val adj         : 'a graph -> (node * 'a adj) list
133end
134