lib: add ShowTypes, tool to show terms with unambiguous type annotations.
This commit is contained in:
parent
fe8baa86ea
commit
5ef9eb55da
|
@ -19,6 +19,7 @@ imports
|
|||
Eisbach_Methods
|
||||
"~~/src/HOL/Eisbach/Eisbach_Tools"
|
||||
Insulin
|
||||
ShowTypes
|
||||
begin
|
||||
|
||||
section "Detect unused meta-forall"
|
||||
|
|
|
@ -0,0 +1,154 @@
|
|||
(*
|
||||
* @LICENSE(NICTA_BSD)
|
||||
*
|
||||
* ShowTypes: show "hidden" type constraints in terms.
|
||||
* This is a simple utility around Sledgehammer's type annotation code.
|
||||
*
|
||||
* Based on Sledgehammer_Isar_Annotate and related modules
|
||||
* (by Blanchette and Smolka).
|
||||
*
|
||||
*
|
||||
* Usage
|
||||
* ----
|
||||
* This theory provides the improper commands
|
||||
* term_show_types <term>
|
||||
* thm_show_types <thm> [<thm> ...]
|
||||
* goal_show_types [N]
|
||||
* as well as the ML function Show_Types.term_show_types.
|
||||
*
|
||||
* term_show_types and thm_show_types can be used as replacements
|
||||
* for the term and thm commands.
|
||||
*
|
||||
*
|
||||
* Known issues
|
||||
* ----
|
||||
* \<bullet> Type constraints for variables, etc. are not always printed.
|
||||
* In that case, set show_types/show_sorts to get extra annotations.
|
||||
*
|
||||
* \<bullet> Doesn't print sort constraints. show_sorts will print them but
|
||||
* the output may not be formatted properly.
|
||||
*
|
||||
* \<bullet> Doesn't compose with other term-display utils like Insulin.
|
||||
*)
|
||||
|
||||
theory ShowTypes imports
|
||||
Main
|
||||
keywords "term_show_types" "thm_show_types" "goal_show_types" :: diag
|
||||
begin
|
||||
|
||||
ML {*
|
||||
structure Show_Types = struct
|
||||
|
||||
fun pretty_markup_to_string no_markup =
|
||||
Pretty.string_of
|
||||
#> YXML.parse_body
|
||||
#> (if no_markup then XML.content_of else YXML.string_of_body)
|
||||
|
||||
fun term_show_types no_markup ctxt term =
|
||||
let val keywords = Thy_Header.get_keywords' ctxt
|
||||
val ctxt' = ctxt
|
||||
|> Config.put show_markup false
|
||||
|> Config.put Printer.show_type_emphasis false
|
||||
|
||||
(* FIXME: the sledgehammer code also sets these,
|
||||
* but do we always want to force them on the user? *)
|
||||
(*
|
||||
|> Config.put show_types false
|
||||
|> Config.put show_sorts false
|
||||
|> Config.put show_consts false
|
||||
*)
|
||||
|> Variable.auto_fixes term
|
||||
in
|
||||
singleton (Syntax.uncheck_terms ctxt') term
|
||||
|> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt'
|
||||
|> Syntax.unparse_term ctxt'
|
||||
|> pretty_markup_to_string no_markup
|
||||
end
|
||||
|
||||
fun goal_show_types no_markup ctxt goal n = let
|
||||
val subgoals = goal |> Thm.prems_of
|
||||
val subgoals = if n = 0 then subgoals else
|
||||
if n < 1 orelse n > length subgoals then
|
||||
(* trigger error *) [Logic.get_goal (Thm.term_of (Thm.cprop_of goal)) n]
|
||||
else [nth subgoals (n - 1)]
|
||||
val results = map (fn t => (NONE, term_show_types no_markup ctxt t)
|
||||
handle ex as TERM _ => (SOME ex, term_show_types no_markup ctxt t))
|
||||
subgoals
|
||||
in if null results
|
||||
then error "No subgoals to show"
|
||||
else if forall (Option.isSome o fst) results
|
||||
then raise the (fst (hd results))
|
||||
else map snd results
|
||||
end
|
||||
|
||||
end;
|
||||
|
||||
Outer_Syntax.command @{command_keyword term_show_types}
|
||||
"term_show_types TERM -> show TERM with type annotations"
|
||||
(Parse.term >> (fn t =>
|
||||
Toplevel.keep (fn state =>
|
||||
let val ctxt = Toplevel.context_of state in
|
||||
Show_Types.term_show_types false ctxt (Syntax.read_term ctxt t)
|
||||
|> writeln end)));
|
||||
|
||||
Outer_Syntax.command @{command_keyword thm_show_types}
|
||||
"thm_show_types THM1 THM2 ... -> show theorems with type annotations"
|
||||
(Parse.xthms1 >> (fn ts =>
|
||||
Toplevel.keep (fn state =>
|
||||
let val ctxt = Toplevel.context_of state in
|
||||
Attrib.eval_thms ctxt ts
|
||||
|> app (Thm.prop_of #> Show_Types.term_show_types false ctxt #> writeln) end)));
|
||||
|
||||
let
|
||||
fun print_subgoals (x::xs) n = (writeln (Int.toString n ^ ". " ^ x); print_subgoals xs (n+1))
|
||||
| print_subgoals [] _ = ();
|
||||
in
|
||||
Outer_Syntax.command @{command_keyword goal_show_types}
|
||||
"goal_show_types [N] -> show subgoals (or Nth goal) with type annotations"
|
||||
(Scan.option Parse.int >> (fn n =>
|
||||
Toplevel.keep (fn state =>
|
||||
let val ctxt = Toplevel.context_of state
|
||||
val goal = Toplevel.proof_of state |> Proof.raw_goal |> #goal
|
||||
in Show_Types.goal_show_types false ctxt goal (Option.getOpt (n, 0))
|
||||
|> (fn xs => case xs of
|
||||
[x] => writeln x
|
||||
| _ => print_subgoals xs 1) end)))
|
||||
end;
|
||||
*}
|
||||
|
||||
|
||||
text \<open>
|
||||
Simple demo. The main HOL theories don't have that much
|
||||
hidden polymorphism, so we use l4.verified.
|
||||
\<close>
|
||||
|
||||
(*
|
||||
experiment begin
|
||||
lemma c_guard_cast_byte: "c_guard (x :: ('a :: {mem_type}) ptr) \<Longrightarrow> c_guard (ptr_coerce x :: 8 word ptr)"
|
||||
goal_show_types 0
|
||||
using [[show_sorts]]
|
||||
goal_show_types 0
|
||||
apply (case_tac x)
|
||||
apply (fastforce intro!: byte_ptr_guarded simp: c_guard_def dest: c_null_guard)
|
||||
done
|
||||
|
||||
thm c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word))"]
|
||||
thm_show_types c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word))"]
|
||||
|
||||
(* Round-trip test *)
|
||||
ML {*
|
||||
let val ctxt = Config.put show_sorts true @{context}
|
||||
(* NB: this test fails if we leave some polymorphism in the term *)
|
||||
val term = @{thm c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word)) :: unit ptr"]} |> Thm.prop_of
|
||||
val string_no_types = Syntax.pretty_term ctxt term
|
||||
|> Pretty.string_of |> YXML.content_of
|
||||
val string_show_types = Show_Types.term_show_types true ctxt term
|
||||
|
||||
val _ = assert (Syntax.read_term ctxt string_no_types <> term) "Show_Types test (baseline)"
|
||||
val _ = assert (Syntax.read_term ctxt string_show_types = term) "Show_Types test"
|
||||
in () end
|
||||
*}
|
||||
end
|
||||
*)
|
||||
|
||||
end
|
Loading…
Reference in New Issue