src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author blanchet
Fri Apr 16 15:49:13 2010 +0200 (2010-04-16)
changeset 36170 0cdb76723c88
parent 36143 6490319b1703
child 36183 f723348b2231
permissions -rw-r--r--
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
     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 default_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 orelse #only r2}
    35 fun merge_relevance_overrides rs =
    36   fold merge_relevance_override_pairwise rs default_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    ("respect_no_atp", "true"),
    45    ("relevance_threshold", "50"),
    46    ("convergence", "320"),
    47    ("theory_const", "smart"),
    48    ("higher_order", "smart"),
    49    ("follow_defs", "false"),
    50    ("isar_proof", "false"),
    51    ("modulus", "1"),
    52    ("sorts", "false"),
    53    ("minimize_timeout", "5 s")]
    54 
    55 val alias_params =
    56   [("atp", "atps")]
    57 val negated_alias_params =
    58   [("no_debug", "debug"),
    59    ("quiet", "verbose"),
    60    ("no_overlord", "overlord"),
    61    ("ignore_no_atp", "respect_no_atp"),
    62    ("partial_types", "full_types"),
    63    ("no_theory_const", "theory_const"),
    64    ("first_order", "higher_order"),
    65    ("dont_follow_defs", "follow_defs"),
    66    ("metis_proof", "isar_proof"),
    67    ("no_sorts", "sorts")]
    68 
    69 val property_dependent_params = ["atps", "full_types", "timeout"]
    70 
    71 fun is_known_raw_param s =
    72   AList.defined (op =) default_default_params s orelse
    73   AList.defined (op =) alias_params s orelse
    74   AList.defined (op =) negated_alias_params s orelse
    75   member (op =) property_dependent_params s
    76 
    77 fun check_raw_param (s, _) =
    78   if is_known_raw_param s then ()
    79   else error ("Unknown parameter: " ^ quote s ^ ".")
    80 
    81 fun unalias_raw_param (name, value) =
    82   case AList.lookup (op =) alias_params name of
    83     SOME name' => (name', value)
    84   | NONE =>
    85     case AList.lookup (op =) negated_alias_params name of
    86       SOME name' => (name', case value of
    87                               ["false"] => ["true"]
    88                             | ["true"] => ["false"]
    89                             | [] => ["false"]
    90                             | _ => value)
    91     | NONE => (name, value)
    92 
    93 structure Data = Theory_Data(
    94   type T = raw_param list
    95   val empty = default_default_params |> map (apsnd single)
    96   val extend = I
    97   fun merge p : T = AList.merge (op =) (K true) p)
    98 
    99 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
   100 fun default_raw_params thy =
   101   Data.get thy
   102   |> fold (AList.default (op =))
   103           [("atps", [!atps]),
   104            ("full_types", [if !full_types then "true" else "false"]),
   105            ("timeout", let val timeout = !timeout in
   106                          [if timeout <= 0 then "none"
   107                           else string_of_int timeout ^ " s"]
   108                        end)]
   109 
   110 val infinity_time_in_secs = 60 * 60 * 24 * 365
   111 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
   112 
   113 fun extract_params thy default_params override_params =
   114   let
   115     val override_params = map unalias_raw_param override_params
   116     val raw_params = rev override_params @ rev default_params
   117     val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
   118     val lookup_string = the_default "" o lookup
   119     fun general_lookup_bool option default_value name =
   120       case lookup name of
   121         SOME s => parse_bool_option option name s
   122       | NONE => default_value
   123     val lookup_bool = the o general_lookup_bool false (SOME false)
   124     val lookup_bool_option = general_lookup_bool true NONE
   125     fun lookup_time name =
   126       the_timeout (case lookup name of
   127                      NONE => NONE
   128                    | SOME s => parse_time_option name s)
   129     fun lookup_int name =
   130       case lookup name of
   131         NONE => 0
   132       | SOME s => case Int.fromString s of
   133                     SOME n => n
   134                   | NONE => error ("Parameter " ^ quote name ^
   135                                    " must be assigned an integer value.")
   136     val debug = lookup_bool "debug"
   137     val verbose = debug orelse lookup_bool "verbose"
   138     val overlord = lookup_bool "overlord"
   139     val atps = lookup_string "atps" |> space_explode " "
   140     val full_types = lookup_bool "full_types"
   141     val respect_no_atp = lookup_bool "respect_no_atp"
   142     val relevance_threshold =
   143       0.01 * Real.fromInt (lookup_int "relevance_threshold")
   144     val convergence = 0.01 * Real.fromInt (lookup_int "convergence")
   145     val theory_const = lookup_bool_option "theory_const"
   146     val higher_order = lookup_bool_option "higher_order"
   147     val follow_defs = lookup_bool "follow_defs"
   148     val isar_proof = lookup_bool "isar_proof"
   149     val modulus = Int.max (1, lookup_int "modulus")
   150     val sorts = lookup_bool "sorts"
   151     val timeout = lookup_time "timeout"
   152     val minimize_timeout = lookup_time "minimize_timeout"
   153   in
   154     {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
   155      full_types = full_types, respect_no_atp = respect_no_atp,
   156      relevance_threshold = relevance_threshold, convergence = convergence,
   157      theory_const = theory_const, higher_order = higher_order,
   158      follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus,
   159      sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout}
   160   end
   161 
   162 fun get_params thy = extract_params thy (default_raw_params thy)
   163 fun default_params thy = get_params thy o map (apsnd single)
   164 
   165 fun minimize override_params old_style_args i fact_refs state =
   166   let
   167     val thy = Proof.theory_of state
   168     val ctxt = Proof.context_of state
   169     fun theorems_from_refs ctxt =
   170       map (fn fact_ref =>
   171               let
   172                 val ths = ProofContext.get_fact ctxt fact_ref
   173                 val name' = Facts.string_of_ref fact_ref
   174               in (name', ths) end)
   175     fun get_time_limit_arg s =
   176       (case Int.fromString s of
   177         SOME t => Time.fromSeconds t
   178       | NONE => error ("Invalid time limit: " ^ quote s))
   179     fun get_opt (name, a) (p, t) =
   180       (case name of
   181         "time" => (p, get_time_limit_arg a)
   182       | "atp" => (a, t)
   183       | n => error ("Invalid argument: " ^ n))
   184     val {atps, minimize_timeout, ...} = get_params thy override_params
   185     val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout)
   186     val params =
   187       get_params thy
   188           [("atps", [atp]),
   189            ("minimize_timeout",
   190             [string_of_int (Time.toMilliseconds timeout) ^ " ms"])]
   191     val prover =
   192       (case get_prover thy atp of
   193         SOME prover => prover
   194       | NONE => error ("Unknown ATP: " ^ quote atp))
   195     val name_thms_pairs = theorems_from_refs ctxt fact_refs
   196   in
   197     writeln (#2 (minimize_theorems params linear_minimize prover atp i state
   198                                    name_thms_pairs))
   199   end
   200 
   201 val runN = "run"
   202 val minimizeN = "minimize"
   203 val messagesN = "messages"
   204 val available_atpsN = "available_atps"
   205 val running_atpsN = "running_atps"
   206 val kill_atpsN = "kill_atps"
   207 val refresh_tptpN = "refresh_tptp"
   208 val helpN = "help"
   209 
   210 val addN = "add"
   211 val delN = "del"
   212 val onlyN = "only"
   213 
   214 fun minimizize_raw_param_name "timeout" = "minimize_timeout"
   215   | minimizize_raw_param_name name = name
   216 
   217 fun hammer_away override_params subcommand opt_i relevance_override state =
   218   let
   219     val thy = Proof.theory_of state
   220     val _ = List.app check_raw_param override_params
   221   in
   222     if subcommand = runN then
   223       sledgehammer (get_params thy override_params) (the_default 1 opt_i)
   224                    relevance_override state
   225     else if subcommand = minimizeN then
   226       minimize (map (apfst minimizize_raw_param_name) override_params) []
   227                (the_default 1 opt_i) (#add relevance_override) state
   228     else if subcommand = messagesN then
   229       messages opt_i
   230     else if subcommand = available_atpsN then
   231       available_atps thy
   232     else if subcommand = running_atpsN then
   233       running_atps ()
   234     else if subcommand = kill_atpsN then
   235       kill_atps ()
   236     else if subcommand = refresh_tptpN then
   237       refresh_systems_on_tptp ()
   238     else
   239       error ("Unknown subcommand: " ^ quote subcommand ^ ".")
   240   end
   241 
   242 fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =
   243   Toplevel.keep (hammer_away params subcommand opt_i relevance_override
   244                  o Toplevel.proof_of)
   245 
   246 fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
   247 
   248 fun sledgehammer_params_trans params =
   249   Toplevel.theory
   250       (fold set_default_raw_param params
   251        #> tap (fn thy => 
   252                   writeln ("Default parameters for Sledgehammer:\n" ^
   253                            (case rev (default_raw_params thy) of
   254                               [] => "none"
   255                             | params =>
   256                               (map check_raw_param params;
   257                                params |> map string_for_raw_param
   258                                       |> sort_strings |> cat_lines)))))
   259 
   260 val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
   261 val parse_value = Scan.repeat1 P.xname
   262 val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
   263 val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []
   264 val parse_fact_refs =
   265   Scan.repeat1 (Scan.unless (P.name -- Args.colon)
   266                             (P.xname -- Scan.option Attrib.thm_sel)
   267                 >> (fn (name, interval) =>
   268                        Facts.Named ((name, Position.none), interval)))
   269 val parse_relevance_chunk =
   270   (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
   271   || (Args.del |-- Args.colon |-- parse_fact_refs
   272       >> del_from_relevance_override)
   273   || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_relevance_override)
   274 val parse_relevance_override =
   275   Scan.optional (Args.parens
   276       (Scan.optional (parse_fact_refs >> only_relevance_override)
   277                      default_relevance_override
   278        -- Scan.repeat parse_relevance_chunk)
   279        >> op :: >> merge_relevance_overrides)
   280       default_relevance_override
   281 val parse_sledgehammer_command =
   282   (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
   283    -- Scan.option P.nat) #>> sledgehammer_trans
   284 val parse_sledgehammer_params_command =
   285   parse_params #>> sledgehammer_params_trans
   286 
   287 val parse_minimize_args =
   288   Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname)))
   289                 []
   290 val _ =
   291   OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
   292     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps))
   293 val _ =
   294   OuterSyntax.improper_command "atp_info"
   295     "print information about managed provers" K.diag
   296     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps))
   297 val _ =
   298   OuterSyntax.improper_command "atp_messages"
   299     "print recent messages issued by managed provers" K.diag
   300     (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
   301       (fn limit => Toplevel.no_timing
   302                    o Toplevel.imperative (fn () => messages limit)))
   303 val _ =
   304   OuterSyntax.improper_command "print_atps" "print external provers" K.diag
   305     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
   306       Toplevel.keep (available_atps o Toplevel.theory_of)))
   307 val _ =
   308   OuterSyntax.improper_command "atp_minimize"
   309     "minimize theorem list with external prover" K.diag
   310     (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
   311       Toplevel.no_timing o Toplevel.unknown_proof o
   312         Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of)))
   313 
   314 val _ =
   315   OuterSyntax.improper_command "sledgehammer"
   316     "search for first-order proof using automatic theorem provers" K.diag
   317     parse_sledgehammer_command
   318 val _ =
   319   OuterSyntax.command "sledgehammer_params"
   320     "set and display the default parameters for Sledgehammer" K.thy_decl
   321     parse_sledgehammer_params_command
   322 
   323 end;