uncheck terms before annotation to avoid awkward syntax
authorsmolkas
Tue Jun 11 19:58:09 2013 -0400 (2013-06-11 ago)
changeset 523690b395800fdf0
parent 52368 13ca6876f748
child 52370 ec46a485bf60
uncheck terms before annotation to avoid awkward syntax
src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Jun 11 19:11:31 2013 -0400
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Jun 11 19:58:09 2013 -0400
     1.3 @@ -2,8 +2,16 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5      Author:     Steffen Juilf Smolka, TU Muenchen
     1.6  
     1.7 -Supplement term with explicit type constraints that show up as
     1.8 -type annotations when printing the term.
     1.9 +Supplements term with a locally minmal, complete set of type constraints.
    1.10 +Complete: The constraints suffice to infer the term's types.
    1.11 +Minimal: Reducing the set of constraints further will make it incomplete.
    1.12 +
    1.13 +When configuring the pretty printer appropriately, the constraints will show up
    1.14 +as type annotations when printing the term. This allows the term to be reparsed
    1.15 +without a change of types.
    1.16 +
    1.17 +NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
    1.18 +syntax.
    1.19  *)
    1.20  
    1.21  signature SLEDGEHAMMER_ANNOTATE =
    1.22 @@ -42,9 +50,14 @@
    1.23  
    1.24  (* (1) Generalize types *)
    1.25  fun generalize_types ctxt t =
    1.26 -  t |> map_types (fn _ => dummyT)
    1.27 -    |> Syntax.check_term
    1.28 -         (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    1.29 +  let
    1.30 +    val erase_types = map_types (fn _ => dummyT)
    1.31 +    (* use schematic type variables *)
    1.32 +    val ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_pattern
    1.33 +    val infer_types = singleton (Type_Infer_Context.infer_types ctxt)
    1.34 +  in
    1.35 +     t |> erase_types |> infer_types
    1.36 +  end
    1.37  
    1.38  (* (2) Typing-spot table *)
    1.39  local
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jun 11 19:11:31 2013 -0400
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jun 11 19:58:09 2013 -0400
     2.3 @@ -463,8 +463,10 @@
     2.4        else
     2.5          of_show_have qs
     2.6      fun add_term term (s, ctxt) =
     2.7 -      (s ^ (annotate_types ctxt term
     2.8 -            |> with_vanilla_print_mode (Syntax.string_of_term ctxt)
     2.9 +      (s ^ (term
    2.10 +            |> singleton (Syntax.uncheck_terms ctxt)
    2.11 +            |> annotate_types ctxt
    2.12 +            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
    2.13              |> simplify_spaces
    2.14              |> maybe_quote),
    2.15         ctxt |> Variable.auto_fixes term)