src/Pure/General/graph.ML
changeset 49560 11430dd89e35
parent 48350 09bf3b73e446
child 55154 2733a57d100f
equal deleted inserted replaced
49559:c3a6e110679b 49560:11430dd89e35
    20   exception SAME
    20   exception SAME
    21   exception UNDEF of key
    21   exception UNDEF of key
    22   val empty: 'a T
    22   val empty: 'a T
    23   val is_empty: 'a T -> bool
    23   val is_empty: 'a T -> bool
    24   val keys: 'a T -> key list
    24   val keys: 'a T -> key list
    25   val dest: 'a T -> (key * key list) list
       
    26   val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
    25   val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
    27   val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
    26   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*)
    27   val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
    29   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    28   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    30   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    29   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    46   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
    45   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
    47   val is_edge: 'a T -> key * key -> bool
    46   val is_edge: 'a T -> key * key -> bool
    48   val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    47   val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    49   val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    48   val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    50   val restrict: (key -> bool) -> 'a T -> 'a T
    49   val restrict: (key -> bool) -> 'a T -> 'a T
       
    50   val dest: 'a T -> ((key * 'a) * key list) list
       
    51   val make: ((key * 'a) * key list) list -> 'a T                      (*exception DUP | UNDEF*)
    51   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
    52   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
    52   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    53   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    53     'a T * 'a T -> 'a T                                               (*exception DUP*)
    54     'a T * 'a T -> 'a T                                               (*exception DUP*)
    54   val irreducible_paths: 'a T -> key * key -> key list list
    55   val irreducible_paths: 'a T -> key * key -> key list list
    55   exception CYCLES of key list list
    56   exception CYCLES of key list list
    59   val topological_order: 'a T -> key list
    60   val topological_order: 'a T -> key list
    60   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception UNDEF | CYCLES*)
    61   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception UNDEF | CYCLES*)
    61   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
    62   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
    62   exception DEP of key * key
    63   exception DEP of key * key
    63   val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
    64   val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
       
    65   val encode: key XML.Encode.T -> 'a XML.Encode.T -> 'a T XML.Encode.T
       
    66   val decode: key XML.Decode.T -> 'a XML.Decode.T -> 'a T XML.Decode.T
    64 end;
    67 end;
    65 
    68 
    66 functor Graph(Key: KEY): GRAPH =
    69 functor Graph(Key: KEY): GRAPH =
    67 struct
    70 struct
    68 
    71 
   106 exception SAME = Table.SAME;
   109 exception SAME = Table.SAME;
   107 
   110 
   108 val empty = Graph Table.empty;
   111 val empty = Graph Table.empty;
   109 fun is_empty (Graph tab) = Table.is_empty tab;
   112 fun is_empty (Graph tab) = Table.is_empty tab;
   110 fun keys (Graph tab) = Table.keys tab;
   113 fun keys (Graph tab) = Table.keys tab;
   111 fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
       
   112 
   114 
   113 fun get_first f (Graph tab) = Table.get_first f tab;
   115 fun get_first f (Graph tab) = Table.get_first f tab;
   114 fun fold_graph f (Graph tab) = Table.fold f tab;
   116 fun fold_graph f (Graph tab) = Table.fold f tab;
   115 
   117 
   116 fun get_entry (Graph tab) x =
   118 fun get_entry (Graph tab) x =
   213     G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs)))
   215     G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs)))
   214       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs)))
   216       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs)))
   215   else G;
   217   else G;
   216 
   218 
   217 fun diff_edges G1 G2 =
   219 fun diff_edges G1 G2 =
   218   flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y =>
   220   fold_graph (fn (x, (_, (_, succs))) =>
   219     if is_edge G2 (x, y) then NONE else SOME (x, y))));
   221     Keys.fold (fn y => not (is_edge G2 (x, y)) ? cons (x, y)) succs) G1 [];
   220 
   222 
   221 fun edges G = diff_edges G empty;
   223 fun edges G = diff_edges G empty;
       
   224 
       
   225 
       
   226 (* dest and make *)
       
   227 
       
   228 fun dest G = fold_graph (fn (x, (i, (_, succs))) => cons ((x, i), Keys.dest succs)) G [];
       
   229 
       
   230 fun make entries =
       
   231   empty
       
   232   |> fold (new_node o fst) entries
       
   233   |> fold (fn ((x, _), ys) => fold (fn y => add_edge (x, y)) ys) entries;
   222 
   234 
   223 
   235 
   224 (* join and merge *)
   236 (* join and merge *)
   225 
   237 
   226 fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
   238 fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
   310           | NONE => raise DEP (x, y)));
   322           | NONE => raise DEP (x, y)));
   311       in Table.update (x, f deps (x, a)) tab end);
   323       in Table.update (x, f deps (x, a)) tab end);
   312   in map (the o Table.lookup results) xs end;
   324   in map (the o Table.lookup results) xs end;
   313 
   325 
   314 
   326 
       
   327 (* XML data representation *)
       
   328 
       
   329 fun encode key info G =
       
   330   dest G |>
       
   331     let open XML.Encode
       
   332     in list (pair (pair key info) (list key)) end;
       
   333 
       
   334 fun decode key info body =
       
   335   body |>
       
   336     let open XML.Decode
       
   337     in list (pair (pair key info) (list key)) end |> make;
       
   338 
       
   339 
   315 (*final declarations of this structure!*)
   340 (*final declarations of this structure!*)
   316 val map = map_nodes;
   341 val map = map_nodes;
   317 val fold = fold_graph;
   342 val fold = fold_graph;
   318 
   343 
   319 end;
   344 end;