tuned ML file name
authorblanchet
Fri Jan 31 10:23:32 2014 +0100 (2014-01-31)
changeset 551987a538e58b64e
parent 55197 5a54ed681ba2
child 55199 ba93ef2c0d27
tuned ML file name
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Sledgehammer.thy
src/HOL/TPTP/MaSh_Eval.thy
src/HOL/TPTP/MaSh_Export.thy
src/HOL/TPTP/mash_eval.ML
src/HOL/TPTP/sledgehammer_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 10:02:36 2014 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 10:23:32 2014 +0100
     1.3 @@ -364,7 +364,7 @@
     1.4  fun get_prover_name ctxt args =
     1.5    let
     1.6      fun default_prover_name () =
     1.7 -      hd (#provers (Sledgehammer_Isar.default_params ctxt []))
     1.8 +      hd (#provers (Sledgehammer_Commands.default_params ctxt []))
     1.9        handle List.Empty => error "No ATP available."
    1.10    in
    1.11      (case AList.lookup (op =) args proverK of
    1.12 @@ -439,7 +439,7 @@
    1.13              #> (Option.map (Config.put ATP_Systems.force_sos)
    1.14                    force_sos |> the_default I))
    1.15      val params as {max_facts, ...} =
    1.16 -      Sledgehammer_Isar.default_params ctxt
    1.17 +      Sledgehammer_Commands.default_params ctxt
    1.18           ([("verbose", "true"),
    1.19             ("fact_filter", fact_filter),
    1.20             ("type_enc", type_enc),
    1.21 @@ -597,7 +597,7 @@
    1.22      val max_new_mono_instancesLST =
    1.23        available_parameter args max_new_mono_instancesK max_new_mono_instancesK
    1.24      val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
    1.25 -    val params = Sledgehammer_Isar.default_params ctxt
    1.26 +    val params = Sledgehammer_Commands.default_params ctxt
    1.27       ([("provers", prover_name),
    1.28         ("verbose", "true"),
    1.29         ("type_enc", type_enc),
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 31 10:02:36 2014 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 31 10:23:32 2014 +0100
     2.3 @@ -112,7 +112,7 @@
     2.4           val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
     2.5           val prover = AList.lookup (op =) args "prover" |> the_default default_prover
     2.6           val params as {max_facts, ...} =
     2.7 -           Sledgehammer_Isar.default_params ctxt args
     2.8 +           Sledgehammer_Commands.default_params ctxt args
     2.9           val default_max_facts = Sledgehammer_Provers.default_max_facts_of_prover ctxt prover
    2.10           val is_appropriate_prop =
    2.11             Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt default_prover
     3.1 --- a/src/HOL/Sledgehammer.thy	Fri Jan 31 10:02:36 2014 +0100
     3.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jan 31 10:23:32 2014 +0100
     3.3 @@ -31,6 +31,6 @@
     3.4  ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
     3.5  ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
     3.6  ML_file "Tools/Sledgehammer/sledgehammer_run.ML"
     3.7 -ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
     3.8 +ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
     3.9  
    3.10  end
     4.1 --- a/src/HOL/TPTP/MaSh_Eval.thy	Fri Jan 31 10:02:36 2014 +0100
     4.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy	Fri Jan 31 10:23:32 2014 +0100
     4.3 @@ -26,7 +26,7 @@
     4.4  
     4.5  ML {*
     4.6  val do_it = false (* switch to "true" to generate the files *)
     4.7 -val params = Sledgehammer_Isar.default_params @{context} []
     4.8 +val params = Sledgehammer_Commands.default_params @{context} []
     4.9  val range = (1, NONE)
    4.10  val linearize = false
    4.11  val dir = "List"
     5.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 31 10:02:36 2014 +0100
     5.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 31 10:23:32 2014 +0100
     5.3 @@ -29,7 +29,7 @@
     5.4  ML {*
     5.5  val do_it = false (* switch to "true" to generate the files *)
     5.6  val thys = [@{theory List}]
     5.7 -val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
     5.8 +val params as {provers, ...} = Sledgehammer_Commands.default_params @{context} []
     5.9  val prover = hd provers
    5.10  val range = (1, NONE)
    5.11  val step = 1
     6.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jan 31 10:02:36 2014 +0100
     6.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jan 31 10:23:32 2014 +0100
     6.3 @@ -29,7 +29,7 @@
     6.4  open Sledgehammer_MePo
     6.5  open Sledgehammer_MaSh
     6.6  open Sledgehammer_Provers
     6.7 -open Sledgehammer_Isar
     6.8 +open Sledgehammer_Commands
     6.9  
    6.10  val prefix = Library.prefix
    6.11  
     7.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 10:02:36 2014 +0100
     7.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 10:23:32 2014 +0100
     7.3 @@ -22,7 +22,7 @@
     7.4  open Sledgehammer_Fact
     7.5  open Sledgehammer_Provers
     7.6  open Sledgehammer_MaSh
     7.7 -open Sledgehammer_Isar
     7.8 +open Sledgehammer_Commands
     7.9  
    7.10  fun run_prover override_params fact_override i n ctxt goal =
    7.11    let
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Jan 31 10:23:32 2014 +0100
     8.3 @@ -0,0 +1,496 @@
     8.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_commands.ML
     8.5 +    Author:     Jasmin Blanchette, TU Muenchen
     8.6 +
     8.7 +Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
     8.8 +*)
     8.9 +
    8.10 +signature SLEDGEHAMMER_COMMANDS =
    8.11 +sig
    8.12 +  type params = Sledgehammer_Provers.params
    8.13 +
    8.14 +  val provers : string Unsynchronized.ref
    8.15 +  val default_params : Proof.context -> (string * string) list -> params
    8.16 +end;
    8.17 +
    8.18 +structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS =
    8.19 +struct
    8.20 +
    8.21 +open ATP_Util
    8.22 +open ATP_Systems
    8.23 +open ATP_Problem_Generate
    8.24 +open ATP_Proof_Reconstruct
    8.25 +open Sledgehammer_Util
    8.26 +open Sledgehammer_Fact
    8.27 +open Sledgehammer_Provers
    8.28 +open Sledgehammer_Minimize
    8.29 +open Sledgehammer_MaSh
    8.30 +open Sledgehammer_Run
    8.31 +
    8.32 +(* val cvc3N = "cvc3" *)
    8.33 +val yicesN = "yices"
    8.34 +val z3N = "z3"
    8.35 +
    8.36 +val runN = "run"
    8.37 +val minN = "min"
    8.38 +val messagesN = "messages"
    8.39 +val supported_proversN = "supported_provers"
    8.40 +val kill_allN = "kill_all"
    8.41 +val running_proversN = "running_provers"
    8.42 +val running_learnersN = "running_learners"
    8.43 +val refresh_tptpN = "refresh_tptp"
    8.44 +
    8.45 +val _ =
    8.46 +  ProofGeneral.preference_option ProofGeneral.category_tracing
    8.47 +    NONE
    8.48 +    @{option auto_sledgehammer}
    8.49 +    "auto-sledgehammer"
    8.50 +    "Run Sledgehammer automatically"
    8.51 +
    8.52 +(** Sledgehammer commands **)
    8.53 +
    8.54 +fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
    8.55 +fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}
    8.56 +fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}
    8.57 +fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =
    8.58 +  {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
    8.59 +   only = #only r1 andalso #only r2}
    8.60 +fun merge_fact_overrides rs =
    8.61 +  fold merge_fact_override_pairwise rs (only_fact_override [])
    8.62 +
    8.63 +(*** parameters ***)
    8.64 +
    8.65 +val provers = Unsynchronized.ref ""
    8.66 +
    8.67 +val _ =
    8.68 +  ProofGeneral.preference_string ProofGeneral.category_proof
    8.69 +    NONE
    8.70 +    provers
    8.71 +    "Sledgehammer: Provers"
    8.72 +    "Default automatic provers (separated by whitespace)"
    8.73 +
    8.74 +val _ =
    8.75 +  ProofGeneral.preference_option ProofGeneral.category_proof
    8.76 +    NONE
    8.77 +    @{option sledgehammer_timeout}
    8.78 +    "Sledgehammer: Time Limit"
    8.79 +    "ATPs will be interrupted after this time (in seconds)"
    8.80 +
    8.81 +type raw_param = string * string list
    8.82 +
    8.83 +val default_default_params =
    8.84 +  [("debug", "false"),
    8.85 +   ("verbose", "false"),
    8.86 +   ("overlord", "false"),
    8.87 +   ("spy", "false"),
    8.88 +   ("blocking", "false"),
    8.89 +   ("type_enc", "smart"),
    8.90 +   ("strict", "false"),
    8.91 +   ("lam_trans", "smart"),
    8.92 +   ("uncurried_aliases", "smart"),
    8.93 +   ("learn", "true"),
    8.94 +   ("fact_filter", "smart"),
    8.95 +   ("max_facts", "smart"),
    8.96 +   ("fact_thresholds", "0.45 0.85"),
    8.97 +   ("max_mono_iters", "smart"),
    8.98 +   ("max_new_mono_instances", "smart"),
    8.99 +   ("isar_proofs", "smart"),
   8.100 +   ("compress_isar", "10"),
   8.101 +   ("try0_isar", "true"),
   8.102 +   ("slice", "true"),
   8.103 +   ("minimize", "smart"),
   8.104 +   ("preplay_timeout", "3")]
   8.105 +
   8.106 +val alias_params =
   8.107 +  [("prover", ("provers", [])), (* undocumented *)
   8.108 +   ("dont_preplay", ("preplay_timeout", ["0"])),
   8.109 +   ("dont_compress_isar", ("compress_isar", ["0"])),
   8.110 +   ("isar_proof", ("isar_proofs", [])) (* legacy *)]
   8.111 +val negated_alias_params =
   8.112 +  [("no_debug", "debug"),
   8.113 +   ("quiet", "verbose"),
   8.114 +   ("no_overlord", "overlord"),
   8.115 +   ("dont_spy", "spy"),
   8.116 +   ("non_blocking", "blocking"),
   8.117 +   ("non_strict", "strict"),
   8.118 +   ("no_uncurried_aliases", "uncurried_aliases"),
   8.119 +   ("dont_learn", "learn"),
   8.120 +   ("no_isar_proofs", "isar_proofs"),
   8.121 +   ("dont_slice", "slice"),
   8.122 +   ("dont_minimize", "minimize"),
   8.123 +   ("dont_try0_isar", "try0_isar")]
   8.124 +
   8.125 +val params_not_for_minimize =
   8.126 +  ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
   8.127 +
   8.128 +val property_dependent_params = ["provers", "timeout"]
   8.129 +
   8.130 +fun is_known_raw_param s =
   8.131 +  AList.defined (op =) default_default_params s orelse
   8.132 +  AList.defined (op =) alias_params s orelse
   8.133 +  AList.defined (op =) negated_alias_params s orelse
   8.134 +  member (op =) property_dependent_params s orelse s = "expect"
   8.135 +
   8.136 +fun is_prover_list ctxt s =
   8.137 +  case space_explode " " s of
   8.138 +    ss as _ :: _ => forall (is_prover_supported ctxt) ss
   8.139 +  | _ => false
   8.140 +
   8.141 +fun unalias_raw_param (name, value) =
   8.142 +  case AList.lookup (op =) alias_params name of
   8.143 +    SOME (name', []) => (name', value)
   8.144 +  | SOME (param' as (name', _)) =>
   8.145 +    if value <> ["false"] then
   8.146 +      param'
   8.147 +    else
   8.148 +      error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \
   8.149 +             \(cf. " ^ quote name' ^ ").")
   8.150 +  | NONE =>
   8.151 +    case AList.lookup (op =) negated_alias_params name of
   8.152 +      SOME name' => (name', case value of
   8.153 +                              ["false"] => ["true"]
   8.154 +                            | ["true"] => ["false"]
   8.155 +                            | [] => ["false"]
   8.156 +                            | _ => value)
   8.157 +    | NONE => (name, value)
   8.158 +
   8.159 +val any_type_enc = type_enc_of_string Strict "erased"
   8.160 +
   8.161 +(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
   8.162 +   can be omitted. For the last four, this is a secret feature. *)
   8.163 +fun normalize_raw_param ctxt =
   8.164 +  unalias_raw_param
   8.165 +  #> (fn (name, value) =>
   8.166 +         if is_known_raw_param name then
   8.167 +           (name, value)
   8.168 +         else if null value then
   8.169 +           if is_prover_list ctxt name then
   8.170 +             ("provers", [name])
   8.171 +           else if can (type_enc_of_string Strict) name then
   8.172 +             ("type_enc", [name])
   8.173 +           else if can (trans_lams_of_string ctxt any_type_enc) name then
   8.174 +             ("lam_trans", [name])
   8.175 +           else if member (op =) fact_filters name then
   8.176 +             ("fact_filter", [name])
   8.177 +           else if is_some (Int.fromString name) then
   8.178 +             ("max_facts", [name])
   8.179 +           else
   8.180 +             error ("Unknown parameter: " ^ quote name ^ ".")
   8.181 +         else
   8.182 +           error ("Unknown parameter: " ^ quote name ^ "."))
   8.183 +
   8.184 +(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
   8.185 +   read correctly. *)
   8.186 +val implode_param = strip_spaces_except_between_idents o space_implode " "
   8.187 +
   8.188 +(* FIXME: use "Generic_Data" *)
   8.189 +structure Data = Theory_Data
   8.190 +(
   8.191 +  type T = raw_param list
   8.192 +  val empty = default_default_params |> map (apsnd single)
   8.193 +  val extend = I
   8.194 +  fun merge data : T = AList.merge (op =) (K true) data
   8.195 +)
   8.196 +
   8.197 +(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
   8.198 +   timeout, it makes sense to put E first. *)
   8.199 +fun default_provers_param_value mode ctxt =
   8.200 +  [eN, spassN, z3N, vampireN, e_sineN, yicesN]
   8.201 +  |> map_filter (remotify_prover_if_not_installed ctxt)
   8.202 +  (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   8.203 +  |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
   8.204 +  |> implode_param
   8.205 +
   8.206 +fun set_default_raw_param param thy =
   8.207 +  let val ctxt = Proof_Context.init_global thy in
   8.208 +    thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))
   8.209 +  end
   8.210 +
   8.211 +fun default_raw_params mode ctxt =
   8.212 +  let val thy = Proof_Context.theory_of ctxt in
   8.213 +    Data.get thy
   8.214 +    |> fold (AList.default (op =))
   8.215 +            [("provers", [case !provers of
   8.216 +                            "" => default_provers_param_value mode ctxt
   8.217 +                          | s => s]),
   8.218 +             ("timeout", let val timeout = Options.default_int @{option sledgehammer_timeout} in
   8.219 +                           [if timeout <= 0 then "none"
   8.220 +                            else string_of_int timeout]
   8.221 +                         end)]
   8.222 +  end
   8.223 +
   8.224 +fun extract_params mode default_params override_params =
   8.225 +  let
   8.226 +    val raw_params = rev override_params @ rev default_params
   8.227 +    val lookup = Option.map implode_param o AList.lookup (op =) raw_params
   8.228 +    val lookup_string = the_default "" o lookup
   8.229 +    fun general_lookup_bool option default_value name =
   8.230 +      (case lookup name of
   8.231 +        SOME s => parse_bool_option option name s
   8.232 +      | NONE => default_value)
   8.233 +    val lookup_bool = the o general_lookup_bool false (SOME false)
   8.234 +    fun lookup_time name =
   8.235 +      (case lookup name of
   8.236 +        SOME s => parse_time name s
   8.237 +      | NONE => Time.zeroTime)
   8.238 +    fun lookup_int name =
   8.239 +      (case lookup name of
   8.240 +        NONE => 0
   8.241 +      | SOME s =>
   8.242 +        (case Int.fromString s of
   8.243 +          SOME n => n
   8.244 +        | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value.")))
   8.245 +    fun lookup_real name =
   8.246 +      (case lookup name of
   8.247 +        NONE => 0.0
   8.248 +      | SOME s =>
   8.249 +        (case Real.fromString s of
   8.250 +          SOME n => n
   8.251 +        | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value.")))
   8.252 +    fun lookup_real_pair name =
   8.253 +      (case lookup name of
   8.254 +        NONE => (0.0, 0.0)
   8.255 +      | SOME s =>
   8.256 +        (case s |> space_explode " " |> map Real.fromString of
   8.257 +          [SOME r1, SOME r2] => (r1, r2)
   8.258 +        | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \
   8.259 +                 \values (e.g., \"0.6 0.95\")")))
   8.260 +    fun lookup_option lookup' name =
   8.261 +      (case lookup name of
   8.262 +        SOME "smart" => NONE
   8.263 +      | _ => SOME (lookup' name))
   8.264 +    val debug = mode <> Auto_Try andalso lookup_bool "debug"
   8.265 +    val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
   8.266 +    val overlord = lookup_bool "overlord"
   8.267 +    val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
   8.268 +    val blocking =
   8.269 +      Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
   8.270 +      lookup_bool "blocking"
   8.271 +    val provers = lookup_string "provers" |> space_explode " "
   8.272 +                  |> mode = Auto_Try ? single o hd
   8.273 +    val type_enc =
   8.274 +      if mode = Auto_Try then
   8.275 +        NONE
   8.276 +      else case lookup_string "type_enc" of
   8.277 +        "smart" => NONE
   8.278 +      | s => (type_enc_of_string Strict s; SOME s)
   8.279 +    val strict = mode = Auto_Try orelse lookup_bool "strict"
   8.280 +    val lam_trans = lookup_option lookup_string "lam_trans"
   8.281 +    val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
   8.282 +    val learn = lookup_bool "learn"
   8.283 +    val fact_filter =
   8.284 +      lookup_option lookup_string "fact_filter"
   8.285 +      |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf)
   8.286 +    val max_facts = lookup_option lookup_int "max_facts"
   8.287 +    val fact_thresholds = lookup_real_pair "fact_thresholds"
   8.288 +    val max_mono_iters = lookup_option lookup_int "max_mono_iters"
   8.289 +    val max_new_mono_instances =
   8.290 +      lookup_option lookup_int "max_new_mono_instances"
   8.291 +    val isar_proofs = lookup_option lookup_bool "isar_proofs"
   8.292 +    val compress_isar = Real.max (1.0, lookup_real "compress_isar")
   8.293 +    val try0_isar = lookup_bool "try0_isar"
   8.294 +    val slice = mode <> Auto_Try andalso lookup_bool "slice"
   8.295 +    val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
   8.296 +    val timeout = lookup_time "timeout"
   8.297 +    val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout"
   8.298 +    val expect = lookup_string "expect"
   8.299 +  in
   8.300 +    {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,
   8.301 +     provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
   8.302 +     uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
   8.303 +     max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
   8.304 +     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
   8.305 +     compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
   8.306 +     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   8.307 +  end
   8.308 +
   8.309 +fun get_params mode = extract_params mode o default_raw_params mode
   8.310 +fun default_params thy = get_params Normal thy o map (apsnd single)
   8.311 +
   8.312 +(* Sledgehammer the given subgoal *)
   8.313 +
   8.314 +val default_minimize_prover = metisN
   8.315 +
   8.316 +fun is_raw_param_relevant_for_minimize (name, _) =
   8.317 +  not (member (op =) params_not_for_minimize name)
   8.318 +fun string_of_raw_param (key, values) =
   8.319 +  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
   8.320 +fun nice_string_of_raw_param (p as (key, ["false"])) =
   8.321 +    (case AList.find (op =) negated_alias_params key of
   8.322 +       [neg] => neg
   8.323 +     | _ => string_of_raw_param p)
   8.324 +  | nice_string_of_raw_param p = string_of_raw_param p
   8.325 +
   8.326 +fun minimize_command override_params i more_override_params prover_name
   8.327 +                     fact_names =
   8.328 +  let
   8.329 +    val params =
   8.330 +      (override_params
   8.331 +       |> filter_out (AList.defined (op =) more_override_params o fst)) @
   8.332 +      more_override_params
   8.333 +      |> filter is_raw_param_relevant_for_minimize
   8.334 +      |> map nice_string_of_raw_param
   8.335 +      |> (if prover_name = default_minimize_prover then I else cons prover_name)
   8.336 +      |> space_implode ", "
   8.337 +  in
   8.338 +    sledgehammerN ^ " " ^ minN ^
   8.339 +    (if params = "" then "" else enclose " [" "]" params) ^
   8.340 +    " (" ^ space_implode " " fact_names ^ ")" ^
   8.341 +    (if i = 1 then "" else " " ^ string_of_int i)
   8.342 +  end
   8.343 +
   8.344 +val default_learn_prover_timeout = 2.0
   8.345 +
   8.346 +fun hammer_away override_params subcommand opt_i fact_override state =
   8.347 +  let
   8.348 +    val ctxt = Proof.context_of state
   8.349 +    val override_params = override_params |> map (normalize_raw_param ctxt)
   8.350 +    val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
   8.351 +  in
   8.352 +    if subcommand = runN then
   8.353 +      let val i = the_default 1 opt_i in
   8.354 +        run_sledgehammer (get_params Normal ctxt override_params) Normal NONE i
   8.355 +                         fact_override (minimize_command override_params i)
   8.356 +                         state
   8.357 +        |> K ()
   8.358 +      end
   8.359 +    else if subcommand = minN then
   8.360 +      let
   8.361 +        val ctxt = ctxt |> Config.put instantiate_inducts false
   8.362 +        val i = the_default 1 opt_i
   8.363 +        val params =
   8.364 +          get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
   8.365 +                                    override_params)
   8.366 +        val goal = prop_of (#goal (Proof.goal state))
   8.367 +        val facts = nearly_all_facts ctxt false fact_override Symtab.empty
   8.368 +                                     Termtab.empty [] [] goal
   8.369 +        val learn = mash_learn_proof ctxt params goal facts
   8.370 +      in run_minimize params learn i (#add fact_override) state end
   8.371 +    else if subcommand = messagesN then
   8.372 +      messages opt_i
   8.373 +    else if subcommand = supported_proversN then
   8.374 +      supported_provers ctxt
   8.375 +    else if subcommand = kill_allN then
   8.376 +      (kill_provers ();
   8.377 +       kill_learners ctxt (get_params Normal ctxt override_params))
   8.378 +    else if subcommand = running_proversN then
   8.379 +      running_provers ()
   8.380 +    else if subcommand = unlearnN then
   8.381 +      mash_unlearn ctxt (get_params Normal ctxt override_params)
   8.382 +    else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
   8.383 +            subcommand = relearn_isarN orelse subcommand = relearn_proverN then
   8.384 +      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then
   8.385 +         mash_unlearn ctxt (get_params Normal ctxt override_params)
   8.386 +       else
   8.387 +         ();
   8.388 +       mash_learn ctxt
   8.389 +           (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
   8.390 +           (get_params Normal ctxt
   8.391 +                ([("timeout",
   8.392 +                   [string_of_real default_learn_prover_timeout]),
   8.393 +                  ("slice", ["false"])] @
   8.394 +                 override_params @
   8.395 +                 [("minimize", ["true"]),
   8.396 +                  ("preplay_timeout", ["0"])]))
   8.397 +           fact_override (#facts (Proof.goal state))
   8.398 +           (subcommand = learn_proverN orelse subcommand = relearn_proverN))
   8.399 +    else if subcommand = running_learnersN then
   8.400 +      running_learners ()
   8.401 +    else if subcommand = refresh_tptpN then
   8.402 +      refresh_systems_on_tptp ()
   8.403 +    else
   8.404 +      error ("Unknown subcommand: " ^ quote subcommand ^ ".")
   8.405 +  end
   8.406 +
   8.407 +fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
   8.408 +  Toplevel.unknown_proof o
   8.409 +  Toplevel.keep (hammer_away params subcommand opt_i fact_override
   8.410 +                 o Toplevel.proof_of)
   8.411 +
   8.412 +fun string_of_raw_param (name, value) = name ^ " = " ^ implode_param value
   8.413 +
   8.414 +fun sledgehammer_params_trans params =
   8.415 +  Toplevel.theory
   8.416 +      (fold set_default_raw_param params
   8.417 +       #> tap (fn thy =>
   8.418 +                  let val ctxt = Proof_Context.init_global thy in
   8.419 +                    writeln ("Default parameters for Sledgehammer:\n" ^
   8.420 +                             (case rev (default_raw_params Normal ctxt) of
   8.421 +                                [] => "none"
   8.422 +                              | params =>
   8.423 +                                params |> map string_of_raw_param
   8.424 +                                       |> sort_strings |> cat_lines))
   8.425 +                  end))
   8.426 +
   8.427 +val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
   8.428 +val parse_key =
   8.429 +  Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
   8.430 +val parse_value =
   8.431 +  Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
   8.432 +val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
   8.433 +val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
   8.434 +val parse_fact_refs =
   8.435 +  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
   8.436 +val parse_fact_override_chunk =
   8.437 +  (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
   8.438 +  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
   8.439 +  || (parse_fact_refs >> only_fact_override)
   8.440 +val parse_fact_override =
   8.441 +  Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk
   8.442 +                              >> merge_fact_overrides))
   8.443 +                no_fact_override
   8.444 +
   8.445 +val _ =
   8.446 +  Outer_Syntax.improper_command @{command_spec "sledgehammer"}
   8.447 +    "search for first-order proof using automatic theorem provers"
   8.448 +    ((Scan.optional Parse.short_ident runN -- parse_params
   8.449 +      -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
   8.450 +val _ =
   8.451 +  Outer_Syntax.command @{command_spec "sledgehammer_params"}
   8.452 +    "set and display the default parameters for Sledgehammer"
   8.453 +    (parse_params #>> sledgehammer_params_trans)
   8.454 +
   8.455 +fun try_sledgehammer auto state =
   8.456 +  let
   8.457 +    val ctxt = Proof.context_of state
   8.458 +    val mode = if auto then Auto_Try else Try
   8.459 +    val i = 1
   8.460 +  in
   8.461 +    run_sledgehammer (get_params mode ctxt []) mode NONE i no_fact_override
   8.462 +                     (minimize_command [] i) state
   8.463 +  end
   8.464 +
   8.465 +val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
   8.466 +
   8.467 +val _ =
   8.468 +  Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
   8.469 +    (case try Toplevel.proof_of st of
   8.470 +      SOME state =>
   8.471 +        let
   8.472 +          val [provers_arg, isar_proofs_arg] = args;
   8.473 +          val ctxt = Proof.context_of state
   8.474 +
   8.475 +          val override_params =
   8.476 +            ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
   8.477 +              [("isar_proofs", [isar_proofs_arg]),
   8.478 +               ("blocking", ["true"]),
   8.479 +               ("minimize", ["true"]),
   8.480 +               ("debug", ["false"]),
   8.481 +               ("verbose", ["false"]),
   8.482 +               ("overlord", ["false"])])
   8.483 +            |> map (normalize_raw_param ctxt)
   8.484 +          val _ =
   8.485 +            run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
   8.486 +              no_fact_override (minimize_command override_params 1) state
   8.487 +        in () end
   8.488 +    | NONE => error "Unknown proof context"))
   8.489 +
   8.490 +val _ = Session.protocol_handler "isabelle.Sledgehammer_Params$Handler"
   8.491 +
   8.492 +val _ = Isabelle_Process.protocol_command "Sledgehammer.provers"
   8.493 +  (fn [] =>
   8.494 +    let
   8.495 +      val this_ctxt = @{context}
   8.496 +      val provers = space_implode " " (#provers (default_params this_ctxt []))
   8.497 +    in Output.protocol_message Markup.sledgehammer_provers provers end)
   8.498 +
   8.499 +end;
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 10:02:36 2014 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,496 +0,0 @@
     9.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     9.5 -    Author:     Jasmin Blanchette, TU Muenchen
     9.6 -
     9.7 -Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
     9.8 -*)
     9.9 -
    9.10 -signature SLEDGEHAMMER_ISAR =
    9.11 -sig
    9.12 -  type params = Sledgehammer_Provers.params
    9.13 -
    9.14 -  val provers : string Unsynchronized.ref
    9.15 -  val default_params : Proof.context -> (string * string) list -> params
    9.16 -end;
    9.17 -
    9.18 -structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    9.19 -struct
    9.20 -
    9.21 -open ATP_Util
    9.22 -open ATP_Systems
    9.23 -open ATP_Problem_Generate
    9.24 -open ATP_Proof_Reconstruct
    9.25 -open Sledgehammer_Util
    9.26 -open Sledgehammer_Fact
    9.27 -open Sledgehammer_Provers
    9.28 -open Sledgehammer_Minimize
    9.29 -open Sledgehammer_MaSh
    9.30 -open Sledgehammer_Run
    9.31 -
    9.32 -(* val cvc3N = "cvc3" *)
    9.33 -val yicesN = "yices"
    9.34 -val z3N = "z3"
    9.35 -
    9.36 -val runN = "run"
    9.37 -val minN = "min"
    9.38 -val messagesN = "messages"
    9.39 -val supported_proversN = "supported_provers"
    9.40 -val kill_allN = "kill_all"
    9.41 -val running_proversN = "running_provers"
    9.42 -val running_learnersN = "running_learners"
    9.43 -val refresh_tptpN = "refresh_tptp"
    9.44 -
    9.45 -val _ =
    9.46 -  ProofGeneral.preference_option ProofGeneral.category_tracing
    9.47 -    NONE
    9.48 -    @{option auto_sledgehammer}
    9.49 -    "auto-sledgehammer"
    9.50 -    "Run Sledgehammer automatically"
    9.51 -
    9.52 -(** Sledgehammer commands **)
    9.53 -
    9.54 -fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
    9.55 -fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}
    9.56 -fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}
    9.57 -fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =
    9.58 -  {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
    9.59 -   only = #only r1 andalso #only r2}
    9.60 -fun merge_fact_overrides rs =
    9.61 -  fold merge_fact_override_pairwise rs (only_fact_override [])
    9.62 -
    9.63 -(*** parameters ***)
    9.64 -
    9.65 -val provers = Unsynchronized.ref ""
    9.66 -
    9.67 -val _ =
    9.68 -  ProofGeneral.preference_string ProofGeneral.category_proof
    9.69 -    NONE
    9.70 -    provers
    9.71 -    "Sledgehammer: Provers"
    9.72 -    "Default automatic provers (separated by whitespace)"
    9.73 -
    9.74 -val _ =
    9.75 -  ProofGeneral.preference_option ProofGeneral.category_proof
    9.76 -    NONE
    9.77 -    @{option sledgehammer_timeout}
    9.78 -    "Sledgehammer: Time Limit"
    9.79 -    "ATPs will be interrupted after this time (in seconds)"
    9.80 -
    9.81 -type raw_param = string * string list
    9.82 -
    9.83 -val default_default_params =
    9.84 -  [("debug", "false"),
    9.85 -   ("verbose", "false"),
    9.86 -   ("overlord", "false"),
    9.87 -   ("spy", "false"),
    9.88 -   ("blocking", "false"),
    9.89 -   ("type_enc", "smart"),
    9.90 -   ("strict", "false"),
    9.91 -   ("lam_trans", "smart"),
    9.92 -   ("uncurried_aliases", "smart"),
    9.93 -   ("learn", "true"),
    9.94 -   ("fact_filter", "smart"),
    9.95 -   ("max_facts", "smart"),
    9.96 -   ("fact_thresholds", "0.45 0.85"),
    9.97 -   ("max_mono_iters", "smart"),
    9.98 -   ("max_new_mono_instances", "smart"),
    9.99 -   ("isar_proofs", "smart"),
   9.100 -   ("compress_isar", "10"),
   9.101 -   ("try0_isar", "true"),
   9.102 -   ("slice", "true"),
   9.103 -   ("minimize", "smart"),
   9.104 -   ("preplay_timeout", "3")]
   9.105 -
   9.106 -val alias_params =
   9.107 -  [("prover", ("provers", [])), (* undocumented *)
   9.108 -   ("dont_preplay", ("preplay_timeout", ["0"])),
   9.109 -   ("dont_compress_isar", ("compress_isar", ["0"])),
   9.110 -   ("isar_proof", ("isar_proofs", [])) (* legacy *)]
   9.111 -val negated_alias_params =
   9.112 -  [("no_debug", "debug"),
   9.113 -   ("quiet", "verbose"),
   9.114 -   ("no_overlord", "overlord"),
   9.115 -   ("dont_spy", "spy"),
   9.116 -   ("non_blocking", "blocking"),
   9.117 -   ("non_strict", "strict"),
   9.118 -   ("no_uncurried_aliases", "uncurried_aliases"),
   9.119 -   ("dont_learn", "learn"),
   9.120 -   ("no_isar_proofs", "isar_proofs"),
   9.121 -   ("dont_slice", "slice"),
   9.122 -   ("dont_minimize", "minimize"),
   9.123 -   ("dont_try0_isar", "try0_isar")]
   9.124 -
   9.125 -val params_not_for_minimize =
   9.126 -  ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
   9.127 -
   9.128 -val property_dependent_params = ["provers", "timeout"]
   9.129 -
   9.130 -fun is_known_raw_param s =
   9.131 -  AList.defined (op =) default_default_params s orelse
   9.132 -  AList.defined (op =) alias_params s orelse
   9.133 -  AList.defined (op =) negated_alias_params s orelse
   9.134 -  member (op =) property_dependent_params s orelse s = "expect"
   9.135 -
   9.136 -fun is_prover_list ctxt s =
   9.137 -  case space_explode " " s of
   9.138 -    ss as _ :: _ => forall (is_prover_supported ctxt) ss
   9.139 -  | _ => false
   9.140 -
   9.141 -fun unalias_raw_param (name, value) =
   9.142 -  case AList.lookup (op =) alias_params name of
   9.143 -    SOME (name', []) => (name', value)
   9.144 -  | SOME (param' as (name', _)) =>
   9.145 -    if value <> ["false"] then
   9.146 -      param'
   9.147 -    else
   9.148 -      error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \
   9.149 -             \(cf. " ^ quote name' ^ ").")
   9.150 -  | NONE =>
   9.151 -    case AList.lookup (op =) negated_alias_params name of
   9.152 -      SOME name' => (name', case value of
   9.153 -                              ["false"] => ["true"]
   9.154 -                            | ["true"] => ["false"]
   9.155 -                            | [] => ["false"]
   9.156 -                            | _ => value)
   9.157 -    | NONE => (name, value)
   9.158 -
   9.159 -val any_type_enc = type_enc_of_string Strict "erased"
   9.160 -
   9.161 -(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
   9.162 -   can be omitted. For the last four, this is a secret feature. *)
   9.163 -fun normalize_raw_param ctxt =
   9.164 -  unalias_raw_param
   9.165 -  #> (fn (name, value) =>
   9.166 -         if is_known_raw_param name then
   9.167 -           (name, value)
   9.168 -         else if null value then
   9.169 -           if is_prover_list ctxt name then
   9.170 -             ("provers", [name])
   9.171 -           else if can (type_enc_of_string Strict) name then
   9.172 -             ("type_enc", [name])
   9.173 -           else if can (trans_lams_of_string ctxt any_type_enc) name then
   9.174 -             ("lam_trans", [name])
   9.175 -           else if member (op =) fact_filters name then
   9.176 -             ("fact_filter", [name])
   9.177 -           else if is_some (Int.fromString name) then
   9.178 -             ("max_facts", [name])
   9.179 -           else
   9.180 -             error ("Unknown parameter: " ^ quote name ^ ".")
   9.181 -         else
   9.182 -           error ("Unknown parameter: " ^ quote name ^ "."))
   9.183 -
   9.184 -(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
   9.185 -   read correctly. *)
   9.186 -val implode_param = strip_spaces_except_between_idents o space_implode " "
   9.187 -
   9.188 -(* FIXME: use "Generic_Data" *)
   9.189 -structure Data = Theory_Data
   9.190 -(
   9.191 -  type T = raw_param list
   9.192 -  val empty = default_default_params |> map (apsnd single)
   9.193 -  val extend = I
   9.194 -  fun merge data : T = AList.merge (op =) (K true) data
   9.195 -)
   9.196 -
   9.197 -(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
   9.198 -   timeout, it makes sense to put E first. *)
   9.199 -fun default_provers_param_value mode ctxt =
   9.200 -  [eN, spassN, z3N, vampireN, e_sineN, yicesN]
   9.201 -  |> map_filter (remotify_prover_if_not_installed ctxt)
   9.202 -  (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   9.203 -  |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
   9.204 -  |> implode_param
   9.205 -
   9.206 -fun set_default_raw_param param thy =
   9.207 -  let val ctxt = Proof_Context.init_global thy in
   9.208 -    thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))
   9.209 -  end
   9.210 -
   9.211 -fun default_raw_params mode ctxt =
   9.212 -  let val thy = Proof_Context.theory_of ctxt in
   9.213 -    Data.get thy
   9.214 -    |> fold (AList.default (op =))
   9.215 -            [("provers", [case !provers of
   9.216 -                            "" => default_provers_param_value mode ctxt
   9.217 -                          | s => s]),
   9.218 -             ("timeout", let val timeout = Options.default_int @{option sledgehammer_timeout} in
   9.219 -                           [if timeout <= 0 then "none"
   9.220 -                            else string_of_int timeout]
   9.221 -                         end)]
   9.222 -  end
   9.223 -
   9.224 -fun extract_params mode default_params override_params =
   9.225 -  let
   9.226 -    val raw_params = rev override_params @ rev default_params
   9.227 -    val lookup = Option.map implode_param o AList.lookup (op =) raw_params
   9.228 -    val lookup_string = the_default "" o lookup
   9.229 -    fun general_lookup_bool option default_value name =
   9.230 -      (case lookup name of
   9.231 -        SOME s => parse_bool_option option name s
   9.232 -      | NONE => default_value)
   9.233 -    val lookup_bool = the o general_lookup_bool false (SOME false)
   9.234 -    fun lookup_time name =
   9.235 -      (case lookup name of
   9.236 -        SOME s => parse_time name s
   9.237 -      | NONE => Time.zeroTime)
   9.238 -    fun lookup_int name =
   9.239 -      (case lookup name of
   9.240 -        NONE => 0
   9.241 -      | SOME s =>
   9.242 -        (case Int.fromString s of
   9.243 -          SOME n => n
   9.244 -        | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value.")))
   9.245 -    fun lookup_real name =
   9.246 -      (case lookup name of
   9.247 -        NONE => 0.0
   9.248 -      | SOME s =>
   9.249 -        (case Real.fromString s of
   9.250 -          SOME n => n
   9.251 -        | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value.")))
   9.252 -    fun lookup_real_pair name =
   9.253 -      (case lookup name of
   9.254 -        NONE => (0.0, 0.0)
   9.255 -      | SOME s =>
   9.256 -        (case s |> space_explode " " |> map Real.fromString of
   9.257 -          [SOME r1, SOME r2] => (r1, r2)
   9.258 -        | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \
   9.259 -                 \values (e.g., \"0.6 0.95\")")))
   9.260 -    fun lookup_option lookup' name =
   9.261 -      (case lookup name of
   9.262 -        SOME "smart" => NONE
   9.263 -      | _ => SOME (lookup' name))
   9.264 -    val debug = mode <> Auto_Try andalso lookup_bool "debug"
   9.265 -    val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
   9.266 -    val overlord = lookup_bool "overlord"
   9.267 -    val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
   9.268 -    val blocking =
   9.269 -      Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
   9.270 -      lookup_bool "blocking"
   9.271 -    val provers = lookup_string "provers" |> space_explode " "
   9.272 -                  |> mode = Auto_Try ? single o hd
   9.273 -    val type_enc =
   9.274 -      if mode = Auto_Try then
   9.275 -        NONE
   9.276 -      else case lookup_string "type_enc" of
   9.277 -        "smart" => NONE
   9.278 -      | s => (type_enc_of_string Strict s; SOME s)
   9.279 -    val strict = mode = Auto_Try orelse lookup_bool "strict"
   9.280 -    val lam_trans = lookup_option lookup_string "lam_trans"
   9.281 -    val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
   9.282 -    val learn = lookup_bool "learn"
   9.283 -    val fact_filter =
   9.284 -      lookup_option lookup_string "fact_filter"
   9.285 -      |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf)
   9.286 -    val max_facts = lookup_option lookup_int "max_facts"
   9.287 -    val fact_thresholds = lookup_real_pair "fact_thresholds"
   9.288 -    val max_mono_iters = lookup_option lookup_int "max_mono_iters"
   9.289 -    val max_new_mono_instances =
   9.290 -      lookup_option lookup_int "max_new_mono_instances"
   9.291 -    val isar_proofs = lookup_option lookup_bool "isar_proofs"
   9.292 -    val compress_isar = Real.max (1.0, lookup_real "compress_isar")
   9.293 -    val try0_isar = lookup_bool "try0_isar"
   9.294 -    val slice = mode <> Auto_Try andalso lookup_bool "slice"
   9.295 -    val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
   9.296 -    val timeout = lookup_time "timeout"
   9.297 -    val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout"
   9.298 -    val expect = lookup_string "expect"
   9.299 -  in
   9.300 -    {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,
   9.301 -     provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
   9.302 -     uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
   9.303 -     max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
   9.304 -     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
   9.305 -     compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
   9.306 -     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   9.307 -  end
   9.308 -
   9.309 -fun get_params mode = extract_params mode o default_raw_params mode
   9.310 -fun default_params thy = get_params Normal thy o map (apsnd single)
   9.311 -
   9.312 -(* Sledgehammer the given subgoal *)
   9.313 -
   9.314 -val default_minimize_prover = metisN
   9.315 -
   9.316 -fun is_raw_param_relevant_for_minimize (name, _) =
   9.317 -  not (member (op =) params_not_for_minimize name)
   9.318 -fun string_of_raw_param (key, values) =
   9.319 -  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
   9.320 -fun nice_string_of_raw_param (p as (key, ["false"])) =
   9.321 -    (case AList.find (op =) negated_alias_params key of
   9.322 -       [neg] => neg
   9.323 -     | _ => string_of_raw_param p)
   9.324 -  | nice_string_of_raw_param p = string_of_raw_param p
   9.325 -
   9.326 -fun minimize_command override_params i more_override_params prover_name
   9.327 -                     fact_names =
   9.328 -  let
   9.329 -    val params =
   9.330 -      (override_params
   9.331 -       |> filter_out (AList.defined (op =) more_override_params o fst)) @
   9.332 -      more_override_params
   9.333 -      |> filter is_raw_param_relevant_for_minimize
   9.334 -      |> map nice_string_of_raw_param
   9.335 -      |> (if prover_name = default_minimize_prover then I else cons prover_name)
   9.336 -      |> space_implode ", "
   9.337 -  in
   9.338 -    sledgehammerN ^ " " ^ minN ^
   9.339 -    (if params = "" then "" else enclose " [" "]" params) ^
   9.340 -    " (" ^ space_implode " " fact_names ^ ")" ^
   9.341 -    (if i = 1 then "" else " " ^ string_of_int i)
   9.342 -  end
   9.343 -
   9.344 -val default_learn_prover_timeout = 2.0
   9.345 -
   9.346 -fun hammer_away override_params subcommand opt_i fact_override state =
   9.347 -  let
   9.348 -    val ctxt = Proof.context_of state
   9.349 -    val override_params = override_params |> map (normalize_raw_param ctxt)
   9.350 -    val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
   9.351 -  in
   9.352 -    if subcommand = runN then
   9.353 -      let val i = the_default 1 opt_i in
   9.354 -        run_sledgehammer (get_params Normal ctxt override_params) Normal NONE i
   9.355 -                         fact_override (minimize_command override_params i)
   9.356 -                         state
   9.357 -        |> K ()
   9.358 -      end
   9.359 -    else if subcommand = minN then
   9.360 -      let
   9.361 -        val ctxt = ctxt |> Config.put instantiate_inducts false
   9.362 -        val i = the_default 1 opt_i
   9.363 -        val params =
   9.364 -          get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
   9.365 -                                    override_params)
   9.366 -        val goal = prop_of (#goal (Proof.goal state))
   9.367 -        val facts = nearly_all_facts ctxt false fact_override Symtab.empty
   9.368 -                                     Termtab.empty [] [] goal
   9.369 -        val learn = mash_learn_proof ctxt params goal facts
   9.370 -      in run_minimize params learn i (#add fact_override) state end
   9.371 -    else if subcommand = messagesN then
   9.372 -      messages opt_i
   9.373 -    else if subcommand = supported_proversN then
   9.374 -      supported_provers ctxt
   9.375 -    else if subcommand = kill_allN then
   9.376 -      (kill_provers ();
   9.377 -       kill_learners ctxt (get_params Normal ctxt override_params))
   9.378 -    else if subcommand = running_proversN then
   9.379 -      running_provers ()
   9.380 -    else if subcommand = unlearnN then
   9.381 -      mash_unlearn ctxt (get_params Normal ctxt override_params)
   9.382 -    else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
   9.383 -            subcommand = relearn_isarN orelse subcommand = relearn_proverN then
   9.384 -      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then
   9.385 -         mash_unlearn ctxt (get_params Normal ctxt override_params)
   9.386 -       else
   9.387 -         ();
   9.388 -       mash_learn ctxt
   9.389 -           (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
   9.390 -           (get_params Normal ctxt
   9.391 -                ([("timeout",
   9.392 -                   [string_of_real default_learn_prover_timeout]),
   9.393 -                  ("slice", ["false"])] @
   9.394 -                 override_params @
   9.395 -                 [("minimize", ["true"]),
   9.396 -                  ("preplay_timeout", ["0"])]))
   9.397 -           fact_override (#facts (Proof.goal state))
   9.398 -           (subcommand = learn_proverN orelse subcommand = relearn_proverN))
   9.399 -    else if subcommand = running_learnersN then
   9.400 -      running_learners ()
   9.401 -    else if subcommand = refresh_tptpN then
   9.402 -      refresh_systems_on_tptp ()
   9.403 -    else
   9.404 -      error ("Unknown subcommand: " ^ quote subcommand ^ ".")
   9.405 -  end
   9.406 -
   9.407 -fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
   9.408 -  Toplevel.unknown_proof o
   9.409 -  Toplevel.keep (hammer_away params subcommand opt_i fact_override
   9.410 -                 o Toplevel.proof_of)
   9.411 -
   9.412 -fun string_of_raw_param (name, value) = name ^ " = " ^ implode_param value
   9.413 -
   9.414 -fun sledgehammer_params_trans params =
   9.415 -  Toplevel.theory
   9.416 -      (fold set_default_raw_param params
   9.417 -       #> tap (fn thy =>
   9.418 -                  let val ctxt = Proof_Context.init_global thy in
   9.419 -                    writeln ("Default parameters for Sledgehammer:\n" ^
   9.420 -                             (case rev (default_raw_params Normal ctxt) of
   9.421 -                                [] => "none"
   9.422 -                              | params =>
   9.423 -                                params |> map string_of_raw_param
   9.424 -                                       |> sort_strings |> cat_lines))
   9.425 -                  end))
   9.426 -
   9.427 -val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
   9.428 -val parse_key =
   9.429 -  Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
   9.430 -val parse_value =
   9.431 -  Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
   9.432 -val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
   9.433 -val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
   9.434 -val parse_fact_refs =
   9.435 -  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
   9.436 -val parse_fact_override_chunk =
   9.437 -  (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
   9.438 -  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
   9.439 -  || (parse_fact_refs >> only_fact_override)
   9.440 -val parse_fact_override =
   9.441 -  Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk
   9.442 -                              >> merge_fact_overrides))
   9.443 -                no_fact_override
   9.444 -
   9.445 -val _ =
   9.446 -  Outer_Syntax.improper_command @{command_spec "sledgehammer"}
   9.447 -    "search for first-order proof using automatic theorem provers"
   9.448 -    ((Scan.optional Parse.short_ident runN -- parse_params
   9.449 -      -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
   9.450 -val _ =
   9.451 -  Outer_Syntax.command @{command_spec "sledgehammer_params"}
   9.452 -    "set and display the default parameters for Sledgehammer"
   9.453 -    (parse_params #>> sledgehammer_params_trans)
   9.454 -
   9.455 -fun try_sledgehammer auto state =
   9.456 -  let
   9.457 -    val ctxt = Proof.context_of state
   9.458 -    val mode = if auto then Auto_Try else Try
   9.459 -    val i = 1
   9.460 -  in
   9.461 -    run_sledgehammer (get_params mode ctxt []) mode NONE i no_fact_override
   9.462 -                     (minimize_command [] i) state
   9.463 -  end
   9.464 -
   9.465 -val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
   9.466 -
   9.467 -val _ =
   9.468 -  Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
   9.469 -    (case try Toplevel.proof_of st of
   9.470 -      SOME state =>
   9.471 -        let
   9.472 -          val [provers_arg, isar_proofs_arg] = args;
   9.473 -          val ctxt = Proof.context_of state
   9.474 -
   9.475 -          val override_params =
   9.476 -            ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
   9.477 -              [("isar_proofs", [isar_proofs_arg]),
   9.478 -               ("blocking", ["true"]),
   9.479 -               ("minimize", ["true"]),
   9.480 -               ("debug", ["false"]),
   9.481 -               ("verbose", ["false"]),
   9.482 -               ("overlord", ["false"])])
   9.483 -            |> map (normalize_raw_param ctxt)
   9.484 -          val _ =
   9.485 -            run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
   9.486 -              no_fact_override (minimize_command override_params 1) state
   9.487 -        in () end
   9.488 -    | NONE => error "Unknown proof context"))
   9.489 -
   9.490 -val _ = Session.protocol_handler "isabelle.Sledgehammer_Params$Handler"
   9.491 -
   9.492 -val _ = Isabelle_Process.protocol_command "Sledgehammer.provers"
   9.493 -  (fn [] =>
   9.494 -    let
   9.495 -      val this_ctxt = @{context}
   9.496 -      val provers = space_implode " " (#provers (default_params this_ctxt []))
   9.497 -    in Output.protocol_message Markup.sledgehammer_provers provers end)
   9.498 -
   9.499 -end;