1(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_commands.ML
2    Author:     Jasmin Blanchette, TU Muenchen
3
4Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
5*)
6
7signature SLEDGEHAMMER_COMMANDS =
8sig
9  type params = Sledgehammer_Prover.params
10
11  val provers : string Unsynchronized.ref
12  val default_params : theory -> (string * string) list -> params
13end;
14
15structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS =
16struct
17
18open ATP_Util
19open ATP_Systems
20open ATP_Problem_Generate
21open ATP_Proof
22open ATP_Proof_Reconstruct
23open Sledgehammer_Util
24open Sledgehammer_Fact
25open Sledgehammer_Prover
26open Sledgehammer_Prover_Minimize
27open Sledgehammer_MaSh
28open Sledgehammer
29
30val cvc4N = "cvc4"
31val veritN = "verit"
32val z3N = "z3"
33
34val runN = "run"
35val supported_proversN = "supported_provers"
36val refresh_tptpN = "refresh_tptp"
37
38(** Sledgehammer commands **)
39
40fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
41fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}
42fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}
43fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =
44  {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2}
45fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override [])
46
47(*** parameters ***)
48
49val provers = Unsynchronized.ref ""
50
51type raw_param = string * string list
52
53val default_default_params =
54  [("debug", "false"),
55   ("verbose", "false"),
56   ("overlord", "false"),
57   ("spy", "false"),
58   ("type_enc", "smart"),
59   ("strict", "false"),
60   ("lam_trans", "smart"),
61   ("uncurried_aliases", "smart"),
62   ("learn", "true"),
63   ("fact_filter", "smart"),
64   ("max_facts", "smart"),
65   ("fact_thresholds", "0.45 0.85"),
66   ("max_mono_iters", "smart"),
67   ("max_new_mono_instances", "smart"),
68   ("isar_proofs", "smart"),
69   ("compress", "smart"),
70   ("try0", "true"),
71   ("smt_proofs", "smart"),
72   ("slice", "true"),
73   ("minimize", "true"),
74   ("preplay_timeout", "1")]
75
76val alias_params =
77  [("prover", ("provers", [])), (* undocumented *)
78   ("dont_preplay", ("preplay_timeout", ["0"])),
79   ("dont_compress", ("compress", ["1"])),
80   ("isar_proof", ("isar_proofs", [])) (* legacy *)]
81val negated_alias_params =
82  [("no_debug", "debug"),
83   ("quiet", "verbose"),
84   ("no_overlord", "overlord"),
85   ("dont_spy", "spy"),
86   ("non_strict", "strict"),
87   ("no_uncurried_aliases", "uncurried_aliases"),
88   ("dont_learn", "learn"),
89   ("no_isar_proofs", "isar_proofs"),
90   ("dont_slice", "slice"),
91   ("dont_minimize", "minimize"),
92   ("dont_try0", "try0"),
93   ("no_smt_proofs", "smt_proofs")]
94
95val property_dependent_params = ["provers", "timeout"]
96
97fun is_known_raw_param s =
98  AList.defined (op =) default_default_params s orelse
99  AList.defined (op =) alias_params s orelse
100  AList.defined (op =) negated_alias_params s orelse
101  member (op =) property_dependent_params s orelse s = "expect"
102
103fun is_prover_list ctxt s =
104  (case space_explode " " s of
105    ss as _ :: _ => forall (is_prover_supported ctxt) ss
106  | _ => false)
107
108fun unalias_raw_param (name, value) =
109  (case AList.lookup (op =) alias_params name of
110    SOME (name', []) => (name', value)
111  | SOME (param' as (name', _)) =>
112    if value <> ["false"] then
113      param'
114    else
115      error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")")
116  | NONE =>
117    (case AList.lookup (op =) negated_alias_params name of
118      SOME name' => (name',
119        (case value of
120          ["false"] => ["true"]
121        | ["true"] => ["false"]
122        | [] => ["false"]
123        | _ => value))
124    | NONE => (name, value)))
125
126val any_type_enc = type_enc_of_string Strict "erased"
127
128(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
129   can be omitted. For the last four, this is a secret feature. *)
130fun normalize_raw_param ctxt =
131  unalias_raw_param
132  #> (fn (name, value) =>
133         if is_known_raw_param name then
134           (name, value)
135         else if null value then
136           if is_prover_list ctxt name then
137             ("provers", [name])
138           else if can (type_enc_of_string Strict) name then
139             ("type_enc", [name])
140           else if can (trans_lams_of_string ctxt any_type_enc) name then
141             ("lam_trans", [name])
142           else if member (op =) fact_filters name then
143             ("fact_filter", [name])
144           else if is_some (Int.fromString name) then
145             ("max_facts", [name])
146           else
147             error ("Unknown parameter: " ^ quote name)
148         else
149           error ("Unknown parameter: " ^ quote name))
150
151(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
152   read correctly. *)
153val implode_param = strip_spaces_except_between_idents o space_implode " "
154
155(* FIXME: use "Generic_Data" *)
156structure Data = Theory_Data
157(
158  type T = raw_param list
159  val empty = default_default_params |> map (apsnd single)
160  val extend = I
161  fun merge data : T = AList.merge (op =) (K true) data
162)
163
164fun remotify_prover_if_supported_and_not_already_remote ctxt name =
165  if String.isPrefix remote_prefix name then
166    SOME name
167  else
168    let val remote_name = remote_prefix ^ name in
169      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
170    end
171
172fun remotify_prover_if_not_installed ctxt name =
173  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
174  else remotify_prover_if_supported_and_not_already_remote ctxt name
175
176(* The first ATP of the list is used by Auto Sledgehammer. *)
177fun default_provers_param_value mode ctxt =
178  [cvc4N] @
179  (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @
180  [z3N, eN, spassN, veritN]
181  |> map_filter (remotify_prover_if_not_installed ctxt)
182  (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
183  |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))
184  |> implode_param
185
186fun set_default_raw_param param thy =
187  let val ctxt = Proof_Context.init_global thy in
188    thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))
189  end
190
191fun default_raw_params mode thy =
192  let val ctxt = Proof_Context.init_global thy in
193    Data.get thy
194    |> fold (AList.default (op =))
195         [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]),
196          ("timeout",
197           let val timeout = Options.default_int \<^system_option>\<open>sledgehammer_timeout\<close> in
198             [if timeout <= 0 then "none" else string_of_int timeout]
199           end)]
200  end
201
202fun extract_params mode default_params override_params =
203  let
204    val raw_params = rev override_params @ rev default_params
205    val lookup = Option.map implode_param o AList.lookup (op =) raw_params
206    val lookup_string = the_default "" o lookup
207
208    fun general_lookup_bool option default_value name =
209      (case lookup name of
210        SOME s => parse_bool_option option name s
211      | NONE => default_value)
212    val lookup_bool = the o general_lookup_bool false (SOME false)
213    fun lookup_time name =
214      (case lookup name of
215        SOME s => parse_time name s
216      | NONE => Time.zeroTime)
217    fun lookup_int name =
218      (case lookup name of
219        NONE => 0
220      | SOME s =>
221        (case Int.fromString s of
222          SOME n => n
223        | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value")))
224    fun lookup_real name =
225      (case lookup name of
226        NONE => 0.0
227      | SOME s =>
228        (case Real.fromString s of
229          SOME n => n
230        | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value")))
231    fun lookup_real_pair name =
232      (case lookup name of
233        NONE => (0.0, 0.0)
234      | SOME s =>
235        (case s |> space_explode " " |> map Real.fromString of
236          [SOME r1, SOME r2] => (r1, r2)
237        | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \
238                 \values (e.g., \"0.6 0.95\")")))
239    fun lookup_option lookup' name =
240      (case lookup name of
241        SOME "smart" => NONE
242      | _ => SOME (lookup' name))
243    val debug = mode <> Auto_Try andalso lookup_bool "debug"
244    val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
245    val overlord = lookup_bool "overlord"
246    val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
247    val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd
248    val type_enc =
249      if mode = Auto_Try then
250        NONE
251      else
252        (case lookup_string "type_enc" of
253          "smart" => NONE
254        | s => (type_enc_of_string Strict s; SOME s))
255    val strict = mode = Auto_Try orelse lookup_bool "strict"
256    val lam_trans = lookup_option lookup_string "lam_trans"
257    val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
258    val learn = lookup_bool "learn"
259    val fact_filter =
260      lookup_option lookup_string "fact_filter"
261      |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf)
262    val max_facts = lookup_option lookup_int "max_facts"
263    val fact_thresholds = lookup_real_pair "fact_thresholds"
264    val max_mono_iters = lookup_option lookup_int "max_mono_iters"
265    val max_new_mono_instances =
266      lookup_option lookup_int "max_new_mono_instances"
267    val isar_proofs = lookup_option lookup_bool "isar_proofs"
268    val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
269    val try0 = lookup_bool "try0"
270    val smt_proofs = lookup_option lookup_bool "smt_proofs"
271    val slice = mode <> Auto_Try andalso lookup_bool "slice"
272    val minimize = lookup_bool "minimize"
273    val timeout = lookup_time "timeout"
274    val preplay_timeout = lookup_time "preplay_timeout"
275    val expect = lookup_string "expect"
276  in
277    {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
278     type_enc = type_enc, strict = strict, lam_trans = lam_trans,
279     uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
280     max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
281     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
282     compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
283     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
284  end
285
286fun get_params mode = extract_params mode o default_raw_params mode
287fun default_params thy = get_params Normal thy o map (apsnd single)
288
289val silence_state =
290  Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false)
291
292(* Sledgehammer the given subgoal *)
293
294val default_learn_prover_timeout = 2.0
295
296fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 =
297  let
298    (* We generally want chained facts to be picked up by the relevance filter, because it can then
299       give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs,
300       verbose output, machine learning). However, if the fact is available by no other means (not
301       even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice
302       but to insert it into the state as an additional hypothesis.
303    *)
304    val {facts = chained0, ...} = Proof.goal state0
305    val (inserts, keep_chained) =
306      if null chained0 orelse #only fact_override then
307        (chained0, [])
308      else
309        let val ctxt0 = Proof.context_of state0 in
310          List.partition (is_useful_unnamed_local_fact ctxt0) chained0
311        end
312    val state = state0
313      |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained)
314      |> silence_state
315
316    val thy = Proof.theory_of state
317    val ctxt = Proof.context_of state
318
319    val override_params = override_params |> map (normalize_raw_param ctxt)
320  in
321    if subcommand = runN then
322      let val i = the_default 1 opt_i in
323        ignore (run_sledgehammer
324          (get_params Normal thy override_params) Normal writeln_result i fact_override state)
325      end
326    else if subcommand = supported_proversN then
327      supported_provers ctxt
328    else if subcommand = unlearnN then
329      mash_unlearn ctxt
330    else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
331            subcommand = relearn_isarN orelse subcommand = relearn_proverN then
332      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt
333       else ();
334       mash_learn ctxt
335           (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
336           (get_params Normal thy
337                ([("timeout", [string_of_real default_learn_prover_timeout]),
338                  ("slice", ["false"])] @
339                 override_params @
340                 [("preplay_timeout", ["0"])]))
341           fact_override (#facts (Proof.goal state))
342           (subcommand = learn_proverN orelse subcommand = relearn_proverN))
343    else if subcommand = refresh_tptpN then
344      refresh_systems_on_tptp ()
345    else
346      error ("Unknown subcommand: " ^ quote subcommand)
347  end
348
349fun string_of_raw_param (key, values) =
350  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
351
352val parse_query_bang = \<^keyword>\<open>?\<close> || \<^keyword>\<open>!\<close> || \<^keyword>\<open>!!\<close>
353val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param
354val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang)
355val parse_param = parse_key -- Scan.optional (\<^keyword>\<open>=\<close> |-- parse_value) []
356val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
357val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)
358val parse_fact_override_chunk =
359  (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
360  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
361  || (parse_fact_refs >> only_fact_override)
362val parse_fact_override =
363  Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides))
364    no_fact_override
365
366val _ =
367  Outer_Syntax.command \<^command_keyword>\<open>sledgehammer\<close>
368    "search for first-order proof using automatic theorem provers"
369    (Scan.optional Parse.name runN -- parse_params
370      -- parse_fact_override -- Scan.option Parse.nat >>
371      (fn (((subcommand, params), fact_override), opt_i) =>
372        Toplevel.keep_proof
373          (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of)))
374val _ =
375  Outer_Syntax.command \<^command_keyword>\<open>sledgehammer_params\<close>
376    "set and display the default parameters for Sledgehammer"
377    (parse_params >> (fn params =>
378      Toplevel.theory (fold set_default_raw_param params #> tap (fn thy =>
379        writeln ("Default parameters for Sledgehammer:\n" ^
380          (case rev (default_raw_params Normal thy) of
381            [] => "none"
382          | params => params |> map string_of_raw_param |> sort_strings |> cat_lines))))))
383
384fun try_sledgehammer auto state =
385  let
386    val thy = Proof.theory_of state
387    val mode = if auto then Auto_Try else Try
388    val i = 1
389  in
390    run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state)
391  end
392
393val _ = Try.tool_setup (sledgehammerN, (40, \<^system_option>\<open>auto_sledgehammer\<close>, try_sledgehammer))
394
395val _ =
396  Query_Operation.register {name = sledgehammerN, pri = 0}
397    (fn {state = st, args, writeln_result, ...} =>
398      (case try Toplevel.proof_of st of
399        SOME state =>
400          let
401            val [provers_arg, isar_proofs_arg, try0_arg] = args
402            val override_params =
403              ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
404                [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]),
405                 ("try0", [try0_arg]),
406                 ("debug", ["false"]),
407                 ("verbose", ["false"]),
408                 ("overlord", ["false"])]);
409          in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end
410      | NONE => error "Unknown proof context"))
411
412end;
413