src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author smolkas
Fri, 11 Jan 2013 14:35:28 +0100
changeset 50824 a991d603aac6
parent 50823 0583db803066
child 51130 76d68444cd59
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36375
2482446a604c move the minimizer to the Sledgehammer directory
blanchet
parents: 36373
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar.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
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
     7
signature SLEDGEHAMMER_ISAR =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
     8
sig
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40941
diff changeset
     9
  type params = Sledgehammer_Provers.params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    10
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    11
  val auto : bool Unsynchronized.ref
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    12
  val provers : string Unsynchronized.ref
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    13
  val timeout : int Unsynchronized.ref
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
    14
  val default_params : Proof.context -> (string * string) list -> params
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    15
  val setup : theory -> theory
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    16
end;
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    17
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
    18
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    19
struct
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    20
44784
blanchet
parents: 44768
diff changeset
    21
open ATP_Util
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38021
diff changeset
    22
open ATP_Systems
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    23
open ATP_Problem_Generate
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    24
open ATP_Proof_Reconstruct
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35970
diff changeset
    25
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
    26
open Sledgehammer_Fact
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40941
diff changeset
    27
open Sledgehammer_Provers
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    28
open Sledgehammer_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48332
diff changeset
    29
open Sledgehammer_MaSh
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40941
diff changeset
    30
open Sledgehammer_Run
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
    31
48433
9e9b6e363859 don't relearn old facts in Isar mode
blanchet
parents: 48432
diff changeset
    32
(* val cvc3N = "cvc3" *)
48405
7682bc885e8a use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents: 48400
diff changeset
    33
val yicesN = "yices"
7682bc885e8a use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents: 48400
diff changeset
    34
val z3N = "z3"
7682bc885e8a use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents: 48400
diff changeset
    35
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    36
val runN = "run"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    37
val minN = "min"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    38
val messagesN = "messages"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    39
val supported_proversN = "supported_provers"
50719
58b0b44da54a renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
blanchet
parents: 50604
diff changeset
    40
val kill_allN = "kill_all"
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    41
val running_proversN = "running_provers"
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
    42
val running_learnersN = "running_learners"
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    43
val refresh_tptpN = "refresh_tptp"
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48293
diff changeset
    44
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    45
val auto = Unsynchronized.ref false
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    46
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    47
val _ =
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    48
  ProofGeneralPgip.add_preference Preferences.category_tracing
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    49
      (Preferences.bool_pref auto "auto-sledgehammer"
39327
blanchet
parents: 39324
diff changeset
    50
           "Run Sledgehammer automatically.")
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
    51
36394
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
    52
