# HG changeset patch # User blanchet # Date 1301563011 -7200 # Node ID 24662b614fd425752f279c39b1c004f6601d0cc3 # Parent b992c8e6394b9fa807f726879743eb8dd666fee1 added support for "dest:" to "try" diff -r b992c8e6394b -r 24662b614fd4 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 31 09:43:36 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 31 11:16:51 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 b992c8e6394b -r 24662b614fd4 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 31 09:43:36 2011 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 31 11:16:51 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 b992c8e6394b -r 24662b614fd4 src/HOL/Tools/try.ML --- a/src/HOL/Tools/try.ML Thu Mar 31 09:43:36 2011 +0200 +++ b/src/HOL/Tools/try.ML Thu Mar 31 11:16:51 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)