src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author blanchet
Tue Aug 17 16:47:40 2010 +0200 (2010-08-17)
changeset 38490 57de0f12516f
parent 38282 319c59682c51
child 38589 b03f8fe043ec
permissions -rw-r--r--
tuning
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
     5 *)
     6 
     7 signature SLEDGEHAMMER_ISAR =
     8 sig
     9   type params = Sledgehammer.params
    10 
    11   val atps: string Unsynchronized.ref
    12   val timeout: int Unsynchronized.ref
    13   val full_types: bool Unsynchronized.ref
    14   val default_params : theory -> (string * string) list -> params
    15 end;
    16 
    17 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    18 struct
    19 
    20 open ATP_Systems
    21 open Sledgehammer_Util
    22 open Sledgehammer
    23 open Sledgehammer_Fact_Minimize
    24 
    25 (** Sledgehammer commands **)
    26 
    27 fun add_to_relevance_override ns : relevance_override =
    28   {add = ns, del = [], only = false}
    29 fun del_from_relevance_override ns : relevance_override =
    30   {add = [], del = ns, only = false}
    31 fun only_relevance_override ns : relevance_override =
    32   {add = ns, del = [], only = true}
    33 fun merge_relevance_override_pairwise (r1 : relevance_override)
    34                                       (r2 : relevance_override) =
    35   {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
    36    only = #only r1 andalso #only r2}
    37 fun merge_relevance_overrides rs =
    38   fold merge_relevance_override_pairwise rs (only_relevance_override [])
    39 
    40 (*** parameters ***)
    41 
    42 val atps = Unsynchronized.ref ""
    43 val timeout = Unsynchronized.ref 60
    44 val full_types = Unsynchronized.ref false
    45 
    46 val _ =
    47   ProofGeneralPgip.add_preference Preferences.category_proof
    48       (Preferences.string_pref atps
    49           "Sledgehammer: ATPs"
    50           "Default automatic provers (separated by whitespace)")
    51 
    52 val _ =
    53   ProofGeneralPgip.add_preference Preferences.category_proof
    54       (Preferences.int_pref timeout
    55           "Sledgehammer: Time Limit"
    56           "ATPs will be interrupted after this time (in seconds)")
    57 
    58 val _ =
    59   ProofGeneralPgip.add_preference Preferences.category_proof
    60       (Preferences.bool_pref full_types
    61           "Sledgehammer: Full Types" "ATPs will use full type information")
    62 
    63 type raw_param = string * string list
    64 
    65 val default_default_params =
    66   [("debug", "false"),
    67    ("verbose", "false"),
    68    ("overlord", "false"),
    69    ("explicit_apply", "false"),
    70    ("relevance_threshold", "50"),
    71    ("relevance_convergence", "320"),
    72    ("theory_relevant", "smart"),
    73    ("defs_relevant", "false"),
    74    ("isar_proof", "false"),
    75    ("isar_shrink_factor", "1"),
    76    ("minimize_timeout", "5 s")]
    77 
    78 val alias_params =
    79   [("atp", "atps")]
    80 val negated_alias_params =
    81   [("no_debug", "debug"),
    82    ("quiet", "verbose"),
    83    ("no_overlord", "overlord"),
    84    ("partial_types", "full_types"),
    85    ("implicit_apply", "explicit_apply"),
    86    ("theory_irrelevant", "theory_relevant"),
    87    ("defs_irrelevant", "defs_relevant"),
    88    ("no_isar_proof", "isar_proof")]
    89 
    90 val params_for_minimize =
    91   ["debug", "verbose", "overlord", "full_types", "isar_proof",
    92    "isar_shrink_factor", "minimize_timeout"]
    93 
    94 val property_dependent_params = ["atps", "full_types", "timeout"]
    95 
    96 fun is_known_raw_param s =
    97   AList.defined (op =) default_default_params s orelse
    98   AList.defined (op =) alias_params s orelse
    99   AList.defined (op =) negated_alias_params s orelse
   100   member (op =) property_dependent_params s
   101 
   102 fun check_raw_param (s, _) =
   103   if is_known_raw_param s then ()
   104   else error ("Unknown parameter: " ^ quote s ^ ".")
   105 
   106 fun unalias_raw_param (name, value) =
   107   case AList.lookup (op =) alias_params name of
   108     SOME name' => (name', value)
   109   | NONE =>
   110     case AList.lookup (op =) negated_alias_params name of
   111       SOME name' => (name', case value of
   112                               ["false"] => ["true"]
   113                             | ["true"] => ["false"]
   114                             | [] => ["false"]
   115                             | _ => value)
   116     | NONE => (name, value)
   117 
   118 structure Data = Theory_Data(
   119   type T = raw_param list
   120   val empty = default_default_params |> map (apsnd single)
   121   val extend = I
   122   fun merge p : T = AList.merge (op =) (K true) p)
   123 
   124 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
   125 fun default_raw_params thy =
   126   Data.get thy
   127   |> fold (AList.default (op =))
   128           [("atps", [case !atps of "" => default_atps_param_value () | s => s]),
   129            ("full_types", [if !full_types then "true" else "false"]),
   130            ("timeout", let val timeout = !timeout in
   131                          [if timeout <= 0 then "none"
   132                           else string_of_int timeout ^ " s"]
   133                        end)]
   134 
   135 val infinity_time_in_secs = 60 * 60 * 24 * 365
   136 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
   137 
   138 fun extract_params default_params override_params =
   139   let
   140     val override_params = map unalias_raw_param override_params
   141     val raw_params = rev override_params @ rev default_params
   142     val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
   143     val lookup_string = the_default "" o lookup
   144     fun general_lookup_bool option default_value name =
   145       case lookup name of
   146         SOME s => parse_bool_option option name s
   147       | NONE => default_value
   148     val lookup_bool = the o general_lookup_bool false (SOME false)
   149     val lookup_bool_option = general_lookup_bool true NONE
   150     fun lookup_time name =
   151       the_timeout (case lookup name of
   152                      NONE => NONE
   153                    | SOME s => parse_time_option name s)
   154     fun lookup_int name =
   155       case lookup name of
   156         NONE => 0
   157       | SOME s => case Int.fromString s of
   158                     SOME n => n
   159                   | NONE => error ("Parameter " ^ quote name ^
   160                                    " must be assigned an integer value.")
   161     val debug = lookup_bool "debug"
   162     val verbose = debug orelse lookup_bool "verbose"
   163     val overlord = lookup_bool "overlord"
   164     val atps = lookup_string "atps" |> space_explode " "
   165     val full_types = lookup_bool "full_types"
   166     val explicit_apply = lookup_bool "explicit_apply"
   167     val relevance_threshold =
   168       0.01 * Real.fromInt (lookup_int "relevance_threshold")
   169     val relevance_convergence =
   170       0.01 * Real.fromInt (lookup_int "relevance_convergence")
   171     val theory_relevant = lookup_bool_option "theory_relevant"
   172     val defs_relevant = lookup_bool "defs_relevant"
   173     val isar_proof = lookup_bool "isar_proof"
   174     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
   175     val timeout = lookup_time "timeout"
   176     val minimize_timeout = lookup_time "minimize_timeout"
   177   in
   178     {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
   179      full_types = full_types, explicit_apply = explicit_apply,
   180      relevance_threshold = relevance_threshold,
   181      relevance_convergence = relevance_convergence,
   182      theory_relevant = theory_relevant, defs_relevant = defs_relevant,
   183      isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
   184      timeout = timeout, minimize_timeout = minimize_timeout}
   185   end
   186 
   187 fun get_params thy = extract_params (default_raw_params thy)
   188 fun default_params thy = get_params thy o map (apsnd single)
   189 
   190 (* Sledgehammer the given subgoal *)
   191 
   192 val sledgehammerN = "sledgehammer"
   193 val sledgehammer_paramsN = "sledgehammer_params"
   194 
   195 val runN = "run"
   196 val minimizeN = "minimize"
   197 val messagesN = "messages"
   198 val available_atpsN = "available_atps"
   199 val running_atpsN = "running_atps"
   200 val kill_atpsN = "kill_atps"
   201 val refresh_tptpN = "refresh_tptp"
   202 
   203 fun minimizize_raw_param_name "timeout" = "minimize_timeout"
   204   | minimizize_raw_param_name name = name
   205 
   206 val is_raw_param_relevant_for_minimize =
   207   member (op =) params_for_minimize o fst o unalias_raw_param
   208 fun string_for_raw_param (key, values) =
   209   key ^ (case space_implode " " values of "" => "" | value => " = " ^ value)
   210 
   211 fun minimize_command override_params i atp_name fact_names =
   212   sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^
   213   (override_params |> filter is_raw_param_relevant_for_minimize
   214                    |> implode o map (prefix ", " o string_for_raw_param)) ^
   215   "] (" ^ space_implode " " fact_names ^ ")" ^
   216   (if i = 1 then "" else " " ^ string_of_int i)
   217 
   218 fun hammer_away override_params subcommand opt_i relevance_override state =
   219   let
   220     val thy = Proof.theory_of state
   221     val _ = app check_raw_param override_params
   222   in
   223     if subcommand = runN then
   224       let val i = the_default 1 opt_i in
   225         run_sledgehammer (get_params thy override_params) i relevance_override
   226                          (minimize_command override_params i) state
   227       end
   228     else if subcommand = minimizeN then
   229       run_minimize (get_params thy (map (apfst minimizize_raw_param_name)
   230                                override_params))
   231                    (the_default 1 opt_i) (#add relevance_override) state
   232     else if subcommand = messagesN then
   233       messages opt_i
   234     else if subcommand = available_atpsN then
   235       available_atps thy
   236     else if subcommand = running_atpsN then
   237       running_atps ()
   238     else if subcommand = kill_atpsN then
   239       kill_atps ()
   240     else if subcommand = refresh_tptpN then
   241       refresh_systems_on_tptp ()
   242     else
   243       error ("Unknown subcommand: " ^ quote subcommand ^ ".")
   244   end
   245 
   246 fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =
   247   Toplevel.keep (hammer_away params subcommand opt_i relevance_override
   248                  o Toplevel.proof_of)
   249 
   250 fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
   251 
   252 fun sledgehammer_params_trans params =
   253   Toplevel.theory
   254       (fold set_default_raw_param params
   255        #> tap (fn thy => 
   256                   writeln ("Default parameters for Sledgehammer:\n" ^
   257                            (case rev (default_raw_params thy) of
   258                               [] => "none"
   259                             | params =>
   260                               (map check_raw_param params;
   261                                params |> map string_for_raw_param
   262                                       |> sort_strings |> cat_lines)))))
   263 
   264 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
   265 val parse_value = Scan.repeat1 Parse.xname
   266 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
   267 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
   268 val parse_fact_refs =
   269   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
   270                             (Parse.xname -- Scan.option Attrib.thm_sel)
   271                 >> (fn (name, interval) =>
   272                        Facts.Named ((name, Position.none), interval)))
   273 val parse_relevance_chunk =
   274   (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
   275   || (Args.del |-- Args.colon |-- parse_fact_refs
   276       >> del_from_relevance_override)
   277   || (parse_fact_refs >> only_relevance_override)
   278 val parse_relevance_override =
   279   Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
   280                               >> merge_relevance_overrides))
   281                 (add_to_relevance_override [])
   282 val parse_sledgehammer_command =
   283   (Scan.optional Parse.short_ident runN -- parse_params
   284    -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
   285 val parse_sledgehammer_params_command =
   286   parse_params #>> sledgehammer_params_trans
   287 
   288 val _ =
   289   Outer_Syntax.improper_command sledgehammerN
   290       "search for first-order proof using automatic theorem provers" Keyword.diag
   291       parse_sledgehammer_command
   292 val _ =
   293   Outer_Syntax.command sledgehammer_paramsN
   294       "set and display the default parameters for Sledgehammer" Keyword.thy_decl
   295       parse_sledgehammer_params_command
   296 
   297 end;