src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
author desharna
Tue, 28 Sep 2021 10:38:36 +0200
changeset 74369 3301c0d8b560
parent 74352 fb8ce6090437
child 74370 d8dc8fdc46fc
permissions -rw-r--r--
added Zipperposition to sledgehammer's default provers
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55198
7a538e58b64e tuned ML file name
blanchet
parents: 55183
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_commands.ML
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
     3
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
     4
Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
     5
*)
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
     6
55198
7a538e58b64e tuned ML file name
blanchet
parents: 55183
diff changeset
     7
signature SLEDGEHAMMER_COMMANDS =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
     8
sig
55201
1ee776da8da7 renamed ML file
blanchet
parents: 55198
diff changeset
     9
  type params = Sledgehammer_Prover.params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    10
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    11
  val provers : string Unsynchronized.ref
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    12
  val default_params : theory -> (string * string) list -> params
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 72400
diff changeset
    13
  val parse_params: (string * string) list parser
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    14
end;
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    15
55198
7a538e58b64e tuned ML file name
blanchet
parents: 55183
diff changeset
    16
structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS =
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    17
struct
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    18
44784
blanchet
parents: 44768
diff changeset
    19
open ATP_Util
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    20
open ATP_Problem_Generate
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 56982
diff changeset
    21
open ATP_Proof
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    22
open ATP_Proof_Reconstruct
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
    23
open Sledgehammer_Util
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 47962
diff changeset
    24
open Sledgehammer_Fact
72400
abfeed05c323 tune filename
desharna
parents: 71931
diff changeset
    25
open Sledgehammer_ATP_Systems
55201
1ee776da8da7 renamed ML file
blanchet
parents: 55198
diff changeset
    26
open Sledgehammer_Prover
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
    27
open Sledgehammer_Prover_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48332
diff changeset
    28
open Sledgehammer_MaSh
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
    29
open Sledgehammer
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    30
59508
49ca7836ae81 tuned default provers
blanchet
parents: 58893
diff changeset
    31
val cvc4N = "cvc4"
49ca7836ae81 tuned default provers
blanchet
parents: 58893
diff changeset
    32
val veritN = "verit"
57209
7ffa0f7e2775 removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents: 57208
diff changeset
    33
val z3N = "z3"
48405
7682bc885e8a use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents: 48400
diff changeset
    34
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    35
val runN = "run"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    36
val supported_proversN = "supported_provers"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    37
val refresh_tptpN = "refresh_tptp"
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48293
diff changeset
    38
36394
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
    39
(** Sledgehammer commands **)
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
    40
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    41
fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    42
fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    43
fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    44
fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =
57273
01b68f625550 automatically learn MaSh facts also in 'blocking' mode
blanchet
parents: 57245
diff changeset
    45
  {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2}
01b68f625550 automatically learn MaSh facts also in 'blocking' mode
blanchet
parents: 57245
diff changeset
    46
fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override [])
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
    47
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    48
(*** parameters ***)
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    49
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    50
val provers = Unsynchronized.ref ""
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    51
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    52
type raw_param = string * string list
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    53
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    54
val default_default_params =
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
    55
  [("debug", "false"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    56
   ("verbose", "false"),
36143
6490319b1703 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents: 36142
diff changeset
    57
   ("overlord", "false"),
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53764
diff changeset
    58
   ("spy", "false"),
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
    59
   ("type_enc", "smart"),
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
    60
   ("strict", "false"),
45514
973bb7846505 parse lambda translation option in Metis
blanchet
parents: 45063
diff changeset
    61
   ("lam_trans", "smart"),
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
    62
   ("uncurried_aliases", "smart"),
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    63
   ("learn", "true"),
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
    64
   ("fact_filter", "smart"),
73940
f58108b7a60c refactored Sledgehammer option "induction_rules"
desharna
parents: 73939
diff changeset
    65
   ("induction_rules", "smart"),
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
    66
   ("max_facts", "smart"),
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    67
   ("fact_thresholds", "0.45 0.85"),
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
    68
   ("max_mono_iters", "smart"),
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
    69
   ("max_new_mono_instances", "smart"),
51190
2654b3965c8d made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents: 51189
diff changeset
    70
   ("isar_proofs", "smart"),
57783
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57735
diff changeset
    71
   ("compress", "smart"),
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57237
diff changeset
    72
   ("try0", "true"),
71931
0c8a9c028304 simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents: 70934
diff changeset
    73
   ("smt_proofs", "true"),
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45520
diff changeset
    74
   ("slice", "true"),
57721
e4858f85e616 always minimize Sledgehammer results by default
blanchet
parents: 57719
diff changeset
    75
   ("minimize", "true"),
57719
249f13fed1a6 reduced preplay timeout to 1 s
blanchet
parents: 57677
diff changeset
    76
   ("preplay_timeout", "1")]
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    77
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
    78
val alias_params =
51138
583a37b9512d killed legacy alias
blanchet
parents: 51130
diff changeset
    79
  [("prover", ("provers", [])), (* undocumented *)
51189
a55ef201b19d alias for people like me
blanchet
parents: 51138
diff changeset
    80
   ("dont_preplay", ("preplay_timeout", ["0"])),
57783
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57735
diff changeset
    81
   ("dont_compress", ("compress", ["1"])),
52093
f5280907284d added compatibility alias
blanchet
parents: 52031
diff changeset
    82
   ("isar_proof", ("isar_proofs", [])) (* legacy *)]
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
    83
val negated_alias_params =
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
    84
  [("no_debug", "debug"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    85
   ("quiet", "verbose"),
36143
6490319b1703 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents: 36142
diff changeset
    86
   ("no_overlord", "overlord"),
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53764
diff changeset
    87
   ("dont_spy", "spy"),
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
    88
   ("non_strict", "strict"),
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
    89
   ("no_uncurried_aliases", "uncurried_aliases"),
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    90
   ("dont_learn", "learn"),
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
    91
   ("no_isar_proofs", "isar_proofs"),
45707
6bf7eec9b153 added "minimize" option for more control over automatic minimization
blanchet
parents: 45706
diff changeset
    92
   ("dont_slice", "slice"),
51879
ee9562d31778 added preplay tracing
smolkas
parents: 51557
diff changeset
    93
   ("dont_minimize", "minimize"),
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57237
diff changeset
    94
   ("dont_try0", "try0"),
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55288
diff changeset
    95
   ("no_smt_proofs", "smt_proofs")]
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    96
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43353
diff changeset
    97
val property_dependent_params = ["provers", "timeout"]
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    98
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    99
fun is_known_raw_param s =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   100
  AList.defined (op =) default_default_params s orelse
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   101
  AList.defined (op =) alias_params s orelse
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   102
  AList.defined (op =) negated_alias_params s orelse
67405
e9ab4ad7bd15 uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents: 67399
diff changeset
   103
  member (op =) property_dependent_params s orelse s = "expect"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   104
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   105
fun is_prover_list ctxt s =
55286
blanchet
parents: 55277
diff changeset
   106
  (case space_explode " " s of
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   107
    ss as _ :: _ => forall (is_prover_supported ctxt) ss
55286
blanchet
parents: 55277
diff changeset
   108
  | _ => false)
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   109
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   110
fun unalias_raw_param (name, value) =
55286
blanchet
parents: 55277
diff changeset
   111
  (case AList.lookup (op =) alias_params name of
47037
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   112
    SOME (name', []) => (name', value)
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   113
  | SOME (param' as (name', _)) =>
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   114
    if value <> ["false"] then
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   115
      param'
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   116
    else
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63136
diff changeset
   117
      error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")")
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   118
  | NONE =>
55286
blanchet
parents: 55277
diff changeset
   119
    (case AList.lookup (op =) negated_alias_params name of
blanchet
parents: 55277
diff changeset
   120
      SOME name' => (name',
blanchet
parents: 55277
diff changeset
   121
        (case value of
blanchet
parents: 55277
diff changeset
   122
          ["false"] => ["true"]
blanchet
parents: 55277
diff changeset
   123
        | ["true"] => ["false"]
blanchet
parents: 55277
diff changeset
   124
        | [] => ["false"]
blanchet
parents: 55277
diff changeset
   125
        | _ => value))
blanchet
parents: 55277
diff changeset
   126
    | NONE => (name, value)))
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   127
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 52018
diff changeset
   128
