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