remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
authorblanchet
Wed Apr 28 13:00:30 2010 +0200 (2010-04-28)
changeset 3648832c92af68ec9
parent 36487 50fd056cc3ce
child 36489 2b2a2c55d787
remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
what we need is smarter type annotations for variables _and_ constants
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Apr 28 12:49:52 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Apr 28 13:00:30 2010 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  (* minimalization of thms *)
     1.5  
     1.6  fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
     1.7 -                                  shrink_factor, sorts, ...})
     1.8 +                                  shrink_factor, ...})
     1.9                        i n state name_thms_pairs =
    1.10    let
    1.11      val thy = Proof.theory_of state
    1.12 @@ -109,8 +109,7 @@
    1.13          in
    1.14            (SOME min_thms,
    1.15             proof_text isar_proof
    1.16 -                      (pool, debug, shrink_factor, sorts, ctxt,
    1.17 -                       conjecture_shape)
    1.18 +                      (pool, debug, shrink_factor, ctxt, conjecture_shape)
    1.19                        (K "", proof, internal_thm_names, goal, i) |> fst)
    1.20          end
    1.21      | {outcome = SOME TimedOut, ...} =>
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 28 12:49:52 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 28 13:00:30 2010 +0200
     2.3 @@ -99,7 +99,6 @@
     2.4     ("follow_defs", "false"),
     2.5     ("isar_proof", "false"),
     2.6     ("shrink_factor", "1"),
     2.7 -   ("sorts", "false"),
     2.8     ("minimize_timeout", "5 s")]
     2.9  
    2.10  val alias_params =
    2.11 @@ -113,12 +112,11 @@
    2.12     ("ignore_no_atp", "respect_no_atp"),
    2.13     ("theory_irrelevant", "theory_relevant"),
    2.14     ("dont_follow_defs", "follow_defs"),
    2.15 -   ("metis_proof", "isar_proof"),
    2.16 -   ("no_sorts", "sorts")]
    2.17 +   ("metis_proof", "isar_proof")]
    2.18  
    2.19  val params_for_minimize =
    2.20    ["debug", "verbose", "overlord", "full_types", "explicit_apply",
    2.21 -   "isar_proof", "shrink_factor", "sorts", "minimize_timeout"]
    2.22 +   "isar_proof", "shrink_factor", "minimize_timeout"]
    2.23  
    2.24  val property_dependent_params = ["atps", "full_types", "timeout"]
    2.25  
    2.26 @@ -201,7 +199,6 @@
    2.27      val follow_defs = lookup_bool "follow_defs"
    2.28      val isar_proof = lookup_bool "isar_proof"
    2.29      val shrink_factor = Int.max (1, lookup_int "shrink_factor")
    2.30 -    val sorts = lookup_bool "sorts"
    2.31      val timeout = lookup_time "timeout"
    2.32      val minimize_timeout = lookup_time "minimize_timeout"
    2.33    in
    2.34 @@ -210,7 +207,7 @@
    2.35       respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
    2.36       convergence = convergence, theory_relevant = theory_relevant,
    2.37       follow_defs = follow_defs, isar_proof = isar_proof,
    2.38 -     shrink_factor = shrink_factor, sorts = sorts, timeout = timeout,
    2.39 +     shrink_factor = shrink_factor, timeout = timeout,
    2.40       minimize_timeout = minimize_timeout}
    2.41    end
    2.42  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 12:49:52 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 13:00:30 2010 +0200
     3.3 @@ -21,11 +21,11 @@
     3.4      minimize_command * string * string vector * thm * int
     3.5      -> string * string list
     3.6    val isar_proof_text:
     3.7 -    name_pool option * bool * int * bool * Proof.context * int list list
     3.8 +    name_pool option * bool * int * Proof.context * int list list
     3.9      -> minimize_command * string * string vector * thm * int
    3.10      -> string * string list
    3.11    val proof_text:
    3.12 -    bool -> name_pool option * bool * int * bool * Proof.context * int list list
    3.13 +    bool -> name_pool option * bool * int * Proof.context * int list list
    3.14      -> minimize_command * string * string vector * thm * int
    3.15      -> string * string list
    3.16  end;
    3.17 @@ -830,7 +830,7 @@
    3.18        | aux subst depth nextp (ps :: proof) = ps :: aux subst depth nextp proof
    3.19    in aux [] 0 (1, 1) end
    3.20  
    3.21 -fun string_for_proof ctxt sorts i n =
    3.22 +fun string_for_proof ctxt i n =
    3.23    let
    3.24      fun fix_print_mode f =
    3.25        PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    3.26 @@ -883,9 +883,9 @@
    3.27          do_indent 0 ^ "proof -\n" ^
    3.28          do_steps "" "" 1 proof ^
    3.29          do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
    3.30 -  in setmp_CRITICAL show_sorts sorts do_proof end
    3.31 +  in do_proof end
    3.32  
    3.33 -fun isar_proof_text (pool, debug, shrink_factor, sorts, ctxt, conjecture_shape)
    3.34 +fun isar_proof_text (pool, debug, shrink_factor, ctxt, conjecture_shape)
    3.35                      (minimize_command, atp_proof, thm_names, goal, i) =
    3.36    let
    3.37      val thy = ProofContext.theory_of ctxt
    3.38 @@ -901,7 +901,7 @@
    3.39             |> then_chain_proof
    3.40             |> kill_useless_labels_in_proof
    3.41             |> relabel_proof
    3.42 -           |> string_for_proof ctxt sorts i n of
    3.43 +           |> string_for_proof ctxt i n of
    3.44          "" => ""
    3.45        | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
    3.46      val isar_proof =