(** Sledgehammer commands **)
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
    53
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    54
fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    55
fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    56
fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    57
fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
    58
  {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
36183
f723348b2231 Sledgehammer: the empty set of fact () should mean nothing, not unchanged
blanchet
parents: 36143
diff changeset
    59
   only = #only r1 andalso #only r2}
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    60
fun merge_fact_overrides rs =
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
    61
  fold merge_fact_override_pairwise rs (only_fact_override [])
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
    62
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    63
(*** parameters ***)
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    64
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    65
val provers = Unsynchronized.ref ""
39335
87a9ff4d5817 use 30 s instead of 60 s as the default Sledgehammer timeout;
blanchet
parents: 39327
diff changeset
    66
val timeout = Unsynchronized.ref 30
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    67
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    68
val _ =
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    69
  ProofGeneralPgip.add_preference Preferences.category_proof
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    70
      (Preferences.string_pref provers
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
    71
          "Sledgehammer: Provers"
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    72
          "Default automatic provers (separated by whitespace)")
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    73
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    74
val _ =
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    75
  ProofGeneralPgip.add_preference Preferences.category_proof
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    76
      (Preferences.int_pref timeout
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
    77
          "Sledgehammer: Time Limit"
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    78
          "ATPs will be interrupted after this time (in seconds)")
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36290
diff changeset
    79
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    80
type raw_param = string * string list
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    81
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    82
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
    83
  [("debug", "false"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
    84
   ("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
    85
   ("overlord", "false"),
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
    86
   ("blocking", "false"),
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
    87
   ("type_enc", "smart"),
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
    88
   ("strict", "false"),
45514
973bb7846505 parse lambda translation option in Metis
blanchet
parents: 45063
diff changeset
    89
   ("lam_trans", "smart"),
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
    90
   ("uncurried_aliases", "smart"),
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    91
   ("learn", "true"),
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
    92
   ("fact_filter", "smart"),
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
    93
   ("max_facts", "smart"),
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    94
   ("fact_thresholds", "0.45 0.85"),
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
    95
   ("max_mono_iters", "smart"),
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
    96
   ("max_new_mono_instances", "smart"),
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
    97
   ("isar_proofs", "false"),
50020
6b9611abcd4c renamed Sledgehammer option
blanchet
parents: 49918
diff changeset
    98
   ("isar_shrink", "10"),
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45520
diff changeset
    99
   ("slice", "true"),
45707
6bf7eec9b153 added "minimize" option for more control over automatic minimization
blanchet
parents: 45706
diff changeset
   100
   ("minimize", "smart"),
46297
0a4907baf9db lower timeout for preplay, now that we have more preplay methods
blanchet
parents: 45707
diff changeset
   101
   ("preplay_timeout", "3")]
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   102
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   103
val alias_params =
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   104
  [("prover", ("provers", [])), (* legacy *)
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   105
   ("max_relevant", ("max_facts", [])), (* legacy *)
47037
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   106
   ("dont_preplay", ("preplay_timeout", ["0"]))]
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   107
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
   108
  [("no_debug", "debug"),
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   109
   ("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
   110
   ("no_overlord", "overlord"),
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
   111
   ("non_blocking", "blocking"),
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   112
   ("non_strict", "strict"),
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
   113
   ("no_uncurried_aliases", "uncurried_aliases"),
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   114
   ("dont_learn", "learn"),
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   115
   ("no_isar_proofs", "isar_proofs"),
45707
6bf7eec9b153 added "minimize" option for more control over automatic minimization
blanchet
parents: 45706
diff changeset
   116
   ("dont_slice", "slice"),
6bf7eec9b153 added "minimize" option for more control over automatic minimization
blanchet
parents: 45706
diff changeset
   117
   ("dont_minimize", "minimize")]
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   118
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   119
val params_for_minimize =
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   120
  ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
   121
   "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
50747
a057d3fd6783 pass option to minimize
blanchet
parents: 50719
diff changeset
   122
   "learn", "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   123
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43353
diff changeset
   124
val property_dependent_params = ["provers", "timeout"]
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   125
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   126
fun is_known_raw_param s =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   127
  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
   128
  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
   129
  AList.defined (op =) negated_alias_params s orelse
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   130
  member (op =) property_dependent_params s orelse s = "expect"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   131
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   132
fun is_prover_list ctxt s =
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   133
  case space_explode " " s of
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   134
    ss as _ :: _ => forall (is_prover_supported ctxt) ss
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   135
  | _ => false
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   136
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   137
fun unalias_raw_param (name, value) =
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   138
  case AList.lookup (op =) alias_params name of
47037
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   139
    SOME (name', []) => (name', value)
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   140
  | SOME (param' as (name', _)) =>
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   141
    if value <> ["false"] then
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   142
      param'
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   143
    else
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   144
      error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \
ea6695d58aad added "dont_preplay" alias
blanchet
parents: 46961
diff changeset
   145
             \(cf. " ^ quote name' ^ ").")
36140
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   146
  | NONE =>
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   147
    case AList.lookup (op =) negated_alias_params name of
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   148
      SOME name' => (name', case value of
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   149
                              ["false"] => ["true"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   150
                            | ["true"] => ["false"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   151
                            | [] => ["false"]
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   152
                            | _ => value)
08b2a7ecb6c3 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents: 36064
diff changeset
   153
    | NONE => (name, value)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   154
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   155
val any_type_enc = type_enc_from_string Strict "erased"
45514
973bb7846505 parse lambda translation option in Metis
blanchet
parents: 45063
diff changeset
   156
48397
9fe826095a02 convenience
blanchet
parents: 48395
diff changeset
   157
(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
9fe826095a02 convenience
blanchet
parents: 48395
diff changeset
   158
   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
   159
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
   160
  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
   161
  #> (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
   162
         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
   163
           (name, value)
48533
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   164
         else if null value then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   165
           if is_prover_list ctxt name then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   166
             ("provers", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   167
           else if can (type_enc_from_string Strict) name then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   168
             ("type_enc", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   169
           else if can (trans_lams_from_string ctxt any_type_enc) name then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   170
             ("lam_trans", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   171
           else if member (op =) fact_filters name then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   172
             ("fact_filter", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   173
           else if is_some (Int.fromString name) then
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   174
             ("max_facts", [name])
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   175
           else
5ada9fd7507b detect unknown options again
blanchet
parents: 48433
diff changeset
   176
             error ("Unknown parameter: " ^ quote name ^ ".")
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   177
         else
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   178
           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
   179
46435
e9c90516bc0d renamed type encoding
blanchet
parents: 46409
diff changeset
   180
(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
44785
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44784
diff changeset
   181
   read correctly. *)
44784
blanchet
parents: 44768
diff changeset
   182
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
   183
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41258
diff changeset
   184
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
   185
(
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   186
  type T = raw_param list
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   187
  val empty = default_default_params |> map (apsnd single)
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   188
  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
   189
  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
   190
)
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   191
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   192
fun remotify_prover_if_supported_and_not_already_remote ctxt name =
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   193
  if String.isPrefix remote_prefix name then
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   194
    SOME name
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   195
  else
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   196
    let val remote_name = remote_prefix ^ name in
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   197
      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   198
    end
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   199
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   200
fun remotify_prover_if_not_installed ctxt name =
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   201
  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40931
diff changeset
   202
    SOME name
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40931
diff changeset
   203
  else
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   204
    remotify_prover_if_supported_and_not_already_remote ctxt name
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40069
diff changeset
   205
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   206
fun avoid_too_many_threads _ _ [] = []
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   207
  | avoid_too_many_threads _ (0, 0) _ = []
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   208
  | avoid_too_many_threads ctxt (0, max_remote) provers =
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   209
    provers
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   210
    |> map_filter (remotify_prover_if_supported_and_not_already_remote ctxt)
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   211
    |> take max_remote
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   212
  | avoid_too_many_threads _ (max_local, 0) provers =
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   213
    provers
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   214
    |> filter_out (String.isPrefix remote_prefix)
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   215
    |> take max_local
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   216
  | avoid_too_many_threads ctxt max_local_and_remote (prover :: provers) =
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   217
    let
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   218
      val max_local_and_remote =
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   219
        max_local_and_remote
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   220
        |> (if String.isPrefix remote_prefix prover then apsnd else apfst)
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48405
diff changeset
   221
               (Integer.add ~1)
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   222
    in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   223
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   224
val max_default_remote_threads = 4
42688
097a61baeca9 smoother handling of ! and ? in type system names
blanchet
parents: 42613
diff changeset
   225
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   226
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
48405
7682bc885e8a use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents: 48400
diff changeset
   227
   timeout, it makes sense to put E first. *)
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   228
fun default_provers_param_value ctxt =
48432
60759d07df24 took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
blanchet
parents: 48406
diff changeset
   229
  [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN]
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40931
diff changeset
   230
  |> map_filter (remotify_prover_if_not_installed ctxt)
43009
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   231
  |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
f58bab6be6a9 reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents: 43008
diff changeset
   232
                                  max_default_remote_threads)
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   233
  |> implode_param
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   234
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
   235
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
   236
  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
   237
    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
   238
  end
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   239
fun default_raw_params ctxt =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42237
diff changeset
   240
  let val thy = Proof_Context.theory_of ctxt in
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   241
    Data.get thy
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   242
    |> fold (AList.default (op =))
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   243
            [("provers", [case !provers of
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   244
                            "" => default_provers_param_value ctxt
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   245
                          | s => s]),
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   246
             ("timeout", let val timeout = !timeout in
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   247
                           [if timeout <= 0 then "none"
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40181
diff changeset
   248
                            else string_of_int timeout]
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   249
                         end)]
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   250
  end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   251
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   252
fun extract_params mode default_params override_params =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   253
  let
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   254
    val raw_params = rev override_params @ rev default_params
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   255
    val lookup = Option.map implode_param o AList.lookup (op =) raw_params
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   256
    val lookup_string = the_default "" o lookup
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   257
    fun general_lookup_bool option default_value name =
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   258
      case lookup name of
35970
3d41a2a490f0 revert debugging output that shouldn't have been submitted in the first place
blanchet
parents: 35966
diff changeset
   259
        SOME s => parse_bool_option option name s
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   260
      | NONE => default_value
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   261
    val lookup_bool = the o general_lookup_bool false (SOME false)
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   262
    fun lookup_time name =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   263
      case lookup name of
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   264
        SOME s => parse_time_option name s
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   265
      | NONE => NONE
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   266
    fun lookup_int name =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   267
      case lookup name of
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   268
        NONE => 0
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   269
      | SOME s => case Int.fromString s of
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   270
                    SOME n => n
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   271
                  | NONE => error ("Parameter " ^ quote name ^
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   272
                                   " must be assigned an integer value.")
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   273
    fun lookup_real name =
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   274
      case lookup name of
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   275
        NONE => 0.0
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   276
      | SOME s => case Real.fromString s of
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   277
                    SOME n => n
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   278
                  | NONE => error ("Parameter " ^ quote name ^
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   279
                                   " 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
   280
    fun lookup_real_pair name =
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   281
      case lookup name of
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   282
        NONE => (0.0, 0.0)
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   283
      | SOME s => case s |> space_explode " " |> map Real.fromString of
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   284
                    [SOME r1, SOME r2] => (r1, r2)
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   285
                  | _ => error ("Parameter " ^ quote name ^
49632
c44b2a404687 tuned message
blanchet
parents: 49365
diff changeset
   286
                                " must be assigned a pair of floating-point \
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   287
                                \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
   288
    fun lookup_option lookup' name =
38589
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38282
diff changeset
   289
      case lookup name of
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38282
diff changeset
   290
        SOME "smart" => NONE
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
   291
      | _ => SOME (lookup' name)
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   292
    val debug = mode <> Auto_Try andalso lookup_bool "debug"
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   293
    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
   294
    val overlord = lookup_bool "overlord"
42995
e23f61546cf0 always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents: 42944
diff changeset
   295
    val blocking =
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   296
      Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
42995
e23f61546cf0 always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents: 42944
diff changeset
   297
      lookup_bool "blocking"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   298
    val provers = lookup_string "provers" |> space_explode " "
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   299
                  |> mode = Auto_Try ? single o hd
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
   300
    val type_enc =
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   301
      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
   302
        NONE
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
   303
      else case lookup_string "type_enc" of
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43353
diff changeset
   304
        "smart" => NONE
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   305
      | s => (type_enc_from_string Strict s; SOME s)
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   306
    val strict = mode = Auto_Try orelse lookup_bool "strict"
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   307
    val lam_trans = lookup_option lookup_string "lam_trans"
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
   308
    val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   309
    val learn = lookup_bool "learn"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
   310
    val fact_filter = lookup_option lookup_string "fact_filter"
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
   311
    val max_facts = lookup_option lookup_int "max_facts"
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   312
    val fact_thresholds = lookup_real_pair "fact_thresholds"
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
   313
    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
   314
    val max_new_mono_instances =
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47642
diff changeset
   315
      lookup_option lookup_int "max_new_mono_instances"
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   316
    val isar_proofs = lookup_bool "isar_proofs"
50020
6b9611abcd4c renamed Sledgehammer option
blanchet
parents: 49918
diff changeset
   317
    val isar_shrink = Real.max (1.0, lookup_real "isar_shrink")
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45520
diff changeset
   318
    val slice = mode <> Auto_Try andalso lookup_bool "slice"
45707
6bf7eec9b153 added "minimize" option for more control over automatic minimization
blanchet
parents: 45706
diff changeset
   319
    val minimize =
6bf7eec9b153 added "minimize" option for more control over automatic minimization
blanchet
parents: 45706
diff changeset
   320
      if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50484
diff changeset
   321
    val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
43015
21b6baec55b1 renamed "metis_timeout" to "preplay_timeout" and continued implementation
blanchet
parents: 43013
diff changeset
   322
    val preplay_timeout =
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50484
diff changeset
   323
      if mode = Auto_Try then SOME Time.zeroTime
31313171deb5 thread no timeout properly
blanchet
parents: 50484
diff changeset
   324
      else lookup_time "preplay_timeout"
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   325
    val expect = lookup_string "expect"
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   326
  in
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41153
diff changeset
   327
    {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46297
diff changeset
   328
     provers = provers, type_enc = type_enc, strict = strict,
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46398
diff changeset
   329
     lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   330
     learn = learn, fact_filter = fact_filter, max_facts = max_facts,
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48308
diff changeset
   331
     fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   332
     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
50020
6b9611abcd4c renamed Sledgehammer option
blanchet
parents: 49918
diff changeset
   333
     isar_shrink = isar_shrink, slice = slice, minimize = minimize,
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49632
diff changeset
   334
     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   335
  end
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   336
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
   337
fun get_params mode = extract_params mode o default_raw_params
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   338
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
   339
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   340
(* Sledgehammer the given subgoal *)
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36371
diff changeset
   341
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   342
val default_minimize_prover = metisN
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43034
diff changeset
   343
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
   344
fun is_raw_param_relevant_for_minimize (name, _) =
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
   345
  member (op =) params_for_minimize name
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   346
fun string_for_raw_param (key, values) =
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   347
  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
50748
c056718eb687 nicer output
blanchet
parents: 50747
diff changeset
   348
fun nice_string_for_raw_param (p as (key, ["false"])) =
c056718eb687 nicer output
blanchet
parents: 50747
diff changeset
   349
    (case AList.find (op =) negated_alias_params key of
c056718eb687 nicer output
blanchet
parents: 50747
diff changeset
   350
       [neg] => neg
c056718eb687 nicer output
blanchet
parents: 50747
diff changeset
   351
     | _ => string_for_raw_param p)
c056718eb687 nicer output
blanchet
parents: 50747
diff changeset
   352
  | nice_string_for_raw_param p = string_for_raw_param p
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   353
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   354
fun minimize_command override_params i more_override_params prover_name
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   355
                     fact_names =
43057
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   356
  let
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   357
    val params =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   358
      (override_params
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   359
       |> filter_out (AList.defined (op =) more_override_params o fst)) @
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   360
      more_override_params
43057
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   361
      |> filter is_raw_param_relevant_for_minimize
50748
c056718eb687 nicer output
blanchet
parents: 50747
diff changeset
   362
      |> map nice_string_for_raw_param
43057
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   363
      |> (if prover_name = default_minimize_prover then I else cons prover_name)
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   364
      |> space_implode ", "
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   365
  in
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   366
    sledgehammerN ^ " " ^ minN ^
43057
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   367
    (if params = "" then "" else enclose " [" "]" params) ^
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   368
    " (" ^ space_implode " " fact_names ^ ")" ^
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   369
    (if i = 1 then "" else " " ^ string_of_int i)
884b0bc19de4 fixed syntax of min options
blanchet
parents: 43051
diff changeset
   370
  end
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   371
50604
4f840e2e362e crank up default timeout for MaSh ATP learning
blanchet
parents: 50557
diff changeset
   372
val default_learn_prover_timeout = 2.0
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   373
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   374
fun hammer_away override_params subcommand opt_i fact_override state =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   375
  let
50824
smolkas
parents: 50823
diff changeset
   376
    (* necessary to avoid problems in jedit *)
50823
0583db803066 set show_markup to false in order to avoid problems in jedit
smolkas
parents: 50748
diff changeset
   377
    val state = state |> Proof.map_context (Config.put show_markup false)
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   378
    val ctxt = Proof.context_of state
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
   379
    val override_params = override_params |> map (normalize_raw_param ctxt)
50052
c8d141cce517 create temp directory if not already created
blanchet
parents: 50020
diff changeset
   380
    val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   381
  in
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   382
    if subcommand = runN then
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   383
      let val i = the_default 1 opt_i in
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   384
        run_sledgehammer (get_params Normal ctxt override_params) Normal i
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   385
                         fact_override (minimize_command override_params i)
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   386
                         state
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   387
        |> K ()
36281
dbbf4d5d584d pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents: 36235
diff changeset
   388
      end
43008
bb212c2ad238 renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents: 42997
diff changeset
   389
    else if subcommand = minN then
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   390
      let
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48392
diff changeset
   391
        val ctxt = ctxt |> Config.put instantiate_inducts false
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   392
        val i = the_default 1 opt_i
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   393
        val params =
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   394
          get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   395
                                    override_params)
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   396
        val goal = prop_of (#goal (Proof.goal state))
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   397
        val facts = nearly_all_facts ctxt false fact_override Symtab.empty
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   398
                                     Termtab.empty [] [] goal
48399
4bacc8983b3d learn from SMT proofs when they can be minimized by Metis
blanchet
parents: 48397
diff changeset
   399
        fun learn prover = mash_learn_proof ctxt params prover goal facts
4bacc8983b3d learn from SMT proofs when they can be minimized by Metis
blanchet
parents: 48397
diff changeset
   400
      in run_minimize params learn i (#add fact_override) state end
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   401
    else if subcommand = messagesN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   402
      messages opt_i
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   403
    else if subcommand = supported_proversN then
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41472
diff changeset
   404
      supported_provers ctxt
50719
58b0b44da54a renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
blanchet
parents: 50604
diff changeset
   405
    else if subcommand = kill_allN then
49365
8aebe857aaaa merged two commands
blanchet
parents: 48533
diff changeset
   406
      (kill_provers (); kill_learners ())
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   407
    else if subcommand = running_proversN then
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   408
      running_provers ()
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48381
diff changeset
   409
    else if subcommand = unlearnN then
df75b2d7e26a learn command in MaSh
blanchet
parents: 48381
diff changeset
   410
      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
   411
    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
   412
            subcommand = relearn_isarN orelse subcommand = relearn_proverN then
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
   413
      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   414
         mash_unlearn ctxt
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   415
       else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   416
         ();
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
   417
       mash_learn ctxt
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
   418
           (get_params Normal ctxt
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
   419
                ([("timeout",
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
   420
                   [string_of_real default_learn_prover_timeout]),
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
   421
                  ("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
   422
                 override_params @
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
   423
                 [("minimize", ["true"]),
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
   424
                  ("preplay_timeout", ["0"])]))
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
   425
           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
   426
           (subcommand = learn_proverN orelse subcommand = relearn_proverN))
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   427
    else if subcommand = running_learnersN then
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   428
      running_learners ()
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   429
    else if subcommand = refresh_tptpN then
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   430
      refresh_systems_on_tptp ()
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   431
    else
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   432
      error ("Unknown subcommand: " ^ quote subcommand ^ ".")
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   433
  end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   434
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   435
fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   436
  Toplevel.keep (hammer_away params subcommand opt_i fact_override
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35965
diff changeset
   437
                 o Toplevel.proof_of)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   438
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   439
fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   440
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   441
fun sledgehammer_params_trans params =
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   442
  Toplevel.theory
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   443
      (fold set_default_raw_param params
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   444
       #> tap (fn thy =>
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42237
diff changeset
   445
                  let val ctxt = Proof_Context.init_global thy in
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   446
                    writeln ("Default parameters for Sledgehammer:\n" ^
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   447
                             (case default_raw_params ctxt |> rev of
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   448
                                [] => "none"
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   449
                              | params =>
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
   450
                                params |> map string_for_raw_param
41258
73401632a80c convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet
parents: 41208
diff changeset
   451
                                       |> sort_strings |> cat_lines))
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40066
diff changeset
   452
                  end))
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   453
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46435
diff changeset
   454
val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
42776
87389311ba78 added convenience syntax
blanchet
parents: 42740
diff changeset
   455
val parse_key =
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44720
diff changeset
   456
  Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
42581
398fff2c6b8f use ! for mildly unsound and !! for very unsound encodings
blanchet
parents: 42579
diff changeset
   457
val parse_value =
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44720
diff changeset
   458
  Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46435
diff changeset
   459
val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36924
diff changeset
   460
val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
35965
0fce6db7babd added a syntax for specifying facts to Sledgehammer;
blanchet
parents: 35963
diff changeset
   461
val parse_fact_refs =
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38988
diff changeset
   462
  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   463
val parse_fact_override_chunk =
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   464
  (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   465
  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   466
  || (parse_fact_refs >> only_fact_override)
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   467
val parse_fact_override =
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   468
  Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   469
                              >> merge_fact_overrides))
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   470
                no_fact_override
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   471
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   472
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   473
  Outer_Syntax.improper_command @{command_spec "sledgehammer"}
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   474
    "search for first-order proof using automatic theorem provers"
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   475
    ((Scan.optional Parse.short_ident runN -- parse_params
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   476
      -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35962
diff changeset
   477
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   478
  Outer_Syntax.command @{command_spec "sledgehammer_params"}
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   479
    "set and display the default parameters for Sledgehammer"
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   480
    (parse_params #>> sledgehammer_params_trans)
36394
1a48d18449d8 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents: 36378
diff changeset
   481
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   482
fun try_sledgehammer auto state =
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   483
  let
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   484
    val ctxt = Proof.context_of state
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   485
    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
   486
    val i = 1
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   487
  in
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48250
diff changeset
   488
    run_sledgehammer (get_params mode ctxt []) mode i no_fact_override
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   489
                     (minimize_command [] i) state
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40599
diff changeset
   490
  end
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   491
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48388
diff changeset
   492
val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38997
diff changeset
   493
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff changeset
   494
end;