Adapted to new argument format of MinProof constructor.
authorberghofe
Wed Aug 03 16:28:22 2005 +0200 (2005-08-03)
changeset 17020f3014afac46f
parent 17019 f68598628d08
child 17021 1c361a3de73d
Adapted to new argument format of MinProof constructor.
src/Pure/Thy/thm_deps.ML
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Wed Aug 03 16:26:16 2005 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Wed Aug 03 16:28:22 2005 +0200
     1.3 @@ -26,22 +26,23 @@
     1.4  fun disable () = proofs := 0;
     1.5  
     1.6  fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
     1.7 -  | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof [])
     1.8 -  | dest_thm_axm _ = (("", []), MinProof []);
     1.9 +  | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], []))
    1.10 +  | dest_thm_axm _ = (("", []), MinProof ([], [], []));
    1.11  
    1.12 -fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf)
    1.13 -  | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf)
    1.14 -  | make_deps_graph (p, prf1 %% prf2) =
    1.15 -      make_deps_graph (make_deps_graph (p, prf1), prf2)
    1.16 -  | make_deps_graph (p, prf % _) = make_deps_graph (p, prf)
    1.17 -  | make_deps_graph (p, MinProof prfs) = Library.foldl make_deps_graph (p, prfs)
    1.18 -  | make_deps_graph (p as (gra, parents), prf) =
    1.19 +fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf
    1.20 +  | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf
    1.21 +  | make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2
    1.22 +  | make_deps_graph (prf % _) = make_deps_graph prf
    1.23 +  | make_deps_graph (MinProof (thms, axms, _)) =
    1.24 +      fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #>
    1.25 +      fold (make_deps_graph o Proofterm.proof_of_min_axm) axms
    1.26 +  | make_deps_graph prf = (fn p as (gra, parents) =>
    1.27        let val ((name, tags), prf') = dest_thm_axm prf
    1.28        in
    1.29          if name <> "" andalso not (Drule.has_internal tags) then
    1.30            if not (Symtab.defined gra name) then
    1.31              let
    1.32 -              val (gra', parents') = make_deps_graph ((gra, []), prf');
    1.33 +              val (gra', parents') = make_deps_graph prf' (gra, []);
    1.34                val prefx = #1 (Library.split_last (NameSpace.unpack name));
    1.35                val session =
    1.36                  (case prefx of
    1.37 @@ -62,14 +63,14 @@
    1.38              end
    1.39            else (gra, name ins parents)
    1.40          else
    1.41 -          make_deps_graph ((gra, parents), prf')
    1.42 -      end;
    1.43 +          make_deps_graph prf' (gra, parents)
    1.44 +      end);
    1.45  
    1.46  fun thm_deps thms =
    1.47    let
    1.48      val _ = writeln "Generating graph ...";
    1.49 -    val gra = map snd (Symtab.dest (fst (Library.foldl make_deps_graph ((Symtab.empty, []),
    1.50 -      map Thm.proof_of thms))));
    1.51 +    val gra = map snd (Symtab.dest (fst
    1.52 +      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))));
    1.53      val path = File.tmp_path (Path.unpack "theorems.graph");
    1.54      val _ = Present.write_graph gra path;
    1.55      val _ = File.isatool ("browser -d " ^ File.shell_path path ^ " &");