1(* Title: HOL/Tools/try0.ML 2 Author: Jasmin Blanchette, TU Muenchen 3 4Try a combination of proof methods. 5*) 6 7signature TRY0 = 8sig 9 val try0N : string 10 val noneN : string 11 12 val silence_methods : bool -> Proof.context -> Proof.context 13 val try0 : Time.time option -> string list * string list * string list * string list -> 14 Proof.state -> bool 15end; 16 17structure Try0 : TRY0 = 18struct 19 20val try0N = "try0"; 21val noneN = "none"; 22 23datatype mode = Auto_Try | Try | Normal; 24 25val default_timeout = seconds 5.0; 26 27fun can_apply timeout_opt pre post tac st = 28 let val {goal, ...} = Proof.goal st in 29 (case (case timeout_opt of 30 SOME timeout => Timeout.apply timeout 31 | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of 32 SOME (x, _) => Thm.nprems_of (post x) < Thm.nprems_of goal 33 | NONE => false) 34 end; 35 36fun apply_generic timeout_opt name command pre post apply st = 37 let val timer = Timer.startRealTimer () in 38 if try (can_apply timeout_opt pre post apply) st = SOME true then 39 SOME (name, command, Time.toMilliseconds (Timer.checkRealTimer timer)) 40 else 41 NONE 42 end; 43 44fun parse_method keywords s = 45 enclose "(" ")" s 46 |> Token.explode keywords Position.start 47 |> filter Token.is_proper 48 |> Scan.read Token.stopper Method.parse 49 |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source"); 50 51fun apply_named_method_on_first_goal ctxt = 52 parse_method (Thy_Header.get_keywords' ctxt) 53 #> Method.method_cmd ctxt 54 #> Method.Basic 55 #> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) 56 #> Proof.refine; 57 58fun add_attr_text (NONE, _) s = s 59 | add_attr_text (_, []) s = s 60 | add_attr_text (SOME x, fs) s = 61 s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs; 62 63fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) = 64 "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]; 65 66fun apply_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode timeout_opt quad st = 67 if mode <> Auto_Try orelse run_if_auto_try then 68 let val attrs = attrs_text attrs quad in 69 apply_generic timeout_opt name 70 ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ 71 (if all_goals andalso Thm.nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else "")) 72 I (#goal o Proof.goal) 73 (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs) 74 #> Seq.filter_results) st 75 end 76 else 77 NONE; 78 79val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest"); 80val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest"); 81val simp_attrs = (SOME "add", NONE, NONE, NONE); 82val metis_attrs = (SOME "", SOME "", SOME "", SOME ""); 83val no_attrs = (NONE, NONE, NONE, NONE); 84 85(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *) 86val named_methods = 87 [("simp", ((false, true), simp_attrs)), 88 ("auto", ((true, true), full_attrs)), 89 ("blast", ((false, true), clas_attrs)), 90 ("metis", ((false, true), metis_attrs)), 91 ("argo", ((false, true), no_attrs)), 92 ("linarith", ((false, true), no_attrs)), 93 ("presburger", ((false, true), no_attrs)), 94 ("algebra", ((false, true), no_attrs)), 95 ("fast", ((false, false), clas_attrs)), 96 ("fastforce", ((false, false), full_attrs)), 97 ("force", ((false, false), full_attrs)), 98 ("meson", ((false, false), metis_attrs)), 99 ("satx", ((false, false), no_attrs))]; 100 101val apply_methods = map apply_named_method named_methods; 102 103fun time_string ms = string_of_int ms ^ " ms"; 104fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms; 105 106(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification 107 bound exceeded" warnings and the like. *) 108fun silence_methods debug = 109 Config.put Metis_Tactic.verbose debug 110 #> not debug ? (fn ctxt => 111 ctxt 112 |> Simplifier_Trace.disable 113 |> Context_Position.set_visible false 114 |> Config.put Unify.trace_bound (Config.get ctxt Unify.search_bound) 115 |> Config.put Argo_Tactic.trace "none" 116 |> Proof_Context.background_theory (fn thy => 117 thy 118 |> Context_Position.set_visible_global false 119 |> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound))); 120 121fun generic_try0 mode timeout_opt quad st = 122 let 123 val st = Proof.map_contexts (silence_methods false) st; 124 fun trd (_, _, t) = t; 125 fun try_method method = method mode timeout_opt quad st; 126 fun get_message (_, command, ms) = "Found proof: " ^ Active.sendback_markup_command 127 ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ " " ^ command) ^ 128 " (" ^ time_string ms ^ ")"; 129 val print_step = Option.map (tap (writeln o get_message)); 130 val get_results = 131 if mode = Normal 132 then Par_List.map (try_method #> print_step) #> map_filter I #> sort (int_ord o apply2 trd) 133 else Par_List.get_some try_method #> the_list; 134 in 135 if mode = Normal then 136 "Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^ 137 "..." 138 |> writeln 139 else 140 (); 141 (case get_results apply_methods of 142 [] => 143 (if mode = Normal then writeln "No proof found" else (); (false, (noneN, []))) 144 | xs as (name, command, _) :: _ => 145 let 146 val xs = xs |> map (fn (name, _, n) => (n, name)) 147 |> AList.coalesce (op =) 148 |> map (swap o apsnd commas); 149 val message = 150 (case mode of 151 Auto_Try => "Auto Try0 found a proof" 152 | Try => "Try0 found a proof" 153 | Normal => "Try this") ^ ": " ^ 154 Active.sendback_markup_command 155 ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" 156 else "apply") ^ " " ^ command) ^ 157 (case xs of 158 [(_, ms)] => " (" ^ time_string ms ^ ")" 159 | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ")"); 160 in 161 (true, (name, if mode = Auto_Try then [message] else (writeln message; []))) 162 end) 163 end; 164 165fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt; 166 167fun try0_trans quad = 168 Toplevel.keep_proof 169 (ignore o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of); 170 171fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2); 172 173fun string_of_xthm (xref, args) = 174 Facts.string_of_ref xref ^ 175 implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args); 176 177val parse_fact_refs = 178 Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.thm >> string_of_xthm)); 179 180val parse_attr = 181 Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn ss => (ss, [], [], [])) 182 || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (fn is => ([], is, [], [])) 183 || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (fn es => ([], [], es, [])) 184 || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (fn ds => ([], [], [], ds)); 185 186fun parse_attrs x = 187 (Args.parens parse_attrs 188 || Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x; 189 190val _ = 191 Outer_Syntax.command \<^command_keyword>\<open>try0\<close> "try a combination of proof methods" 192 (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans); 193 194fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []); 195 196val _ = Try.tool_setup (try0N, (30, \<^system_option>\<open>auto_methods\<close>, try_try0)); 197 198end; 199