1.1 --- a/src/HOL/Tools/try.ML Fri May 27 10:30:08 2011 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,179 +0,0 @@
1.4 -(* Title: HOL/Tools/try.ML
1.5 - Author: Jasmin Blanchette, TU Muenchen
1.6 -
1.7 -Try a combination of proof methods.
1.8 -*)
1.9 -
1.10 -signature TRY =
1.11 -sig
1.12 - val auto : bool Unsynchronized.ref
1.13 - val invoke_try :
1.14 - Time.time option -> string list * string list * string list * string list
1.15 - -> Proof.state -> bool
1.16 - val setup : theory -> theory
1.17 -end;
1.18 -
1.19 -structure Try : TRY =
1.20 -struct
1.21 -
1.22 -val auto = Unsynchronized.ref false
1.23 -
1.24 -val _ =
1.25 - ProofGeneralPgip.add_preference Preferences.category_tracing
1.26 - (Preferences.bool_pref auto "auto-try" "Try standard proof methods.")
1.27 -
1.28 -val default_timeout = seconds 5.0
1.29 -
1.30 -fun can_apply timeout_opt pre post tac st =
1.31 - let val {goal, ...} = Proof.goal st in
1.32 - case (case timeout_opt of
1.33 - SOME timeout => TimeLimit.timeLimit timeout
1.34 - | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
1.35 - SOME (x, _) => nprems_of (post x) < nprems_of goal
1.36 - | NONE => false
1.37 - end
1.38 - handle TimeLimit.TimeOut => false
1.39 -
1.40 -fun do_generic timeout_opt command pre post apply st =
1.41 - let val timer = Timer.startRealTimer () in
1.42 - if can_apply timeout_opt pre post apply st then
1.43 - SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
1.44 - else
1.45 - NONE
1.46 - end
1.47 -
1.48 -val parse_method =
1.49 - enclose "(" ")"
1.50 - #> Outer_Syntax.scan Position.start
1.51 - #> filter Token.is_proper
1.52 - #> Scan.read Token.stopper Method.parse
1.53 - #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
1.54 -
1.55 -fun apply_named_method_on_first_goal method thy =
1.56 - method |> parse_method
1.57 - |> Method.method thy
1.58 - |> Method.Basic
1.59 - |> curry Method.SelectGoals 1
1.60 - |> Proof.refine
1.61 - handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
1.62 -
1.63 -fun add_attr_text (NONE, _) s = s
1.64 - | add_attr_text (_, []) s = s
1.65 - | add_attr_text (SOME x, fs) s =
1.66 - s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
1.67 -fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
1.68 - "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
1.69 -
1.70 -fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
1.71 - quad st =
1.72 - if not auto orelse run_if_auto then
1.73 - let val attrs = attrs_text attrs quad in
1.74 - do_generic timeout_opt
1.75 - (name ^ (if all_goals andalso
1.76 - nprems_of (#goal (Proof.goal st)) > 1 then
1.77 - "[1]"
1.78 - else
1.79 - "") ^
1.80 - attrs) I (#goal o Proof.goal)
1.81 - (apply_named_method_on_first_goal (name ^ attrs)
1.82 - (Proof.theory_of st)) st
1.83 - end
1.84 - else
1.85 - NONE
1.86 -
1.87 -val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
1.88 -val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
1.89 -val simp_attrs = (SOME "add", NONE, NONE, NONE)
1.90 -val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
1.91 -val no_attrs = (NONE, NONE, NONE, NONE)
1.92 -
1.93 -(* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *)
1.94 -val named_methods =
1.95 - [("simp", ((false, true), simp_attrs)),
1.96 - ("auto", ((true, true), full_attrs)),
1.97 - ("fast", ((false, false), clas_attrs)),
1.98 - ("fastsimp", ((false, false), full_attrs)),
1.99 - ("force", ((false, false), full_attrs)),
1.100 - ("blast", ((false, true), clas_attrs)),
1.101 - ("metis", ((false, true), metis_attrs)),
1.102 - ("linarith", ((false, true), no_attrs)),
1.103 - ("presburger", ((false, true), no_attrs))]
1.104 -val do_methods = map do_named_method named_methods
1.105 -
1.106 -fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
1.107 -
1.108 -fun do_try auto timeout_opt quad st =
1.109 - let
1.110 - val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
1.111 - in
1.112 - case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)
1.113 - |> map_filter I |> sort (int_ord o pairself snd) of
1.114 - [] => (if auto then () else writeln "No proof found."; (false, st))
1.115 - | xs as (s, _) :: _ =>
1.116 - let
1.117 - val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
1.118 - |> AList.coalesce (op =)
1.119 - |> map (swap o apsnd commas)
1.120 - val need_parens = exists_string (curry (op =) " ") s
1.121 - val message =
1.122 - (if auto then "Auto Try found a proof" else "Try this command") ^
1.123 - ": " ^
1.124 - Markup.markup Markup.sendback
1.125 - ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
1.126 - else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
1.127 - "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
1.128 - in
1.129 - (true, st |> (if auto then
1.130 - Proof.goal_message
1.131 - (fn () => Pretty.chunks [Pretty.str "",
1.132 - Pretty.markup Markup.hilite
1.133 - [Pretty.str message]])
1.134 - else
1.135 - tap (fn _ => Output.urgent_message message)))
1.136 - end
1.137 - end
1.138 -
1.139 -fun invoke_try timeout_opt = fst oo do_try false timeout_opt
1.140 -
1.141 -val tryN = "try"
1.142 -
1.143 -fun try_trans quad =
1.144 - Toplevel.keep (K () o do_try false (SOME default_timeout) quad
1.145 - o Toplevel.proof_of)
1.146 -
1.147 -fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
1.148 - (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
1.149 -
1.150 -fun string_of_xthm (xref, args) =
1.151 - Facts.string_of_ref xref ^
1.152 - implode (map (enclose "[" "]" o Pretty.str_of
1.153 - o Args.pretty_src @{context}) args)
1.154 -
1.155 -val parse_fact_refs =
1.156 - Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
1.157 - (Parse_Spec.xthm >> string_of_xthm))
1.158 -val parse_attr =
1.159 - Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
1.160 - >> (fn ss => (ss, [], [], []))
1.161 - || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
1.162 - >> (fn is => ([], is, [], []))
1.163 - || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
1.164 - >> (fn es => ([], [], es, []))
1.165 - || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
1.166 - >> (fn ds => ([], [], [], ds))
1.167 -fun parse_attrs x =
1.168 - (Args.parens parse_attrs
1.169 - || Scan.repeat parse_attr
1.170 - >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
1.171 -
1.172 -val parse_try_command = Scan.optional parse_attrs ([], [], [], []) #>> try_trans
1.173 -
1.174 -val _ =
1.175 - Outer_Syntax.improper_command tryN
1.176 - "try a combination of proof methods" Keyword.diag parse_try_command
1.177 -
1.178 -val auto_try = do_try true NONE ([], [], [], [])
1.179 -
1.180 -val setup = Auto_Tools.register_tool (auto, auto_try)
1.181 -
1.182 -end;