# HG changeset patch
# User wenzelm
# Date 916690107 -3600
# Node ID ec6092b0599d7f36a322e777646023c372d9781e
# Parent  4f224fd882f9bf8905d389693c7c29755c0f3ee4
added General/graph.ML: generic direct graphs;

diff -r 4f224fd882f9 -r ec6092b0599d src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Fri Jan 15 16:13:31 1999 +0100
+++ b/src/Pure/General/ROOT.ML	Mon Jan 18 21:08:27 1999 +0100
@@ -5,6 +5,7 @@
 *)
 
 use "table.ML";
+use "graph.ML";
 use "object.ML";
 use "seq.ML";
 use "name_space.ML";
diff -r 4f224fd882f9 -r ec6092b0599d src/Pure/General/graph.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/graph.ML	Mon Jan 18 21:08:27 1999 +0100
@@ -0,0 +1,153 @@
+(*  Title:      Pure/General/graph.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Directed graphs.
+*)
+
+signature GRAPH =
+sig
+  type key
+  type 'a T
+  exception UNDEFINED of key
+  exception DUPLICATE of key
+  exception CYCLES of key list list
+  val empty: 'a T
+  val map : ('a -> 'b) -> 'a T -> 'b T
+  val foldl : ('a * (key * ('b * (key list * key list))) -> 'a) -> 'a * 'b T -> 'a
+  val info: 'a T -> key -> 'a
+  val map_info: ('a -> 'a) -> key -> 'a T -> 'a T
+  val preds: 'a T -> key -> key list
+  val succs: 'a T -> key -> key list
+  val all_preds: 'a T -> key list -> key list
+  val all_succs: 'a T -> key list -> key list
+  val find_paths: 'a T -> key * key -> key list list
+  val add_node: key * 'a -> 'a T -> 'a T
+  val add_edge: key * key -> 'a T -> 'a T
+  val add_edge_acyclic: key * key -> 'a T -> 'a T
+  val derive_node: key * 'a -> key list -> 'a T -> 'a T
+end;
+
+functor GraphFun(Key: KEY): GRAPH =
+struct
+
+
+(* keys *)
+
+type key = Key.key;
+
+val eq_key = equal EQUAL o Key.ord;
+
+infix mem_key;
+val op mem_key = gen_mem eq_key;
+
+infix ins_key;
+val op ins_key = gen_ins eq_key;
+
+
+(* tables and sets of keys *)
+
+structure Table = TableFun(Key);
+type keys = unit Table.table;
+
+infix mem_keys;
+fun x mem_keys tab = is_some (Table.lookup (tab: keys, x));
+
+infix ins_keys;
+fun x ins_keys tab = if x mem_keys tab then tab else Table.update ((x, ()), tab);
+
+val empty_keys = Table.empty: keys;
+fun make_keys xs = foldl (fn (tab, x) => x ins_keys tab) (empty_keys, xs);
+fun dest_keys tab = rev (Table.foldl (fn (xs, (x, ())) => x :: xs) ([], tab: keys));
+
+
+(* datatype of graphs *)
+
+datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
+
+exception UNDEFINED of key;
+exception DUPLICATE of key;
+exception CYCLES of key list list;
+
+
+(* basic operations *)
+
+fun map_graph f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
+fun foldl_graph f (x, Graph tab) = Table.foldl f (x, tab);
+
+val empty = Graph Table.empty;
+
+fun get_node (Graph tab) x =
+  (case Table.lookup (tab, x) of
+    Some node => node
+  | None => raise UNDEFINED x);
+
+fun info G = #1 o get_node G;
+fun preds G = #1 o #2 o get_node G;
+fun succs G = #2 o #2 o get_node G;
+
+fun map_node f x (G as Graph tab) =
+  let val node = get_node G x
+  in Graph (Table.update ((x, f node), tab)) end;
+
+fun map_info f = map_node (fn (info, ps) => (f info, ps));
+
+
+(* reachable nodes *)
+
+fun reachable_keys next xs =
+  let
+    fun reach (R, x) =
+      if x mem_keys R then R
+      else reachs (x ins_keys R, next x)
+    and reachs R_xs = foldl reach R_xs;
+  in reachs (empty_keys, xs) end;
+
+val reachable = dest_keys oo reachable_keys;
+
+fun all_preds G = reachable (preds G);
+fun all_succs G = reachable (succs G);
+
+
+(* find_paths *)
+
+fun find_paths G (x, y) =
+  let
+    val X = reachable_keys (succs G) [x];
+    fun paths ps p =
+      if eq_key (p, x) then [p :: ps]
+      else flat (map (paths (p :: ps))
+        (filter (fn pp => pp mem_keys X andalso not (pp mem_key ps)) (preds G p)));
+  in if y mem_keys X then (paths [] y) else [] end;
+
+
+(* build graphs *)
+
+fun add_node (x, info) (Graph tab) =
+  Graph (Table.update_new ((x, (info, ([], []))), tab)
+    handle Table.DUP key => raise DUPLICATE key);
+
+fun add_edge (x, y) G =
+  (get_node G x; get_node G y;
+    G |> map_node (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) x
+      |> map_node (fn (i, (preds, succs)) => (i, (x ins_key preds, succs))) y);
+
+fun add_edge_acyclic (x, y) G =
+  (case find_paths G (y, x) of
+    [] => add_edge (x, y) G
+  | cycles => raise CYCLES (map (cons x) cycles));
+
+fun derive_node (x, y) zs G =
+  foldl (fn (H, z) => add_edge_acyclic (z, x) H) (add_node (x, y) G, zs);
+
+
+(*final declarations of this structure!*)
+val map = map_graph;
+val foldl = foldl_graph;
+
+
+end;
+
+
+(*graphs indexed by strings*)
+structure Graph = GraphFun(type key = string val ord = string_ord);
diff -r 4f224fd882f9 -r ec6092b0599d src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Jan 15 16:13:31 1999 +0100
+++ b/src/Pure/IsaMakefile	Mon Jan 18 21:08:27 1999 +0100
@@ -23,7 +23,7 @@
 
 Pure: $(OUT)/Pure
 
-$(OUT)/Pure: General/ROOT.ML General/file.ML General/history.ML \
+$(OUT)/Pure: General/ROOT.ML General/file.ML General/graph.ML General/history.ML \
   General/name_space.ML General/object.ML General/path.ML \
   General/position.ML General/pretty.ML General/scan.ML General/seq.ML \
   General/source.ML General/symbol.ML General/table.ML Isar/ROOT.ML \