src/portableML/Graph.sml

10   structure Keys:
25   val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T ->
27   val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
28   val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
32   val imm_preds: 'a T -> key -> Keys.T
33   val imm_succs: 'a T -> key -> Keys.T
90 structure Keys =
93 abstype T = Keys of unit Table.table
96 val empty = Keys Table.empty;
97 fun is_empty (Keys tab) = Table.is_empty tab;
99 fun member (Keys tab) = Table.defined tab;
100 fun insert x (Keys tab) =
101   Keys (Table.insert (fn _ => fn _ => true) (x, ()) tab);
102 fun remove x (Keys tab) = Keys (Table.delete_safe x tab);
104 fun fold f (Keys tab) = Table.fold (f o #1) tab;
105 fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab;
117 datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table;
153       if Keys.member R x then (rs, R)
154       else Keys.fold_rev reach (next x) (rs, Keys.insert x R) |>> cons x;
157   in foldl' reachs xs ([], Keys.empty) end;
163 fun immediate_preds G = Keys.dest o imm_preds G;
164 fun immediate_succs G = Keys.dest o imm_succs G;
190 fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G [];
191 fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
192 fun is_minimal G x = Keys.is_empty (imm_preds G x);
193 fun is_maximal G x = Keys.is_empty (imm_succs G x);
201   Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
204   Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
209       Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps)));
214       |> Keys.fold (del_adjacent apsnd) preds
215       |> Keys.fold (del_adjacent apfst) succs)
224 fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
229     G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs)))
230       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs)));
234     G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs)))
235       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs)))
240     Keys.fold (fn y => not (is_edge G2 (x, y)) ? cons (x, y)) succs) G1 [];
247 fun dest G = fold_graph (fn (x, (i, (_, succs))) => cons ((x, i), Keys.dest succs)) G [];
257 fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
290           if not (Keys.member X x) orelse eq_key x z orelse