# HG changeset patch # User wenzelm # Date 1571336911 -7200 # Node ID ce1e27dcc9f4acb3a643dee65f93ba1cf02d7722 # Parent aadb5c23af24d9b70e552082f4d851877d14ddb3 clarified files; diff -r aadb5c23af24 -r ce1e27dcc9f4 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Oct 17 17:24:13 2019 +0200 +++ b/src/Pure/ROOT.ML Thu Oct 17 20:28:31 2019 +0200 @@ -310,7 +310,7 @@ ML_file "PIDE/resources.ML"; ML_file "Thy/present.ML"; ML_file "Thy/thy_info.ML"; -ML_file "Thy/thm_deps.ML"; +ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; diff -r aadb5c23af24 -r ce1e27dcc9f4 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Thu Oct 17 17:24:13 2019 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,135 +0,0 @@ -(* Title: Pure/Thy/thm_deps.ML - Author: Stefan Berghofer, TU Muenchen - Author: Makarius - -Dependencies of theorems wrt. internal derivation. -*) - -signature THM_DEPS = -sig - val all_oracles: thm list -> Proofterm.oracle list - val has_skip_proof: thm list -> bool - val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T - val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list - val pretty_thm_deps: theory -> thm list -> Pretty.T - val unused_thms_cmd: theory list * theory list -> (string * thm) list -end; - -structure Thm_Deps: THM_DEPS = -struct - -(* oracles *) - -fun all_oracles thms = - let - fun collect (PBody {oracles, thms, ...}) = - (if null oracles then I else apfst (cons oracles)) #> - (tap Proofterm.join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) => - if Inttab.defined seen i then (res, seen) - else - let val body = Future.join (Proofterm.thm_node_body thm_node) - in collect body (res, Inttab.update (i, ()) seen) end)); - val bodies = map Thm.proof_body_of thms; - in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end; - -fun has_skip_proof thms = - all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\skip_proof\); - -fun pretty_thm_oracles ctxt thms = - let - val thy = Proof_Context.theory_of ctxt; - fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name] - | prt_oracle (name, SOME prop) = - [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1, - Syntax.pretty_term_global thy prop]; - in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end; - - -(* thm_deps *) - -fun thm_deps thy = - let - val lookup = Global_Theory.lookup_thm_id thy; - fun deps (i, thm_node) res = - if Inttab.defined res i then res - else - let val thm_id = Proofterm.thm_id (i, thm_node) in - (case lookup thm_id of - SOME thm_name => - Inttab.update (i, SOME (thm_id, thm_name)) res - | NONE => - Inttab.update (i, NONE) res - |> fold deps (Proofterm.thm_node_thms thm_node)) - end; - in - fn thms => - (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms Inttab.empty, []) - |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I) - end; - -fun pretty_thm_deps thy thms = - let - val ctxt = Proof_Context.init_global thy; - val items = - map #2 (thm_deps thy thms) - |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i)) - |> sort_by (#2 o #1) - |> map (fn ((marks, xname), i) => - Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]); - in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; - - -(* unused_thms_cmd *) - -fun unused_thms_cmd (base_thys, thys) = - let - fun add_fact transfer space (name, ths) = - if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I - else - let val {concealed, group, ...} = Name_Space.the_entry space name in - fold_rev (fn th => - (case Thm.derivation_name th of - "" => I - | a => cons (a, (transfer th, concealed, group)))) ths - end; - fun add_facts thy = - let - val transfer = Global_Theory.transfer_theories thy; - val facts = Global_Theory.facts_of thy; - in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end; - - val new_thms = - fold add_facts thys [] - |> sort_distinct (string_ord o apply2 #1); - - val used = - Proofterm.fold_body_thms - (fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) - (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms))) - Symtab.empty; - - fun is_unused a = not (Symtab.defined used a); - - (*groups containing at least one used theorem*) - val used_groups = fold (fn (a, (_, _, group)) => - if is_unused a then I - else - (case group of - NONE => I - | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty; - - val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) => - if not concealed andalso - (* FIXME replace by robust treatment of thm groups *) - Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a - then - (case group of - NONE => ((a, th) :: thms, seen_groups) - | SOME grp => - if Inttab.defined used_groups grp orelse - Inttab.defined seen_groups grp then q - else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups)) - else q) new_thms ([], Inttab.empty); - in rev thms' end; - -end; diff -r aadb5c23af24 -r ce1e27dcc9f4 src/Pure/thm_deps.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/thm_deps.ML Thu Oct 17 20:28:31 2019 +0200 @@ -0,0 +1,135 @@ +(* Title: Pure/thm_deps.ML + Author: Stefan Berghofer, TU Muenchen + Author: Makarius + +Dependencies of theorems wrt. internal derivation. +*) + +signature THM_DEPS = +sig + val all_oracles: thm list -> Proofterm.oracle list + val has_skip_proof: thm list -> bool + val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T + val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list + val pretty_thm_deps: theory -> thm list -> Pretty.T + val unused_thms_cmd: theory list * theory list -> (string * thm) list +end; + +structure Thm_Deps: THM_DEPS = +struct + +(* oracles *) + +fun all_oracles thms = + let + fun collect (PBody {oracles, thms, ...}) = + (if null oracles then I else apfst (cons oracles)) #> + (tap Proofterm.join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) => + if Inttab.defined seen i then (res, seen) + else + let val body = Future.join (Proofterm.thm_node_body thm_node) + in collect body (res, Inttab.update (i, ()) seen) end)); + val bodies = map Thm.proof_body_of thms; + in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end; + +fun has_skip_proof thms = + all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\skip_proof\); + +fun pretty_thm_oracles ctxt thms = + let + val thy = Proof_Context.theory_of ctxt; + fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name] + | prt_oracle (name, SOME prop) = + [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1, + Syntax.pretty_term_global thy prop]; + in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end; + + +(* thm_deps *) + +fun thm_deps thy = + let + val lookup = Global_Theory.lookup_thm_id thy; + fun deps (i, thm_node) res = + if Inttab.defined res i then res + else + let val thm_id = Proofterm.thm_id (i, thm_node) in + (case lookup thm_id of + SOME thm_name => + Inttab.update (i, SOME (thm_id, thm_name)) res + | NONE => + Inttab.update (i, NONE) res + |> fold deps (Proofterm.thm_node_thms thm_node)) + end; + in + fn thms => + (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms Inttab.empty, []) + |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I) + end; + +fun pretty_thm_deps thy thms = + let + val ctxt = Proof_Context.init_global thy; + val items = + map #2 (thm_deps thy thms) + |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i)) + |> sort_by (#2 o #1) + |> map (fn ((marks, xname), i) => + Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]); + in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; + + +(* unused_thms_cmd *) + +fun unused_thms_cmd (base_thys, thys) = + let + fun add_fact transfer space (name, ths) = + if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I + else + let val {concealed, group, ...} = Name_Space.the_entry space name in + fold_rev (fn th => + (case Thm.derivation_name th of + "" => I + | a => cons (a, (transfer th, concealed, group)))) ths + end; + fun add_facts thy = + let + val transfer = Global_Theory.transfer_theories thy; + val facts = Global_Theory.facts_of thy; + in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end; + + val new_thms = + fold add_facts thys [] + |> sort_distinct (string_ord o apply2 #1); + + val used = + Proofterm.fold_body_thms + (fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) + (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms))) + Symtab.empty; + + fun is_unused a = not (Symtab.defined used a); + + (*groups containing at least one used theorem*) + val used_groups = fold (fn (a, (_, _, group)) => + if is_unused a then I + else + (case group of + NONE => I + | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty; + + val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) => + if not concealed andalso + (* FIXME replace by robust treatment of thm groups *) + Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a + then + (case group of + NONE => ((a, th) :: thms, seen_groups) + | SOME grp => + if Inttab.defined used_groups grp orelse + Inttab.defined seen_groups grp then q + else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups)) + else q) new_thms ([], Inttab.empty); + in rev thms' end; + +end;