Diagnostic command to show locale dependencies.
1 (* Title: Pure/Isar/isar_cmd.ML
2 Author: Markus Wenzel, TU Muenchen
4 Miscellaneous Isar commands.
9 val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
10 val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
11 val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
12 val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
13 val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
14 val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
15 val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
16 val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
17 val add_axioms: (Attrib.binding * string) list -> theory -> theory
18 val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
19 val declaration: {syntax: bool, pervasive: bool} ->
20 Symbol_Pos.text * Position.T -> local_theory -> local_theory
21 val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
22 local_theory -> local_theory
23 val hide_class: bool -> xstring list -> theory -> theory
24 val hide_type: bool -> xstring list -> theory -> theory
25 val hide_const: bool -> xstring list -> theory -> theory
26 val hide_fact: bool -> xstring list -> theory -> theory
27 val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
28 val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
29 val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
30 val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
31 val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
32 val terminal_proof: Method.text * Method.text option ->
33 Toplevel.transition -> Toplevel.transition
34 val default_proof: Toplevel.transition -> Toplevel.transition
35 val immediate_proof: Toplevel.transition -> Toplevel.transition
36 val done_proof: Toplevel.transition -> Toplevel.transition
37 val skip_proof: Toplevel.transition -> Toplevel.transition
38 val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
39 val diag_state: unit -> Toplevel.state
40 val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
41 val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
42 val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
43 val print_context: Toplevel.transition -> Toplevel.transition
44 val print_theory: bool -> Toplevel.transition -> Toplevel.transition
45 val print_syntax: Toplevel.transition -> Toplevel.transition
46 val print_abbrevs: Toplevel.transition -> Toplevel.transition
47 val print_facts: Toplevel.transition -> Toplevel.transition
48 val print_configs: Toplevel.transition -> Toplevel.transition
49 val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
50 val print_locales: Toplevel.transition -> Toplevel.transition
51 val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
52 val print_registrations: string -> Toplevel.transition -> Toplevel.transition
53 val print_dependencies: bool * Expression.expression -> Toplevel.transition
54 -> Toplevel.transition
55 val print_attributes: Toplevel.transition -> Toplevel.transition
56 val print_simpset: Toplevel.transition -> Toplevel.transition
57 val print_rules: Toplevel.transition -> Toplevel.transition
58 val print_trans_rules: Toplevel.transition -> Toplevel.transition
59 val print_methods: Toplevel.transition -> Toplevel.transition
60 val print_antiquotations: Toplevel.transition -> Toplevel.transition
61 val class_deps: Toplevel.transition -> Toplevel.transition
62 val thy_deps: Toplevel.transition -> Toplevel.transition
63 val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
64 val unused_thms: (string list * string list option) option ->
65 Toplevel.transition -> Toplevel.transition
66 val print_binds: Toplevel.transition -> Toplevel.transition
67 val print_cases: Toplevel.transition -> Toplevel.transition
68 val print_stmts: string list * (Facts.ref * Attrib.src list) list
69 -> Toplevel.transition -> Toplevel.transition
70 val print_thms: string list * (Facts.ref * Attrib.src list) list
71 -> Toplevel.transition -> Toplevel.transition
72 val print_prfs: bool -> string list * (Facts.ref * Attrib.src list) list option
73 -> Toplevel.transition -> Toplevel.transition
74 val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
75 val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
76 val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
77 val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
78 val local_theory_markup: xstring option * (Symbol_Pos.text * Position.T) ->
79 Toplevel.transition -> Toplevel.transition
80 val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
83 structure Isar_Cmd: ISAR_CMD =
87 (** theory declarations **)
91 fun global_setup (txt, pos) =
93 |> ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup"
94 |> Context.theory_map;
96 fun local_setup (txt, pos) =
98 |> ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup"
102 (* translation functions *)
106 fun advancedT false = ""
107 | advancedT true = "Proof.context -> ";
109 fun advancedN false = ""
110 | advancedN true = "advanced_";
114 fun parse_ast_translation (a, (txt, pos)) =
116 |> ML_Context.expression pos
117 ("val parse_ast_translation: (string * (" ^ advancedT a ^
118 "Syntax.ast list -> Syntax.ast)) list")
119 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
120 |> Context.theory_map;
122 fun parse_translation (a, (txt, pos)) =
124 |> ML_Context.expression pos
125 ("val parse_translation: (string * (" ^ advancedT a ^
126 "term list -> term)) list")
127 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
128 |> Context.theory_map;
130 fun print_translation (a, (txt, pos)) =
132 |> ML_Context.expression pos
133 ("val print_translation: (string * (" ^ advancedT a ^
134 "term list -> term)) list")
135 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
136 |> Context.theory_map;
138 fun print_ast_translation (a, (txt, pos)) =
140 |> ML_Context.expression pos
141 ("val print_ast_translation: (string * (" ^ advancedT a ^
142 "Syntax.ast list -> Syntax.ast)) list")
143 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
144 |> Context.theory_map;
146 fun typed_print_translation (a, (txt, pos)) =
148 |> ML_Context.expression pos
149 ("val typed_print_translation: (string * (" ^ advancedT a ^
150 "bool -> typ -> term list -> term)) list")
151 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
152 |> Context.theory_map;
159 fun oracle (name, pos) (body_txt, body_pos) =
161 val body = ML_Lex.read body_pos body_txt;
163 ML_Lex.read Position.none
165 \ val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
166 \ val body = ") @ body @ ML_Lex.read Position.none (";\n\
168 \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
170 in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos ants)) end;
173 (* old-style axioms *)
175 val add_axioms = fold (snd oo Specification.axiom_cmd);
177 fun add_defs ((unchecked, overloaded), args) thy =
179 (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
180 overloaded (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
186 fun declaration {syntax, pervasive} (txt, pos) =
188 |> ML_Context.expression pos
189 "val declaration: Morphism.declaration"
190 ("Context.map_proof (Local_Theory." ^
191 (if syntax then "syntax_declaration" else "declaration") ^ " " ^
192 Bool.toString pervasive ^ " declaration)")
193 |> Context.proof_map;
198 fun simproc_setup name lhss (txt, pos) identifier =
200 |> ML_Context.expression pos
201 "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
202 ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
203 \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
204 \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
205 |> Context.proof_map;
210 fun hide_names intern check hide fully xnames thy =
212 val names = map (intern thy) xnames;
213 val bads = filter_out (check thy) names;
215 if null bads then fold (hide fully) names thy
216 else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
219 val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
220 val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
221 val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
223 hide_names Global_Theory.intern_fact Global_Theory.defined_fact Global_Theory.hide_fact;
228 fun goal opt_chain goal stmt int =
229 opt_chain #> goal NONE (K I) stmt int;
231 val have = goal I Proof.have_cmd;
232 val hence = goal Proof.chain Proof.have_cmd;
233 val show = goal I Proof.show_cmd;
234 val thus = goal Proof.chain Proof.show_cmd;
239 fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
240 val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
241 val local_default_proof = Toplevel.proof Proof.local_default_proof;
242 val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
243 val local_done_proof = Toplevel.proof Proof.local_done_proof;
244 val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
246 val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
251 fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
252 val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof;
253 val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
254 val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
255 val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
256 val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
258 val skip_global_qed = Toplevel.skip_proof_to_theory (fn n => n = 1);
263 fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed;
264 fun terminal_proof m = local_terminal_proof m o global_terminal_proof m;
265 val default_proof = local_default_proof o global_default_proof;
266 val immediate_proof = local_immediate_proof o global_immediate_proof;
267 val done_proof = local_done_proof o global_done_proof;
268 val skip_proof = local_skip_proof o global_skip_proof;
271 (* diagnostic ML evaluation *)
273 structure Diag_State = Proof_Data
275 type T = Toplevel.state;
276 fun init _ = Toplevel.toplevel;
279 fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
281 try Toplevel.generic_theory_of state
282 |> Option.map (Context.proof_of #> Diag_State.put state)
283 in ML_Context.eval_text_in opt_ctxt verbose pos txt end);
285 fun diag_state () = Diag_State.get (ML_Context.the_local_context ());
288 Proof.goal (Toplevel.proof_of (diag_state ()))
289 handle Toplevel.UNDEF => error "No goal present";
291 val _ = ML_Antiquote.value "Isar.state" (Scan.succeed "Isar_Cmd.diag_state ()");
292 val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()");
295 (* present draft files *)
297 fun display_drafts files = Toplevel.imperative (fn () =>
298 let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
299 in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
301 fun print_drafts files = Toplevel.imperative (fn () =>
302 let val outfile = File.shell_path (Present.drafts "ps" files)
303 in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
306 (* print parts of theory and proof context *)
308 val print_context = Toplevel.keep Toplevel.print_state_context;
310 fun print_theory verbose = Toplevel.unknown_theory o
311 Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of);
313 val print_syntax = Toplevel.unknown_context o
314 Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);
316 val print_abbrevs = Toplevel.unknown_context o
317 Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of);
319 val print_facts = Toplevel.unknown_context o
320 Toplevel.keep (ProofContext.print_lthms o Toplevel.context_of);
322 val print_configs = Toplevel.unknown_context o
323 Toplevel.keep (Attrib.print_configs o Toplevel.context_of);
325 val print_theorems_proof =
326 Toplevel.keep (ProofContext.print_lthms o Proof.context_of o Toplevel.proof_of);
328 fun print_theorems_theory verbose = Toplevel.keep (fn state =>
329 Toplevel.theory_of state |>
330 (case Toplevel.previous_context_of state of
331 SOME prev => Proof_Display.print_theorems_diff verbose (ProofContext.theory_of prev)
332 | NONE => Proof_Display.print_theorems verbose));
334 fun print_theorems verbose =
335 Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof;
337 val print_locales = Toplevel.unknown_theory o
338 Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
340 fun print_locale (verbose, name) = Toplevel.unknown_theory o
341 Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) verbose name);
343 fun print_registrations name = Toplevel.unknown_context o
344 Toplevel.keep (fn state =>
345 Locale.print_registrations (Toplevel.context_of state) name);
347 fun print_dependencies (clean, expression) = Toplevel.unknown_context o
348 Toplevel.keep (fn state =>
349 Expression.print_dependencies (Toplevel.context_of state) clean expression);
351 val print_attributes = Toplevel.unknown_theory o
352 Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
354 val print_simpset = Toplevel.unknown_context o
355 Toplevel.keep (fn state =>
356 let val ctxt = Toplevel.context_of state
357 in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end);
359 val print_rules = Toplevel.unknown_context o
360 Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of);
362 val print_trans_rules = Toplevel.unknown_context o
363 Toplevel.keep (Calculation.print_rules o Toplevel.context_of);
365 val print_methods = Toplevel.unknown_theory o
366 Toplevel.keep (Method.print_methods o Toplevel.theory_of);
368 val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations;
370 val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
372 val thy = Toplevel.theory_of state;
373 val thy_session = Present.session_name thy;
375 val all_thys = rev (thy :: Theory.ancestors_of thy);
376 val gr = all_thys |> map (fn node =>
378 val name = Context.theory_name node;
379 val parents = map Context.theory_name (Theory.parents_of node);
380 val session = Present.session_name node;
381 val unfold = (session = thy_session);
382 in {name = name, ID = name, parents = parents, dir = session, unfold = unfold, path = ""} end);
383 in Present.display_graph gr end);
385 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
387 val thy = Toplevel.theory_of state;
388 val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
389 val classes = Sorts.classes_of algebra;
390 fun entry (c, (i, (_, cs))) =
391 (i, {name = Name_Space.extern space c, ID = c, parents = cs,
392 dir = "", unfold = true, path = ""});
394 Graph.fold (cons o entry) classes []
395 |> sort (int_ord o pairself #1) |> map #2;
396 in Present.display_graph gr end);
398 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
399 Thm_Deps.thm_deps (Toplevel.theory_of state)
400 (Attrib.eval_thms (Toplevel.context_of state) args));
403 (* find unused theorems *)
405 fun unused_thms opt_range = Toplevel.keep (fn state =>
407 val thy = Toplevel.theory_of state;
408 val ctxt = Toplevel.context_of state;
409 fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]);
410 val get_theory = Context.get_theory thy;
414 NONE => (Theory.parents_of thy, [thy])
415 | SOME (xs, NONE) => (map get_theory xs, [thy])
416 | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
417 |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
421 (* print proof context contents *)
423 val print_binds = Toplevel.unknown_context o
424 Toplevel.keep (ProofContext.print_binds o Toplevel.context_of);
426 val print_cases = Toplevel.unknown_context o
427 Toplevel.keep (ProofContext.print_cases o Toplevel.context_of);
430 (* print theorems, terms, types etc. *)
434 fun string_of_stmts ctxt args =
435 Attrib.eval_thms ctxt args
436 |> map (Element.pretty_statement ctxt Thm.theoremK)
437 |> Pretty.chunks2 |> Pretty.string_of;
439 fun string_of_thms ctxt args =
440 Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args));
442 fun string_of_prfs full state arg =
447 val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
448 val thy = ProofContext.theory_of ctxt;
449 val prf = Thm.proof_of thm;
450 val prop = Thm.full_prop_of thm;
451 val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
453 Proof_Syntax.pretty_proof ctxt
454 (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
457 let val ctxt = Toplevel.context_of state
458 in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end
461 fun string_of_prop ctxt s =
463 val prop = Syntax.read_prop ctxt s;
464 val ctxt' = Variable.auto_fixes prop ctxt;
465 in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
467 fun string_of_term ctxt s =
469 val t = Syntax.read_term ctxt s;
470 val T = Term.type_of t;
471 val ctxt' = Variable.auto_fixes t ctxt;
474 (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
475 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
478 fun string_of_type ctxt s =
479 let val T = Syntax.read_typ ctxt s
480 in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
482 fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
483 Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
487 val print_stmts = print_item (string_of_stmts o Toplevel.context_of);
488 val print_thms = print_item (string_of_thms o Toplevel.context_of);
489 val print_prfs = print_item o string_of_prfs;
490 val print_prop = print_item (string_of_prop o Toplevel.context_of);
491 val print_term = print_item (string_of_term o Toplevel.context_of);
492 val print_type = print_item (string_of_type o Toplevel.context_of);
497 (* markup commands *)
499 fun check_text (txt, pos) state =
500 (Position.report pos Markup.doc_source;
501 ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
503 fun header_markup txt = Toplevel.keep (fn state =>
504 if Toplevel.is_toplevel state then check_text txt state
505 else raise Toplevel.UNDEF);
507 fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt);
508 val proof_markup = Toplevel.present_proof o check_text;