src/Pure/General/graph.ML
changeset 46668 9034b44844bd
parent 46667 318b669fe660
child 48350 09bf3b73e446
equal deleted inserted replaced
46667:318b669fe660 46668:9034b44844bd
   172 fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
   172 fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
   173 fun is_minimal G x = Keys.is_empty (imm_preds G x);
   173 fun is_minimal G x = Keys.is_empty (imm_preds G x);
   174 fun is_maximal G x = Keys.is_empty (imm_succs G x);
   174 fun is_maximal G x = Keys.is_empty (imm_succs G x);
   175 
   175 
   176 
   176 
   177 (* nodes *)
   177 (* node operations *)
   178 
   178 
   179 fun new_node (x, info) (Graph tab) =
   179 fun new_node (x, info) (Graph tab) =
   180   Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
   180   Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
   181 
   181 
   182 fun default_node (x, info) (Graph tab) =
   182 fun default_node (x, info) (Graph tab) =
   196 
   196 
   197 fun restrict pred G =
   197 fun restrict pred G =
   198   fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;
   198   fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;
   199 
   199 
   200 
   200 
   201 (* edges *)
   201 (* edge operations *)
   202 
   202 
   203 fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
   203 fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
   204 
   204 
   205 fun add_edge (x, y) G =
   205 fun add_edge (x, y) G =
   206   if is_edge G (x, y) then G
   206   if is_edge G (x, y) then G