src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author blanchet
Wed Apr 21 16:21:19 2010 +0200 (2010-04-21 ago)
changeset 36281 dbbf4d5d584d
parent 36235 61159615a0c5
child 36290 c29283184c7a
permissions -rw-r--r--
pass relevant options from "sledgehammer" to "sledgehammer minimize";
one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files
     1 (*  Title:      HOL/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 = ATP_Manager.params
    10 
    11   val default_params : theory -> (string * string) list -> params
    12 end;
    13 
    14 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    15 struct
    16 
    17 open Sledgehammer_Util
    18 open ATP_Manager
    19 open ATP_Minimal
    20 open ATP_Wrapper
    21 
    22 structure K = OuterKeyword and P = OuterParse
    23 
    24 fun add_to_relevance_override ns : relevance_override =
    25   {add = ns, del = [], only = false}
    26 fun del_from_relevance_override ns : relevance_override =
    27   {add = [], del = ns, only = false}
    28 fun only_relevance_override ns : relevance_override =
    29   {add = ns, del = [], only = true}
    30 val no_relevance_override = add_to_relevance_override []
    31 fun merge_relevance_override_pairwise (r1 : relevance_override)
    32                                       (r2 : relevance_override) =
    33   {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
    34    only = #only r1 andalso #only r2}
    35 fun merge_relevance_overrides rs =
    36   fold merge_relevance_override_pairwise rs (only_relevance_override [])
    37 
    38 type raw_param = string * string list
    39 
    40 val default_default_params =
    41   [("debug", "false"),
    42    ("verbose", "false"),
    43    ("overlord", "false"),
    44    ("explicit_apply", "false"),
    45    ("respect_no_atp", "true"),
    46    ("relevance_threshold", "50"),
    47    ("convergence", "320"),
    48    ("theory_relevant", "smart"),
    49    ("higher_order", "smart"),
    50    ("follow_defs", "false"),
    51    ("isar_proof", "false"),
    52    ("modulus", "1"),
    53    ("sorts", "false"),
    54    ("minimize_timeout", "5 s")]
    55 
    56 val alias_params =
    57   [("atp", "atps")]
    58 val negated_alias_params =
    59   [("no_debug", "debug"),
    60    ("quiet", "verbose"),
    61    ("no_overlord", "overlord"),
    62    ("implicit_apply", "explicit_apply"),
    63    ("ignore_no_atp", "respect_no_atp"),
    64    ("partial_types", "full_types"),
    65    ("theory_irrelevant", "theory_relevant"),
    66    ("first_order", "higher_order"),
    67    ("dont_follow_defs", "follow_defs"),
    68    ("metis_proof", "isar_proof"),
    69    ("no_sorts", "sorts")]
    70 
    71 val params_for_minimize =
    72   ["full_types", "explicit_apply", "higher_order", "isar_proof", "modulus",
    73    "sorts", "minimize_timeout"]
    74 
    75 val property_dependent_params = ["atps", "full_types", "timeout"]
    76 
    77 fun is_known_raw_param s =
    78   AList.defined (op =) default_default_params s orelse
    79   AList.defined (op =) alias_params s orelse
    80   AList.defined (op =) negated_alias_params s orelse
    81   member (op =) property_dependent_params s
    82 
    83 fun check_raw_param (s, _) =
    84   if is_known_raw_param s then ()
    85   else error ("Unknown parameter: " ^ quote s ^ ".")
    86 
    87 fun unalias_raw_param (name, value) =
    88   case AList.lookup (op =) alias_params name of
    89     SOME name' => (name', value)
    90   | NONE =>
    91     case AList.lookup (op =) negated_alias_params name of
    92       SOME name' => (name', case value of
    93                               ["false"] => ["true"]
    94                             | ["true"] => ["false"]
    95                             | [] => ["false"]
    96                             | _ => value)
    97     | NONE => (name, value)
    98 
    99 structure Data = Theory_Data(
   100   type T = raw_param list
   101   val empty = default_default_params |> map (apsnd single)
   102   val extend = I
   103   fun merge p : T = AList.merge (op =) (K true) p)
   104 
   105 (* Don't even try to start ATPs that are not installed.
   106    Hack: Should not rely on naming convention. *)
   107 val filter_atps =
   108   space_explode " "
   109   #> filter (fn s => String.isPrefix "remote_" s orelse
   110                      getenv (String.map Char.toUpper s ^ "_HOME") <> "")
   111   #> space_implode " "
   112 
   113 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
   114 fun default_raw_params thy =
   115   Data.get thy
   116   |> fold (AList.default (op =))
   117           [("atps", [filter_atps (!atps)]),
   118            ("full_types", [if !full_types then "true" else "false"]),
   119            ("timeout", let val timeout = !timeout in
   120                          [if timeout <= 0 then "none"
   121                           else string_of_int timeout ^ " s"]
   122                        end)]
   123 
   124 val infinity_time_in_secs = 60 * 60 * 24 * 365
   125 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
   126 
   127 fun extract_params thy default_params override_params =
   128   let
   129     val override_params = map unalias_raw_param override_params
   130     val raw_params = rev override_params @ rev default_params
   131     val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
   132     val lookup_string = the_default "" o lookup
   133     fun general_lookup_bool option default_value name =
   134       case lookup name of
   135         SOME s => parse_bool_option option name s
   136       | NONE => default_value
   137     val lookup_bool = the o general_lookup_bool false (SOME false)
   138     val lookup_bool_option = general_lookup_bool true NONE
   139     fun lookup_time name =
   140       the_timeout (case lookup name of
   141                      NONE => NONE
   142                    | SOME s => parse_time_option name s)
   143     fun lookup_int name =
   144       case lookup name of
   145         NONE => 0
   146       | SOME s => case Int.fromString s of
   147                     SOME n => n
   148                   | NONE => error ("Parameter " ^ quote name ^
   149                                    " must be assigned an integer value.")
   150     val debug = lookup_bool "debug"
   151     val verbose = debug orelse lookup_bool "verbose"
   152     val overlord = lookup_bool "overlord"
   153     val atps = lookup_string "atps" |> space_explode " "
   154     val full_types = lookup_bool "full_types"
   155     val explicit_apply = lookup_bool "explicit_apply"
   156     val respect_no_atp = lookup_bool "respect_no_atp"
   157     val relevance_threshold =
   158       0.01 * Real.fromInt (lookup_int "relevance_threshold")
   159     val convergence = 0.01 * Real.fromInt (lookup_int "convergence")
   160     val theory_relevant = lookup_bool_option "theory_relevant"
   161     val higher_order = lookup_bool_option "higher_order"
   162     val follow_defs = lookup_bool "follow_defs"
   163     val isar_proof = lookup_bool "isar_proof"
   164     val modulus = Int.max (1, lookup_int "modulus")
   165     val sorts = lookup_bool "sorts"
   166     val timeout = lookup_time "timeout"
   167     val minimize_timeout = lookup_time "minimize_timeout"
   168   in
   169     {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
   170      full_types = full_types, explicit_apply = explicit_apply,
   171      respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
   172      convergence = convergence, theory_relevant = theory_relevant,
   173      higher_order = higher_order, follow_defs = follow_defs,
   174      isar_proof = isar_proof, modulus = modulus, sorts = sorts,
   175      timeout = timeout, minimize_timeout = minimize_timeout}
   176   end
   177 
   178 fun get_params thy = extract_params thy (default_raw_params thy)
   179 fun default_params thy = get_params thy o map (apsnd single)
   180 
   181 fun minimize override_params old_style_args i fact_refs state =
   182   let
   183     val thy = Proof.theory_of state
   184     val ctxt = Proof.context_of state
   185     fun theorems_from_refs ctxt =
   186       map (fn fact_ref =>
   187               let
   188                 val ths = ProofContext.get_fact ctxt fact_ref
   189                 val name' = Facts.string_of_ref fact_ref
   190               in (name', ths) end)
   191     fun get_time_limit_arg s =
   192       (case Int.fromString s of
   193         SOME t => Time.fromSeconds t
   194       | NONE => error ("Invalid time limit: " ^ quote s ^ "."))
   195     fun get_opt (name, a) (p, t) =
   196       (case name of
   197         "time" => (p, get_time_limit_arg a)
   198       | "atp" => (a, t)
   199       | n => error ("Invalid argument: " ^ n ^ "."))
   200     val {atps, minimize_timeout, ...} = get_params thy override_params
   201     val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout)
   202     val params =
   203       get_params thy
   204           (override_params @
   205            [("atps", [atp]),
   206             ("minimize_timeout",
   207              [string_of_int (Time.toMilliseconds timeout) ^ " ms"])])
   208     val prover =
   209       (case get_prover thy atp of
   210         SOME prover => prover
   211       | NONE => error ("Unknown ATP: " ^ quote atp ^ "."))
   212     val name_thms_pairs = theorems_from_refs ctxt fact_refs
   213   in
   214     priority (#2 (minimize_theorems params prover atp i state name_thms_pairs))
   215   end
   216 
   217 val runN = "run"
   218 val minimizeN = "minimize"
   219 val messagesN = "messages"
   220 val available_atpsN = "available_atps"
   221 val running_atpsN = "running_atps"
   222 val kill_atpsN = "kill_atps"
   223 val refresh_tptpN = "refresh_tptp"
   224 val helpN = "help"
   225 
   226 fun minimizize_raw_param_name "timeout" = "minimize_timeout"
   227   | minimizize_raw_param_name name = name
   228 
   229 val is_raw_param_relevant_for_minimize =
   230   member (op =) params_for_minimize o fst o unalias_raw_param
   231 fun string_for_raw_param (key, values) =
   232   key ^ (case space_implode " " values of
   233            "" => ""
   234          | value => " = " ^ value)
   235 
   236 fun minimize_command override_params i atp_name facts =
   237   "sledgehammer minimize [atp = " ^ atp_name ^
   238   (override_params |> filter is_raw_param_relevant_for_minimize
   239                    |> implode o map (prefix ", " o string_for_raw_param)) ^
   240   "] (" ^ space_implode " " facts ^ ")" ^
   241   (if i = 1 then "" else " " ^ string_of_int i)
   242 
   243 fun hammer_away override_params subcommand opt_i relevance_override state =
   244   let
   245     val thy = Proof.theory_of state
   246     val _ = List.app check_raw_param override_params
   247   in
   248     if subcommand = runN then
   249       let val i = the_default 1 opt_i in
   250         sledgehammer (get_params thy override_params) i relevance_override
   251                      (minimize_command override_params i) state
   252       end
   253     else if subcommand = minimizeN then
   254       minimize (map (apfst minimizize_raw_param_name) override_params) []
   255                (the_default 1 opt_i) (#add relevance_override) state
   256     else if subcommand = messagesN then
   257       messages opt_i
   258     else if subcommand = available_atpsN then
   259       available_atps thy
   260     else if subcommand = running_atpsN then
   261       running_atps ()
   262     else if subcommand = kill_atpsN then
   263       kill_atps ()
   264     else if subcommand = refresh_tptpN then
   265       refresh_systems_on_tptp ()
   266     else
   267       error ("Unknown subcommand: " ^ quote subcommand ^ ".")
   268   end
   269 
   270 fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =
   271   Toplevel.keep (hammer_away params subcommand opt_i relevance_override
   272                  o Toplevel.proof_of)
   273 
   274 fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
   275 
   276 fun sledgehammer_params_trans params =
   277   Toplevel.theory
   278       (fold set_default_raw_param params
   279        #> tap (fn thy => 
   280                   writeln ("Default parameters for Sledgehammer:\n" ^
   281                            (case rev (default_raw_params thy) of
   282                               [] => "none"
   283                             | params =>
   284                               (map check_raw_param params;
   285                                params |> map string_for_raw_param
   286                                       |> sort_strings |> cat_lines)))))
   287 
   288 val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
   289 val parse_value = Scan.repeat1 P.xname
   290 val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
   291 val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []
   292 val parse_fact_refs =
   293   Scan.repeat1 (Scan.unless (P.name -- Args.colon)
   294                             (P.xname -- Scan.option Attrib.thm_sel)
   295                 >> (fn (name, interval) =>
   296                        Facts.Named ((name, Position.none), interval)))
   297 val parse_relevance_chunk =
   298   (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
   299   || (Args.del |-- Args.colon |-- parse_fact_refs
   300       >> del_from_relevance_override)
   301   || (parse_fact_refs >> only_relevance_override)
   302 val parse_relevance_override =
   303   Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
   304                               >> merge_relevance_overrides))
   305                 (add_to_relevance_override [])
   306 val parse_sledgehammer_command =
   307   (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
   308    -- Scan.option P.nat) #>> sledgehammer_trans
   309 val parse_sledgehammer_params_command =
   310   parse_params #>> sledgehammer_params_trans
   311 
   312 val parse_minimize_args =
   313   Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname)))
   314                 []
   315 val _ =
   316   OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
   317     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps))
   318 val _ =
   319   OuterSyntax.improper_command "atp_info"
   320     "print information about managed provers" K.diag
   321     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps))
   322 val _ =
   323   OuterSyntax.improper_command "atp_messages"
   324     "print recent messages issued by managed provers" K.diag
   325     (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
   326       (fn limit => Toplevel.no_timing
   327                    o Toplevel.imperative (fn () => messages limit)))
   328 val _ =
   329   OuterSyntax.improper_command "print_atps" "print external provers" K.diag
   330     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
   331       Toplevel.keep (available_atps o Toplevel.theory_of)))
   332 val _ =
   333   OuterSyntax.improper_command "atp_minimize"
   334     "minimize theorem list with external prover" K.diag
   335     (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
   336       Toplevel.no_timing o Toplevel.unknown_proof o
   337         Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of)))
   338 
   339 val _ =
   340   OuterSyntax.improper_command "sledgehammer"
   341     "search for first-order proof using automatic theorem provers" K.diag
   342     parse_sledgehammer_command
   343 val _ =
   344   OuterSyntax.command "sledgehammer_params"
   345     "set and display the default parameters for Sledgehammer" K.thy_decl
   346     parse_sledgehammer_params_command
   347 
   348 end;