merged
authorwenzelm
Sun Sep 27 22:25:13 2009 +0200 (2009-09-27)
changeset 327169b014e62b716
parent 32715 becd87e4039b
parent 32711 e24acd21e60e
child 32723 866cebde3fca
child 32755 a4ae77549ed1
merged
     1.1 --- a/src/Pure/General/graph.ML	Sun Sep 27 19:58:24 2009 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Sun Sep 27 22:25:13 2009 +0200
     1.3 @@ -132,21 +132,23 @@
     1.4    let
     1.5      fun reach x (rs, R) =
     1.6        if member_keys R x then (rs, R)
     1.7 -      else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
     1.8 -  in fold_map (fn x => fn X => reach x ([], X)) xs empty_keys end;
     1.9 +      else fold reach (next x) (rs, insert_keys x R) |>> cons x;
    1.10 +    fun reachs x (rss, R) =
    1.11 +      reach x ([], R) |>> (fn rs => rs :: rss);
    1.12 +  in fold reachs xs ([], empty_keys) end;
    1.13  
    1.14  (*immediate*)
    1.15  fun imm_preds G = #1 o #2 o get_entry G;
    1.16  fun imm_succs G = #2 o #2 o get_entry G;
    1.17  
    1.18  (*transitive*)
    1.19 -fun all_preds G = flat o fst o reachable (imm_preds G);
    1.20 -fun all_succs G = flat o fst o reachable (imm_succs G);
    1.21 +fun all_preds G = flat o #1 o reachable (imm_preds G);
    1.22 +fun all_succs G = flat o #1 o reachable (imm_succs G);
    1.23  
    1.24  (*strongly connected components; see: David King and John Launchbury,
    1.25    "Structuring Depth First Search Algorithms in Haskell"*)
    1.26 -fun strong_conn G = filter_out null (fst (reachable (imm_preds G)
    1.27 -  (flat (rev (fst (reachable (imm_succs G) (keys G)))))));
    1.28 +fun strong_conn G =
    1.29 +  rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
    1.30  
    1.31  
    1.32  (* nodes *)
     2.1 --- a/src/Pure/proofterm.ML	Sun Sep 27 19:58:24 2009 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Sun Sep 27 22:25:13 2009 +0200
     2.3 @@ -173,16 +173,19 @@
     2.4  
     2.5  fun fold_body_thms f =
     2.6    let
     2.7 -    fun app (PBody {thms, ...}) =
     2.8 +    fun app path (PBody {thms, ...}) =
     2.9       (Future.join_results (map (#3 o #2) thms);
    2.10        thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
    2.11 -        if Inttab.defined seen i then (x, seen)
    2.12 +        if Inttab.defined path i then
    2.13 +          error ("Cyclic reference to theorem " ^ quote name)
    2.14 +        else if Inttab.defined seen i then (x, seen)
    2.15          else
    2.16            let
    2.17              val body' = Future.join body;
    2.18 -            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    2.19 +            val path' = Inttab.update (i, ()) path;
    2.20 +            val (x', seen') = app path' body' (x, Inttab.update (i, ()) seen);
    2.21            in (f (name, prop, body') x', seen') end));
    2.22 -  in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    2.23 +  in fn bodies => fn x => #1 (fold (app Inttab.empty) bodies (x, Inttab.empty)) end;
    2.24  
    2.25  fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
    2.26