refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
authorwenzelm
Sat Aug 20 23:35:30 2011 +0200 (2011-08-20)
changeset 44338700008399ee5
parent 44337 d453faed4815
child 44339 eda6aef75939
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
src/HOL/Tools/Function/context_tree.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/General/graph.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/PIDE/document.ML
src/Pure/axclass.ML
src/Pure/sorts.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_thingol.ML
src/Tools/codegen.ML
src/Tools/nbe.ML
src/Tools/subtyping.ML
     1.1 --- a/src/HOL/Tools/Function/context_tree.ML	Sat Aug 20 22:46:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Sat Aug 20 23:35:30 2011 +0200
     1.3 @@ -205,7 +205,7 @@
     1.4          SOME _ => (T, x)
     1.5        | NONE =>
     1.6          let
     1.7 -          val (T', x') = fold fill_table (Int_Graph.imm_succs G i) (T, x)
     1.8 +          val (T', x') = Int_Graph.Keys.fold fill_table (Int_Graph.imm_succs G i) (T, x)
     1.9            val (v, x'') = f (the o Inttab.lookup T') i x'
    1.10          in
    1.11            (Inttab.update (i, v) T', x'')
    1.12 @@ -226,7 +226,7 @@
    1.13              fun sub_step lu i x =
    1.14                let
    1.15                  val (ctxt', subtree) = nth branches i
    1.16 -                val used = fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
    1.17 +                val used = Int_Graph.Keys.fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
    1.18                  val (subs, x') = traverse_help (compose ctxt ctxt') subtree used x
    1.19                  val exported_subs = map (apfst (compose ctxt')) subs (* FIXME: Right order of composition? *)
    1.20                in
    1.21 @@ -264,7 +264,7 @@
    1.22            fun sub_step lu i x =
    1.23              let
    1.24                val ((fixes, assumes), st) = nth branches i
    1.25 -              val used = map lu (Int_Graph.imm_succs deps i)
    1.26 +              val used = map lu (Int_Graph.immediate_succs deps i)
    1.27                  |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
    1.28                  |> filter_out Thm.is_reflexive
    1.29  
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 20 22:46:19 2011 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 20 23:35:30 2011 +0200
     2.3 @@ -303,7 +303,7 @@
     2.4      val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
     2.5        Termtab.update (const, consts)) consts) constss;
     2.6      fun succs consts = consts
     2.7 -      |> maps (Term_Graph.imm_succs gr)
     2.8 +      |> maps (Term_Graph.immediate_succs gr)
     2.9        |> subtract eq_cname consts
    2.10        |> map (the o Termtab.lookup mapping)
    2.11        |> distinct (eq_list eq_cname);
     3.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Aug 20 22:46:19 2011 +0200
     3.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sat Aug 20 23:35:30 2011 +0200
     3.3 @@ -211,9 +211,11 @@
     3.4  
     3.5  (* job status *)
     3.6  
     3.7 -fun ready_job task (Job list, ([], _)) = SOME (task, rev list)
     3.8 -  | ready_job task (Passive abort, ([], _)) =
     3.9 -      if is_canceled (group_of_task task) then SOME (task, [fn _ => abort ()])
    3.10 +fun ready_job task (Job list, (deps, _)) =
    3.11 +      if Task_Graph.Keys.is_empty deps then SOME (task, rev list) else NONE
    3.12 +  | ready_job task (Passive abort, (deps, _)) =
    3.13 +      if Task_Graph.Keys.is_empty deps andalso is_canceled (group_of_task task)
    3.14 +      then SOME (task, [fn _ => abort ()])
    3.15        else NONE
    3.16    | ready_job _ _ = NONE;
    3.17  
    3.18 @@ -232,7 +234,7 @@
    3.19      val (x, y, z, w) =
    3.20        Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
    3.21            (case job of
    3.22 -            Job _ => if null deps then (x + 1, y, z, w) else (x, y + 1, z, w)
    3.23 +            Job _ => if Task_Graph.Keys.is_empty deps then (x + 1, y, z, w) else (x, y + 1, z, w)
    3.24            | Running _ => (x, y, z + 1, w)
    3.25            | Passive _ => (x, y, z, w + 1)))
    3.26          jobs (0, 0, 0, 0);
    3.27 @@ -278,7 +280,7 @@
    3.28      val group = group_of_task task;
    3.29      val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups;
    3.30      val jobs' = Task_Graph.del_node task jobs;
    3.31 -    val maximal = null (Task_Graph.imm_succs jobs task);
    3.32 +    val maximal = Task_Graph.is_maximal jobs task;
    3.33    in (maximal, make_queue groups' jobs') end;
    3.34  
    3.35  
    3.36 @@ -342,7 +344,7 @@
    3.37            else
    3.38              let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
    3.39                (case ready_job task entry of
    3.40 -                NONE => ready_dep (Tasks.update (task, ()) seen) (ds @ tasks)
    3.41 +                NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks)
    3.42                | some => some)
    3.43              end;
    3.44  
     4.1 --- a/src/Pure/General/graph.ML	Sat Aug 20 22:46:19 2011 +0200
     4.2 +++ b/src/Pure/General/graph.ML	Sat Aug 20 23:35:30 2011 +0200
     4.3 @@ -7,6 +7,14 @@
     4.4  signature GRAPH =
     4.5  sig
     4.6    type key
     4.7 +  structure Keys:
     4.8 +  sig
     4.9 +    type T
    4.10 +    val is_empty: T -> bool
    4.11 +    val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a
    4.12 +    val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a
    4.13 +    val dest: T -> key list
    4.14 +  end
    4.15    type 'a T
    4.16    exception DUP of key
    4.17    exception SAME
    4.18 @@ -15,20 +23,24 @@
    4.19    val is_empty: 'a T -> bool
    4.20    val keys: 'a T -> key list
    4.21    val dest: 'a T -> (key * key list) list
    4.22 -  val get_first: (key * ('a * (key list * key list)) -> 'b option) -> 'a T -> 'b option
    4.23 -  val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
    4.24 -  val minimals: 'a T -> key list
    4.25 -  val maximals: 'a T -> key list
    4.26 +  val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
    4.27 +  val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
    4.28    val subgraph: (key -> bool) -> 'a T -> 'a T
    4.29 -  val get_entry: 'a T -> key -> key * ('a * (key list * key list))    (*exception UNDEF*)
    4.30 +  val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
    4.31    val map: (key -> 'a -> 'b) -> 'a T -> 'b T
    4.32    val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    4.33    val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    4.34    val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
    4.35 -  val imm_preds: 'a T -> key -> key list
    4.36 -  val imm_succs: 'a T -> key -> key list
    4.37 +  val imm_preds: 'a T -> key -> Keys.T
    4.38 +  val imm_succs: 'a T -> key -> Keys.T
    4.39 +  val immediate_preds: 'a T -> key -> key list
    4.40 +  val immediate_succs: 'a T -> key -> key list
    4.41    val all_preds: 'a T -> key list -> key list
    4.42    val all_succs: 'a T -> key list -> key list
    4.43 +  val minimals: 'a T -> key list
    4.44 +  val maximals: 'a T -> key list
    4.45 +  val is_minimal: 'a T -> key -> bool
    4.46 +  val is_maximal: 'a T -> key -> bool
    4.47    val strong_conn: 'a T -> key list list
    4.48    val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
    4.49    val default_node: key * 'a -> 'a T -> 'a T
    4.50 @@ -59,27 +71,38 @@
    4.51  (* keys *)
    4.52  
    4.53  type key = Key.key;
    4.54 -
    4.55  val eq_key = is_equal o Key.ord;
    4.56  
    4.57 -val member_key = member eq_key;
    4.58 -val remove_key = remove eq_key;
    4.59 +structure Table = Table(Key);
    4.60 +
    4.61 +structure Keys =
    4.62 +struct
    4.63  
    4.64 +abstype T = Keys of unit Table.table
    4.65 +with
    4.66  
    4.67 -(* tables and sets of keys *)
    4.68 +val empty = Keys Table.empty;
    4.69 +fun is_empty (Keys tab) = Table.is_empty tab;
    4.70  
    4.71 -structure Table = Table(Key);
    4.72 -type keys = unit Table.table;
    4.73 +fun member (Keys tab) = Table.defined tab;
    4.74 +fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab);
    4.75 +fun remove x (Keys tab) = Keys (Table.delete_safe x tab);
    4.76 +
    4.77 +fun fold f (Keys tab) = Table.fold (f o #1) tab;
    4.78 +fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab;
    4.79  
    4.80 -val empty_keys = Table.empty: keys;
    4.81 +fun make xs = Basics.fold insert xs empty;
    4.82 +fun dest keys = fold_rev cons keys [];
    4.83  
    4.84 -fun member_keys tab = Table.defined (tab: keys);
    4.85 -fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
    4.86 +fun filter P keys = fold (fn x => P x ? insert x) keys empty;
    4.87 +
    4.88 +end;
    4.89 +end;
    4.90  
    4.91  
    4.92  (* graphs *)
    4.93  
    4.94 -datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
    4.95 +datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table;
    4.96  
    4.97  exception DUP = Table.DUP;
    4.98  exception UNDEF = Table.UNDEF;
    4.99 @@ -88,18 +111,16 @@
   4.100  val empty = Graph Table.empty;
   4.101  fun is_empty (Graph tab) = Table.is_empty tab;
   4.102  fun keys (Graph tab) = Table.keys tab;
   4.103 -fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
   4.104 +fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
   4.105  
   4.106  fun get_first f (Graph tab) = Table.get_first f tab;
   4.107  fun fold_graph f (Graph tab) = Table.fold f tab;
   4.108  
   4.109 -fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
   4.110 -fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G [];
   4.111 -
   4.112  fun subgraph P G =
   4.113    let
   4.114      fun subg (k, (i, (preds, succs))) =
   4.115 -      if P k then Table.update (k, (i, (filter P preds, filter P succs))) else I;
   4.116 +      if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs)))
   4.117 +      else I;
   4.118    in Graph (fold_graph subg G Table.empty) end;
   4.119  
   4.120  fun get_entry (Graph tab) x =
   4.121 @@ -132,20 +153,29 @@
   4.122  fun reachable next xs =
   4.123    let
   4.124      fun reach x (rs, R) =
   4.125 -      if member_keys R x then (rs, R)
   4.126 -      else fold reach (next x) (rs, insert_keys x R) |>> cons x;
   4.127 +      if Keys.member R x then (rs, R)
   4.128 +      else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
   4.129      fun reachs x (rss, R) =
   4.130        reach x ([], R) |>> (fn rs => rs :: rss);
   4.131 -  in fold reachs xs ([], empty_keys) end;
   4.132 +  in fold reachs xs ([], Keys.empty) end;
   4.133  
   4.134  (*immediate*)
   4.135  fun imm_preds G = #1 o #2 o #2 o get_entry G;
   4.136  fun imm_succs G = #2 o #2 o #2 o get_entry G;
   4.137  
   4.138 +fun immediate_preds G = Keys.dest o imm_preds G;
   4.139 +fun immediate_succs G = Keys.dest o imm_succs G;
   4.140 +
   4.141  (*transitive*)
   4.142  fun all_preds G = flat o #1 o reachable (imm_preds G);
   4.143  fun all_succs G = flat o #1 o reachable (imm_succs G);
   4.144  
   4.145 +(*minimal and maximal elements*)
   4.146 +fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G [];
   4.147 +fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
   4.148 +fun is_minimal G x = Keys.is_empty (imm_preds G x);
   4.149 +fun is_maximal G x = Keys.is_empty (imm_succs G x);
   4.150 +
   4.151  (*strongly connected components; see: David King and John Launchbury,
   4.152    "Structuring Depth First Search Algorithms in Haskell"*)
   4.153  fun strong_conn G =
   4.154 @@ -155,43 +185,44 @@
   4.155  (* nodes *)
   4.156  
   4.157  fun new_node (x, info) (Graph tab) =
   4.158 -  Graph (Table.update_new (x, (info, ([], []))) tab);
   4.159 +  Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
   4.160  
   4.161  fun default_node (x, info) (Graph tab) =
   4.162 -  Graph (Table.default (x, (info, ([], []))) tab);
   4.163 +  Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
   4.164  
   4.165  fun del_nodes xs (Graph tab) =
   4.166    Graph (tab
   4.167      |> fold Table.delete xs
   4.168      |> Table.map (fn _ => fn (i, (preds, succs)) =>
   4.169 -      (i, (fold remove_key xs preds, fold remove_key xs succs))));
   4.170 +      (i, (fold Keys.remove xs preds, fold Keys.remove xs succs))));
   4.171  
   4.172  fun del_node x (G as Graph tab) =
   4.173    let
   4.174 -    fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps)));
   4.175 +    fun del_adjacent which y =
   4.176 +      Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps)));
   4.177      val (preds, succs) = #2 (#2 (get_entry G x));
   4.178    in
   4.179      Graph (tab
   4.180        |> Table.delete x
   4.181 -      |> fold (del_adjacent apsnd) preds
   4.182 -      |> fold (del_adjacent apfst) succs)
   4.183 +      |> Keys.fold (del_adjacent apsnd) preds
   4.184 +      |> Keys.fold (del_adjacent apfst) succs)
   4.185    end;
   4.186  
   4.187  
   4.188  (* edges *)
   4.189  
   4.190 -fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
   4.191 +fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
   4.192  
   4.193  fun add_edge (x, y) G =
   4.194    if is_edge G (x, y) then G
   4.195    else
   4.196 -    G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
   4.197 -      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
   4.198 +    G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs)))
   4.199 +      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs)));
   4.200  
   4.201  fun del_edge (x, y) G =
   4.202    if is_edge G (x, y) then
   4.203 -    G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs)))
   4.204 -      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs)))
   4.205 +    G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs)))
   4.206 +      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs)))
   4.207    else G;
   4.208  
   4.209  fun diff_edges G1 G2 =
   4.210 @@ -203,7 +234,7 @@
   4.211  
   4.212  (* join and merge *)
   4.213  
   4.214 -fun no_edges (i, _) = (i, ([], []));
   4.215 +fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
   4.216  
   4.217  fun join f (G1 as Graph tab1, G2 as Graph tab2) =
   4.218    let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
   4.219 @@ -227,11 +258,11 @@
   4.220      fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z));
   4.221      fun irreds [] xs' = xs'
   4.222        | irreds (x :: xs) xs' =
   4.223 -          if not (member_keys X x) orelse eq_key (x, z) orelse member_key path x orelse
   4.224 +          if not (Keys.member X x) orelse eq_key (x, z) orelse member eq_key path x orelse
   4.225              exists (red x) xs orelse exists (red x) xs'
   4.226            then irreds xs xs'
   4.227            else irreds xs (x :: xs');
   4.228 -  in irreds (imm_preds G z) [] end;
   4.229 +  in irreds (immediate_preds G z) [] end;
   4.230  
   4.231  fun irreducible_paths G (x, y) =
   4.232    let
   4.233 @@ -249,8 +280,8 @@
   4.234      val (_, X) = reachable (imm_succs G) [x];
   4.235      fun paths path z =
   4.236        if not (null path) andalso eq_key (x, z) then [z :: path]
   4.237 -      else if member_keys X z andalso not (member_key path z)
   4.238 -      then maps (paths (z :: path)) (imm_preds G z)
   4.239 +      else if Keys.member X z andalso not (member eq_key path z)
   4.240 +      then maps (paths (z :: path)) (immediate_preds G z)
   4.241        else [];
   4.242    in paths [] y end;
   4.243  
   4.244 @@ -297,7 +328,7 @@
   4.245      val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
   4.246        let
   4.247          val a = get_node G x;
   4.248 -        val deps = imm_preds G x |> map (fn y =>
   4.249 +        val deps = immediate_preds G x |> map (fn y =>
   4.250            (case Table.lookup tab y of
   4.251              SOME b => (y, b)
   4.252            | NONE => raise DEP (x, y)));
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 20 22:46:19 2011 +0200
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Aug 20 23:35:30 2011 +0200
     5.3 @@ -407,7 +407,7 @@
     5.4      val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
     5.5      val classes = Sorts.classes_of algebra;
     5.6      fun entry (c, (i, (_, cs))) =
     5.7 -      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs,
     5.8 +      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
     5.9              dir = "", unfold = true, path = ""});
    5.10      val gr =
    5.11        Graph.fold (cons o entry) classes []
     6.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 20 22:46:19 2011 +0200
     6.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 20 23:35:30 2011 +0200
     6.3 @@ -145,7 +145,8 @@
     6.4                |> default_node name
     6.5                |> fold default_node parents;
     6.6              val nodes2 = nodes1
     6.7 -              |> fold (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
     6.8 +              |> Graph.Keys.fold
     6.9 +                  (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    6.10              val (header', nodes3) =
    6.11                (header, Graph.add_deps_acyclic (name, parents) nodes2)
    6.12                  handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
     7.1 --- a/src/Pure/axclass.ML	Sat Aug 20 22:46:19 2011 +0200
     7.2 +++ b/src/Pure/axclass.ML	Sat Aug 20 23:35:30 2011 +0200
     7.3 @@ -220,7 +220,9 @@
     7.4        in ((c1_pred, c2_succ), th') end;
     7.5  
     7.6      val new_classrels =
     7.7 -      Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
     7.8 +      Library.map_product pair
     7.9 +        (c1 :: Graph.immediate_preds classes c1)
    7.10 +        (c2 :: Graph.immediate_succs classes c2)
    7.11        |> filter_out ((op =) orf Symreltab.defined classrels)
    7.12        |> map gen_classrel;
    7.13      val needed = not (null new_classrels);
     8.1 --- a/src/Pure/sorts.ML	Sat Aug 20 22:46:19 2011 +0200
     8.2 +++ b/src/Pure/sorts.ML	Sat Aug 20 23:35:30 2011 +0200
     8.3 @@ -128,7 +128,7 @@
     8.4  
     8.5  fun all_classes (Algebra {classes, ...}) = Graph.all_preds classes (Graph.maximals classes);
     8.6  
     8.7 -val super_classes = Graph.imm_succs o classes_of;
     8.8 +val super_classes = Graph.immediate_succs o classes_of;
     8.9  
    8.10  
    8.11  (* class relations *)
    8.12 @@ -413,7 +413,7 @@
    8.13        end;
    8.14  
    8.15      fun derive (_, []) = []
    8.16 -      | derive (T as Type (a, Us), S) =
    8.17 +      | derive (Type (a, Us), S) =
    8.18            let
    8.19              val Ss = mg_domain algebra a S;
    8.20              val dom = map2 (fn U => fn S => derive (U, S) ~~ S) Us Ss;
     9.1 --- a/src/Tools/Code/code_namespace.ML	Sat Aug 20 22:46:19 2011 +0200
     9.2 +++ b/src/Tools/Code/code_namespace.ML	Sat Aug 20 23:35:30 2011 +0200
     9.3 @@ -86,7 +86,8 @@
     9.4        end;
     9.5      val proto_program = Graph.empty
     9.6        |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
     9.7 -      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
     9.8 +      |> Graph.fold (fn (name, (_, (_, names))) =>
     9.9 +          Graph.Keys.fold (add_dependency name) names) program;
    9.10  
    9.11      (* name declarations and statement modifications *)
    9.12      fun declare name (base, stmt) (gr, nsp) = 
    9.13 @@ -191,7 +192,8 @@
    9.14        in (map_module name_fragments_common o apsnd) add_edge end;
    9.15      val proto_program = empty_program
    9.16        |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
    9.17 -      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
    9.18 +      |> Graph.fold (fn (name, (_, (_, names))) =>
    9.19 +          Graph.Keys.fold (add_dependency name) names) program;
    9.20  
    9.21      (* name declarations, data and statement modifications *)
    9.22      fun make_declarations nsps (data, nodes) =
    10.1 --- a/src/Tools/Code/code_preproc.ML	Sat Aug 20 22:46:19 2011 +0200
    10.2 +++ b/src/Tools/Code/code_preproc.ML	Sat Aug 20 23:35:30 2011 +0200
    10.3 @@ -309,7 +309,7 @@
    10.4      val diff_classes = new_classes |> subtract (op =) old_classes;
    10.5    in if null diff_classes then vardeps_data
    10.6    else let
    10.7 -    val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k;
    10.8 +    val c_ks = Vargraph.immediate_succs (fst vardeps_data) c_k |> insert (op =) c_k;
    10.9    in
   10.10      vardeps_data
   10.11      |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
    11.1 --- a/src/Tools/Code/code_scala.ML	Sat Aug 20 22:46:19 2011 +0200
    11.2 +++ b/src/Tools/Code/code_scala.ML	Sat Aug 20 23:35:30 2011 +0200
    11.3 @@ -321,7 +321,7 @@
    11.4           of Code_Thingol.Classinst _ => true
    11.5            | _ => false;
    11.6          val implicits = filter (is_classinst o Graph.get_node program)
    11.7 -          (Graph.imm_succs program name);
    11.8 +          (Graph.immediate_succs program name);
    11.9        in union (op =) implicits end;
   11.10      fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE
   11.11        | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
    12.1 --- a/src/Tools/Code/code_thingol.ML	Sat Aug 20 22:46:19 2011 +0200
    12.2 +++ b/src/Tools/Code/code_thingol.ML	Sat Aug 20 23:35:30 2011 +0200
    12.3 @@ -921,7 +921,7 @@
    12.4        let
    12.5          val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
    12.6            Graph.get_node program1 Term.dummy_patternN;
    12.7 -        val deps = Graph.imm_succs program1 Term.dummy_patternN;
    12.8 +        val deps = Graph.immediate_succs program1 Term.dummy_patternN;
    12.9          val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
   12.10          val deps_all = Graph.all_succs program2 deps;
   12.11          val program3 = Graph.subgraph (member (op =) deps_all) program2;
   12.12 @@ -1010,7 +1010,7 @@
   12.13      val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
   12.14        Symtab.update (const, consts)) consts) constss;
   12.15      fun succs consts = consts
   12.16 -      |> maps (Graph.imm_succs eqngr)
   12.17 +      |> maps (Graph.immediate_succs eqngr)
   12.18        |> subtract (op =) consts
   12.19        |> map (the o Symtab.lookup mapping)
   12.20        |> distinct (op =);
    13.1 --- a/src/Tools/codegen.ML	Sat Aug 20 22:46:19 2011 +0200
    13.2 +++ b/src/Tools/codegen.ML	Sat Aug 20 23:35:30 2011 +0200
    13.3 @@ -756,7 +756,7 @@
    13.4            let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
    13.5              if a = a' then Option.map (pair x)
    13.6                (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr)
    13.7 -                (Graph.imm_succs gr x))
    13.8 +                (Graph.immediate_succs gr x))
    13.9              else NONE) code
   13.10            in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
   13.11        | string_of_cycle _ = ""
   13.12 @@ -767,7 +767,7 @@
   13.13          val mod_gr = fold_rev Graph.add_edge_acyclic
   13.14            (maps (fn (s, (_, module, _)) => map (pair module)
   13.15              (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr)
   13.16 -              (Graph.imm_succs gr s)))) code)
   13.17 +              (Graph.immediate_succs gr s)))) code)
   13.18            (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
   13.19          val modules' =
   13.20            rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
    14.1 --- a/src/Tools/nbe.ML	Sat Aug 20 22:46:19 2011 +0200
    14.2 +++ b/src/Tools/nbe.ML	Sat Aug 20 23:35:30 2011 +0200
    14.3 @@ -471,7 +471,7 @@
    14.4        then (nbe_program, (maxidx, idx_tab))
    14.5        else (nbe_program, (maxidx, idx_tab))
    14.6          |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name),
    14.7 -          Graph.imm_succs program name)) names);
    14.8 +          Graph.immediate_succs program name)) names);
    14.9    in
   14.10      fold_rev add_stmts (Graph.strong_conn program)
   14.11    end;
    15.1 --- a/src/Tools/subtyping.ML	Sat Aug 20 22:46:19 2011 +0200
    15.2 +++ b/src/Tools/subtyping.ML	Sat Aug 20 23:35:30 2011 +0200
    15.3 @@ -171,10 +171,10 @@
    15.4  fun get_succs G T = Typ_Graph.all_succs G [T];
    15.5  fun maybe_new_typnode T G = perhaps (try (Typ_Graph.new_node (T, ()))) G;
    15.6  fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G;
    15.7 -fun new_imm_preds G Ts =
    15.8 -  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.imm_preds G) Ts));
    15.9 -fun new_imm_succs G Ts =
   15.10 -  subtract op= Ts (distinct (op =) (maps (Typ_Graph.imm_succs G) Ts));
   15.11 +fun new_imm_preds G Ts =  (* FIXME inefficient *)
   15.12 +  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_preds G) Ts));
   15.13 +fun new_imm_succs G Ts =  (* FIXME inefficient *)
   15.14 +  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_succs G) Ts));
   15.15  
   15.16  
   15.17  (* Graph shortcuts *)
   15.18 @@ -406,7 +406,7 @@
   15.19      (*styps stands either for supertypes or for subtypes of a type T
   15.20        in terms of the subtype-relation (excluding T itself)*)
   15.21      fun styps super T =
   15.22 -      (if super then Graph.imm_succs else Graph.imm_preds) coes_graph T
   15.23 +      (if super then Graph.immediate_succs else Graph.immediate_preds) coes_graph T
   15.24          handle Graph.UNDEF _ => [];
   15.25  
   15.26      fun minmax sup (T :: Ts) =