Be less verbose
[isa-where-to-move.git] / where_to_move.ML
1 (*  Title: where_to_move.ML
2     Author: Joachim Breitner
3
4 Utility commands to suggest lemma reorganisations.
5 *)
6
7 signature WHERE_TO_MOVE =
8 sig
9   val thms_used_by_thm : thm -> string list
10   val theories_used_by_thm : theory -> thm -> theory list
11   val theories_used_by_thms : theory -> thm list -> theory list
12
13   val theorems_used_by_cmd : (string * Position.T) -> Toplevel.transition -> Toplevel.transition
14   val where_to_move_cmd : (string * Position.T) list option -> Toplevel.transition -> Toplevel.transition
15 end
16
17 structure Where_To_Move : WHERE_TO_MOVE =
18 struct
19
20 fun thms_used_by_thm thm =
21   let
22   fun  used_by_proof_body (PBody {thms, ...}) = thms |> map #2 |> maps go
23   and go ("", _, pbodyf) = pbodyf |> Future.join |> used_by_proof_body
24     | go (s, _, _) = [s]
25   in thm |> Thm.proof_body_of |> Proofterm.strip_thm |> used_by_proof_body
26   end;
27
28 fun nub ss = fold (fn x => Symtab.update (x, ())) ss Symtab.empty |> Symtab.keys;
29
30 fun theories_used_by_thm thy thm =
31       thm |> thms_used_by_thm 
32           |> map (hd o Long_Name.explode) 
33           |> nub 
34           |> map (Context.this_theory thy);
35
36 fun theories_used_by_thms thy thms =
37       thms |> maps thms_used_by_thm
38            |> map (hd o Long_Name.explode) 
39            |> nub 
40            |> map (Context.this_theory thy);
41
42
43 fun ok_for thys thy =
44   forall (fn thy' => 
45     let (* val _ = writeln (@{make_string} (theory_name thy', theory_name  thy,  Context.subthy (thy', thy))) *)
46     in  Context.subthy (thy', thy) end) thys
47
48 fun better_theory thys this_thy =
49   Context.ancestors_of this_thy 
50   |> rev (* this way we get a minimal solution *)
51   |> find_first  (ok_for thys);
52
53
54 fun theorems_used_by_cmd arg = Toplevel.keep (fn state =>
55     let val ctxt = Toplevel.context_of state
56         val thy = Toplevel.theory_of state
57         val (_, thms) =  Facts.retrieve (Context.Proof ctxt) (Global_Theory.facts_of thy) arg
58     in thms |> maps thms_used_by_thm
59             |> map (Pretty.mark_str o Proof_Context.markup_extern_fact ctxt)
60             |> Pretty.commas
61             |> Pretty.paragraph
62             |> Pretty.writeln
63     end
64     );
65
66
67 fun facts_of_theory thy =
68   let val prev_thys = (Theory.parents_of thy) 
69       val facts = Global_Theory.facts_of thy
70       val thms =  Facts.dest_static false (map Global_Theory.facts_of prev_thys) facts
71   in thms end;
72
73 fun where_to_move_cmd args_o =
74   Toplevel.keep ( fn state =>
75     let val ctxt = Toplevel.context_of state
76         val this_thy = Toplevel.theory_of state
77         val (verbose, named_thms) = case args_o of
78             SOME args => (true, args |> map (Facts.retrieve (Context.Proof ctxt) (Global_Theory.facts_of this_thy)))
79             | NONE =>    (false, facts_of_theory this_thy)
80     in named_thms |> map (fn (name, thms) =>
81       let val pretty_name = Pretty.mark_str (Proof_Context.markup_extern_fact ctxt name)
82       in case better_theory (theories_used_by_thms this_thy thms) this_thy of
83           SOME thy =>
84            [ Pretty.str "Theorem ", pretty_name,
85              Pretty.str " could be moved to theory ",
86              Pretty.quote (Pretty.str (Context.theory_name thy)), Pretty.str "."
87            ] |> Pretty.paragraph |> Pretty.writeln
88         | NONE =>
89           if verbose then
90            [ Pretty.str "Theorem ", pretty_name,
91              Pretty.str" is fine where it is."] |> Pretty.paragraph |> Pretty.writeln
92           else ()
93       end
94     ) |> K ()
95    end
96    );
97
98
99 val _ = Outer_Syntax.improper_command @{command_spec "theorems_used_by"} 
100     "prints all theorems used by the given theorem"
101     (Parse.position Parse.xname >> theorems_used_by_cmd);
102
103 val _ = Outer_Syntax.improper_command @{command_spec "where_to_move"}
104     "suggests a new location for the given theorem or, of none is given, all theorems in the current theory"
105     (Scan.option (Scan.repeat1 (Parse.position Parse.xname)) >> where_to_move_cmd);
106
107 end