wneuper/isa: src/HOL/Tools/Sledgehammer/sledgehammer

     1 (*  Title:      HOL/Sledgehammer/sledgehammer_isar.ML

     2     Author:     Jasmin Blanchette, TU Muenchen

     4 Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.

     5 *)

     7 signature SLEDGEHAMMER_ISAR =

     8 sig

     9   type params = ATP_Manager.params

    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;

    17 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =

    18 struct

    20 open Sledgehammer_Util

    21 open ATP_Manager

    22 open ATP_Minimal

    23 open ATP_Wrapper

    25 structure K = OuterKeyword and P = OuterParse

    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 val no_relevance_override = add_to_relevance_override []

    34 fun merge_relevance_override_pairwise (r1 : relevance_override)

    35                                       (r2 : relevance_override) =

    36   {add = #add r1 @ #add r2, del = #del r1 @ #del r2,

    37    only = #only r1 andalso #only r2}

    38 fun merge_relevance_overrides rs =

    39   fold merge_relevance_override_pairwise rs (only_relevance_override [])

    41 (*** parameters ***)

    43 val atps = Unsynchronized.ref (default_atps_param_value ())

    44 val timeout = Unsynchronized.ref 60

    45 val full_types = Unsynchronized.ref false

    47 val _ =

    48   ProofGeneralPgip.add_preference Preferences.category_proof

    49       (Preferences.string_pref atps

    50           "Sledgehammer: ATPs"

    51           "Default automatic provers (separated by whitespace)")

    53 val _ =

    54   ProofGeneralPgip.add_preference Preferences.category_proof

    55       (Preferences.int_pref timeout

    56           "Sledgehammer: Time Limit"

    57           "ATPs will be interrupted after this time (in seconds)")

    59 val _ =

    60   ProofGeneralPgip.add_preference Preferences.category_proof

    61       (Preferences.bool_pref full_types

    62           "Sledgehammer: Full Types" "ATPs will use full type information")

    64 type raw_param = string * string list

    66 val default_default_params =

    67   [("debug", "false"),

    68    ("verbose", "false"),

    69    ("overlord", "false"),

    70    ("explicit_apply", "false"),

    71    ("respect_no_atp", "true"),

    72    ("relevance_threshold", "50"),

    73    ("convergence", "320"),

    74    ("theory_relevant", "smart"),

    75    ("higher_order", "smart"),

    76    ("follow_defs", "false"),

    77    ("isar_proof", "false"),

    78    ("modulus", "1"),

    79    ("sorts", "false"),

    80    ("minimize_timeout", "5 s")]

    82 val alias_params =

    83   [("atp", "atps")]

    84 val negated_alias_params =

    85   [("no_debug", "debug"),

    86    ("quiet", "verbose"),

    87    ("no_overlord", "overlord"),

    88    ("implicit_apply", "explicit_apply"),

    89    ("ignore_no_atp", "respect_no_atp"),

    90    ("partial_types", "full_types"),

    91    ("theory_irrelevant", "theory_relevant"),

    92    ("first_order", "higher_order"),

    93    ("dont_follow_defs", "follow_defs"),

    94    ("metis_proof", "isar_proof"),

    95    ("no_sorts", "sorts")]

    97 val params_for_minimize =

    98   ["full_types", "explicit_apply", "higher_order", "isar_proof", "modulus",

    99    "sorts", "minimize_timeout"]

   101 val property_dependent_params = ["atps", "full_types", "timeout"]

   103 fun is_known_raw_param s =

   104   AList.defined (op =) default_default_params s orelse

   105   AList.defined (op =) alias_params s orelse

   106   AList.defined (op =) negated_alias_params s orelse

   107   member (op =) property_dependent_params s

   109 fun check_raw_param (s, _) =

   110   if is_known_raw_param s then ()

   111   else error ("Unknown parameter: " ^ quote s ^ ".")

   113 fun unalias_raw_param (name, value) =

   114   case AList.lookup (op =) alias_params name of

   115     SOME name' => (name', value)

   116   | NONE =>

   117     case AList.lookup (op =) negated_alias_params name of

   118       SOME name' => (name', case value of

   119                               ["false"] => ["true"]

   120                             | ["true"] => ["false"]

   121                             | [] => ["false"]

   122                             | _ => value)

   123     | NONE => (name, value)

   125 structure Data = Theory_Data(

   126   type T = raw_param list

   127   val empty = default_default_params |> map (apsnd single)

   128   val extend = I

   129   fun merge p : T = AList.merge (op =) (K true) p)

   131 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param

   132 fun default_raw_params thy =

   133   Data.get thy

   134   |> fold (AList.default (op =))

   135           [("atps", [!atps]),

   136            ("full_types", [if !full_types then "true" else "false"]),

   137            ("timeout", let val timeout = !timeout in

   138                          [if timeout <= 0 then "none"

   139                           else string_of_int timeout ^ " s"]

   140                        end)]

   142 val infinity_time_in_secs = 60 * 60 * 24 * 365

   143 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)

   145 fun extract_params thy default_params override_params =

   146   let

   147     val override_params = map unalias_raw_param override_params

   148     val raw_params = rev override_params @ rev default_params

   149     val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params

   150     val lookup_string = the_default "" o lookup

   151     fun general_lookup_bool option default_value name =

   152       case lookup name of

   153         SOME s => parse_bool_option option name s

   154       | NONE => default_value

   155     val lookup_bool = the o general_lookup_bool false (SOME false)

   156     val lookup_bool_option = general_lookup_bool true NONE

   157     fun lookup_time name =

   158       the_timeout (case lookup name of

   159                      NONE => NONE

   160                    | SOME s => parse_time_option name s)

   161     fun lookup_int name =

   162       case lookup name of

   163         NONE => 0

   164       | SOME s => case Int.fromString s of

   165                     SOME n => n

   166                   | NONE => error ("Parameter " ^ quote name ^

   167                                    " must be assigned an integer value.")

   168     val debug = lookup_bool "debug"

   169     val verbose = debug orelse lookup_bool "verbose"

   170     val overlord = lookup_bool "overlord"

   171     val atps = lookup_string "atps" |> space_explode " "

   172     val full_types = lookup_bool "full_types"

   173     val explicit_apply = lookup_bool "explicit_apply"

   174     val respect_no_atp = lookup_bool "respect_no_atp"

   175     val relevance_threshold =

   176       0.01 * Real.fromInt (lookup_int "relevance_threshold")

   177     val convergence = 0.01 * Real.fromInt (lookup_int "convergence")

   178     val theory_relevant = lookup_bool_option "theory_relevant"

   179     val higher_order = lookup_bool_option "higher_order"

   180     val follow_defs = lookup_bool "follow_defs"

   181     val isar_proof = lookup_bool "isar_proof"

   182     val modulus = Int.max (1, lookup_int "modulus")

   183     val sorts = lookup_bool "sorts"

   184     val timeout = lookup_time "timeout"

   185     val minimize_timeout = lookup_time "minimize_timeout"

   186   in

   187     {debug = debug, verbose = verbose, overlord = overlord, atps = atps,

   188      full_types = full_types, explicit_apply = explicit_apply,

   189      respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,

   190      convergence = convergence, theory_relevant = theory_relevant,

   191      higher_order = higher_order, follow_defs = follow_defs,

   192      isar_proof = isar_proof, modulus = modulus, sorts = sorts,

   193      timeout = timeout, minimize_timeout = minimize_timeout}

   194   end

   196 fun get_params thy = extract_params thy (default_raw_params thy)

   197 fun default_params thy = get_params thy o map (apsnd single)

   199 (* Sledgehammer the given subgoal *)

   201 fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."

   202   | run (params as {atps, timeout, ...}) i relevance_override minimize_command

   203         proof_state =

   204     let

   205       val birth_time = Time.now ()

   206       val death_time = Time.+ (birth_time, timeout)

   207       val _ = kill_atps ()  (* race w.r.t. other invocations of Sledgehammer *)

   208       val _ = priority "Sledgehammering..."

   209       val _ = List.app (start_prover_thread params birth_time death_time i

   210                                             relevance_override minimize_command

   211                                             proof_state) atps

   212     in () end

   214 fun minimize override_params old_style_args i fact_refs state =

   215   let

   216     val thy = Proof.theory_of state

   217     val ctxt = Proof.context_of state

   218     fun theorems_from_refs ctxt =

   219       map (fn fact_ref =>

   220               let

   221                 val ths = ProofContext.get_fact ctxt fact_ref

   222                 val name' = Facts.string_of_ref fact_ref

   223               in (name', ths) end)

   224     fun get_time_limit_arg s =

   225       (case Int.fromString s of

   226         SOME t => Time.fromSeconds t

   227       | NONE => error ("Invalid time limit: " ^ quote s ^ "."))

   228     fun get_opt (name, a) (p, t) =

   229       (case name of

   230         "time" => (p, get_time_limit_arg a)

   231       | "atp" => (a, t)

   232       | n => error ("Invalid argument: " ^ n ^ "."))

   233     val {atps, minimize_timeout, ...} = get_params thy override_params

   234     val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout)

   235     val params =

   236       get_params thy

   237           (override_params @

   238            [("atps", [atp]),

   239             ("minimize_timeout",

   240              [string_of_int (Time.toMilliseconds timeout) ^ " ms"])])

   241     val prover =

   242       (case get_prover thy atp of

   243         SOME prover => prover

   244       | NONE => error ("Unknown ATP: " ^ quote atp ^ "."))

   245     val name_thms_pairs = theorems_from_refs ctxt fact_refs

   246   in

   247     priority (#2 (minimize_theorems params prover atp i state name_thms_pairs))

   248   end

   250 val sledgehammerN = "sledgehammer"

   251 val sledgehammer_paramsN = "sledgehammer_params"

   253 val runN = "run"

   254 val minimizeN = "minimize"

   255 val messagesN = "messages"

   256 val available_atpsN = "available_atps"

   257 val running_atpsN = "running_atps"

   258 val kill_atpsN = "kill_atps"

   259 val refresh_tptpN = "refresh_tptp"

   260 val helpN = "help"

   262 fun minimizize_raw_param_name "timeout" = "minimize_timeout"

   263   | minimizize_raw_param_name name = name

   265 val is_raw_param_relevant_for_minimize =

   266   member (op =) params_for_minimize o fst o unalias_raw_param

   267 fun string_for_raw_param (key, values) =

   268   key ^ (case space_implode " " values of

   269            "" => ""

   270          | value => " = " ^ value)

   272 fun minimize_command override_params i atp_name facts =

   273   sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^

   274   (override_params |> filter is_raw_param_relevant_for_minimize

   275                    |> implode o map (prefix ", " o string_for_raw_param)) ^

   276   "] (" ^ space_implode " " facts ^ ")" ^

   277   (if i = 1 then "" else " " ^ string_of_int i)

   279 fun hammer_away override_params subcommand opt_i relevance_override state =

   280   let

   281     val thy = Proof.theory_of state

   282     val _ = List.app check_raw_param override_params

   283   in

   284     if subcommand = runN then

   285       let val i = the_default 1 opt_i in

   286         run (get_params thy override_params) i relevance_override

   287             (minimize_command override_params i) state

   288       end

   289     else if subcommand = minimizeN then

   290       minimize (map (apfst minimizize_raw_param_name) override_params) []

   291                (the_default 1 opt_i) (#add relevance_override) state

   292     else if subcommand = messagesN then

   293       messages opt_i

   294     else if subcommand = available_atpsN then

   295       available_atps thy

   296     else if subcommand = running_atpsN then

   297       running_atps ()

   298     else if subcommand = kill_atpsN then

   299       kill_atps ()

   300     else if subcommand = refresh_tptpN then

   301       refresh_systems_on_tptp ()

   302     else

   303       error ("Unknown subcommand: " ^ quote subcommand ^ ".")

   304   end

   306 fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =

   307   Toplevel.keep (hammer_away params subcommand opt_i relevance_override

   308                  o Toplevel.proof_of)

   310 fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value

   312 fun sledgehammer_params_trans params =

   313   Toplevel.theory

   314       (fold set_default_raw_param params

   315        #> tap (fn thy =>

   316                   writeln ("Default parameters for Sledgehammer:\n" ^

   317                            (case rev (default_raw_params thy) of

   318                               [] => "none"

   319                             | params =>

   320                               (map check_raw_param params;

   321                                params |> map string_for_raw_param

   322                                       |> sort_strings |> cat_lines)))))

   324 val parse_key = Scan.repeat1 P.typ_group >> space_implode " "

   325 val parse_value = Scan.repeat1 P.xname

   326 val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []

   327 val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []

   328 val parse_fact_refs =

   329   Scan.repeat1 (Scan.unless (P.name -- Args.colon)

   330                             (P.xname -- Scan.option Attrib.thm_sel)

   331                 >> (fn (name, interval) =>

   332                        Facts.Named ((name, Position.none), interval)))

   333 val parse_relevance_chunk =

   334   (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)

   335   || (Args.del |-- Args.colon |-- parse_fact_refs

   336       >> del_from_relevance_override)

   337   || (parse_fact_refs >> only_relevance_override)

   338 val parse_relevance_override =

   339   Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk

   340                               >> merge_relevance_overrides))

   341                 (add_to_relevance_override [])

   342 val parse_sledgehammer_command =

   343   (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override

   344    -- Scan.option P.nat) #>> sledgehammer_trans

   345 val parse_sledgehammer_params_command =

   346   parse_params #>> sledgehammer_params_trans

   348 val parse_minimize_args =

   349   Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname)))

   350                 []

   351 val _ =

   352   OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag

   353     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps))

   354 val _ =

   355   OuterSyntax.improper_command "atp_info"

   356     "print information about managed provers" K.diag

   357     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps))

   358 val _ =

   359   OuterSyntax.improper_command "atp_messages"

   360     "print recent messages issued by managed provers" K.diag

   361     (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>

   362       (fn limit => Toplevel.no_timing

   363                    o Toplevel.imperative (fn () => messages limit)))

   364 val _ =

   365   OuterSyntax.improper_command "print_atps" "print external provers" K.diag

   366     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o

   367       Toplevel.keep (available_atps o Toplevel.theory_of)))

   368 val _ =

   369   OuterSyntax.improper_command "atp_minimize"

   370     "minimize theorem list with external prover" K.diag

   371     (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>

   372       Toplevel.no_timing o Toplevel.unknown_proof o

   373         Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of)))

   375 val _ =

   376   OuterSyntax.improper_command sledgehammerN

   377     "search for first-order proof using automatic theorem provers" K.diag

   378     parse_sledgehammer_command

   379 val _ =

   380   OuterSyntax.command sledgehammer_paramsN

   381     "set and display the default parameters for Sledgehammer" K.thy_decl

   382     parse_sledgehammer_params_command

   384 end;

author	blanchet
	Fri, 23 Apr 2010 16:55:51 +0200
changeset 36373	66af0a49de39
parent 36371	8c83ea1a7740
child 36375	2482446a604c
permissions	-rw-r--r--