src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 36281 dbbf4d5d584d
parent 36235 61159615a0c5
child 36290 c29283184c7a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 21 14:46:29 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 21 16:21:19 2010 +0200
     1.3 @@ -68,6 +68,10 @@
     1.4     ("metis_proof", "isar_proof"),
     1.5     ("no_sorts", "sorts")]
     1.6  
     1.7 +val params_for_minimize =
     1.8 +  ["full_types", "explicit_apply", "higher_order", "isar_proof", "modulus",
     1.9 +   "sorts", "minimize_timeout"]
    1.10 +
    1.11  val property_dependent_params = ["atps", "full_types", "timeout"]
    1.12  
    1.13  fun is_known_raw_param s =
    1.14 @@ -219,18 +223,33 @@
    1.15  val refresh_tptpN = "refresh_tptp"
    1.16  val helpN = "help"
    1.17  
    1.18 -
    1.19  fun minimizize_raw_param_name "timeout" = "minimize_timeout"
    1.20    | minimizize_raw_param_name name = name
    1.21  
    1.22 +val is_raw_param_relevant_for_minimize =
    1.23 +  member (op =) params_for_minimize o fst o unalias_raw_param
    1.24 +fun string_for_raw_param (key, values) =
    1.25 +  key ^ (case space_implode " " values of
    1.26 +           "" => ""
    1.27 +         | value => " = " ^ value)
    1.28 +
    1.29 +fun minimize_command override_params i atp_name facts =
    1.30 +  "sledgehammer minimize [atp = " ^ atp_name ^
    1.31 +  (override_params |> filter is_raw_param_relevant_for_minimize
    1.32 +                   |> implode o map (prefix ", " o string_for_raw_param)) ^
    1.33 +  "] (" ^ space_implode " " facts ^ ")" ^
    1.34 +  (if i = 1 then "" else " " ^ string_of_int i)
    1.35 +
    1.36  fun hammer_away override_params subcommand opt_i relevance_override state =
    1.37    let
    1.38      val thy = Proof.theory_of state
    1.39      val _ = List.app check_raw_param override_params
    1.40    in
    1.41      if subcommand = runN then
    1.42 -      sledgehammer (get_params thy override_params) (the_default 1 opt_i)
    1.43 -                   relevance_override state
    1.44 +      let val i = the_default 1 opt_i in
    1.45 +        sledgehammer (get_params thy override_params) i relevance_override
    1.46 +                     (minimize_command override_params i) state
    1.47 +      end
    1.48      else if subcommand = minimizeN then
    1.49        minimize (map (apfst minimizize_raw_param_name) override_params) []
    1.50                 (the_default 1 opt_i) (#add relevance_override) state