val any_type_enc = type_enc_of_string Strict "erased"
45514
973bb7846505 parse lambda translation option in Metis
blanchet
parents: 45063
diff changeset
   129
48397
9fe826095a02 convenience
blanchet
parents: 48395
diff changeset
   130
(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
9fe826095a02 convenience
blanchet
parents: 48395
diff changeset
   131
   can be omitted. For the last four, this is a secret feature. *)
44720
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   132
fun normalize_raw_param ctxt =
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   133
  unalias_raw_param
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   134
  #> (fn (name, value) =>
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   135
         if is_known_raw_param name then
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   136
           (name, value)
48533
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   137
         else if null value then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   138
           if is_prover_list ctxt name then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   139
             ("provers", [name])
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 52018
diff changeset
   140
           else if can (type_enc_of_string Strict) name then
48533
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   141
             ("type_enc", [name])
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 52018
diff changeset
   142
           else if can (trans_lams_of_string ctxt any_type_enc) name then
48533
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   143
             ("lam_trans", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   144
           else if member (op =) fact_filters name then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   145
             ("fact_filter", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   146
           else if is_some (Int.fromString name) then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   147
             ("max_facts", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   148
           else
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63136
diff changeset
   149
             error ("Unknown parameter: " ^ quote name)
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   150
         else
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63136
diff changeset
   151
           error ("Unknown parameter: " ^ quote name))
44720
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   152
46435
e9c90516bc0d renamed type encoding
blanchet
parents: 46409
diff changeset
   153
(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
44785
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44784
diff changeset
   154
   read correctly. *)
44784
blanchet
parents: 44768
diff changeset
   155
val implode_param = strip_spaces_except_between_idents o space_implode " "
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   156
54059
896b55752938 run fewer provers in "try" mode
blanchet
parents: 54058
diff changeset
   157
(* FIXME: use "Generic_Data" *)
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41258
diff changeset
   158
structure Data = Theory_Data
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41258
diff changeset
   159
(
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   160
  type T = raw_param list
54546
8b403a7a8c44 fixed spying so that the envirnoment variables are queried at run-time not at build-time
blanchet
parents: 54503
diff changeset
   161
  val empty = default_default_params |> map (apsnd single)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   162
  val extend = I
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41258
diff changeset
   163
  fun merge data : T = AList.merge (op =) (K true) data
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41258
diff changeset
   164
)
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   165
55475
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   166
fun remotify_prover_if_supported_and_not_already_remote ctxt name =
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   167
  if String.isPrefix remote_prefix name then
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   168
    SOME name
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   169
  else
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   170
    let val remote_name = remote_prefix ^ name in
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   171
      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   172
    end
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   173
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   174
fun remotify_prover_if_not_installed ctxt name =
57237
bc51864c2ac4 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
blanchet
parents: 57209
diff changeset
   175
  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
bc51864c2ac4 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
blanchet
parents: 57209
diff changeset
   176
  else remotify_prover_if_supported_and_not_already_remote ctxt name
55475
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   177
57677
9bfa4cb2fee6 reordered provers
blanchet
parents: 57433
diff changeset
   178
(* The first ATP of the list is used by Auto Sledgehammer. *)
55475
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   179
fun default_provers_param_value mode ctxt =
74369
3301c0d8b560 added Zipperposition to sledgehammer's default provers
desharna
parents: 74352
diff changeset
   180
  [cvc4N, vampireN, z3N, eN, spassN, veritN, zipperpositionN]
55475
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   181
  |> map_filter (remotify_prover_if_not_installed ctxt)
54059
896b55752938 run fewer provers in "try" mode
blanchet
parents: 54058
diff changeset
   182
  (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
62925
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62601
diff changeset
   183
  |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   184
  |> implode_param
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   185
44720
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   186
fun set_default_raw_param param thy =
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   187
  let val ctxt = Proof_Context.init_global thy in
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   188
    thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   189
  end
54059
896b55752938 run fewer provers in "try" mode
blanchet
parents: 54058
diff changeset
   190
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   191
fun default_raw_params mode thy =
55475
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   192
  let val ctxt = Proof_Context.init_global thy in
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   193
    Data.get thy
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   194
    |> fold (AList.default (op =))
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   195
         [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]),
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   196
          ("timeout",
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 68563
diff changeset
   197
           let val timeout = Options.default_int \<^system_option>\<open>sledgehammer_timeout\<close> in
55475
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   198
             [if timeout <= 0 then "none" else string_of_int timeout]
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   199
           end)]
b8ebbcc5e49a restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
blanchet
parents: 55458
diff changeset
   200
  end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   201
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   202
fun extract_params mode default_params override_params =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   203
  let
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   204
    val raw_params = rev override_params @ rev default_params
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   205
    val lookup = Option.map implode_param o AList.lookup (op =) raw_params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   206
    val lookup_string = the_default "" o lookup
57290
bc06471cb7b7 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents: 57274
diff changeset
   207
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   208
    fun general_lookup_bool option default_value name =
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   209
      (case lookup name of
35970
3d41a2a490f0 revert debugging output that shouldn't have been submitted in the first place
blanchet
parents: 35966
diff changeset
   210
        SOME s => parse_bool_option option name s
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   211
      | NONE => default_value)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   212
    val lookup_bool = the o general_lookup_bool false (SOME false)
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   213
    fun lookup_time name =
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   214
      (case lookup name of
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   215
        SOME s => parse_time name s
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   216
      | NONE => Time.zeroTime)
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   217
    fun lookup_int name =
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   218
      (case lookup name of
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   219
        NONE => 0
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   220
      | SOME s =>
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   221
        (case Int.fromString s of
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   222
          SOME n => n
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63136
diff changeset
   223
        | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value")))
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   224
    fun lookup_real name =
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   225
      (case lookup name of
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   226
        NONE => 0.0
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   227
      | SOME s =>
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   228
        (case Real.fromString s of
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   229
          SOME n => n
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63136
diff changeset
   230
        | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value")))
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   231
    fun lookup_real_pair name =
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   232
      (case lookup name of
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   233
        NONE => (0.0, 0.0)
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   234
      | SOME s =>
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   235
        (case s |> space_explode " " |> map Real.fromString of
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   236
          [SOME r1, SOME r2] => (r1, r2)
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   237
        | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   238
                 \values (e.g., \"0.6 0.95\")")))
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43057
diff changeset
   239
    fun lookup_option lookup' name =
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   240
      (case lookup name of
38589
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38282
diff changeset
   241
        SOME "smart" => NONE
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   242
      | _ => SOME (lookup' name))
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   243
    val debug = mode <> Auto_Try andalso lookup_bool "debug"
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   244
    val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
36143
6490319b1703 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents: 36142
diff changeset
   245
    val overlord = lookup_bool "overlord"
54546
8b403a7a8c44 fixed spying so that the envirnoment variables are queried at run-time not at build-time
blanchet
parents: 54503
diff changeset
   246
    val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
57290
bc06471cb7b7 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents: 57274
diff changeset
   247
    val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
   248
    val type_enc =
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   249
      if mode = Auto_Try then
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43353
diff changeset
   250
        NONE
55286
blanchet
parents: 55277
diff changeset
   251
      else
blanchet
parents: 55277
diff changeset
   252
        (case lookup_string "type_enc" of
blanchet
parents: 55277
diff changeset
   253
          "smart" => NONE
blanchet
parents: 55277
diff changeset
   254
        | s => (type_enc_of_string Strict s; SOME s))
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   255
    val strict = mode = Auto_Try orelse lookup_bool "strict"
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   256
    val lam_trans = lookup_option lookup_string "lam_trans"
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
   257
    val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   258
    val learn = lookup_bool "learn"
54113
df080dfefddc use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
blanchet
parents: 54059
diff changeset
   259
    val fact_filter =
df080dfefddc use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
blanchet
parents: 54059
diff changeset
   260
      lookup_option lookup_string "fact_filter"
df080dfefddc use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
blanchet
parents: 54059
diff changeset
   261
      |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf)
73940
f58108b7a60c refactored Sledgehammer option "induction_rules"
desharna
parents: 73939
diff changeset
   262
    val induction_rules =
f58108b7a60c refactored Sledgehammer option "induction_rules"
desharna
parents: 73939
diff changeset
   263
      lookup_option (the o induction_rules_of_string o lookup_string) "induction_rules"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
   264
    val max_facts = lookup_option lookup_int "max_facts"
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   265
    val fact_thresholds = lookup_real_pair "fact_thresholds"
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
   266
    val max_mono_iters = lookup_option lookup_int "max_mono_iters"
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
   267
    val max_new_mono_instances =
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
   268
      lookup_option lookup_int "max_new_mono_instances"
51190
2654b3965c8d made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents: 51189
diff changeset
   269
    val isar_proofs = lookup_option lookup_bool "isar_proofs"
57783
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57735
diff changeset
   270
    val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57237
diff changeset
   271
    val try0 = lookup_bool "try0"
71931
0c8a9c028304 simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents: 70934
diff changeset
   272
    val smt_proofs = lookup_bool "smt_proofs"
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45520
diff changeset
   273
    val slice = mode <> Auto_Try andalso lookup_bool "slice"
60306
6b7c64ab8bd2 made Auto Sledgehammer behave more like the real thing
blanchet
parents: 60277
diff changeset
   274
    val minimize = lookup_bool "minimize"
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54546
diff changeset
   275
    val timeout = lookup_time "timeout"
60306
6b7c64ab8bd2 made Auto Sledgehammer behave more like the real thing
blanchet
parents: 60277
diff changeset
   276
    val preplay_timeout = lookup_time "preplay_timeout"
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   277
    val expect = lookup_string "expect"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   278
  in
61311
150aa3015c47 removed legacy asynchronous mode in Sledgehammer
blanchet
parents: 61223
diff changeset
   279
    {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
150aa3015c47 removed legacy asynchronous mode in Sledgehammer
blanchet
parents: 61223
diff changeset
   280
     type_enc = type_enc, strict = strict, lam_trans = lam_trans,
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53764
diff changeset
   281
     uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
73939
9231ea46e041 promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents: 73691
diff changeset
   282
     induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds,
9231ea46e041 promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents: 73691
diff changeset
   283
     max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
9231ea46e041 promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents: 73691
diff changeset
   284
     isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
9231ea46e041 promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents: 73691
diff changeset
   285
     slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
9231ea46e041 promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents: 73691
diff changeset
   286
     expect = expect}
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   287
  end
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   288
54059
896b55752938 run fewer provers in "try" mode
blanchet
parents: 54058
diff changeset
   289
fun get_params mode = extract_params mode o default_raw_params mode
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   290
fun default_params thy = get_params Normal thy o map (apsnd single)
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   291
60564
6a363e56ffff silence 'try'
blanchet
parents: 60306
diff changeset
   292
val silence_state =
6a363e56ffff silence 'try'
blanchet
parents: 60306
diff changeset
   293
  Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false)
6a363e56ffff silence 'try'
blanchet
parents: 60306
diff changeset
   294
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   295
(* Sledgehammer the given subgoal *)
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   296
50604
4f840e2e362e crank up default timeout for MaSh ATP learning
blanchet
parents: 50557
diff changeset
   297
val default_learn_prover_timeout = 2.0
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   298
61223
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   299
fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   300
  let
58089
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   301
    (* We generally want chained facts to be picked up by the relevance filter, because it can then
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   302
       give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs,
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   303
       verbose output, machine learning). However, if the fact is available by no other means (not
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   304
       even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   305
       but to insert it into the state as an additional hypothesis.
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   306
    *)
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   307
    val {facts = chained0, ...} = Proof.goal state0
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   308
    val (inserts, keep_chained) =
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   309
      if null chained0 orelse #only fact_override then
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   310
        (chained0, [])
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   311
      else
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   312
        let val ctxt0 = Proof.context_of state0 in
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   313
          List.partition (is_useful_unnamed_local_fact ctxt0) chained0
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   314
        end
58075
95bab16eac45 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents: 58028
diff changeset
   315
    val state = state0
58089
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   316
      |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained)
60564
6a363e56ffff silence 'try'
blanchet
parents: 60306
diff changeset
   317
      |> silence_state
58089
20e76da3a0ef gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents: 58075
diff changeset
   318
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   319
    val thy = Proof.theory_of state
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   320
    val ctxt = Proof.context_of state
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   321
44720
f3a8c19708c8 fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents: 44651
diff changeset
   322
    val override_params = override_params |> map (normalize_raw_param ctxt)
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   323
  in
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   324
    if subcommand = runN then
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   325
      let val i = the_default 1 opt_i in
60564
6a363e56ffff silence 'try'
blanchet
parents: 60306
diff changeset
   326
        ignore (run_sledgehammer
61223
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   327
          (get_params Normal thy override_params) Normal writeln_result i fact_override state)
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   328
      end
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   329
    else if subcommand = supported_proversN then
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   330
      supported_provers ctxt
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48381
diff changeset
   331
    else if subcommand = unlearnN then
64522
b66f8caf86b6 made MaSh faster and less likely to hang seemingly forever
blanchet
parents: 63692
diff changeset
   332
      mash_unlearn ctxt
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   333
    else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   334
            subcommand = relearn_isarN orelse subcommand = relearn_proverN then
64522
b66f8caf86b6 made MaSh faster and less likely to hang seemingly forever
blanchet
parents: 63692
diff changeset
   335
      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt
57433
7e55bd4f9b0e compile
blanchet
parents: 57290
diff changeset
   336
       else ();
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   337
       mash_learn ctxt
54129
9ee9eee93c06 added comment
blanchet
parents: 54113
diff changeset
   338
           (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   339
           (get_params Normal thy
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   340
                ([("timeout", [string_of_real default_learn_prover_timeout]),
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   341
                  ("slice", ["false"])] @
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   342
                 override_params @
57721
e4858f85e616 always minimize Sledgehammer results by default
blanchet
parents: 57719
diff changeset
   343
                 [("preplay_timeout", ["0"])]))
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   344
           fact_override (#facts (Proof.goal state))
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50052
diff changeset
   345
           (subcommand = learn_proverN orelse subcommand = relearn_proverN))
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   346
    else if subcommand = refresh_tptpN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   347
      refresh_systems_on_tptp ()
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   348
    else
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63136
diff changeset
   349
      error ("Unknown subcommand: " ^ quote subcommand)
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   350
  end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   351
57735
056a55b44ec7 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents: 57732
diff changeset
   352
fun string_of_raw_param (key, values) =
056a55b44ec7 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents: 57732
diff changeset
   353
  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   354
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 68563
diff changeset
   355
val parse_query_bang = \<^keyword>\<open>?\<close> || \<^keyword>\<open>!\<close> || \<^keyword>\<open>!!\<close>
63136
fd11a538daac clarified syntax categories;
wenzelm
parents: 62969
diff changeset
   356
val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param
62969
9f394a16c557 eliminated "xname" and variants;
wenzelm
parents: 62925
diff changeset
   357
val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang)
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 68563
diff changeset
   358
val parse_param = parse_key -- Scan.optional (\<^keyword>\<open>=\<close> |-- parse_value) []
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 72400
diff changeset
   359
val parse_raw_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 72400
diff changeset
   360
val parse_params = parse_raw_params >> map (apsnd implode_param)
62969
9f394a16c557 eliminated "xname" and variants;
wenzelm
parents: 62925
diff changeset
   361
val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   362
val parse_fact_override_chunk =
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   363
  (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   364
  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   365
  || (parse_fact_refs >> only_fact_override)
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   366
val parse_fact_override =
57290
bc06471cb7b7 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents: 57274
diff changeset
   367
  Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides))
57433
7e55bd4f9b0e compile
blanchet
parents: 57290
diff changeset
   368
    no_fact_override
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   369
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   370
val _ =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 68563
diff changeset
   371
  Outer_Syntax.command \<^command_keyword>\<open>sledgehammer\<close>
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   372
    "search for first-order proof using automatic theorem provers"
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 72400
diff changeset
   373
    (Scan.optional Parse.name runN -- parse_raw_params
60277
bcd9a70342be sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
wenzelm
parents: 60276
diff changeset
   374
      -- parse_fact_override -- Scan.option Parse.nat >>
60276
3bb094031275 more standard command setup;
wenzelm
parents: 60202
diff changeset
   375
      (fn (((subcommand, params), fact_override), opt_i) =>
60277
bcd9a70342be sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
wenzelm
parents: 60276
diff changeset
   376
        Toplevel.keep_proof
bcd9a70342be sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
wenzelm
parents: 60276
diff changeset
   377
          (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of)))
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   378
val _ =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 68563
diff changeset
   379
  Outer_Syntax.command \<^command_keyword>\<open>sledgehammer_params\<close>
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   380
    "set and display the default parameters for Sledgehammer"
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 72400
diff changeset
   381
    (parse_raw_params >> (fn params =>
60276
3bb094031275 more standard command setup;
wenzelm
parents: 60202
diff changeset
   382
      Toplevel.theory (fold set_default_raw_param params #> tap (fn thy =>
3bb094031275 more standard command setup;
wenzelm
parents: 60202
diff changeset
   383
        writeln ("Default parameters for Sledgehammer:\n" ^
3bb094031275 more standard command setup;
wenzelm
parents: 60202
diff changeset
   384
          (case rev (default_raw_params Normal thy) of
3bb094031275 more standard command setup;
wenzelm
parents: 60202
diff changeset
   385
            [] => "none"
3bb094031275 more standard command setup;
wenzelm
parents: 60202
diff changeset
   386
          | params => params |> map string_of_raw_param |> sort_strings |> cat_lines))))))
36394
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
   387
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   388
fun try_sledgehammer auto state =
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   389
  let
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   390
    val thy = Proof.theory_of state
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   391
    val mode = if auto then Auto_Try else Try
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   392
    val i = 1
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   393
  in
60564
6a363e56ffff silence 'try'
blanchet
parents: 60306
diff changeset
   394
    run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state)
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40599
diff changeset
   395
  end
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   396
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 68563
diff changeset
   397
val _ = Try.tool_setup (sledgehammerN, (40, \<^system_option>\<open>auto_sledgehammer\<close>, try_sledgehammer))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   398
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents: 52653
diff changeset
   399
val _ =
61223
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   400
  Query_Operation.register {name = sledgehammerN, pri = 0}
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   401
    (fn {state = st, args, writeln_result, ...} =>
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   402
      (case try Toplevel.proof_of st of
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   403
        SOME state =>
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   404
          let
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   405
            val [provers_arg, isar_proofs_arg, try0_arg] = args
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   406
            val override_params =
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   407
              ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   408
                [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]),
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   409
                 ("try0", [try0_arg]),
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   410
                 ("debug", ["false"]),
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   411
                 ("verbose", ["false"]),
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   412
                 ("overlord", ["false"])]);
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   413
          in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end
dfccf6c06201 clarified markup;
wenzelm
parents: 60740
diff changeset
   414
      | NONE => error "Unknown proof context"))
53055
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 53053
diff changeset
   415
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   416
end;