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