1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 31 09:43:36 2011 +0200
1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 31 11:16:51 2011 +0200
1.3 @@ -558,7 +558,7 @@
1.4 Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
1.5 val minimize = AList.defined (op =) args minimizeK
1.6 val metis_ft = AList.defined (op =) args metis_ftK
1.7 - val trivial = Try.invoke_try (SOME try_timeout) ([], [], []) pre
1.8 + val trivial = Try.invoke_try (SOME try_timeout) ([], [], [], []) pre
1.9 handle TimeLimit.TimeOut => false
1.10 fun apply_reconstructor m1 m2 =
1.11 if metis_ft
2.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 31 09:43:36 2011 +0200
2.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 31 11:16:51 2011 +0200
2.3 @@ -154,7 +154,7 @@
2.4 let
2.5 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
2.6 in
2.7 - case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of
2.8 + case Try.invoke_try (SOME (seconds 5.0)) ([], [], [], []) state of
2.9 true => (Solved, [])
2.10 | false => (Unsolved, [])
2.11 end
3.1 --- a/src/HOL/Tools/try.ML Thu Mar 31 09:43:36 2011 +0200
3.2 +++ b/src/HOL/Tools/try.ML Thu Mar 31 11:16:51 2011 +0200
3.3 @@ -8,8 +8,8 @@
3.4 sig
3.5 val auto : bool Unsynchronized.ref
3.6 val invoke_try :
3.7 - Time.time option -> string list * string list * string list -> Proof.state
3.8 - -> bool
3.9 + Time.time option -> string list * string list * string list * string list
3.10 + -> Proof.state -> bool
3.11 val setup : theory -> theory
3.12 end;
3.13
3.14 @@ -61,13 +61,13 @@
3.15 | add_attr_text (_, []) s = s
3.16 | add_attr_text (SOME x, fs) s =
3.17 s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
3.18 -fun attrs_text (sx, ix, ex) (ss, is, es) =
3.19 - "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es)]
3.20 +fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
3.21 + "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
3.22
3.23 fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
3.24 - triple st =
3.25 + quad st =
3.26 if not auto orelse run_if_auto then
3.27 - let val attrs = attrs_text attrs triple in
3.28 + let val attrs = attrs_text attrs quad in
3.29 do_generic timeout_opt
3.30 (name ^ (if all_goals andalso
3.31 nprems_of (#goal (Proof.goal st)) > 1 then
3.32 @@ -81,13 +81,13 @@
3.33 else
3.34 NONE
3.35
3.36 -val full_attrs = (SOME "simp", SOME "intro", SOME "elim")
3.37 -val clas_attrs = (NONE, SOME "intro", SOME "elim")
3.38 -val simp_attrs = (SOME "add", NONE, NONE)
3.39 -val metis_attrs = (SOME "", SOME "", SOME "")
3.40 -val no_attrs = (NONE, NONE, NONE)
3.41 +val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
3.42 +val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
3.43 +val simp_attrs = (SOME "add", NONE, NONE, NONE)
3.44 +val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
3.45 +val no_attrs = (NONE, NONE, NONE, NONE)
3.46
3.47 -(* name * ((all_goals, run_if_auto), (simp, intro, elim) *)
3.48 +(* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *)
3.49 val named_methods =
3.50 [("simp", ((false, true), simp_attrs)),
3.51 ("auto", ((true, true), full_attrs)),
3.52 @@ -102,11 +102,11 @@
3.53
3.54 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
3.55
3.56 -fun do_try auto timeout_opt triple st =
3.57 +fun do_try auto timeout_opt quad st =
3.58 let
3.59 val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
3.60 in
3.61 - case do_methods |> Par_List.map (fn f => f auto timeout_opt triple st)
3.62 + case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)
3.63 |> map_filter I |> sort (int_ord o pairself snd) of
3.64 [] => (if auto then () else writeln "No proof found."; (false, st))
3.65 | xs as (s, _) :: _ =>
3.66 @@ -137,11 +137,12 @@
3.67
3.68 val tryN = "try"
3.69
3.70 -fun try_trans triple =
3.71 - Toplevel.keep (K () o do_try false (SOME default_timeout) triple
3.72 +fun try_trans quad =
3.73 + Toplevel.keep (K () o do_try false (SOME default_timeout) quad
3.74 o Toplevel.proof_of)
3.75
3.76 -fun merge_attrs (s1, i1, e1) (s2, i2, e2) = (s1 @ s2, i1 @ i2, e1 @ e2)
3.77 +fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
3.78 + (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
3.79
3.80 fun string_of_xthm (xref, args) =
3.81 Facts.string_of_ref xref ^
3.82 @@ -153,23 +154,25 @@
3.83 (Parse_Spec.xthm >> string_of_xthm))
3.84 val parse_attr =
3.85 Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
3.86 - >> (fn ss => (ss, [], []))
3.87 + >> (fn ss => (ss, [], [], []))
3.88 || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
3.89 - >> (fn is => ([], is, []))
3.90 + >> (fn is => ([], is, [], []))
3.91 || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
3.92 - >> (fn es => ([], [], es))
3.93 + >> (fn es => ([], [], es, []))
3.94 + || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
3.95 + >> (fn ds => ([], [], [], ds))
3.96 fun parse_attrs x =
3.97 (Args.parens parse_attrs
3.98 || Scan.repeat parse_attr
3.99 - >> (fn triple => fold merge_attrs triple ([], [], []))) x
3.100 + >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
3.101
3.102 -val parse_try_command = Scan.optional parse_attrs ([], [], []) #>> try_trans
3.103 +val parse_try_command = Scan.optional parse_attrs ([], [], [], []) #>> try_trans
3.104
3.105 val _ =
3.106 Outer_Syntax.improper_command tryN
3.107 "try a combination of proof methods" Keyword.diag parse_try_command
3.108
3.109 -val auto_try = do_try true NONE ([], [], [])
3.110 +val auto_try = do_try true NONE ([], [], [], [])
3.111
3.112 val setup = Auto_Tools.register_tool (auto, auto_try)
3.113