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