--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 22 15:23:18 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 23 11:39:21 2010 +0100
@@ -4,43 +4,125 @@
Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
*)
+signature SLEDGEHAMMER_ISAR =
+sig
+ type params = ATP_Manager.params
+
+ val default_params : theory -> (string * string) list -> params
+end;
+
structure Sledgehammer_Isar : sig end =
struct
open ATP_Manager
open ATP_Minimal
+open Sledgehammer_Util
structure K = OuterKeyword and P = OuterParse
-val _ =
- OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
+type raw_param = string * string list
+
+val default_default_params =
+ [("debug", "false"),
+ ("verbose", "false"),
+ ("relevance_threshold", "0.5"),
+ ("higher_order", "smart"),
+ ("respect_no_atp", "true"),
+ ("follow_defs", "false"),
+ ("isar_proof", "false"),
+ ("minimize_timeout", "5 s")]
+
+val negated_params =
+ [("no_debug", "debug"),
+ ("quiet", "verbose"),
+ ("partial_types", "full_types"),
+ ("first_order", "higher_order"),
+ ("ignore_no_atp", "respect_no_atp"),
+ ("dont_follow_defs", "follow_defs"),
+ ("metis_proof", "isar_proof")]
+
+val property_affected_params = ["atps", "full_types", "timeout"]
-val _ =
- OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
+fun is_known_raw_param s =
+ AList.defined (op =) default_default_params s orelse
+ AList.defined (op =) negated_params s orelse
+ member (op =) property_affected_params s
+
+fun check_raw_param (s, _) =
+ if is_known_raw_param s then ()
+ else error ("Unknown parameter: " ^ quote s ^ ".")
-val _ =
- OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
- (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
- (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
+fun unnegate_raw_param (name, value) =
+ case AList.lookup (op =) negated_params name of
+ SOME name' => (name', case value of
+ ["false"] => ["true"]
+ | ["true"] => ["false"]
+ | [] => ["false"]
+ | _ => value)
+ | NONE => (name, value)
+
+structure Data = Theory_Data(
+ type T = raw_param list
+ val empty = default_default_params |> map (apsnd single)
+ val extend = I
+ fun merge p : T = AList.merge (op =) (K true) p)
-val _ =
- OuterSyntax.improper_command "print_atps" "print external provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
- Toplevel.keep (print_provers o Toplevel.theory_of)));
+val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
+fun default_raw_params thy =
+ [("atps", [!atps]),
+ ("full_types", [if !full_types then "true" else "false"]),
+ ("timeout", [string_of_int (!timeout) ^ " s"])] @
+ Data.get thy
+
+val infinity_time_in_secs = 60 * 60 * 24 * 365
+val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
-val _ =
- OuterSyntax.improper_command "sledgehammer"
- "search for first-order proof using automatic theorem provers" K.diag
- (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
+fun extract_params thy default_params override_params =
+ let
+ val override_params = map unnegate_raw_param override_params
+ val raw_params = rev override_params @ rev default_params
+ val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
+ val lookup_string = the_default "" o lookup
+ fun general_lookup_bool option default_value name =
+ case lookup name of
+ SOME s => s |> parse_bool_option option name
+ | NONE => default_value
+ val lookup_bool = the o general_lookup_bool false (SOME false)
+ val lookup_bool_option = general_lookup_bool true NONE
+ fun lookup_time name =
+ the_timeout (case lookup name of
+ NONE => NONE
+ | SOME s => parse_time_option name s)
+ fun lookup_real name =
+ case lookup name of
+ NONE => 0.0
+ | SOME s => 0.0 (* FIXME ### *)
+ val debug = lookup_bool "debug"
+ val verbose = debug orelse lookup_bool "verbose"
+ val atps = lookup_string "atps" |> space_explode " "
+ val full_types = lookup_bool "full_types"
+ val relevance_threshold = lookup_real "relevance_threshold"
+ val higher_order = lookup_bool_option "higher_order"
+ val respect_no_atp = lookup_bool "respect_no_atp"
+ val follow_defs = lookup_bool "follow_defs"
+ val isar_proof = lookup_bool "isar_proof"
+ val timeout = lookup_time "timeout"
+ val minimize_timeout = lookup_time "minimize_timeout"
+ in
+ {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
+ relevance_threshold = relevance_threshold, higher_order = higher_order,
+ respect_no_atp = respect_no_atp, follow_defs = follow_defs,
+ isar_proof = isar_proof, timeout = timeout,
+ minimize_timeout = minimize_timeout}
+ end
-val default_minimize_prover = "remote_vampire"
-val default_minimize_time_limit = 5
+fun default_params thy =
+ extract_params thy (default_raw_params thy) o map (apsnd single)
fun atp_minimize_command args thm_names state =
let
+ val thy = Proof.theory_of state
+ val ctxt = Proof.context_of state
fun theorems_from_names ctxt =
map (fn (name, interval) =>
let
@@ -48,40 +130,104 @@
val ths = ProofContext.get_fact ctxt thmref
val name' = Facts.string_of_ref thmref
in (name', ths) end)
- fun get_time_limit_arg time_string =
- (case Int.fromString time_string of
- SOME t => t
- | NONE => error ("Invalid time limit: " ^ quote time_string))
+ fun get_time_limit_arg s =
+ (case Int.fromString s of
+ SOME t => Time.fromSeconds t
+ | NONE => error ("Invalid time limit: " ^ quote s))
fun get_opt (name, a) (p, t) =
(case name of
"time" => (p, get_time_limit_arg a)
| "atp" => (a, t)
| n => error ("Invalid argument: " ^ n))
- fun get_options args =
- fold get_opt args (default_minimize_prover, default_minimize_time_limit)
- val (prover_name, time_limit) = get_options args
+ val {atps, minimize_timeout, ...} = default_params thy []
+ fun get_options args = fold get_opt args (hd atps, minimize_timeout)
+ val (atp, timeout) = get_options args
+ val params =
+ default_params thy
+ [("atps", atp),
+ ("minimize_timeout", string_of_int (Time.toSeconds timeout) ^ " s")]
val prover =
- (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
+ (case get_prover thy atp of
SOME prover => prover
- | NONE => error ("Unknown prover: " ^ quote prover_name))
- val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
+ | NONE => error ("Unknown ATP: " ^ quote atp))
+ val name_thms_pairs = theorems_from_names ctxt thm_names
in
- writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
- state name_thms_pairs))
+ writeln (#2 (minimize_theorems params linear_minimize prover atp state
+ name_thms_pairs))
end
-local structure K = OuterKeyword and P = OuterParse in
-
val parse_args =
Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
-
val _ =
- OuterSyntax.improper_command "atp_minimize" "minimize theorem list with external prover" K.diag
+ OuterSyntax.improper_command "atp_minimize"
+ "minimize theorem list with external prover" K.diag
(parse_args -- parse_thm_names >> (fn (args, thm_names) =>
Toplevel.no_timing o Toplevel.unknown_proof o
Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
-end
+fun hammer_away override_params i state =
+ let
+ val thy = Proof.theory_of state
+ val _ = List.app check_raw_param override_params
+ val params = extract_params thy (default_raw_params thy) override_params
+ in sledgehammer params i state end
+
+fun sledgehammer_trans (opt_params, opt_i) =
+ Toplevel.keep (hammer_away (these opt_params) (the_default 1 opt_i)
+ o Toplevel.proof_of)
+
+fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
+
+fun sledgehammer_params_trans opt_params =
+ Toplevel.theory
+ (fold set_default_raw_param (these opt_params)
+ #> tap (fn thy =>
+ writeln ("Default parameters for Sledgehammer:\n" ^
+ (case rev (default_raw_params thy) of
+ [] => "none"
+ | params =>
+ (map check_raw_param params;
+ params |> map string_for_raw_param
+ |> sort_strings |> cat_lines)))))
+
+val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+val parse_value =
+ Scan.repeat1 (P.minus >> single
+ || Scan.repeat1 (Scan.unless P.minus P.name)) >> flat
+val parse_param =
+ parse_key -- (Scan.option (P.$$$ "=" |-- parse_value) >> these)
+val parse_params =
+ Scan.option (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]")
+val parse_sledgehammer_command =
+ (parse_params -- Scan.option P.nat) #>> sledgehammer_trans
+val parse_sledgehammer_params_command =
+ parse_params #>> sledgehammer_params_trans
+
+val _ =
+ OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill))
+val _ =
+ OuterSyntax.improper_command "atp_info"
+ "print information about managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info))
+val _ =
+ OuterSyntax.improper_command "atp_messages"
+ "print recent messages issued by managed provers" K.diag
+ (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
+ (fn limit => Toplevel.no_timing
+ o Toplevel.imperative (fn () => messages limit)))
+val _ =
+ OuterSyntax.improper_command "print_atps" "print external provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+ Toplevel.keep (print_provers o Toplevel.theory_of)))
+val _ =
+ OuterSyntax.improper_command "sledgehammer"
+ "search for first-order proof using automatic theorem provers" K.diag
+ parse_sledgehammer_command
+val _ =
+ OuterSyntax.command "sledgehammer_params"
+ "set and display the default parameters for Sledgehammer" K.thy_decl
+ parse_sledgehammer_params_command
end;