src/Pure/General/graph.ML
changeset 18921 f47c46d7d654
parent 18133 1d403623dabc
child 18970 d055a29ddd23
equal deleted inserted replaced
18920:7635e0060cd4 18921:f47c46d7d654
    53 
    53 
    54 type key = Key.key;
    54 type key = Key.key;
    55 
    55 
    56 val eq_key = equal EQUAL o Key.ord;
    56 val eq_key = equal EQUAL o Key.ord;
    57 
    57 
    58 infix mem_key;
    58 val member_key = member eq_key;
    59 val op mem_key = gen_mem eq_key;
       
    60 
       
    61 val remove_key = remove eq_key;
    59 val remove_key = remove eq_key;
    62 
    60 
    63 
    61 
    64 (* tables and sets of keys *)
    62 (* tables and sets of keys *)
    65 
    63 
    66 structure Table = TableFun(Key);
    64 structure Table = TableFun(Key);
    67 type keys = unit Table.table;
    65 type keys = unit Table.table;
    68 
    66 
    69 val empty_keys = Table.empty: keys;
    67 val empty_keys = Table.empty: keys;
    70 
    68 
    71 infix mem_keys;
    69 fun member_keys tab = Table.defined (tab: keys);
    72 fun x mem_keys tab = Table.defined (tab: keys) x;
    70 fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
    73 
       
    74 infix ins_keys;
       
    75 fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys);
       
    76 
    71 
    77 
    72 
    78 (* graphs *)
    73 (* graphs *)
    79 
    74 
    80 datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
    75 datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
   124 
   119 
   125 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
   120 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
   126 fun reachable next xs =
   121 fun reachable next xs =
   127   let
   122   let
   128     fun reach x (rs, R) =
   123     fun reach x (rs, R) =
   129       if x mem_keys R then (rs, R)
   124       if member_keys R x then (rs, R)
   130       else apfst (cons x) (fold reach (next x) (rs, x ins_keys R))
   125       else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
   131   in fold_map (fn x => reach x o pair []) xs empty_keys end;
   126   in fold_map (fn x => reach x o pair []) xs empty_keys end;
   132 
   127 
   133 (*immediate*)
   128 (*immediate*)
   134 fun imm_preds G = #1 o #2 o get_entry G;
   129 fun imm_preds G = #1 o #2 o get_entry G;
   135 fun imm_succs G = #2 o #2 o get_entry G;
   130 fun imm_succs G = #2 o #2 o get_entry G;
   159 fun find_paths G (x, y) =
   154 fun find_paths G (x, y) =
   160   let
   155   let
   161     val (_, X) = reachable (imm_succs G) [x];
   156     val (_, X) = reachable (imm_succs G) [x];
   162     fun paths ps p =
   157     fun paths ps p =
   163       if not (null ps) andalso eq_key (p, x) then [p :: ps]
   158       if not (null ps) andalso eq_key (p, x) then [p :: ps]
   164       else if p mem_keys X andalso not (p mem_key ps)
   159       else if member_keys X p andalso not (member_key ps p)
   165       then List.concat (map (paths (p :: ps)) (imm_preds G p))
   160       then List.concat (map (paths (p :: ps)) (imm_preds G p))
   166       else [];
   161       else [];
   167   in paths [] y end;
   162   in paths [] y end;
   168 
   163 
   169 
   164 
   182       (i, (fold remove_key xs preds, fold remove_key xs succs))));
   177       (i, (fold remove_key xs preds, fold remove_key xs succs))));
   183 
   178 
   184 
   179 
   185 (* edges *)
   180 (* edges *)
   186 
   181 
   187 fun is_edge G (x, y) = y mem_key imm_succs G x handle UNDEF _ => false;
   182 fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
   188 
   183 
   189 fun add_edge (x, y) G =
   184 fun add_edge (x, y) G =
   190   if is_edge G (x, y) then G
   185   if is_edge G (x, y) then G
   191   else
   186   else
   192     G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
   187     G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))