--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Tue Jun 11 19:11:31 2013 -0400
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Tue Jun 11 19:58:09 2013 -0400
@@ -2,8 +2,16 @@
Author: Jasmin Blanchette, TU Muenchen
Author: Steffen Juilf Smolka, TU Muenchen
-Supplement term with explicit type constraints that show up as
-type annotations when printing the term.
+Supplements term with a locally minmal, complete set of type constraints.
+Complete: The constraints suffice to infer the term's types.
+Minimal: Reducing the set of constraints further will make it incomplete.
+
+When configuring the pretty printer appropriately, the constraints will show up
+as type annotations when printing the term. This allows the term to be reparsed
+without a change of types.
+
+NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
+syntax.
*)
signature SLEDGEHAMMER_ANNOTATE =
@@ -42,9 +50,14 @@
(* (1) Generalize types *)
fun generalize_types ctxt t =
- t |> map_types (fn _ => dummyT)
- |> Syntax.check_term
- (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
+ let
+ val erase_types = map_types (fn _ => dummyT)
+ (* use schematic type variables *)
+ val ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_pattern
+ val infer_types = singleton (Type_Infer_Context.infer_types ctxt)
+ in
+ t |> erase_types |> infer_types
+ end
(* (2) Typing-spot table *)
local
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Jun 11 19:11:31 2013 -0400
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Jun 11 19:58:09 2013 -0400
@@ -463,8 +463,10 @@
else
of_show_have qs
fun add_term term (s, ctxt) =
- (s ^ (annotate_types ctxt term
- |> with_vanilla_print_mode (Syntax.string_of_term ctxt)
+ (s ^ (term
+ |> singleton (Syntax.uncheck_terms ctxt)
+ |> annotate_types ctxt
+ |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
|> simplify_spaces
|> maybe_quote),
ctxt |> Variable.auto_fixes term)