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