fold_body_thms/join_bodies: explicitly check for cyclic theorem references;
authorwenzelm
Sun Sep 27 21:08:13 2009 +0200 (2009-09-27)
changeset 32711e24acd21e60e
parent 32710 fa46afc8c05f
child 32716 9b014e62b716
fold_body_thms/join_bodies: explicitly check for cyclic theorem references;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Sun Sep 27 21:06:43 2009 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Sun Sep 27 21:08:13 2009 +0200
     1.3 @@ -173,16 +173,19 @@
     1.4  
     1.5  fun fold_body_thms f =
     1.6    let
     1.7 -    fun app (PBody {thms, ...}) =
     1.8 +    fun app path (PBody {thms, ...}) =
     1.9       (Future.join_results (map (#3 o #2) thms);
    1.10        thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
    1.11 -        if Inttab.defined seen i then (x, seen)
    1.12 +        if Inttab.defined path i then
    1.13 +          error ("Cyclic reference to theorem " ^ quote name)
    1.14 +        else if Inttab.defined seen i then (x, seen)
    1.15          else
    1.16            let
    1.17              val body' = Future.join body;
    1.18 -            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    1.19 +            val path' = Inttab.update (i, ()) path;
    1.20 +            val (x', seen') = app path' body' (x, Inttab.update (i, ()) seen);
    1.21            in (f (name, prop, body') x', seen') end));
    1.22 -  in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    1.23 +  in fn bodies => fn x => #1 (fold (app Inttab.empty) bodies (x, Inttab.empty)) end;
    1.24  
    1.25  fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
    1.26