1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Try_Methods 8 9imports Eisbach_Methods 10 11keywords "trym" :: diag 12 and "add_try_method" :: thy_decl 13 14begin 15 16text \<open> 17A collection of methods that can be "tried" against subgoals (similar 18to try, try0 etc). It is easy to add new methods with "add_try_method", 19although the parser currently supports only single names. 20 21Particular subgoals can be tried with "trym 1" etc. By default all 22subgoals are attempted unless they are coupled to others by shared 23schematic variables. 24\<close> 25 26ML \<open> 27structure Try_Methods = struct 28 29structure Methods = Theory_Data 30( 31 type T = Symtab.set; 32 val empty = Symtab.empty; 33 val extend = I; 34 val merge = Symtab.merge (K true); 35); 36 37val get_methods_global = Methods.get #> Symtab.keys 38val add_method = Methods.map o Symtab.insert_set 39 40(* borrowed from try0 implementation (of course) *) 41fun parse_method_name keywords = 42 enclose "(" ")" 43 #> Token.explode keywords Position.start 44 #> filter Token.is_proper 45 #> Scan.read Token.stopper Method.parse 46 #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source"); 47 48fun mk_method ctxt = parse_method_name (Thy_Header.get_keywords' ctxt) 49 #> Method.method_cmd ctxt 50 #> Method.Basic 51 52fun get_methods ctxt = get_methods_global (Proof_Context.theory_of ctxt) 53 |> map (mk_method ctxt) 54 55fun try_one_method m ctxt n goal 56 = can (Timeout.apply (Time.fromSeconds 5) 57 (Goal.restrict n 1 #> NO_CONTEXT_TACTIC ctxt 58 (Method.evaluate_runtime m ctxt []) 59 #> Seq.hd 60 )) goal 61 62fun msg m_nm n = writeln ("method " ^ m_nm ^ " succceeded on goal " ^ string_of_int n) 63 64fun times xs ys = maps (fn x => map (pair x) ys) xs 65 66fun independent_subgoals goal verbose = let 67 fun get_vars t = Term.fold_aterms 68 (fn (Var v) => Termtab.insert_set (Var v) | _ => I) 69 t Termtab.empty 70 val goals = Thm.prems_of goal 71 val goal_vars = map get_vars goals 72 val count_vars = fold (fn t1 => fn t2 => Termtab.join (K (+)) 73 (Termtab.map (K (K 1)) t1, t2)) goal_vars Termtab.empty 74 val indep_vars = Termtab.forall (fst #> Termtab.lookup count_vars 75 #> (fn n => n = SOME 1)) 76 val indep = (1 upto Thm.nprems_of goal) ~~ map indep_vars goal_vars 77 val _ = app (fst #> string_of_int 78 #> prefix "ignoring non-independent goal " #> warning) 79 (filter (fn x => verbose andalso not (snd x)) indep) 80 in indep |> filter snd |> map fst end 81 82fun try_methods opt_n ctxt goal = let 83 val ms = get_methods_global (Proof_Context.theory_of ctxt) 84 ~~ get_methods ctxt 85 val ns = case opt_n of 86 NONE => independent_subgoals goal true 87 | SOME n => [n] 88 fun apply ((m_nm, m), n) = if try_one_method m ctxt n goal 89 then (msg m_nm n; SOME (m_nm, n)) else NONE 90 val results = Par_List.map apply (times ms ns) 91 in map_filter I results end 92 93fun try_methods_command opt_n st = let 94 val ctxt = #context (Proof.goal st) 95 |> Try0.silence_methods false 96 val goal = #goal (Proof.goal st) 97 in try_methods opt_n ctxt goal; () end 98 99val _ = Outer_Syntax.command @{command_keyword trym} 100 "try methods from a library of specialised strategies" 101 (Scan.option Parse.int >> (fn opt_n => 102 Toplevel.keep_proof (try_methods_command opt_n o Toplevel.proof_of))) 103 104fun local_check_add_method nm ctxt = 105 (mk_method ctxt nm; Local_Theory.background_theory (add_method nm) ctxt) 106 107val _ = Outer_Syntax.command @{command_keyword add_try_method} 108 "add a method to a library of strategies tried by trym" 109 (Parse.name >> (Toplevel.local_theory NONE NONE o local_check_add_method)) 110 111end 112\<close> 113 114add_try_method fastforce 115add_try_method blast 116add_try_method metis 117 118method auto_metis = solves \<open>auto; metis\<close> 119add_try_method auto_metis 120 121end 122