1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Apply_Debug_Test
8imports
9  Lib.Apply_Debug
10  Lib.Apply_Trace_Cmd
11begin
12
13chapter \<open>Apply_Debug\<close>
14
15text \<open>
16 Apply_debug can be invoked as a backwards refinement step (wherever "apply" works). It invokes
17 the given proof method (expression) in a managed thread and blocks when it encounters a special
18 "#break" method. Either this is written as part of the definition in an inner method written in Eisbach,
19 or appears directly in the invoked method.
20 Once a break point is hit, the proof thread blocks and the command returns with whatever the proof
21 state was at the breakpoint.
22
23 The provided "continue" command allows for execution to resume. Note that regular proof commands
24 can be written between continue commands and method execution will continue as if that were
25 the proof state at the break point. This can allow for debugging methods without necessarily rewriting
26 their implementation.
27
28 Some interactive markup is given in jEdit: clicking on
29 an apply_debug or continue command will show the subsequent breakpoint that was hit (and
30 the method in the original expression that hit it),
31 clicking on a breakpoint will highlight all "continue" commands which stopped at that breakpoint.
32 Note that breakpoints inside of Eisbach definitions are highlighted as well.
33
34 Finally the "finish" command will resume execution and ignore all further breakpoints.
35
36 Outside of an apply_debug invocation the #break method is ignored and any "continue" or "finish"
37 commands will throw a runtime error. The debug command that finally terminates the method
38 (either finish or continue) will exit the debugger and print "Final Result".
39\<close>
40
41
42method some_break = #break
43
44lemma assumes B: B
45  shows "A \<Longrightarrow> A \<and> B \<and> A \<and> A"
46  apply (rule conjI, #break, assumption) (* #break is ignored here *)
47  apply_debug (rule conjI, #break, some_break, #break, assumption?)+
48  continue
49  continue
50    apply (rule B) (* this effect is saved *)
51  continue
52  continue
53  apply assumption
54  finish
55  done
56
57section \<open>Tags\<close>
58
59text \<open>
60  Tags can be used to filter the kind of breakpoints that are hit by any given breakpoint
61  invocation. By default apply_debug will only hit untagged breakpoints, if any tags are given
62  then both untagged breakpoints and those matching the given tags will trigger a break.
63  Each breakpoint can be given 0 or 1 tags.
64\<close>
65
66method my_conjI = (#break "conjI", rule conjI)
67method my_assumption = (#break "assumption", assumption)
68
69lemma "A \<Longrightarrow> A \<and> A \<and> A \<and> A \<and> A"
70  apply_debug (my_conjI, my_assumption) (* no breakpoints hit *)
71
72  apply_debug (tags "assumption")
73    (#break, my_conjI, my_assumption) (* inline breakpoint *)
74    continue (* assumption breakpoint *)
75    finish (* goal finished *)
76
77  apply_debug (tags "conjI")
78    (my_conjI, my_assumption) (* conjI is hit *)
79  continue (* assumption breakpoint is skipped *)
80
81  apply_debug (tags "assumption", "conjI")
82    (my_conjI, my_assumption) (* conjI is hit *)
83  continue (* assumption is hit *)
84  finish
85  by assumption
86
87section \<open>Arguments to Continue Command\<close>
88
89text \<open>Continue can be given a single positive number that will skip over that many breakpoints.
90NB: continue 1 is the same as a bare continue.\<close>
91
92lemma
93  assumes AB: "A \<Longrightarrow> B"
94  assumes BA: "B \<Longrightarrow> A"
95  assumes BC: "B \<Longrightarrow> C"
96  assumes CB: "C \<Longrightarrow> B"
97  assumes CD: "C \<Longrightarrow> D"
98  assumes DC: "D \<Longrightarrow> C"
99  assumes DE: "D \<Longrightarrow> E"
100  assumes ED: "E \<Longrightarrow> D"
101  assumes FE: "F \<Longrightarrow> E"
102  assumes EF: "E \<Longrightarrow> F"
103  assumes E: "E"
104  shows
105  "A"
106
107  apply_debug ((((#break, rule assms, #break, rule assms,#break, rule assms, #break, rule assms, #break,
108                rule assms, #break, rule assms, #break, rule assms)));fail)
109
110  continue 3
111  continue 11
112  continue
113done
114
115text \<open>
116  Continue may also be given a method, which is understood as a filter on each breakpoint.
117  If the method successfully applies, then the breakpoint is hit and the result of executing the
118  method is left as the proof state. If it fails at a given breakpoint, it is ignored and execution
119  continues, either until the next breakpoint or until the method terminates.
120  NB: "finish" is equivalent to "continue fail".
121
122  Note that a breakpoint alone cannot fail or affect backtracking directly.
123\<close>
124
125lemma
126  assumes B: B and C: C
127  shows "A \<or> D \<or> (B \<and> C)"
128  apply_debug ((rule disjI1 disjI2, #break)+, rule conjI, #break)
129  continue (rule B) (* skip until conjI reveals B *)
130   apply (rule C)
131   finish
132  done
133
134
135section \<open>Element binding\<close>
136
137text \<open>
138 Inside of a "continue" block we can refer to Eisbach variables that are in the
139 lexographical scope of the associated breakpoint.
140 This includes arguments passed to Eisbach methods and variables that are bound inside of a
141 "match" body.
142\<close>
143
144named_theorems rule3
145
146method bazz for C :: int uses rule1 rule2 declares rule3 =
147  (match premises in H[OF rule2]:"PROP G" for G \<Rightarrow> \<open>#break\<close>)
148
149schematic_goal Z:
150  assumes AC: "A \<Longrightarrow> C"
151  assumes BA: "B \<Longrightarrow> A"
152  assumes AB: "A \<Longrightarrow> B"
153  assumes A: "A"
154  assumes rule1: "ZZZ"
155  assumes A: "A"
156  assumes C
157  shows "(A \<Longrightarrow> ?C) \<Longrightarrow> D \<Longrightarrow> A \<and> B \<and> C"
158
159  apply (intro conjI)
160  prefer 2
161
162  apply_debug (match premises in H:"PROP C" for C \<Rightarrow>
163        \<open>#break, bazz 4 rule1: AB rule2: A\<close>)
164    term ?C (* C from match is bound *)
165    thm H (* H is bound as the (focused) fact proving C *)
166    continue (* inside bazz method now *)
167    term ?C (* C is now argument to bazz *)
168    term ?G (* G is bound from inner match from bazz *)
169    thm rule1 (* bound to AB from call site *)
170    thm rule2 (* bound to A from call site *)
171    thm H (* bound to match result from bazz (shadows original H) *)
172    finish
173 oops
174
175section \<open>Tracing used rules\<close>
176
177text \<open>
178 We can observe any used rules between breakpoints by passing apply_debug the "trace" flag. This
179 implicitly invokes apply_trace after each continue, showing the rules that have been used since
180 the last breakpoint. Note that this is subject to backtracking, so any rules that were used
181 as part of a backtracking branch that has since been discarded will not appear.
182\<close>
183
184lemma assumes A: A and B: B
185  shows "A \<and> B"
186  apply_debug (trace) ((rule conjI | rule A B), #break)+
187  continue
188  continue
189  finish
190  done
191
192text \<open>
193 The trace flag can be passed an argument string (in a cartouche) which accepts the same syntax
194 as find_theorems. This will filter the list of all used theorems shown.
195\<close>
196
197lemma assumes A: A and B: B
198  shows "A \<and> B"
199  apply_debug (trace \<open>"_ \<and> _"\<close>) ((rule conjI | rule A B), #break)+
200  continue
201  finish
202  done
203
204section \<open>Show currently-executing method\<close>
205
206text \<open>
207 Internally, apply_debug manages a proof thread that is restarted periodically depending on
208 how far along it is in its execution when "continue" is invoked. This allows us to seamlessly
209 interact with it in jEdit where we might want to rewind time by editing a previous continue
210 statement.
211
212 We can observe this internal state by passing the flag "show_running" to apply_debug, which
213 will give jEdit markup to show which method is currently being executed by the internal thread.
214 Note that this is not necessarily the "continue" that is currently in focus in jEdit.
215
216 This can be particularly useful to discover which method is causing the whole execution to fail
217 or time out (even in the absence of any breakpoints).
218
219 In the following example, try making whitespace edits to the continues to see how the proof thread
220 is affected.
221\<close>
222
223
224lemma "A \<Longrightarrow> A \<and> A \<and> A \<and> A"
225  apply_debug (show_running)
226               (rule conjI,
227               sleep 0.1, #break, sleep 0.1, assumption, sleep 0.1, #break, sleep 0.1, rule conjI,
228               sleep 0.1, #break,
229               assumption, sleep 0.1, #break, sleep 0.1, rule conjI, sleep 0.1, #break, sleep 0.1,
230               assumption)
231  continue
232  continue
233  continue
234  continue
235  continue
236  apply assumption
237  done
238
239section \<open>Final Notes\<close>
240
241text \<open>
242 Breakpoints are subject to the real execution path of the method, which includes all backtracking
243 branches. This can result in potentially confusing traces when, for example, we see the same proof
244 state revisited multiple times.
245\<close>
246
247text \<open>
248 Only the "raw" proof state is lifted when continuing from a breakpoint: any additional context
249 information (e.g. from supply or other Isar commands) is discarded.
250\<close>
251
252text \<open>
253 The jEdit markup is limited in its ability to descend into higher-order method syntax (e.g. in match).
254 The highlighted breakpoint/currently executing method will therefore simply show an entire match
255 execution being executed, rather than any particular sub-method. This is not a fundamental
256 limitation, but requires more cooperation from the Method module to make the method stack trace
257 known as context data.
258\<close>
259
260end
261