1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Time_Methods_Cmd_Test imports
8  Lib.Time_Methods_Cmd
9  Lib.Eisbach_Methods
10  "HOL-Library.Sublist"
11begin
12
13text \<open>
14  @{method time_methods} is a utility that runs several methods on the same
15  proof goal, printing the running time of each one.
16
17  Usage:
18
19    apply (time_methods [(no_check)] [(skip_fail)]
20        [name1:] \<open>method1\<close>
21        [name2:] \<open>method2\<close>
22        ...)
23
24  Options:
25
26    no_check: Don't check that the outputs of each method match.
27
28    skip_fail: Don't print anything for failed methods.
29\<close>
30
31experiment begin
32  section \<open>Basic examples\<close>
33
34  lemma
35    "A \<Longrightarrow> B \<Longrightarrow> A \<or> B"
36    apply (time_methods
37            \<open>erule disjI1\<close>
38            \<open>erule disjI2\<close>)
39    done
40
41  text \<open>Give labels to methods:\<close>
42  lemma
43    "A \<Longrightarrow> B \<Longrightarrow> A \<or> B"
44    apply (time_methods
45            label: \<open>erule disjI1\<close>
46            "another label": \<open>erule disjI2\<close>)
47    done
48
49  text \<open>no_check prevents failing even if the method results differ.\<close>
50  lemma
51    "A \<Longrightarrow> B \<Longrightarrow> A \<or> B"
52    apply (time_methods (no_check)
53            \<open>rule disjI1\<close>
54            \<open>rule disjI2\<close>)
55    apply assumption
56    done
57
58  text \<open>
59    Fast and slow list reversals.
60  \<close>
61  lemma list_eval_rev_append:
62    "rev xs = rev xs @ []"
63    "rev [] @ ys = ys"
64    "rev (x # xs) @ ys = rev xs @ (x # ys)"
65    by auto
66
67  lemma "rev [0..100] = map ((-) 100) [0..100]"
68        "rev [0..200] = map ((-) 200) [0..200]"
69    text \<open>evaluate everything but @{term rev}\<close>
70    apply (all \<open>match conclusion in "rev x = y" for x y \<Rightarrow>
71                  \<open>rule subst[where t = x], simp add: upto.simps\<close>\<close>)
72    apply (all \<open>match conclusion in "rev x = y" for x y \<Rightarrow>
73                  \<open>rule subst[where t = y], simp add: upto.simps\<close>\<close>)
74
75    text \<open>evaluate @{term rev}\<close>
76    apply (time_methods
77            naive100: \<open>simp\<close>
78            slow100: \<open>simp only: rev.simps append.simps\<close>
79            fast100: \<open>subst list_eval_rev_append(1), simp only: list_eval_rev_append(2-3)\<close>
80          )
81    apply (time_methods
82            naive200: \<open>simp\<close>
83            slow200: \<open>simp only: rev.simps append.simps\<close>
84            fast200: \<open>subst list_eval_rev_append(1), simp only: list_eval_rev_append(2-3)\<close>
85          )
86    done
87
88  text \<open>
89    Fast and slow subsequence testing.
90  \<close>
91  lemma
92    "subseq (map ((*) 2) [1 ..  5]) [1 .. 10]"
93    "subseq (map ((*) 2) [1 ..  6]) [1 .. 12]"
94    "subseq (map ((*) 2) [1 ..  7]) [1 .. 14]"
95    "subseq (map ((*) 2) [1 ..  8]) [1 .. 16]"
96    apply (all \<open>match conclusion in "subseq x y" for x y \<Rightarrow>
97                  \<open>rule subst[where t = x], simp add: upto.simps,
98                   rule subst[where t = y], simp add: upto.simps\<close>\<close>)
99
100    apply (time_methods
101      "HOL simp": \<open>simp\<close>
102
103      "l4v simp": \<open>simp cong: if_cong cong del: if_weak_cong\<close>
104        \<comment> \<open>exponential time!\<close>
105      )+
106    done
107
108  text \<open>
109    Which method is a better SAT solver?
110    Instance 01 from the uf20-91 dataset at http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html
111  \<close>
112  lemma "\<exists>x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20.
113          (~x4 & x18 & ~x19) | (~x3 & ~x18 & x5) | (x5 & x8 & x15) | (x20 & ~x7 & x16) |
114          (~x10 & x13 & x7) | (x12 & x9 & ~x17) | (~x17 & ~x19 & ~x5) | (x16 & ~x9 & ~x15) |
115          (~x11 & x5 & x14) | (~x18 & x10 & ~x13) | (x3 & ~x11 & ~x12) | (x6 & x17 & x8) |
116          (x18 & ~x14 & ~x1) | (x19 & x15 & ~x10) | (~x12 & ~x18 & x19) | (x8 & ~x4 & ~x7) |
117          (x8 & x9 & ~x4) | (~x7 & ~x17 & x15) | (~x12 & x7 & x14) | (x10 & x11 & ~x8) |
118          (~x2 & x15 & x11) | (~x9 & ~x6 & ~x1) | (x11 & ~x20 & x17) | (~x9 & x15 & ~x13) |
119          (~x12 & x7 & x17) | (x18 & x2 & ~x20) | (~x20 & ~x12 & ~x4) | (~x19 & ~x11 & ~x14) |
120          (x16 & ~x18 & x4) | (x1 & x17 & x19) | (x13 & ~x15 & ~x10) | (x12 & x14 & x13) |
121          (~x12 & x14 & x7) | (x7 & ~x16 & ~x10) | (~x6 & ~x10 & ~x7) | (~x20 & ~x14 & x16) |
122          (x19 & ~x17 & ~x11) | (x7 & ~x1 & x20) | (x5 & ~x12 & ~x15) | (x4 & x9 & x13) |
123          (~x12 & x11 & x7) | (x5 & ~x19 & x8) | (~x1 & ~x16 & ~x17) | (~x20 & x14 & x15) |
124          (~x13 & x4 & ~x10) | (~x14 & ~x7 & ~x10) | (x5 & ~x9 & ~x20) | (~x10 & ~x1 & x19) |
125          (x16 & x15 & x1) | (~x16 & ~x3 & x11) | (x15 & x10 & ~x4) | (~x4 & x15 & x3) |
126          (x10 & x16 & ~x11) | (x8 & ~x12 & x5) | (~x14 & x6 & ~x12) | (~x1 & ~x6 & ~x11) |
127          (x13 & x5 & x1) | (x7 & x2 & ~x12) | (~x1 & x20 & ~x19) | (x2 & x13 & x8) |
128          (~x15 & ~x18 & ~x4) | (x11 & ~x14 & ~x9) | (x6 & x15 & x2) | (~x5 & x12 & x15) |
129          (x6 & ~x17 & ~x5) | (x13 & ~x5 & x19) | (~x20 & x1 & ~x14) | (~x9 & x17 & ~x15) |
130          (x5 & ~x19 & x18) | (x12 & ~x8 & x10) | (x18 & ~x14 & x4) | (~x15 & x9 & ~x13) |
131          (~x9 & x5 & x1) | (~x10 & x19 & x14) | (~x20 & ~x9 & ~x4) | (x9 & x2 & ~x19) |
132          (x5 & ~x13 & x17) | (~x2 & x10 & x18) | (x18 & ~x3 & ~x11) | (~x7 & x9 & ~x17) |
133          (x15 & x6 & x3) | (x2 & ~x3 & x13) | (~x12 & ~x3 & x2) | (x2 & x3 & ~x17) |
134          (~x20 & x15 & x16) | (x5 & x17 & x19) | (x20 & x18 & ~x11) | (x9 & ~x1 & x5) |
135          (x19 & ~x9 & ~x17) | (~x12 & x2 & ~x17)"
136    using [[meson_max_clauses=99]]
137    apply (time_methods
138              blast: \<open>blast\<close>
139              metis: \<open>metis\<close>
140              meson: \<open>meson\<close>
141              smt:   \<open>smt\<close>
142              force: \<open>force\<close>
143              fastforce: \<open>fastforce intro: ex_bool_eq[THEN iffD2]\<close>
144              fastforce: \<open>fastforce simp: ex_bool_eq\<close>
145              presburger: \<open>use ex_bool_eq[simp] in presburger\<close>
146          )
147    done
148
149  section \<open>Other tests\<close>
150
151  text \<open>Test ML interface\<close>
152  lemma "True"
153    apply (tactic \<open>
154            let val method = SIMPLE_METHOD (simp_tac @{context} 1)
155                fun dummy_callback _ _ = ()
156            in (fn st => Time_Methods.time_methods false false dummy_callback [(NONE, method)] [] st
157                      |> (fn ([timing], st') => (tracing (Timing.message timing); st')))
158               |> NO_CONTEXT_TACTIC @{context}
159            end\<close>)
160    done
161
162  text \<open>Check that we fail when the methods give different results\<close>
163  lemma
164    "A \<or> B"
165    apply (tactic \<open>
166      let
167        fun skip_dummy_state tac = fn st =>
168            case Thm.prop_of st of
169                Const ("Pure.prop", _) $ (Const ("Pure.term", _) $ Const ("Pure.dummy_pattern", _)) =>
170                  Seq.succeed st
171              | _ => tac st;
172        val methods = @{thms disjI1 disjI2}
173              |> map (fn rule => (NONE, SIMPLE_METHOD (resolve_tac @{context} [rule] 1)))
174        fun dummy_callback _ _ = ()
175      in (fn st => Time_Methods.time_methods false false dummy_callback methods [] st
176                   |> (fn (timing, st') => error "test failed: shouldn't reach here")
177                   handle THM _ => Seq.succeed (Seq.Result st)) (* should reach here *)
178         |> NO_CONTEXT_TACTIC @{context}
179         |> skip_dummy_state
180      end\<close>)
181    oops
182
183  text \<open>Check that we propagate failures from the input methods\<close>
184  lemma "A"
185    apply (fails \<open>time_methods \<open>simp\<close>\<close>)
186    oops
187
188  text \<open>Check that we skip failing methods when skip_fail set\<close>
189  lemma "A \<and> B \<Longrightarrow> A"
190    apply (
191        ( \<comment> \<open>roughly corresponds to "time_methods (skip_fail) \<open>fail\<close>",
192              but errors if it calls the output callback\<close>
193          tactic \<open>
194            let
195              fun timing_callback _ _ = error "test failed: shouldn't reach here"
196              val methods = [(NONE, SIMPLE_METHOD no_tac)]
197            in
198              (fn st =>
199                #2 (Time_Methods.time_methods false true timing_callback methods [] st))
200              |> NO_CONTEXT_TACTIC @{context}
201            end\<close>)
202      | time_methods (skip_fail) good_simp: \<open>simp\<close>)
203    done
204end
205
206end
207