src/Pure/Thy/thm_deps.ML
changeset 28826 3b460b6eadae
parent 28817 c8cc94a470d4
child 29606 fedb8be05f24
equal deleted inserted replaced
28825:415c7ffeb4cb 28826:3b460b6eadae
    14 structure ThmDeps: THM_DEPS =
    14 structure ThmDeps: THM_DEPS =
    15 struct
    15 struct
    16 
    16 
    17 (* thm_deps *)
    17 (* thm_deps *)
    18 
    18 
    19 fun add_dep (name, _, PBody {thms = thms', ...}) =
       
    20   name <> "" ?
       
    21     Graph.new_node (name, ()) #>
       
    22     fold (fn (_, (name', _, _)) => name <> "" ? Graph.add_edge (name', name)) thms';
       
    23 
       
    24 fun thm_deps thms =
    19 fun thm_deps thms =
    25   let
    20   let
    26     val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) Graph.empty;
    21     fun add_dep ("", _, _) = I
    27     fun add_entry (name, (_, (preds, _))) =
    22       | add_dep (name, _, PBody {thms = thms', ...}) =
    28       let
    23           let
    29         val prefix = #1 (Library.split_last (NameSpace.explode name));
    24             val prefix = #1 (Library.split_last (NameSpace.explode name));
    30         val session =
    25             val session =
    31           (case prefix of
    26               (case prefix of
    32             a :: _ =>
    27                 a :: _ =>
    33               (case ThyInfo.lookup_theory a of
    28                   (case ThyInfo.lookup_theory a of
    34                 SOME thy =>
    29                     SOME thy =>
    35                   (case Present.session_name thy of
    30                       (case Present.session_name thy of
    36                     "" => []
    31                         "" => []
    37                   | session => [session])
    32                       | session => [session])
    38               | NONE => [])
    33                   | NONE => [])
    39            | _ => ["global"]);
    34                | _ => ["global"]);
    40         val entry =
    35             val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
    41           {name = Sign.base_name name,
    36             val entry =
    42            ID = name,
    37               {name = Sign.base_name name,
    43            dir = space_implode "/" (session @ prefix),
    38                ID = name,
    44            unfold = false,
    39                dir = space_implode "/" (session @ prefix),
    45            path = "",
    40                unfold = false,
    46            parents = preds};
    41                path = "",
    47       in cons entry end;
    42                parents = parents};
    48   in Present.display_graph (sort_wrt #ID (Graph.fold add_entry graph [])) end;
    43           in cons entry end;
       
    44     val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
       
    45   in Present.display_graph (sort_wrt #ID deps) end;
    49 
    46 
    50 
    47 
    51 (* unused_thms *)
    48 (* unused_thms *)
    52 
    49 
    53 fun unused_thms (base_thys, thys) =
    50 fun unused_thms (base_thys, thys) =