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