diff --git a/src/HOL/Tools/Nitpick/nitpick_commands.ML b/src/HOL/Tools/Nitpick/nitpick_commands.ML --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML @@ -1,382 +1,383 @@ (* Title: HOL/Tools/Nitpick/nitpick_commands.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2008, 2009, 2010 Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer syntax. *) signature NITPICK_COMMANDS = sig type params = Nitpick.params val nitpickN : string val nitpick_paramsN : string val default_params : theory -> (string * string) list -> params end; structure Nitpick_Commands : NITPICK_COMMANDS = struct open Nitpick_Util open Nitpick_HOL open Nitpick_Rep open Nitpick_Nut open Nitpick val nitpickN = "nitpick" val nitpick_paramsN = "nitpick_params" (* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share its time slot with several other automatic tools. *) val auto_try_max_scopes = 6 type raw_param = string * string list val default_default_params = [("card", "1-10"), ("iter", "0,1,2,4,8,12,16,20,24,28"), ("bits", "1-10"), ("bisim_depth", "9"), ("box", "smart"), ("finitize", "smart"), ("mono", "smart"), ("wf", "smart"), ("sat_solver", "smart"), ("batch_size", "smart"), ("falsify", "true"), ("user_axioms", "smart"), ("assms", "true"), ("merge_type_vars", "false"), ("binary_ints", "smart"), ("destroy_constrs", "true"), ("specialize", "true"), ("star_linear_preds", "true"), ("total_consts", "smart"), ("peephole_optim", "true"), ("datatype_sym_break", "5"), ("kodkod_sym_break", "15"), ("timeout", "30"), ("tac_timeout", "0.5"), ("max_threads", "0"), ("debug", "false"), ("verbose", "false"), ("overlord", "false"), ("spy", "false"), ("show_types", "false"), ("show_skolems", "true"), ("show_consts", "false"), ("format", "1"), ("max_potential", "1"), ("max_genuine", "1")] val negated_params = [("dont_box", "box"), ("dont_finitize", "finitize"), ("non_mono", "mono"), ("non_wf", "wf"), ("satisfy", "falsify"), ("no_user_axioms", "user_axioms"), ("no_assms", "assms"), ("dont_merge_type_vars", "merge_type_vars"), ("unary_ints", "binary_ints"), ("dont_destroy_constrs", "destroy_constrs"), ("dont_specialize", "specialize"), ("dont_star_linear_preds", "star_linear_preds"), ("partial_consts", "total_consts"), ("no_peephole_optim", "peephole_optim"), ("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), ("hide_types", "show_types"), ("hide_skolems", "show_skolems"), ("hide_consts", "show_consts")] fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) negated_params s orelse member (op =) ["max", "show_all", "whack", "eval", "need", "atoms", "expect"] s orelse exists (fn p => String.isPrefix (p ^ " ") s) ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize", "mono", "non_mono", "wf", "non_wf", "format", "atoms"] fun check_raw_param (s, _) = if is_known_raw_param s then () else error ("Unknown parameter: " ^ quote s) fun unnegate_param_name name = case AList.lookup (op =) negated_params name of NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name) else if String.isPrefix "non_" name then SOME (unprefix "non_" name) else NONE | some_name => some_name fun normalize_raw_param (name, value) = case unnegate_param_name name of SOME name' => [(name', case value of ["false"] => ["true"] | ["true"] => ["false"] | [] => ["false"] | _ => value)] | NONE => if name = "show_all" then [("show_types", value), ("show_skolems", value), ("show_consts", value)] else [(name, value)] structure Data = Theory_Data ( type T = raw_param list val empty = default_default_params |> map (apsnd single) val extend = I fun merge data = AList.merge (op =) (K true) data ) val set_default_raw_param = Data.map o fold (AList.update (op =)) o normalize_raw_param val default_raw_params = Data.get fun is_punctuation s = (s = "," orelse s = "-") fun stringify_raw_param_value [] = "" | stringify_raw_param_value [s] = s | stringify_raw_param_value (s1 :: s2 :: ss) = s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^ stringify_raw_param_value (s2 :: ss) fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s)) fun extract_params ctxt mode default_params override_params = let val override_params = maps normalize_raw_param override_params val raw_params = rev override_params @ rev default_params val raw_lookup = AList.lookup (op =) raw_params val lookup = Option.map stringify_raw_param_value o raw_lookup val lookup_string = the_default "" o lookup fun general_lookup_bool option default_value name = case lookup name of SOME s => parse_bool_option option name s | NONE => default_value val lookup_bool = the o general_lookup_bool false (SOME false) val lookup_bool_option = general_lookup_bool true NONE fun do_int name value = case value of SOME s => (case Int.fromString s of SOME i => i | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value")) | NONE => 0 fun lookup_int name = do_int name (lookup name) fun lookup_int_option name = case lookup name of SOME "smart" => NONE | value => SOME (do_int name value) fun int_range_from_string name min_int s = let val (k1, k2) = (case space_explode "-" s of [s] => (s, s) | ["", s2] => ("-" ^ s2, "-" ^ s2) | [s1, s2] => (s1, s2) | _ => raise Option.Option) |> apply2 (maxed_int_from_string min_int) in if k1 <= k2 then k1 upto k2 else k1 downto k2 end handle Option.Option => error ("Parameter " ^ quote name ^ " must be assigned a sequence of integers") fun int_seq_from_string name min_int s = maps (int_range_from_string name min_int) (space_explode "," s) fun lookup_int_seq name min_int = case lookup name of SOME s => (case int_seq_from_string name min_int s of [] => [min_int] | value => value) | NONE => [min_int] fun lookup_assigns read prefix default convert = (NONE, convert (the_default default (lookup prefix))) :: map (fn (name, value) => (SOME (read (String.extract (name, size prefix + 1, NONE))), convert (stringify_raw_param_value value))) (filter (String.isPrefix (prefix ^ " ") o fst) raw_params) fun lookup_ints_assigns read prefix min_int = lookup_assigns read prefix (signed_string_of_int min_int) (int_seq_from_string prefix min_int) fun lookup_bool_option_assigns read prefix = lookup_assigns read prefix "" (parse_bool_option true prefix) fun lookup_strings_assigns read prefix = lookup_assigns read prefix "" (space_explode " ") fun lookup_time name = case lookup name of SOME s => parse_time name s | NONE => Time.zeroTime val read_type_polymorphic = Syntax.read_typ ctxt #> Logic.mk_type #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type val read_term_polymorphic = Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt) val lookup_term_list_option_polymorphic = AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic) val read_const_polymorphic = read_term_polymorphic #> dest_Const val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1 |> mode = Auto_Try ? map (apsnd (take auto_try_max_scopes)) val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1 val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0 val bitss = lookup_int_seq "bits" 1 val bisim_depths = lookup_int_seq "bisim_depth" ~1 val boxes = lookup_bool_option_assigns read_type_polymorphic "box" val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize" val monos = if mode = Auto_Try then [(NONE, SOME true)] else lookup_bool_option_assigns read_type_polymorphic "mono" val wfs = lookup_bool_option_assigns read_const_polymorphic "wf" val sat_solver = lookup_string "sat_solver" val falsify = lookup_bool "falsify" val debug = (mode <> Auto_Try andalso lookup_bool "debug") val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val spy = getenv "NITPICK_SPY" = "yes" orelse lookup_bool "spy" val user_axioms = lookup_bool_option "user_axioms" val assms = lookup_bool "assms" val whacks = lookup_term_list_option_polymorphic "whack" |> these val merge_type_vars = lookup_bool "merge_type_vars" val binary_ints = lookup_bool_option "binary_ints" val destroy_constrs = lookup_bool "destroy_constrs" val specialize = lookup_bool "specialize" val star_linear_preds = lookup_bool "star_linear_preds" val total_consts = lookup_bool_option "total_consts" val needs = lookup_term_list_option_polymorphic "need" val peephole_optim = lookup_bool "peephole_optim" val datatype_sym_break = lookup_int "datatype_sym_break" val kodkod_sym_break = lookup_int "kodkod_sym_break" val timeout = lookup_time "timeout" val tac_timeout = lookup_time "tac_timeout" val max_threads = if mode = Normal then Int.max (0, lookup_int "max_threads") else 1 val show_types = debug orelse lookup_bool "show_types" val show_skolems = debug orelse lookup_bool "show_skolems" val show_consts = debug orelse lookup_bool "show_consts" val evals = lookup_term_list_option_polymorphic "eval" |> these val formats = lookup_ints_assigns read_term_polymorphic "format" 0 val atomss = lookup_strings_assigns read_type_polymorphic "atoms" val max_potential = if mode = Normal then Int.max (0, lookup_int "max_potential") else 0 val max_genuine = Int.max (0, lookup_int "max_genuine") val batch_size = case lookup_int_option "batch_size" of SOME n => Int.max (1, n) | NONE => if debug then 1 else 50 val expect = lookup_string "expect" in {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths, boxes = boxes, finitizes = finitizes, monos = monos, wfs = wfs, sat_solver = sat_solver, falsify = falsify, debug = debug, verbose = verbose, overlord = overlord, spy = spy, user_axioms = user_axioms, assms = assms, whacks = whacks, merge_type_vars = merge_type_vars, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, star_linear_preds = star_linear_preds, total_consts = total_consts, needs = needs, peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break, kodkod_sym_break = kodkod_sym_break, timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads, show_types = show_types, show_skolems = show_skolems, show_consts = show_consts, evals = evals, formats = formats, atomss = atomss, max_potential = max_potential, max_genuine = max_genuine, batch_size = batch_size, expect = expect} end fun default_params thy = extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy) o map (apsnd single) val parse_key = Scan.repeat1 Parse.embedded >> space_implode " " val parse_value = Scan.repeats1 (Parse.minus >> single || Scan.repeat1 (Scan.unless Parse.minus (Parse.name || Parse.float_number)) || \<^keyword>\,\ |-- Parse.number >> prefix "," >> single) val parse_param = parse_key -- Scan.optional (\<^keyword>\=\ |-- parse_value) [] val parse_params = Scan.optional (\<^keyword>\[\ |-- Parse.list parse_param --| \<^keyword>\]\) [] fun handle_exceptions ctxt f x = f x handle ARG (loc, details) => error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details) | BAD (loc, details) => error ("Internal error (" ^ quote loc ^ "): " ^ details) | NOT_SUPPORTED details => (warning ("Unsupported case: " ^ details); x) | NUT (loc, us) => error ("Invalid intermediate term" ^ plural_s_for_list us ^ " (" ^ quote loc ^ "): " ^ commas (map (string_for_nut ctxt) us)) | REP (loc, Rs) => error ("Invalid representation" ^ plural_s_for_list Rs ^ " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs)) | TERM (loc, ts) => error ("Invalid term" ^ plural_s_for_list ts ^ " (" ^ quote loc ^ "): " ^ commas (map (Syntax.string_of_term ctxt) ts)) | TYPE (loc, Ts, ts) => error ("Invalid type" ^ plural_s_for_list Ts ^ (if null ts then "" else " for term" ^ plural_s_for_list ts ^ " " ^ commas (map (quote o Syntax.string_of_term ctxt) ts)) ^ " (" ^ quote loc ^ "): " ^ commas (map (Syntax.string_of_typ ctxt) Ts)) fun pick_nits override_params mode i step state = let val thy = Proof.theory_of state val ctxt = Proof.context_of state val _ = List.app check_raw_param override_params val params as {debug, ...} = extract_params ctxt mode (default_raw_params thy) override_params fun go () = (unknownN, []) |> (if mode = Auto_Try then perhaps o try else if debug then fn f => fn x => f x else handle_exceptions ctxt) (fn _ => pick_nits_in_subgoal state params mode i step) in go () end |> `(fn (outcome_code, _) => outcome_code = genuineN) fun string_for_raw_param (name, value) = name ^ " = " ^ stringify_raw_param_value value fun nitpick_params_trans params = Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Nitpick:\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 _ = Outer_Syntax.command \<^command_keyword>\nitpick\ "try to find a counterexample for a given subgoal using Nitpick" (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) => Toplevel.keep_proof (fn state => ignore (pick_nits params Normal i (Toplevel.proof_position_of state) (Toplevel.proof_of state))))) val _ = Outer_Syntax.command \<^command_keyword>\nitpick_params\ "set and display the default parameters for Nitpick" (parse_params #>> nitpick_params_trans) -fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0 - -val _ = Try.tool_setup (nitpickN, (50, \<^system_option>\auto_nitpick\, try_nitpick)) +val _ = + Try.tool_setup + {name = nitpickN, weight = 50, auto_option = \<^system_option>\auto_nitpick\, + body = fn auto => pick_nits [] (if auto then Auto_Try else Try) 1 0} end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML @@ -1,416 +1,417 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_commands.ML Author: Jasmin Blanchette, TU Muenchen Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. *) signature SLEDGEHAMMER_COMMANDS = sig type params = Sledgehammer_Prover.params val provers : string Unsynchronized.ref val default_params : theory -> (string * string) list -> params val parse_params: (string * string) list parser end; structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = struct open ATP_Util open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh open Sledgehammer val cvc4N = "cvc4" val veritN = "verit" val z3N = "z3" val runN = "run" val supported_proversN = "supported_provers" val refresh_tptpN = "refresh_tptp" (** Sledgehammer commands **) fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2} fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override []) (*** parameters ***) val provers = Unsynchronized.ref "" type raw_param = string * string list val default_default_params = [("debug", "false"), ("verbose", "false"), ("overlord", "false"), ("spy", "false"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), ("uncurried_aliases", "smart"), ("learn", "true"), ("fact_filter", "smart"), ("induction_rules", "smart"), ("max_facts", "smart"), ("fact_thresholds", "0.45 0.85"), ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), ("isar_proofs", "smart"), ("compress", "smart"), ("try0", "true"), ("smt_proofs", "true"), ("slice", "true"), ("minimize", "true"), ("preplay_timeout", "1")] val alias_params = [("prover", ("provers", [])), (* undocumented *) ("dont_preplay", ("preplay_timeout", ["0"])), ("dont_compress", ("compress", ["1"])), ("isar_proof", ("isar_proofs", [])) (* legacy *)] val negated_alias_params = [("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), ("no_isar_proofs", "isar_proofs"), ("dont_slice", "slice"), ("dont_minimize", "minimize"), ("dont_try0", "try0"), ("no_smt_proofs", "smt_proofs")] val property_dependent_params = ["provers", "timeout"] fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) alias_params s orelse AList.defined (op =) negated_alias_params s orelse member (op =) property_dependent_params s orelse s = "expect" fun is_prover_list ctxt s = (case space_explode " " s of ss as _ :: _ => forall (is_prover_supported ctxt) ss | _ => false) fun unalias_raw_param (name, value) = (case AList.lookup (op =) alias_params name of SOME (name', []) => (name', value) | SOME (param' as (name', _)) => if value <> ["false"] then param' else error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")") | NONE => (case AList.lookup (op =) negated_alias_params name of SOME name' => (name', (case value of ["false"] => ["true"] | ["true"] => ["false"] | [] => ["false"] | _ => value)) | NONE => (name, value))) val any_type_enc = type_enc_of_string Strict "erased" (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" can be omitted. For the last four, this is a secret feature. *) fun normalize_raw_param ctxt = unalias_raw_param #> (fn (name, value) => if is_known_raw_param name then (name, value) else if null value then if is_prover_list ctxt name then ("provers", [name]) else if can (type_enc_of_string Strict) name then ("type_enc", [name]) else if can (trans_lams_of_string ctxt any_type_enc) name then ("lam_trans", [name]) else if member (op =) fact_filters name then ("fact_filter", [name]) else if is_some (Int.fromString name) then ("max_facts", [name]) else error ("Unknown parameter: " ^ quote name) else error ("Unknown parameter: " ^ quote name)) (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are read correctly. *) val implode_param = strip_spaces_except_between_idents o space_implode " " (* FIXME: use "Generic_Data" *) structure Data = Theory_Data ( type T = raw_param list val empty = default_default_params |> map (apsnd single) val extend = I fun merge data : T = AList.merge (op =) (K true) data ) fun remotify_prover_if_supported_and_not_already_remote ctxt name = if String.isPrefix remote_prefix name then SOME name else let val remote_name = remote_prefix ^ name in if is_prover_supported ctxt remote_name then SOME remote_name else NONE end fun remotify_prover_if_not_installed ctxt name = if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name else remotify_prover_if_supported_and_not_already_remote ctxt name (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value mode ctxt = [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN] \ \see also \<^system_option>\sledgehammer_provers\\ |> map_filter (remotify_prover_if_not_installed ctxt) (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0)) |> implode_param fun set_default_raw_param param thy = let val ctxt = Proof_Context.init_global thy in thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) end fun default_raw_params mode thy = let val ctxt = Proof_Context.init_global thy in Data.get thy |> fold (AList.default (op =)) [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]), ("timeout", let val timeout = Options.default_int \<^system_option>\sledgehammer_timeout\ in [if timeout <= 0 then "none" else string_of_int timeout] end)] end fun extract_params mode default_params override_params = let val raw_params = rev override_params @ rev default_params val lookup = Option.map implode_param 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 => parse_bool_option option name s | NONE => default_value) val lookup_bool = the o general_lookup_bool false (SOME false) fun lookup_time name = (case lookup name of SOME s => parse_time name s | NONE => Time.zeroTime) fun lookup_int name = (case lookup name of NONE => 0 | SOME s => (case Int.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value"))) fun lookup_real name = (case lookup name of NONE => 0.0 | SOME s => (case Real.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value"))) fun lookup_real_pair name = (case lookup name of NONE => (0.0, 0.0) | SOME s => (case s |> space_explode " " |> map Real.fromString of [SOME r1, SOME r2] => (r1, r2) | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ \values (e.g., \"0.6 0.95\")"))) fun lookup_option lookup' name = (case lookup name of SOME "smart" => NONE | _ => SOME (lookup' name)) val debug = mode <> Auto_Try andalso lookup_bool "debug" val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd val type_enc = if mode = Auto_Try then NONE else (case lookup_string "type_enc" of "smart" => NONE | s => (type_enc_of_string Strict s; SOME s)) val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" val learn = lookup_bool "learn" val fact_filter = lookup_option lookup_string "fact_filter" |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf) val induction_rules = lookup_option (the o induction_rules_of_string o lookup_string) "induction_rules" val max_facts = lookup_option lookup_int "max_facts" val fact_thresholds = lookup_real_pair "fact_thresholds" val max_mono_iters = lookup_option lookup_int "max_mono_iters" val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" val isar_proofs = lookup_option lookup_bool "isar_proofs" val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") val try0 = lookup_bool "try0" val smt_proofs = lookup_bool "smt_proofs" val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = lookup_bool "minimize" val timeout = lookup_time "timeout" val preplay_timeout = lookup_time "preplay_timeout" val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params mode = extract_params mode o default_raw_params mode fun default_params thy = get_params Normal thy o map (apsnd single) val silence_state = Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) (* Sledgehammer the given subgoal *) val default_learn_prover_timeout = 2.0 fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 = let (* We generally want chained facts to be picked up by the relevance filter, because it can then give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs, verbose output, machine learning). However, if the fact is available by no other means (not even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice but to insert it into the state as an additional hypothesis. *) val {facts = chained0, ...} = Proof.goal state0 val (inserts, keep_chained) = if null chained0 orelse #only fact_override then (chained0, []) else let val ctxt0 = Proof.context_of state0 in List.partition (is_useful_unnamed_local_fact ctxt0) chained0 end val state = state0 |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained) |> silence_state val thy = Proof.theory_of state val ctxt = Proof.context_of state val override_params = override_params |> map (normalize_raw_param ctxt) in if subcommand = runN then let val i = the_default 1 opt_i in ignore (run_sledgehammer (get_params Normal thy override_params) Normal writeln_result i fact_override state) end else if subcommand = supported_proversN then supported_provers ctxt else if subcommand = unlearnN then mash_unlearn ctxt else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse subcommand = relearn_isarN orelse subcommand = relearn_proverN then (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt else (); mash_learn ctxt (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) (get_params Normal thy ([("timeout", [string_of_real default_learn_prover_timeout]), ("slice", ["false"])] @ override_params @ [("preplay_timeout", ["0"])])) fact_override (#facts (Proof.goal state)) (subcommand = learn_proverN orelse subcommand = relearn_proverN)) else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else error ("Unknown subcommand: " ^ quote subcommand) end fun string_of_raw_param (key, values) = key ^ (case implode_param values of "" => "" | value => " = " ^ value) val parse_query_bang = \<^keyword>\?\ || \<^keyword>\!\ || \<^keyword>\!!\ val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang) val parse_param = parse_key -- Scan.optional (\<^keyword>\=\ |-- parse_value) [] val parse_raw_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] val parse_params = parse_raw_params >> map (apsnd implode_param) val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_fact_override_chunk = (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) || (parse_fact_refs >> only_fact_override) val parse_fact_override = Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) no_fact_override val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer\ "search for first-order proof using automatic theorem provers" (Scan.optional Parse.name runN -- parse_raw_params -- parse_fact_override -- Scan.option Parse.nat >> (fn (((subcommand, params), fact_override), opt_i) => Toplevel.keep_proof (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of))) val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer_params\ "set and display the default parameters for Sledgehammer" (parse_raw_params >> (fn params => Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Sledgehammer:\n" ^ (case rev (default_raw_params Normal thy) of [] => "none" | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))))) -fun try_sledgehammer auto state = - let - val thy = Proof.theory_of state - val mode = if auto then Auto_Try else Try - val i = 1 - in - run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) - end - -val _ = Try.tool_setup (sledgehammerN, (40, \<^system_option>\auto_sledgehammer\, try_sledgehammer)) +val _ = + Try.tool_setup + {name = sledgehammerN, weight = 40, auto_option = \<^system_option>\auto_sledgehammer\, + body = fn auto => fn state => + let + val thy = Proof.theory_of state + val mode = if auto then Auto_Try else Try + val i = 1 + in + run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) + end} val _ = Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, writeln_result, ...} => (case try Toplevel.proof_of st of SOME state => let val [provers_arg, isar_proofs_arg, try0_arg] = args val override_params = ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), ("try0", [try0_arg]), ("debug", ["false"]), ("verbose", ["false"]), ("overlord", ["false"])]); in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end | NONE => error "Unknown proof context")) end; diff --git a/src/HOL/Tools/try0.ML b/src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML +++ b/src/HOL/Tools/try0.ML @@ -1,198 +1,196 @@ (* Title: HOL/Tools/try0.ML Author: Jasmin Blanchette, TU Muenchen Try a combination of proof methods. *) signature TRY0 = sig - val try0N : string val noneN : string - val silence_methods : bool -> Proof.context -> Proof.context val try0 : Time.time option -> string list * string list * string list * string list -> Proof.state -> bool end; structure Try0 : TRY0 = struct -val try0N = "try0"; val noneN = "none"; datatype mode = Auto_Try | Try | Normal; val default_timeout = seconds 5.0; fun can_apply timeout_opt pre post tac st = let val {goal, ...} = Proof.goal st in (case (case timeout_opt of SOME timeout => Timeout.apply timeout | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of SOME (x, _) => Thm.nprems_of (post x) < Thm.nprems_of goal | NONE => false) end; fun apply_generic timeout_opt name command pre post apply st = let val time_start = Time.now () in if try (can_apply timeout_opt pre post apply) st = SOME true then SOME (name, command, Time.toMilliseconds (Time.now () - time_start)) else NONE end; fun parse_method keywords s = enclose "(" ")" s |> Token.explode keywords Position.start |> filter Token.is_proper |> Scan.read Token.stopper Method.parse |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source"); fun apply_named_method_on_first_goal ctxt = parse_method (Thy_Header.get_keywords' ctxt) #> Method.method_cmd ctxt #> Method.Basic #> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) #> Proof.refine; fun add_attr_text (NONE, _) s = s | add_attr_text (_, []) s = s | add_attr_text (SOME x, fs) s = s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs; fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) = "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]; fun apply_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode timeout_opt quad st = if mode <> Auto_Try orelse run_if_auto_try then let val attrs = attrs_text attrs quad in apply_generic timeout_opt name ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ (if all_goals andalso Thm.nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else "")) I (#goal o Proof.goal) (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs) #> Seq.filter_results) st end else NONE; val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest"); val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest"); val simp_attrs = (SOME "add", NONE, NONE, NONE); val metis_attrs = (SOME "", SOME "", SOME "", SOME ""); val no_attrs = (NONE, NONE, NONE, NONE); (* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *) val named_methods = [("simp", ((false, true), simp_attrs)), ("auto", ((true, true), full_attrs)), ("blast", ((false, true), clas_attrs)), ("metis", ((false, true), metis_attrs)), ("argo", ((false, true), no_attrs)), ("linarith", ((false, true), no_attrs)), ("presburger", ((false, true), no_attrs)), ("algebra", ((false, true), no_attrs)), ("fast", ((false, false), clas_attrs)), ("fastforce", ((false, false), full_attrs)), ("force", ((false, false), full_attrs)), ("meson", ((false, false), metis_attrs)), ("satx", ((false, false), no_attrs))]; val apply_methods = map apply_named_method named_methods; fun time_string ms = string_of_int ms ^ " ms"; fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms; (* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification bound exceeded" warnings and the like. *) fun silence_methods debug = Config.put Metis_Tactic.verbose debug #> not debug ? (fn ctxt => ctxt |> Simplifier_Trace.disable |> Context_Position.set_visible false |> Config.put Unify.trace_bound (Config.get ctxt Unify.search_bound) |> Config.put Argo_Tactic.trace "none" |> Proof_Context.background_theory (fn thy => thy |> Context_Position.set_visible_global false |> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound))); fun generic_try0 mode timeout_opt quad st = let val st = Proof.map_contexts (silence_methods false) st; fun trd (_, _, t) = t; fun try_method method = method mode timeout_opt quad st; fun get_message (_, command, ms) = "Found proof: " ^ Active.sendback_markup_command ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ " " ^ command) ^ " (" ^ time_string ms ^ ")"; val print_step = Option.map (tap (writeln o get_message)); val get_results = if mode = Normal then Par_List.map (try_method #> print_step) #> map_filter I #> sort (int_ord o apply2 trd) else Par_List.get_some try_method #> the_list; in if mode = Normal then "Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^ "..." |> writeln else (); (case get_results apply_methods of [] => (if mode = Normal then writeln "No proof found" else (); (false, (noneN, []))) | xs as (name, command, _) :: _ => let val xs = xs |> map (fn (name, _, n) => (n, name)) |> AList.coalesce (op =) |> map (swap o apsnd commas); val message = (case mode of Auto_Try => "Auto Try0 found a proof" | Try => "Try0 found a proof" | Normal => "Try this") ^ ": " ^ Active.sendback_markup_command ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ " " ^ command) ^ (case xs of [(_, ms)] => " (" ^ time_string ms ^ ")" | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ")"); in (true, (name, if mode = Auto_Try then [message] else (writeln message; []))) end) end; fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt; fun try0_trans quad = Toplevel.keep_proof (ignore o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of); fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2); fun string_of_xthm (xref, args) = Facts.string_of_ref xref ^ implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args); val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.thm >> string_of_xthm)); val parse_attr = Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn ss => (ss, [], [], [])) || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (fn is => ([], is, [], [])) || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (fn es => ([], [], es, [])) || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (fn ds => ([], [], [], ds)); fun parse_attrs x = (Args.parens parse_attrs || Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x; val _ = Outer_Syntax.command \<^command_keyword>\try0\ "try a combination of proof methods" (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans); -fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []); - -val _ = Try.tool_setup (try0N, (30, \<^system_option>\auto_methods\, try_try0)); +val _ = + Try.tool_setup + {name = "try0", weight = 30, auto_option = \<^system_option>\auto_methods\, + body = fn auto => generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])}; end; diff --git a/src/Tools/quickcheck.ML b/src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML +++ b/src/Tools/quickcheck.ML @@ -1,569 +1,569 @@ (* Title: Tools/quickcheck.ML Author: Stefan Berghofer, Florian Haftmann, Lukas Bulwahn, TU Muenchen Generic counterexample search engine. *) signature QUICKCHECK = sig val quickcheckN: string val genuineN: string val noneN: string val unknownN: string (*configuration*) val batch_tester : string Config.T val size : int Config.T val iterations : int Config.T val depth : int Config.T val no_assms : bool Config.T val report : bool Config.T val timeout : real Config.T val timing : bool Config.T val genuine_only : bool Config.T val abort_potential : bool Config.T val quiet : bool Config.T val verbose : bool Config.T val use_subtype : bool Config.T val allow_function_inversion : bool Config.T val finite_types : bool Config.T val finite_type_size : int Config.T val tag : string Config.T val locale : string Config.T val set_active_testers: string list -> Context.generic -> Context.generic datatype expectation = No_Expectation | No_Counterexample | Counterexample; datatype test_params = Test_Params of {default_type: typ list, expect : expectation}; val test_params_of : Proof.context -> test_params val map_test_params : (typ list * expectation -> typ list * expectation) -> Context.generic -> Context.generic val default_type : Proof.context -> typ list datatype report = Report of { iterations : int, raised_match_errors : int, satisfied_assms : int list, positive_concl_tests : int } (*quickcheck's result*) datatype result = Result of {counterexample : (bool * (string * term) list) option, evaluation_terms : (term * term) list option, timings : (string * int) list, reports : (int * report) list} val empty_result : result val found_counterexample : result -> bool val add_timing : (string * int) -> result Unsynchronized.ref -> unit val add_response : string list -> term list -> (bool * term list) option -> result Unsynchronized.ref -> unit val add_report : int -> report option -> result Unsynchronized.ref -> unit val counterexample_of : result -> (bool * (string * term) list) option val timings_of : result -> (string * int) list (*registering testers & generators*) type tester = Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list val add_tester : string * (bool Config.T * tester) -> Context.generic -> Context.generic val add_batch_generator : string * (Proof.context -> term list -> (int -> term list option) list) -> Context.generic -> Context.generic val add_batch_validator : string * (Proof.context -> term list -> (int -> bool) list) -> Context.generic -> Context.generic (*basic operations*) val message : Proof.context -> string -> unit val verbose_message : Proof.context -> string -> unit val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a val pretty_counterex : Proof.context -> bool -> ((bool * (string * term) list) * (term * term) list) option -> Pretty.T (*testing terms and proof states*) val mk_batch_validator : Proof.context -> term list -> (int -> bool) list option val mk_batch_tester : Proof.context -> term list -> (int -> term list option) list option val active_testers : Proof.context -> tester list val test_terms : Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option val quickcheck: (string * string list) list -> int -> Proof.state -> (bool * (string * term) list) option end; structure Quickcheck : QUICKCHECK = struct val quickcheckN = "quickcheck"; val genuineN = "genuine"; val noneN = "none"; val unknownN = "unknown"; (* quickcheck report *) datatype report = Report of {iterations : int, raised_match_errors : int, satisfied_assms : int list, positive_concl_tests : int}; (* Quickcheck Result *) datatype result = Result of {counterexample : (bool * (string * term) list) option, evaluation_terms : (term * term) list option, timings : (string * int) list, reports : (int * report) list}; val empty_result = Result {counterexample = NONE, evaluation_terms = NONE, timings = [], reports = []}; fun counterexample_of (Result r) = #counterexample r; fun found_counterexample (Result r) = is_some (#counterexample r); fun response_of (Result r) = (case (#counterexample r, #evaluation_terms r) of (SOME ts, SOME evals) => SOME (ts, evals) | (NONE, NONE) => NONE); fun timings_of (Result r) = #timings r; fun set_response names eval_terms (SOME (genuine, ts)) (Result r) = let val (ts1, ts2) = chop (length names) ts val (eval_terms', _) = chop (length ts2) eval_terms in Result {counterexample = SOME (genuine, (names ~~ ts1)), evaluation_terms = SOME (eval_terms' ~~ ts2), timings = #timings r, reports = #reports r} end | set_response _ _ NONE result = result; fun cons_timing timing (Result r) = Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r, timings = cons timing (#timings r), reports = #reports r}; fun cons_report size (SOME report) (Result r) = Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r, timings = #timings r, reports = cons (size, report) (#reports r)} | cons_report _ NONE result = result; fun add_timing timing result_ref = Unsynchronized.change result_ref (cons_timing timing); fun add_report size report result_ref = Unsynchronized.change result_ref (cons_report size report); fun add_response names eval_terms response result_ref = Unsynchronized.change result_ref (set_response names eval_terms response); (* expectation *) datatype expectation = No_Expectation | No_Counterexample | Counterexample; fun merge_expectation (expect1, expect2) = if expect1 = expect2 then expect1 else No_Expectation; (*quickcheck configuration -- default parameters, test generators*) val batch_tester = Attrib.setup_config_string \<^binding>\quickcheck_batch_tester\ (K ""); val size = Attrib.setup_config_int \<^binding>\quickcheck_size\ (K 10); val iterations = Attrib.setup_config_int \<^binding>\quickcheck_iterations\ (K 100); val depth = Attrib.setup_config_int \<^binding>\quickcheck_depth\ (K 10); val no_assms = Attrib.setup_config_bool \<^binding>\quickcheck_no_assms\ (K false); val locale = Attrib.setup_config_string \<^binding>\quickcheck_locale\ (K "interpret expand"); val report = Attrib.setup_config_bool \<^binding>\quickcheck_report\ (K true); val timing = Attrib.setup_config_bool \<^binding>\quickcheck_timing\ (K false); val timeout = Attrib.setup_config_real \<^binding>\quickcheck_timeout\ (K 30.0); val genuine_only = Attrib.setup_config_bool \<^binding>\quickcheck_genuine_only\ (K false); val abort_potential = Attrib.setup_config_bool \<^binding>\quickcheck_abort_potential\ (K false); val quiet = Attrib.setup_config_bool \<^binding>\quickcheck_quiet\ (K false); val verbose = Attrib.setup_config_bool \<^binding>\quickcheck_verbose\ (K false); val tag = Attrib.setup_config_string \<^binding>\quickcheck_tag\ (K ""); val use_subtype = Attrib.setup_config_bool \<^binding>\quickcheck_use_subtype\ (K false); val allow_function_inversion = Attrib.setup_config_bool \<^binding>\quickcheck_allow_function_inversion\ (K false); val finite_types = Attrib.setup_config_bool \<^binding>\quickcheck_finite_types\ (K true); val finite_type_size = Attrib.setup_config_int \<^binding>\quickcheck_finite_type_size\ (K 3); datatype test_params = Test_Params of {default_type: typ list, expect : expectation}; fun dest_test_params (Test_Params {default_type, expect}) = (default_type, expect); fun make_test_params (default_type, expect) = Test_Params {default_type = default_type, expect = expect}; fun map_test_params' f (Test_Params {default_type, expect}) = make_test_params (f (default_type, expect)); fun merge_test_params (Test_Params {default_type = default_type1, expect = expect1}, Test_Params {default_type = default_type2, expect = expect2}) = make_test_params (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2)); type tester = Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list; structure Data = Generic_Data ( type T = (string * (bool Config.T * tester)) list * (string * (Proof.context -> term list -> (int -> term list option) list)) list * (string * (Proof.context -> term list -> (int -> bool) list)) list * test_params; val empty = ([], [], [], Test_Params {default_type = [], expect = No_Expectation}); val extend = I; fun merge ((testers1, batch_generators1, batch_validators1, params1), (testers2, batch_generators2, batch_validators2, params2)) : T = (AList.merge (op =) (K true) (testers1, testers2), AList.merge (op =) (K true) (batch_generators1, batch_generators2), AList.merge (op =) (K true) (batch_validators1, batch_validators2), merge_test_params (params1, params2)); ); val test_params_of = #4 o Data.get o Context.Proof; val default_type = fst o dest_test_params o test_params_of; val expect = snd o dest_test_params o test_params_of; val map_test_params = Data.map o @{apply 4(4)} o map_test_params'; val add_tester = Data.map o @{apply 4(1)} o AList.update (op =); val add_batch_generator = Data.map o @{apply 4(2)} o AList.update (op =); val add_batch_validator = Data.map o @{apply 4(3)} o AList.update (op =); fun active_testers ctxt = let val testers = map snd (#1 (Data.get (Context.Proof ctxt))); in map snd (filter (fn (active, _) => Config.get ctxt active) testers) end; fun set_active_testers [] context = context | set_active_testers testers context = let val registered_testers = #1 (Data.get context); in fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name)) registered_testers context end; (* generating tests *) fun gen_mk_tester lookup ctxt v = let val name = Config.get ctxt batch_tester val tester = (case lookup ctxt name of NONE => error ("No such quickcheck batch-tester: " ^ name) | SOME tester => tester ctxt); in if Config.get ctxt quiet then try tester v else let (* FIXME !?!? *) val tester = Exn.interruptible_capture tester v in (case Exn.get_res tester of NONE => SOME (Exn.release tester) | SOME tester => SOME tester) end end; val mk_batch_tester = gen_mk_tester (AList.lookup (op =) o #2 o Data.get o Context.Proof); val mk_batch_validator = gen_mk_tester (AList.lookup (op =) o #3 o Data.get o Context.Proof); (* testing propositions *) type compile_generator = Proof.context -> (term * term list) list -> int list -> term list option * report option; fun limit timeout (limit_time, is_interactive) f exc () = if limit_time then Timeout.apply timeout f () handle timeout_exn as Timeout.TIMEOUT _ => if is_interactive then exc () else Exn.reraise timeout_exn else f (); fun message ctxt s = if Config.get ctxt quiet then () else writeln s; fun verbose_message ctxt s = if not (Config.get ctxt quiet) andalso Config.get ctxt verbose then writeln s else (); fun test_terms ctxt0 (limit_time, is_interactive) insts goals = let val ctxt = Simplifier_Trace.disable ctxt0 in (case active_testers ctxt of [] => error "No active testers for quickcheck" | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () => Par_List.get_some (fn tester => tester ctxt (length testers > 1) insts goals |> (fn result => if exists found_counterexample result then SOME result else NONE)) testers) (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ()) end fun all_axioms_of ctxt t = let val intros = Locale.get_intros ctxt; val unfolds = Locale.get_unfolds ctxt; fun retrieve_prems thms t = (case filter (fn th => Term.could_unify (Thm.concl_of th, t)) thms of [] => NONE | [th] => let val (tyenv, tenv) = Pattern.match (Proof_Context.theory_of ctxt) (Thm.concl_of th, t) (Vartab.empty, Vartab.empty) in SOME (map (Envir.subst_term (tyenv, tenv)) (Thm.prems_of th)) end); fun all t = (case retrieve_prems intros t of NONE => retrieve_prems unfolds t | SOME ts => SOME (maps (fn t => the_default [t] (all t)) ts)); in all t end; fun locale_config_of s = let val cs = space_explode " " s; in if forall (fn c => c = "expand" orelse c = "interpret") cs then cs else (warning ("Invalid quickcheck_locale setting: falling back to the default setting."); ["interpret", "expand"]) end; fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state = let val ctxt = Proof.context_of state; val thy = Proof.theory_of state; val opt_locale = Named_Target.bottom_locale_of ctxt; fun axioms_of locale = (case fst (Locale.specification_of thy locale) of NONE => [] | SOME t => the_default [] (all_axioms_of ctxt t)); val config = locale_config_of (Config.get ctxt locale); val assms = if Config.get ctxt no_assms then [] else (case opt_locale of NONE => Assumption.all_assms_of ctxt | SOME locale => Assumption.local_assms_of ctxt (Locale.init locale thy)); val {goal = st, ...} = Proof.raw_goal state; val (gi, _) = Logic.goal_params (Thm.prop_of st) i; val ((_, raw_goal), ctxt') = Variable.focus NONE gi ctxt; val proto_goal = Logic.list_implies (map Thm.term_of assms, raw_goal); val goals = (case opt_locale of NONE => [(proto_goal, eval_terms)] | SOME locale => fold (fn c => if c = "expand" then cons (Logic.list_implies (axioms_of locale, proto_goal), eval_terms) else if c = "interpret" then append (map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms)) (Locale.registrations_of (Context.Theory thy) (* FIXME !? *) locale)) else I) config []); val _ = verbose_message ctxt' (Pretty.string_of (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term ctxt' o fst) goals))); in test_terms ctxt' (time_limit, is_interactive) insts goals end; (* pretty printing *) fun tool_name auto = if auto then "Auto Quickcheck" else "Quickcheck"; fun pretty_counterex ctxt auto NONE = Pretty.para (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag) | pretty_counterex ctxt auto (SOME ((genuine, cex), eval_terms)) = let val header = Pretty.para (tool_name auto ^ " found a " ^ (if genuine then "counterexample" else "potentially spurious counterexample due to underspecified functions") ^ (if null cex then "." else ":") ^ Config.get ctxt tag); fun pretty_cex (x, t) = Pretty.block [Pretty.str (x ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]; in Pretty.chunks (Pretty.block (Pretty.fbreaks (header :: map pretty_cex (rev cex))) :: (if null eval_terms then [] else [Pretty.big_list "Evaluated terms:" (map (fn (t, u) => Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u]) (rev eval_terms))])) end; (* Isar commands *) fun read_nat s = (case Library.read_int (Symbol.explode s) of (k, []) => if k >= 0 then k else error ("Not a natural number: " ^ s) | _ => error ("Not a natural number: " ^ s)); fun read_bool "false" = false | read_bool "true" = true | read_bool s = error ("Not a Boolean value: " ^ s); fun read_real s = (case Real.fromString s of SOME s => s | NONE => error ("Not a real number: " ^ s)); fun read_expectation "no_expectation" = No_Expectation | read_expectation "no_counterexample" = No_Counterexample | read_expectation "counterexample" = Counterexample | read_expectation s = error ("Not an expectation value: " ^ s); fun valid_tester_name context name = AList.defined (op =) (#1 (Data.get context)) name; fun parse_tester name (testers, context) = if valid_tester_name context name then (insert (op =) name testers, context) else error ("Unknown tester: " ^ name); fun parse_test_param ("tester", args) = fold parse_tester args | parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg)) | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg)) | parse_test_param ("depth", [arg]) = apsnd (Config.put_generic depth (read_nat arg)) | parse_test_param ("default_type", arg) = (fn (testers, context) => (testers, map_test_params (apfst (K (map (Proof_Context.read_typ (Context.proof_of context)) arg))) context)) | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg)) | parse_test_param ("expect", [arg]) = apsnd (map_test_params (apsnd (K (read_expectation arg)))) | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg)) | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg)) | parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg)) | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg)) | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg)) | parse_test_param ("tag", [arg]) = apsnd (Config.put_generic tag arg) | parse_test_param ("use_subtype", [arg]) = apsnd (Config.put_generic use_subtype (read_bool arg)) | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg)) | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg)) | parse_test_param ("allow_function_inversion", [arg]) = apsnd (Config.put_generic allow_function_inversion (read_bool arg)) | parse_test_param ("finite_type_size", [arg]) = apsnd (Config.put_generic finite_type_size (read_nat arg)) | parse_test_param (name, _) = (fn (testers, context) => if valid_tester_name context name then (insert (op =) name testers, context) else error ("Unknown tester or test parameter: " ^ name)); fun parse_test_param_inst (name, arg) ((insts, eval_terms), (testers, ctxt)) = (case try (Proof_Context.read_typ ctxt) name of SOME (TFree (v, _)) => ((AList.update (op =) (v, Proof_Context.read_typ ctxt (the_single arg)) insts, eval_terms), (testers, ctxt)) | NONE => (case name of "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), (testers, ctxt)) | _ => ((insts, eval_terms), let val (testers', Context.Proof ctxt') = parse_test_param (name, arg) (testers, Context.Proof ctxt); in (testers', ctxt') end))); fun quickcheck_params_cmd args = Context.theory_map (fn context => uncurry set_active_testers (fold parse_test_param args ([], context))); fun check_expectation state results = if is_some results andalso expect (Proof.context_of state) = No_Counterexample then error "quickcheck expected to find no counterexample but found one" else if is_none results andalso expect (Proof.context_of state) = Counterexample then error "quickcheck expected to find a counterexample but did not find one" else (); fun gen_quickcheck args i state = state |> Proof.map_context_result (fn ctxt => apsnd (fn (testers, ctxt) => Context.proof_map (set_active_testers testers) ctxt) (fold parse_test_param_inst args (([], []), ([], ctxt)))) |> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) i state' |> tap (check_expectation state') |> rpair state'); fun quickcheck args i state = Option.map (the o get_first counterexample_of) (fst (gen_quickcheck args i state)); fun quickcheck_cmd args i st = gen_quickcheck args i (Toplevel.proof_of st) |> apfst (Option.map (the o get_first response_of)) |> (fn (r, state) => writeln (Pretty.string_of (pretty_counterex (Proof.context_of state) false r))); val parse_arg = Parse.name -- (Scan.optional (\<^keyword>\=\ |-- (((Parse.name || Parse.float_number) >> single) || (\<^keyword>\[\ |-- Parse.list1 Parse.name --| \<^keyword>\]\))) ["true"]); val parse_args = \<^keyword>\[\ |-- Parse.list1 parse_arg --| \<^keyword>\]\ || Scan.succeed []; val _ = Outer_Syntax.command \<^command_keyword>\quickcheck_params\ "set parameters for random testing" (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args))); val _ = Outer_Syntax.command \<^command_keyword>\quickcheck\ "try to find counterexample for subgoal" (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) => Toplevel.keep_proof (quickcheck_cmd args i))); -(* automatic testing *) +(* 'try' setup *) -fun try_quickcheck auto state = - let - val ctxt = Proof.context_of state; - val i = 1; - val res = - state - |> Proof.map_context (Config.put report false #> Config.put quiet true) - |> try (test_goal (false, false) ([], []) i); - in - (case res of - NONE => (unknownN, []) - | SOME results => - let - val msg = - Pretty.string_of - (pretty_counterex ctxt auto (Option.map (the o get_first response_of) results)) - in - if is_some results then (genuineN, if auto then [msg] else (writeln msg; [])) - else (noneN, []) - end) - end - |> `(fn (outcome_code, _) => outcome_code = genuineN); - -val _ = Try.tool_setup (quickcheckN, (20, \<^system_option>\auto_quickcheck\, try_quickcheck)); +val _ = + Try.tool_setup + {name = quickcheckN, weight = 20, auto_option = \<^system_option>\auto_quickcheck\, + body = fn auto => fn state => + let + val ctxt = Proof.context_of state; + val i = 1; + val res = + state + |> Proof.map_context (Config.put report false #> Config.put quiet true) + |> try (test_goal (false, false) ([], []) i); + in + (case res of + NONE => (unknownN, []) + | SOME results => + let + val msg = + Pretty.string_of + (pretty_counterex ctxt auto (Option.map (the o get_first response_of) results)) + in + if is_some results then (genuineN, if auto then [msg] else (writeln msg; [])) + else (noneN, []) + end) + end + |> `(fn (outcome_code, _) => outcome_code = genuineN)}; end; - diff --git a/src/Tools/solve_direct.ML b/src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML +++ b/src/Tools/solve_direct.ML @@ -1,105 +1,105 @@ (* Title: Tools/solve_direct.ML Author: Timothy Bourke and Gerwin Klein, NICTA Check whether a newly stated theorem can be solved directly by an existing theorem. Duplicate lemmas can be detected in this way. The implementation relies critically on the Find_Theorems solves feature. *) signature SOLVE_DIRECT = sig val solve_directN: string val someN: string val noneN: string val unknownN: string val max_solutions: int Config.T val strict_warnings: bool Config.T val solve_direct: Proof.state -> bool * (string * string list) end; structure Solve_Direct: SOLVE_DIRECT = struct datatype mode = Auto_Try | Try | Normal val solve_directN = "solve_direct"; val someN = "some"; val noneN = "none"; val unknownN = "none"; (* preferences *) val max_solutions = Attrib.setup_config_int \<^binding>\solve_direct_max_solutions\ (K 5); val strict_warnings = Attrib.setup_config_bool \<^binding>\solve_direct_strict_warnings\ (K false); (* solve_direct command *) fun do_solve_direct mode state = let val ctxt = Proof.context_of state; fun find goal = #2 (Find_Theorems.find_theorems ctxt (SOME goal) (SOME (Config.get ctxt max_solutions)) false [(true, Find_Theorems.Solves)]); fun prt_result (subgoal, results) = Pretty.big_list ((if mode = Auto_Try then "Auto " else "") ^ solve_directN ^ ": " ^ (case subgoal of NONE => "the current goal" | SOME i => "subgoal #" ^ string_of_int i) ^ " can be solved directly with") (map (Find_Theorems.pretty_thm ctxt) results); fun seek_against_goal () = (case try (#goal o Proof.simple_goal) state of NONE => NONE | SOME goal => let val subgoals = Drule.strip_imp_prems (Thm.cprop_of goal); val rs = if length subgoals = 1 then [(NONE, find goal)] else map_index (fn (i, sg) => (SOME (i + 1), find (Goal.init sg))) subgoals; val results = filter_out (null o #2) rs; in if null results then NONE else SOME results end); in (case try seek_against_goal () of SOME (SOME results) => (someN, let val chunks = separate (Pretty.str "") (map prt_result results); val msg = Pretty.string_of (Pretty.chunks chunks); in if Config.get ctxt strict_warnings then (warning msg; []) else if mode = Auto_Try then [msg] else (writeln msg; []) end) | SOME NONE => (if mode = Normal then writeln "No proof found" else (); (noneN, [])) | NONE => (if mode = Normal then writeln "An error occurred" else (); (unknownN, []))) end |> `(fn (outcome_code, _) => outcome_code = someN); val solve_direct = do_solve_direct Normal val _ = Outer_Syntax.command \<^command_keyword>\solve_direct\ "try to solve conjectures directly with existing theorems" (Scan.succeed (Toplevel.keep_proof (ignore o solve_direct o Toplevel.proof_of))); -(* hook *) - -fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try) +(* 'try' setup *) val _ = - Try.tool_setup (solve_directN, (10, \<^system_option>\auto_solve_direct\, try_solve_direct)); + Try.tool_setup + {name = solve_directN, weight = 10, auto_option = \<^system_option>\auto_solve_direct\, + body = fn auto => do_solve_direct (if auto then Auto_Try else Try)}; end; diff --git a/src/Tools/try.ML b/src/Tools/try.ML --- a/src/Tools/try.ML +++ b/src/Tools/try.ML @@ -1,112 +1,108 @@ (* Title: Tools/try.ML Author: Jasmin Blanchette, TU Muenchen Author: Makarius Manager for tools that should be tried on conjectures. *) signature TRY = sig - type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list))) - - val tryN: string - val serial_commas: string -> string list -> string list val subgoal_count: Proof.state -> int + type body = bool -> Proof.state -> bool * (string * string list) + type tool = {name: string, weight: int, auto_option: string, body: body} val get_tools: theory -> tool list val try_tools: Proof.state -> (string * string) option val tool_setup: tool -> unit end; structure Try : TRY = struct -type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list))); - -val tryN = "try"; - - (* helpers *) fun serial_commas _ [] = ["??"] | serial_commas _ [s] = [s] | serial_commas conj [s1, s2] = [s1, conj, s2] | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss; val subgoal_count = Logic.count_prems o Thm.prop_of o #goal o Proof.goal; (* configuration *) -fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) = - prod_ord int_ord string_ord ((weight1, name1), (weight2, name2)); +type body = bool -> Proof.state -> bool * (string * string list); +type tool = {name: string, weight: int, auto_option: string, body: body}; + +fun tool_ord (tool1: tool, tool2: tool) = + prod_ord int_ord string_ord ((#weight tool1, #name tool1), (#weight tool2, #name tool2)); structure Data = Theory_Data ( type T = tool list; val empty = []; val extend = I; fun merge data : T = Ord_List.merge tool_ord data; ); val get_tools = Data.get; val register_tool = Data.map o Ord_List.insert tool_ord; (* try command *) fun try_tools state = if subgoal_count state = 0 then (writeln "No subgoal!"; NONE) else get_tools (Proof.theory_of state) |> tap (fn tools => "Trying " ^ space_implode " " - (serial_commas "and" (map (quote o fst) tools)) ^ "..." + (serial_commas "and" (map (quote o #name) tools)) ^ "..." |> writeln) |> Par_List.get_some - (fn (name, (_, _, tool)) => - case try (tool false) state of + (fn {name, body, ...} => + case try (body false) state of SOME (true, (outcome_code, _)) => SOME (name, outcome_code) | _ => NONE) |> tap (fn NONE => writeln "Tried in vain" | _ => ()); val _ = Outer_Syntax.command \<^command_keyword>\try\ "try a combination of automatic proving and disproving tools" (Scan.succeed (Toplevel.keep_proof (ignore o try_tools o Toplevel.proof_of))); (* asynchronous print function *) -fun print_function ((name, (weight, auto, tool)): tool) = +fun print_function ({name, weight, auto_option, body}: tool) = Command.print_function ("auto_" ^ name) (fn {keywords, command_name, ...} => - if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then + if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto_option then SOME {delay = SOME (seconds (Options.default_real \<^system_option>\auto_time_start\)), pri = ~ weight, persistent = true, strict = true, print_fn = fn _ => fn st => let val state = Toplevel.proof_of st |> Proof.map_context (Context_Position.set_visible false) val auto_time_limit = Options.default_real \<^system_option>\auto_time_limit\ in if auto_time_limit > 0.0 then - (case Timeout.apply (seconds auto_time_limit) (fn () => tool true state) () of + (case Timeout.apply (seconds auto_time_limit) (fn () => body true state) () of (true, (_, outcome)) => List.app Output.information outcome | _ => ()) else () end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()} else NONE); -(* hybrid tool setup *) +(* tool setup *) fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool); end;