1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(*
8 * ShowTypes: show "hidden" type constraints in terms.
9 * This is a simple utility around Sledgehammer's type annotation code.
10 *
11 * Based on Sledgehammer_Isar_Annotate and related modules
12 * (by Blanchette and Smolka).
13 *
14 *
15 * Usage
16 * ----
17 * This theory provides the improper commands
18 *   term_show_types <term>
19 *   thm_show_types <thm> [<thm> ...]
20 *   goal_show_types [N]
21 * as well as the ML function Show_Types.term_show_types.
22 *
23 * term_show_types and thm_show_types can be used as replacements
24 * for the term and thm commands.
25 *
26 *
27 * Known issues
28 * ----
29 * \<bullet> Type constraints for variables, etc. are not always printed.
30 *   In that case, set show_types/show_sorts to get extra annotations.
31 *
32 * \<bullet> Doesn't print sort constraints. show_sorts will print them but
33 *   the output may not be formatted properly.
34 *
35 * \<bullet> Doesn't compose with other term-display utils like Insulin.
36 *)
37
38theory ShowTypes imports
39  Main
40keywords "term_show_types" "thm_show_types" "goal_show_types" :: diag
41begin
42
43ML \<open>
44structure Show_Types = struct
45
46fun pretty_markup_to_string no_markup =
47  Pretty.string_of
48  #> YXML.parse_body
49  #> (if no_markup then XML.content_of else YXML.string_of_body)
50
51fun term_show_types no_markup ctxt term =
52  let val keywords = Thy_Header.get_keywords' ctxt
53      val ctxt' = ctxt
54      |> Config.put show_markup false
55      |> Config.put Printer.show_type_emphasis false
56
57      (* FIXME: the sledgehammer code also sets these,
58       *        but do we always want to force them on the user? *)
59      (*
60      |> Config.put show_types false
61      |> Config.put show_sorts false
62      |> Config.put show_consts false
63      *)
64      |> Proof_Context.augment term
65  in
66    singleton (Syntax.uncheck_terms ctxt') term
67    |> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt'
68    |> Syntax.unparse_term ctxt'
69    |> pretty_markup_to_string no_markup
70  end
71
72fun goal_show_types no_markup ctxt goal n = let
73  val subgoals = goal |> Thm.prems_of
74  val subgoals = if n = 0 then subgoals else
75                 if n < 1 orelse n > length subgoals then
76                      (* trigger error *) [Logic.get_goal (Thm.term_of (Thm.cprop_of goal)) n]
77                 else [nth subgoals (n - 1)]
78  val results = map (fn t => (NONE, term_show_types no_markup ctxt t)
79                             handle ex as TERM _ => (SOME ex, term_show_types no_markup ctxt t))
80                    subgoals
81  in if null results
82        then error "No subgoals to show"
83     else if forall (Option.isSome o fst) results
84        then raise the (fst (hd results))
85     else map snd results
86  end
87
88end;
89
90Outer_Syntax.command @{command_keyword term_show_types}
91  "term_show_types TERM -> show TERM with type annotations"
92  (Parse.term >> (fn t =>
93    Toplevel.keep (fn state =>
94      let val ctxt = Toplevel.context_of state in
95        Show_Types.term_show_types false ctxt (Syntax.read_term ctxt t)
96        |> writeln end)));
97
98Outer_Syntax.command @{command_keyword thm_show_types}
99  "thm_show_types THM1 THM2 ... -> show theorems with type annotations"
100  (Parse.thms1 >> (fn ts =>
101    Toplevel.keep (fn state =>
102      let val ctxt = Toplevel.context_of state in
103        Attrib.eval_thms ctxt ts
104        |> app (Thm.prop_of #> Show_Types.term_show_types false ctxt #> writeln) end)));
105
106let
107  fun print_subgoals (x::xs) n = (writeln (Int.toString n ^ ". " ^ x); print_subgoals xs (n+1))
108    | print_subgoals [] _ = ();
109in
110Outer_Syntax.command @{command_keyword goal_show_types}
111  "goal_show_types [N] -> show subgoals (or Nth goal) with type annotations"
112  (Scan.option Parse.int >> (fn n =>
113    Toplevel.keep (fn state =>
114      let val ctxt = Toplevel.context_of state
115          val goal = Toplevel.proof_of state |> Proof.raw_goal |> #goal
116      in Show_Types.goal_show_types false ctxt goal (Option.getOpt (n, 0))
117         |> (fn xs => case xs of
118                         [x] => writeln x
119                       | _ => print_subgoals xs 1) end)))
120end;
121\<close>
122
123end
124