# HG changeset patch # User bulwahn # Date 1301584513 -7200 # Node ID 7101712baae825f833a47c9ba828743ee405c76e # Parent 1d4fae76ba5eab104eb9d6595d08c050bd8ce290# Parent 173b0f488428e06e58ff4e77b9108eae64226305 merged diff -r 1d4fae76ba5e -r 7101712baae8 NEWS --- a/NEWS Thu Mar 31 11:17:52 2011 +0200 +++ b/NEWS Thu Mar 31 17:15:13 2011 +0200 @@ -49,6 +49,7 @@ * Sledgehammer: - sledgehammer available_provers ~> sledgehammer supported_provers INCOMPATIBILITY. + - Added "monomorphize" and "monomorphize_limit" options. * "try": - Added "simp:", "intro:", and "elim:" options. diff -r 1d4fae76ba5e -r 7101712baae8 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Thu Mar 31 11:17:52 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Mar 31 17:15:13 2011 +0200 @@ -555,6 +555,19 @@ filter. If the option is set to \textit{smart}, it is set to a value that was empirically found to be appropriate for the prover. A typical value would be 300. + +\opfalse{monomorphize}{dont\_monomorphize} +Specifies whether the relevant facts should be monomorphized---i.e., whether +their type variables should be instantiated with relevant ground types. +Monomorphization is always performed for SMT solvers, irrespective of this +option. Monomorphization can simplify reasoning but also leads to larger fact +bases, which can slow down the ATPs. + +\opdefault{monomorphize\_limit}{int}{\upshape 4} +Specifies the maximum number of iterations for the monomorphization fixpoint +construction. The higher this limit is, the more monomorphic instances are +potentially generated. + \end{enum} \subsection{Output Format} diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 31 17:15:13 2011 +0200 @@ -558,7 +558,7 @@ Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) val minimize = AList.defined (op =) args minimizeK val metis_ft = AList.defined (op =) args metis_ftK - val trivial = Try.invoke_try (SOME try_timeout) ([], [], []) pre + val trivial = Try.invoke_try (SOME try_timeout) ([], [], [], []) pre handle TimeLimit.TimeOut => false fun apply_reconstructor m1 m2 = if metis_ft diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 31 17:15:13 2011 +0200 @@ -154,7 +154,7 @@ let val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) in - case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of + case Try.invoke_try (SOME (seconds 5.0)) ([], [], [], []) state of true => (Solved, []) | false => (Unsolved, []) end diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Tools/SMT/smt_monomorph.ML --- a/src/HOL/Tools/SMT/smt_monomorph.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML Thu Mar 31 17:15:13 2011 +0200 @@ -28,8 +28,9 @@ signature SMT_MONOMORPH = sig - val monomorph: (int * thm) list -> Proof.context -> - (int * thm) list * Proof.context + val typ_has_tvars: typ -> bool + val monomorph: bool -> ('a * thm) list -> Proof.context -> + ('a * thm) list * Proof.context end structure SMT_Monomorph: SMT_MONOMORPH = @@ -159,37 +160,44 @@ in most_specific [] end -fun instantiate (i, thm) substs (ithms, ctxt) = +fun instantiate full (i, thm) substs (ithms, ctxt) = let + val thy = ProofContext.theory_of ctxt + val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) []) val (Tenv, ctxt') = ctxt |> Variable.invent_types Ss |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs - val thy = ProofContext.theory_of ctxt' + exception PARTIAL_INST of unit + + fun update_subst vT subst = + if full then Vartab.update vT subst + else raise PARTIAL_INST () fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U | replace _ T = T fun complete (vT as (v, _)) subst = subst - |> not (Vartab.defined subst v) ? Vartab.update vT + |> not (Vartab.defined subst v) ? update_subst vT |> Vartab.map (K (apsnd (Term.map_atyps (replace vT)))) fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T) fun inst subst = let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) [] - in (i, Thm.instantiate (cTs, []) thm) end + in SOME (i, Thm.instantiate (cTs, []) thm) end + handle PARTIAL_INST () => NONE - in (map inst substs @ ithms, ctxt') end + in (map_filter inst substs @ ithms, if full then ctxt' else ctxt) end (* overall procedure *) -fun mono_all ctxt polys monos = +fun mono_all full ctxt polys monos = let val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys @@ -208,13 +216,13 @@ |> search_substitutions ctxt limit instances Symtab.empty grounds |> map (filter_most_specific (ProofContext.theory_of ctxt)) |> rpair (monos, ctxt) - |-> fold2 instantiate polys + |-> fold2 (instantiate full) polys end -fun monomorph irules ctxt = +fun monomorph full irules ctxt = irules |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd) |>> incr_indexes (* avoid clashes of schematic type variables *) - |-> (fn [] => rpair ctxt | polys => mono_all ctxt polys) + |-> (fn [] => rpair ctxt | polys => mono_all full ctxt polys) end diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Thu Mar 31 17:15:13 2011 +0200 @@ -631,7 +631,7 @@ |> gen_normalize ctxt |> unfold1 ctxt |> rpair ctxt - |-> SMT_Monomorph.monomorph + |-> SMT_Monomorph.monomorph true |-> unfold2 |-> apply_extra_norms diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Mar 31 17:15:13 2011 +0200 @@ -88,6 +88,8 @@ #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation #> fst +val unprefix_fact_number = space_implode "_" o tl o space_explode "_" + fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names = if String.isSubstring set_ClauseFormulaRelationN output then let @@ -100,7 +102,8 @@ |> map (fn s => find_index (curry (op =) s) seq + 1) fun names_for_number j = j |> AList.lookup (op =) name_map |> these - |> map_filter (try (unprefix fact_prefix)) |> map unascii_of + |> map_filter (try (unascii_of o unprefix_fact_number + o unprefix fact_prefix)) |> map (fn name => (name, name |> find_first_in_list_vector fact_names |> the) handle Option.Option => @@ -145,16 +148,19 @@ "\nTo minimize the number of lemmas, try this: " ^ Markup.markup Markup.sendback command ^ "." -val vampire_fact_prefix = "f" (* grrr... *) +val vampire_step_prefix = "f" (* grrr... *) fun resolve_fact fact_names ((_, SOME s)) = - (case strip_prefix_and_unascii fact_prefix s of - SOME s' => (case find_first_in_list_vector fact_names s' of - SOME x => [(s', x)] - | NONE => []) + (case try (unprefix fact_prefix) s of + SOME s' => + let val s' = s' |> unprefix_fact_number |> unascii_of in + case find_first_in_list_vector fact_names s' of + SOME x => [(s', x)] + | NONE => [] + end | NONE => []) | resolve_fact fact_names (num, NONE) = - case Int.fromString (perhaps (try (unprefix vampire_fact_prefix)) num) of + case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of SOME j => if j > 0 andalso j <= Vector.length fact_names then Vector.sub (fact_names, j - 1) @@ -233,7 +239,7 @@ val raw_prefix = "X" val assum_prefix = "A" -val fact_prefix = "F" +val have_prefix = "F" fun resolve_conjecture conjecture_shape (num, s_opt) = let @@ -847,7 +853,7 @@ (l, subst, next_fact) else let - val l' = (prefix_for_depth depth fact_prefix, next_fact) + val l' = (prefix_for_depth depth have_prefix, next_fact) in (l', (l, l') :: subst, next_fact + 1) end val relabel_facts = apfst (maps (the_list o AList.lookup (op =) subst)) diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Mar 31 17:15:13 2011 +0200 @@ -442,9 +442,13 @@ (atp_type_literals_for_types type_sys ctypes_sorts)) (formula_for_combformula ctxt type_sys combformula) -fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) = - Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula, - NONE) +(* Each fact is given a unique fact number to avoid name clashes (e.g., because + of monomorphization). The TPTP explicitly forbids name clashes, and some of + the remote provers might care. *) +fun problem_line_for_fact ctxt prefix type_sys + (j, formula as {name, kind, ...}) = + Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind, + formula_for_fact ctxt type_sys formula, NONE) fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, superclass, ...}) = @@ -626,7 +630,8 @@ (* Reordering these might or might not confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem = - [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) facts), + [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) + (0 upto length facts - 1 ~~ facts)), (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses), (aritiesN, map problem_line_for_arity_clause arity_clauses), (helpersN, []), @@ -638,7 +643,8 @@ val helper_lines = get_helper_facts ctxt explicit_forall type_sys (maps (map (#3 o dest_Fof) o snd) problem) - |>> map (problem_line_for_fact ctxt helper_prefix type_sys + |>> map (pair 0 + #> problem_line_for_fact ctxt helper_prefix type_sys #> repair_problem_line thy explicit_forall type_sys const_tab) |> op @ val (problem, pool) = diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 31 17:15:13 2011 +0200 @@ -79,10 +79,12 @@ ("verbose", "false"), ("overlord", "false"), ("blocking", "false"), + ("relevance_thresholds", "0.45 0.85"), + ("max_relevant", "smart"), + ("monomorphize", "false"), + ("monomorphize_limit", "4"), ("type_sys", "smart"), ("explicit_apply", "false"), - ("relevance_thresholds", "0.45 0.85"), - ("max_relevant", "smart"), ("isar_proof", "false"), ("isar_shrink_factor", "1")] @@ -95,6 +97,7 @@ ("quiet", "verbose"), ("no_overlord", "overlord"), ("non_blocking", "blocking"), + ("dont_monomorphize", "monomorphize"), ("partial_types", "full_types"), ("implicit_apply", "explicit_apply"), ("no_isar_proof", "isar_proof")] @@ -233,6 +236,10 @@ val blocking = auto orelse debug orelse lookup_bool "blocking" val provers = lookup_string "provers" |> space_explode " " |> auto ? single o hd + val relevance_thresholds = lookup_real_pair "relevance_thresholds" + val max_relevant = lookup_int_option "max_relevant" + val monomorphize = lookup_bool "monomorphize" + val monomorphize_limit = lookup_int "monomorphize_limit" val type_sys = case (lookup_string "type_sys", lookup_bool "full_types") of ("tags", full_types) => Tags full_types @@ -245,18 +252,18 @@ else error ("Unknown type system: " ^ quote type_sys ^ ".") val explicit_apply = lookup_bool "explicit_apply" - val relevance_thresholds = lookup_real_pair "relevance_thresholds" - val max_relevant = lookup_int_option "max_relevant" val isar_proof = lookup_bool "isar_proof" val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, - provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, - relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, - timeout = timeout, expect = expect} + provers = provers, relevance_thresholds = relevance_thresholds, + max_relevant = max_relevant, monomorphize = monomorphize, + monomorphize_limit = monomorphize_limit, type_sys = type_sys, + explicit_apply = explicit_apply, isar_proof = isar_proof, + isar_shrink_factor = isar_shrink_factor, timeout = timeout, + expect = expect} end fun get_params auto ctxt = extract_params auto (default_raw_params ctxt) diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Mar 31 17:15:13 2011 +0200 @@ -42,8 +42,8 @@ fun print silent f = if silent then () else Output.urgent_message (f ()) -fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof, - isar_shrink_factor, ...} : params) +fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit, + type_sys, isar_proof, isar_shrink_factor, ...} : params) explicit_apply_opt silent (prover : prover) timeout i n state facts = let val thy = Proof.theory_of state @@ -65,6 +65,7 @@ {debug = debug, verbose = verbose, overlord = overlord, blocking = true, provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), max_relevant = NONE, + monomorphize = false, monomorphize_limit = monomorphize_limit, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} val facts = diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Mar 31 17:15:13 2011 +0200 @@ -21,10 +21,12 @@ overlord: bool, blocking: bool, provers: string list, + relevance_thresholds: real * real, + max_relevant: int option, + monomorphize: bool, + monomorphize_limit: int, type_sys: type_system, explicit_apply: bool, - relevance_thresholds: real * real, - max_relevant: int option, isar_proof: bool, isar_shrink_factor: int, timeout: Time.time, @@ -66,7 +68,6 @@ val smt_iter_fact_frac : real Unsynchronized.ref val smt_iter_time_frac : real Unsynchronized.ref val smt_iter_min_msecs : int Unsynchronized.ref - val smt_monomorphize_limit : int Unsynchronized.ref val das_Tool : string val select_smt_solver : string -> Proof.context -> Proof.context @@ -229,10 +230,12 @@ overlord: bool, blocking: bool, provers: string list, + relevance_thresholds: real * real, + max_relevant: int option, + monomorphize: bool, + monomorphize_limit: int, type_sys: type_system, explicit_apply: bool, - relevance_thresholds: real * real, - max_relevant: int option, isar_proof: bool, isar_shrink_factor: int, timeout: Time.time, @@ -333,13 +336,40 @@ ({exec, required_execs, arguments, has_incomplete_mode, proof_delims, known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config) - ({debug, verbose, overlord, type_sys, explicit_apply, isar_proof, - isar_shrink_factor, timeout, ...} : params) + ({debug, verbose, overlord, monomorphize, monomorphize_limit, type_sys, + explicit_apply, isar_proof, isar_shrink_factor, timeout, ...} + : params) minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = let + val thy = Proof.theory_of state val ctxt = Proof.context_of state val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal - val facts = facts |> map (atp_translated_fact ctxt) + fun monomorphize_facts facts = + let + val facts = facts |> map untranslated_fact + (* pseudo-theorem involving the same constants as the subgoal *) + val subgoal_th = + Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy + val indexed_facts = + (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts) + val (mono_facts, ctxt') = + ctxt |> Config.put SMT_Config.verbose debug + |> Config.put SMT_Config.monomorph_limit monomorphize_limit + |> SMT_Monomorph.monomorph true indexed_facts + in + mono_facts + |> sort (int_ord o pairself fst) + |> filter_out (curry (op =) ~1 o fst) + (* The next step shouldn't be necessary but currently the monomorphizer + generates unexpected instances with fresh TFrees, which typically + become TVars once exported. *) + |> filter_out (Term.exists_type SMT_Monomorph.typ_has_tvars + o singleton (Variable.export_terms ctxt' ctxt) + o prop_of o snd) + |> map (Untranslated_Fact o apfst (fst o nth facts)) + end + val facts = facts |> monomorphize ? monomorphize_facts + |> map (atp_translated_fact ctxt) val (dest_dir, problem_prefix) = if overlord then overlord_file_location_for_prover name else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix) @@ -513,9 +543,9 @@ val smt_iter_fact_frac = Unsynchronized.ref 0.5 val smt_iter_time_frac = Unsynchronized.ref 0.5 val smt_iter_min_msecs = Unsynchronized.ref 5000 -val smt_monomorphize_limit = Unsynchronized.ref 4 -fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params) +fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit, + timeout, ...} : params) state i smt_filter = let val ctxt = Proof.context_of state @@ -529,7 +559,7 @@ else I) #> Config.put SMT_Config.infer_triggers (!smt_triggers) - #> Config.put SMT_Config.monomorph_limit (!smt_monomorphize_limit) + #> Config.put SMT_Config.monomorph_limit monomorphize_limit val state = state |> Proof.map_context repair_context fun iter timeout iter_num outcome0 time_so_far facts = diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Mar 31 17:15:13 2011 +0200 @@ -164,9 +164,9 @@ (* FUDGE *) val auto_max_relevant_divisor = 2 -fun run_sledgehammer (params as {debug, blocking, provers, type_sys, - relevance_thresholds, max_relevant, timeout, - ...}) +fun run_sledgehammer (params as {debug, blocking, provers, monomorphize, + type_sys, relevance_thresholds, max_relevant, + timeout, ...}) auto i (relevance_override as {only, ...}) minimize_command state = if null provers then @@ -246,7 +246,10 @@ else launch_provers state (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps) - (ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst)) + (if monomorphize then + K (Untranslated_Fact o fst) + else + ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst)) (K (K NONE)) atps fun launch_smts accum = if null smts then diff -r 1d4fae76ba5e -r 7101712baae8 src/HOL/Tools/try.ML --- a/src/HOL/Tools/try.ML Thu Mar 31 11:17:52 2011 +0200 +++ b/src/HOL/Tools/try.ML Thu Mar 31 17:15:13 2011 +0200 @@ -8,8 +8,8 @@ sig val auto : bool Unsynchronized.ref val invoke_try : - Time.time option -> string list * string list * string list -> Proof.state - -> bool + Time.time option -> string list * string list * string list * string list + -> Proof.state -> bool val setup : theory -> theory end; @@ -61,13 +61,13 @@ | 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) (ss, is, es) = - "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es)] +fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) = + "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)] fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt - triple st = + quad st = if not auto orelse run_if_auto then - let val attrs = attrs_text attrs triple in + let val attrs = attrs_text attrs quad in do_generic timeout_opt (name ^ (if all_goals andalso nprems_of (#goal (Proof.goal st)) > 1 then @@ -81,13 +81,13 @@ else NONE -val full_attrs = (SOME "simp", SOME "intro", SOME "elim") -val clas_attrs = (NONE, SOME "intro", SOME "elim") -val simp_attrs = (SOME "add", NONE, NONE) -val metis_attrs = (SOME "", SOME "", SOME "") -val no_attrs = (NONE, NONE, 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), (simp, intro, elim) *) +(* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *) val named_methods = [("simp", ((false, true), simp_attrs)), ("auto", ((true, true), full_attrs)), @@ -102,11 +102,11 @@ fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms" -fun do_try auto timeout_opt triple st = +fun do_try auto timeout_opt quad st = let val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false) in - case do_methods |> Par_List.map (fn f => f auto timeout_opt triple st) + case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st) |> map_filter I |> sort (int_ord o pairself snd) of [] => (if auto then () else writeln "No proof found."; (false, st)) | xs as (s, _) :: _ => @@ -137,11 +137,12 @@ val tryN = "try" -fun try_trans triple = - Toplevel.keep (K () o do_try false (SOME default_timeout) triple +fun try_trans quad = + Toplevel.keep (K () o do_try false (SOME default_timeout) quad o Toplevel.proof_of) -fun merge_attrs (s1, i1, e1) (s2, i2, e2) = (s1 @ s2, i1 @ i2, e1 @ e2) +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 ^ @@ -153,23 +154,25 @@ (Parse_Spec.xthm >> string_of_xthm)) val parse_attr = Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs - >> (fn ss => (ss, [], [])) + >> (fn ss => (ss, [], [], [])) || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs - >> (fn is => ([], is, [])) + >> (fn is => ([], is, [], [])) || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs - >> (fn es => ([], [], es)) + >> (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 triple => fold merge_attrs triple ([], [], []))) x + >> (fn quad => fold merge_attrs quad ([], [], [], []))) x -val parse_try_command = Scan.optional parse_attrs ([], [], []) #>> try_trans +val parse_try_command = Scan.optional parse_attrs ([], [], [], []) #>> try_trans val _ = Outer_Syntax.improper_command tryN "try a combination of proof methods" Keyword.diag parse_try_command -val auto_try = do_try true NONE ([], [], []) +val auto_try = do_try true NONE ([], [], [], []) val setup = Auto_Tools.register_tool (auto, auto_try)