# HG changeset patch # User wenzelm # Date 1313876130 -7200 # Node ID 700008399ee5074279b930007936155def810870 # Parent d453faed48158e563987aa68cc5781c91ae7d26b refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord; diff -r d453faed4815 -r 700008399ee5 src/HOL/Tools/Function/context_tree.ML --- a/src/HOL/Tools/Function/context_tree.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/HOL/Tools/Function/context_tree.ML Sat Aug 20 23:35:30 2011 +0200 @@ -205,7 +205,7 @@ SOME _ => (T, x) | NONE => let - val (T', x') = fold fill_table (Int_Graph.imm_succs G i) (T, x) + val (T', x') = Int_Graph.Keys.fold fill_table (Int_Graph.imm_succs G i) (T, x) val (v, x'') = f (the o Inttab.lookup T') i x' in (Inttab.update (i, v) T', x'') @@ -226,7 +226,7 @@ fun sub_step lu i x = let val (ctxt', subtree) = nth branches i - val used = fold_rev (append o lu) (Int_Graph.imm_succs deps i) u + val used = Int_Graph.Keys.fold_rev (append o lu) (Int_Graph.imm_succs deps i) u val (subs, x') = traverse_help (compose ctxt ctxt') subtree used x val exported_subs = map (apfst (compose ctxt')) subs (* FIXME: Right order of composition? *) in @@ -264,7 +264,7 @@ fun sub_step lu i x = let val ((fixes, assumes), st) = nth branches i - val used = map lu (Int_Graph.imm_succs deps i) + val used = map lu (Int_Graph.immediate_succs deps i) |> map (fn u_eq => (u_eq RS sym) RS eq_reflection) |> filter_out Thm.is_reflexive diff -r d453faed4815 -r 700008399ee5 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Aug 20 23:35:30 2011 +0200 @@ -303,7 +303,7 @@ val mapping = Termtab.empty |> fold (fn consts => fold (fn const => Termtab.update (const, consts)) consts) constss; fun succs consts = consts - |> maps (Term_Graph.imm_succs gr) + |> maps (Term_Graph.immediate_succs gr) |> subtract eq_cname consts |> map (the o Termtab.lookup mapping) |> distinct (eq_list eq_cname); diff -r d453faed4815 -r 700008399ee5 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Sat Aug 20 23:35:30 2011 +0200 @@ -211,9 +211,11 @@ (* job status *) -fun ready_job task (Job list, ([], _)) = SOME (task, rev list) - | ready_job task (Passive abort, ([], _)) = - if is_canceled (group_of_task task) then SOME (task, [fn _ => abort ()]) +fun ready_job task (Job list, (deps, _)) = + if Task_Graph.Keys.is_empty deps then SOME (task, rev list) else NONE + | ready_job task (Passive abort, (deps, _)) = + if Task_Graph.Keys.is_empty deps andalso is_canceled (group_of_task task) + then SOME (task, [fn _ => abort ()]) else NONE | ready_job _ _ = NONE; @@ -232,7 +234,7 @@ val (x, y, z, w) = Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) => (case job of - Job _ => if null deps then (x + 1, y, z, w) else (x, y + 1, z, w) + Job _ => if Task_Graph.Keys.is_empty deps then (x + 1, y, z, w) else (x, y + 1, z, w) | Running _ => (x, y, z + 1, w) | Passive _ => (x, y, z, w + 1))) jobs (0, 0, 0, 0); @@ -278,7 +280,7 @@ val group = group_of_task task; val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups; val jobs' = Task_Graph.del_node task jobs; - val maximal = null (Task_Graph.imm_succs jobs task); + val maximal = Task_Graph.is_maximal jobs task; in (maximal, make_queue groups' jobs') end; @@ -342,7 +344,7 @@ else let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in (case ready_job task entry of - NONE => ready_dep (Tasks.update (task, ()) seen) (ds @ tasks) + NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks) | some => some) end; diff -r d453faed4815 -r 700008399ee5 src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Pure/General/graph.ML Sat Aug 20 23:35:30 2011 +0200 @@ -7,6 +7,14 @@ signature GRAPH = sig type key + structure Keys: + sig + type T + val is_empty: T -> bool + val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a + val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a + val dest: T -> key list + end type 'a T exception DUP of key exception SAME @@ -15,20 +23,24 @@ val is_empty: 'a T -> bool val keys: 'a T -> key list val dest: 'a T -> (key * key list) list - val get_first: (key * ('a * (key list * key list)) -> 'b option) -> 'a T -> 'b option - val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b - val minimals: 'a T -> key list - val maximals: 'a T -> key list + val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option + val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b val subgraph: (key -> bool) -> 'a T -> 'a T - val get_entry: 'a T -> key -> key * ('a * (key list * key list)) (*exception UNDEF*) + val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T)) (*exception UNDEF*) val map: (key -> 'a -> 'b) -> 'a T -> 'b T val get_node: 'a T -> key -> 'a (*exception UNDEF*) val map_node: key -> ('a -> 'a) -> 'a T -> 'a T val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T - val imm_preds: 'a T -> key -> key list - val imm_succs: 'a T -> key -> key list + val imm_preds: 'a T -> key -> Keys.T + val imm_succs: 'a T -> key -> Keys.T + val immediate_preds: 'a T -> key -> key list + val immediate_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 minimals: 'a T -> key list + val maximals: 'a T -> key list + val is_minimal: 'a T -> key -> bool + val is_maximal: 'a T -> key -> bool val strong_conn: 'a T -> key list list val new_node: key * 'a -> 'a T -> 'a T (*exception DUP*) val default_node: key * 'a -> 'a T -> 'a T @@ -59,27 +71,38 @@ (* keys *) type key = Key.key; - val eq_key = is_equal o Key.ord; -val member_key = member eq_key; -val remove_key = remove eq_key; +structure Table = Table(Key); + +structure Keys = +struct +abstype T = Keys of unit Table.table +with -(* tables and sets of keys *) +val empty = Keys Table.empty; +fun is_empty (Keys tab) = Table.is_empty tab; -structure Table = Table(Key); -type keys = unit Table.table; +fun member (Keys tab) = Table.defined tab; +fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab); +fun remove x (Keys tab) = Keys (Table.delete_safe x tab); + +fun fold f (Keys tab) = Table.fold (f o #1) tab; +fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab; -val empty_keys = Table.empty: keys; +fun make xs = Basics.fold insert xs empty; +fun dest keys = fold_rev cons keys []; -fun member_keys tab = Table.defined (tab: keys); -fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys); +fun filter P keys = fold (fn x => P x ? insert x) keys empty; + +end; +end; (* graphs *) -datatype 'a T = Graph of ('a * (key list * key list)) Table.table; +datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table; exception DUP = Table.DUP; exception UNDEF = Table.UNDEF; @@ -88,18 +111,16 @@ val empty = Graph Table.empty; fun is_empty (Graph tab) = Table.is_empty tab; fun keys (Graph tab) = Table.keys tab; -fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab); +fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab); fun get_first f (Graph tab) = Table.get_first f tab; fun fold_graph f (Graph tab) = Table.fold f tab; -fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G []; -fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G []; - fun subgraph P G = let fun subg (k, (i, (preds, succs))) = - if P k then Table.update (k, (i, (filter P preds, filter P succs))) else I; + if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs))) + else I; in Graph (fold_graph subg G Table.empty) end; fun get_entry (Graph tab) x = @@ -132,20 +153,29 @@ fun reachable next xs = let fun reach x (rs, R) = - if member_keys R x then (rs, R) - else fold reach (next x) (rs, insert_keys x R) |>> cons x; + if Keys.member R x then (rs, R) + else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x; fun reachs x (rss, R) = reach x ([], R) |>> (fn rs => rs :: rss); - in fold reachs xs ([], empty_keys) end; + in fold reachs xs ([], Keys.empty) end; (*immediate*) fun imm_preds G = #1 o #2 o #2 o get_entry G; fun imm_succs G = #2 o #2 o #2 o get_entry G; +fun immediate_preds G = Keys.dest o imm_preds G; +fun immediate_succs G = Keys.dest o imm_succs G; + (*transitive*) fun all_preds G = flat o #1 o reachable (imm_preds G); fun all_succs G = flat o #1 o reachable (imm_succs G); +(*minimal and maximal elements*) +fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G []; +fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G []; +fun is_minimal G x = Keys.is_empty (imm_preds G x); +fun is_maximal G x = Keys.is_empty (imm_succs G x); + (*strongly connected components; see: David King and John Launchbury, "Structuring Depth First Search Algorithms in Haskell"*) fun strong_conn G = @@ -155,43 +185,44 @@ (* nodes *) fun new_node (x, info) (Graph tab) = - Graph (Table.update_new (x, (info, ([], []))) tab); + Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab); fun default_node (x, info) (Graph tab) = - Graph (Table.default (x, (info, ([], []))) tab); + Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab); fun del_nodes xs (Graph tab) = Graph (tab |> fold Table.delete xs |> Table.map (fn _ => fn (i, (preds, succs)) => - (i, (fold remove_key xs preds, fold remove_key xs succs)))); + (i, (fold Keys.remove xs preds, fold Keys.remove xs succs)))); fun del_node x (G as Graph tab) = let - fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps))); + fun del_adjacent which y = + Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps))); val (preds, succs) = #2 (#2 (get_entry G x)); in Graph (tab |> Table.delete x - |> fold (del_adjacent apsnd) preds - |> fold (del_adjacent apfst) succs) + |> Keys.fold (del_adjacent apsnd) preds + |> Keys.fold (del_adjacent apfst) succs) end; (* edges *) -fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false; +fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false; fun add_edge (x, y) G = if is_edge G (x, y) then G else - G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs))) - |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs))); + G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs))) + |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs))); fun del_edge (x, y) G = if is_edge G (x, y) then - G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs))) - |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs))) + G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs))) + |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs))) else G; fun diff_edges G1 G2 = @@ -203,7 +234,7 @@ (* join and merge *) -fun no_edges (i, _) = (i, ([], [])); +fun no_edges (i, _) = (i, (Keys.empty, Keys.empty)); fun join f (G1 as Graph tab1, G2 as Graph tab2) = let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in @@ -227,11 +258,11 @@ fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z)); fun irreds [] xs' = xs' | irreds (x :: xs) xs' = - if not (member_keys X x) orelse eq_key (x, z) orelse member_key path x orelse + if not (Keys.member X x) orelse eq_key (x, z) orelse member eq_key path x orelse exists (red x) xs orelse exists (red x) xs' then irreds xs xs' else irreds xs (x :: xs'); - in irreds (imm_preds G z) [] end; + in irreds (immediate_preds G z) [] end; fun irreducible_paths G (x, y) = let @@ -249,8 +280,8 @@ val (_, X) = reachable (imm_succs G) [x]; fun paths path z = if not (null path) andalso eq_key (x, z) then [z :: path] - else if member_keys X z andalso not (member_key path z) - then maps (paths (z :: path)) (imm_preds G z) + else if Keys.member X z andalso not (member eq_key path z) + then maps (paths (z :: path)) (immediate_preds G z) else []; in paths [] y end; @@ -297,7 +328,7 @@ val results = (xs, Table.empty) |-> fold (fn x => fn tab => let val a = get_node G x; - val deps = imm_preds G x |> map (fn y => + val deps = immediate_preds G x |> map (fn y => (case Table.lookup tab y of SOME b => (y, b) | NONE => raise DEP (x, y))); diff -r d453faed4815 -r 700008399ee5 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sat Aug 20 23:35:30 2011 +0200 @@ -407,7 +407,7 @@ val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt); val classes = Sorts.classes_of algebra; fun entry (c, (i, (_, cs))) = - (i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs, + (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs, dir = "", unfold = true, path = ""}); val gr = Graph.fold (cons o entry) classes [] diff -r d453faed4815 -r 700008399ee5 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Pure/PIDE/document.ML Sat Aug 20 23:35:30 2011 +0200 @@ -145,7 +145,8 @@ |> default_node name |> fold default_node parents; val nodes2 = nodes1 - |> fold (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); + |> Graph.Keys.fold + (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); val (header', nodes3) = (header, Graph.add_deps_acyclic (name, parents) nodes2) handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); diff -r d453faed4815 -r 700008399ee5 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Pure/axclass.ML Sat Aug 20 23:35:30 2011 +0200 @@ -220,7 +220,9 @@ in ((c1_pred, c2_succ), th') end; val new_classrels = - Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2) + Library.map_product pair + (c1 :: Graph.immediate_preds classes c1) + (c2 :: Graph.immediate_succs classes c2) |> filter_out ((op =) orf Symreltab.defined classrels) |> map gen_classrel; val needed = not (null new_classrels); diff -r d453faed4815 -r 700008399ee5 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Pure/sorts.ML Sat Aug 20 23:35:30 2011 +0200 @@ -128,7 +128,7 @@ fun all_classes (Algebra {classes, ...}) = Graph.all_preds classes (Graph.maximals classes); -val super_classes = Graph.imm_succs o classes_of; +val super_classes = Graph.immediate_succs o classes_of; (* class relations *) @@ -413,7 +413,7 @@ end; fun derive (_, []) = [] - | derive (T as Type (a, Us), S) = + | derive (Type (a, Us), S) = let val Ss = mg_domain algebra a S; val dom = map2 (fn U => fn S => derive (U, S) ~~ S) Us Ss; diff -r d453faed4815 -r 700008399ee5 src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Tools/Code/code_namespace.ML Sat Aug 20 23:35:30 2011 +0200 @@ -86,7 +86,8 @@ end; val proto_program = Graph.empty |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program - |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program; + |> Graph.fold (fn (name, (_, (_, names))) => + Graph.Keys.fold (add_dependency name) names) program; (* name declarations and statement modifications *) fun declare name (base, stmt) (gr, nsp) = @@ -191,7 +192,8 @@ in (map_module name_fragments_common o apsnd) add_edge end; val proto_program = empty_program |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program - |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program; + |> Graph.fold (fn (name, (_, (_, names))) => + Graph.Keys.fold (add_dependency name) names) program; (* name declarations, data and statement modifications *) fun make_declarations nsps (data, nodes) = diff -r d453faed4815 -r 700008399ee5 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Tools/Code/code_preproc.ML Sat Aug 20 23:35:30 2011 +0200 @@ -309,7 +309,7 @@ val diff_classes = new_classes |> subtract (op =) old_classes; in if null diff_classes then vardeps_data else let - val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k; + val c_ks = Vargraph.immediate_succs (fst vardeps_data) c_k |> insert (op =) c_k; in vardeps_data |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes) diff -r d453faed4815 -r 700008399ee5 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Tools/Code/code_scala.ML Sat Aug 20 23:35:30 2011 +0200 @@ -321,7 +321,7 @@ of Code_Thingol.Classinst _ => true | _ => false; val implicits = filter (is_classinst o Graph.get_node program) - (Graph.imm_succs program name); + (Graph.immediate_succs program name); in union (op =) implicits end; fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE diff -r d453faed4815 -r 700008399ee5 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Tools/Code/code_thingol.ML Sat Aug 20 23:35:30 2011 +0200 @@ -921,7 +921,7 @@ let val Fun (_, ((vs_ty, [(([], t), _)]), _)) = Graph.get_node program1 Term.dummy_patternN; - val deps = Graph.imm_succs program1 Term.dummy_patternN; + val deps = Graph.immediate_succs program1 Term.dummy_patternN; val program2 = Graph.del_nodes [Term.dummy_patternN] program1; val deps_all = Graph.all_succs program2 deps; val program3 = Graph.subgraph (member (op =) deps_all) program2; @@ -1010,7 +1010,7 @@ val mapping = Symtab.empty |> fold (fn consts => fold (fn const => Symtab.update (const, consts)) consts) constss; fun succs consts = consts - |> maps (Graph.imm_succs eqngr) + |> maps (Graph.immediate_succs eqngr) |> subtract (op =) consts |> map (the o Symtab.lookup mapping) |> distinct (op =); diff -r d453faed4815 -r 700008399ee5 src/Tools/codegen.ML --- a/src/Tools/codegen.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Tools/codegen.ML Sat Aug 20 23:35:30 2011 +0200 @@ -756,7 +756,7 @@ let val SOME (x, y) = get_first (fn (x, (_, a', _)) => if a = a' then Option.map (pair x) (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr) - (Graph.imm_succs gr x)) + (Graph.immediate_succs gr x)) else NONE) code in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end | string_of_cycle _ = "" @@ -767,7 +767,7 @@ val mod_gr = fold_rev Graph.add_edge_acyclic (maps (fn (s, (_, module, _)) => map (pair module) (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr) - (Graph.imm_succs gr s)))) code) + (Graph.immediate_succs gr s)))) code) (fold_rev (Graph.new_node o rpair ()) modules Graph.empty); val modules' = rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs)) diff -r d453faed4815 -r 700008399ee5 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Tools/nbe.ML Sat Aug 20 23:35:30 2011 +0200 @@ -471,7 +471,7 @@ then (nbe_program, (maxidx, idx_tab)) else (nbe_program, (maxidx, idx_tab)) |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name), - Graph.imm_succs program name)) names); + Graph.immediate_succs program name)) names); in fold_rev add_stmts (Graph.strong_conn program) end; diff -r d453faed4815 -r 700008399ee5 src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Sat Aug 20 22:46:19 2011 +0200 +++ b/src/Tools/subtyping.ML Sat Aug 20 23:35:30 2011 +0200 @@ -171,10 +171,10 @@ fun get_succs G T = Typ_Graph.all_succs G [T]; fun maybe_new_typnode T G = perhaps (try (Typ_Graph.new_node (T, ()))) G; fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G; -fun new_imm_preds G Ts = - subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.imm_preds G) Ts)); -fun new_imm_succs G Ts = - subtract op= Ts (distinct (op =) (maps (Typ_Graph.imm_succs G) Ts)); +fun new_imm_preds G Ts = (* FIXME inefficient *) + subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_preds G) Ts)); +fun new_imm_succs G Ts = (* FIXME inefficient *) + subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_succs G) Ts)); (* Graph shortcuts *) @@ -406,7 +406,7 @@ (*styps stands either for supertypes or for subtypes of a type T in terms of the subtype-relation (excluding T itself)*) fun styps super T = - (if super then Graph.imm_succs else Graph.imm_preds) coes_graph T + (if super then Graph.immediate_succs else Graph.immediate_preds) coes_graph T handle Graph.UNDEF _ => []; fun minmax sup (T :: Ts) =