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