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