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