1/* Title: Pure/Tools/simplifier_trace.scala 2 Author: Lars Hupel 3 4Interactive Simplifier trace. 5*/ 6 7package isabelle 8 9 10import scala.annotation.tailrec 11import scala.collection.immutable.SortedMap 12 13 14object Simplifier_Trace 15{ 16 /* trace items from the prover */ 17 18 val TEXT = "text" 19 val Text = new Properties.String(TEXT) 20 21 val PARENT = "parent" 22 val Parent = new Properties.Long(PARENT) 23 24 val SUCCESS = "success" 25 val Success = new Properties.Boolean(SUCCESS) 26 27 val MEMORY = "memory" 28 val Memory = new Properties.Boolean(MEMORY) 29 30 object Item 31 { 32 case class Data( 33 serial: Long, markup: String, text: String, 34 parent: Long, props: Properties.T, content: XML.Body) 35 { 36 def memory: Boolean = Memory.unapply(props) getOrElse true 37 } 38 39 def unapply(tree: XML.Tree): Option[(String, Data)] = 40 tree match { 41 case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), 42 List(XML.Elem(Markup(markup, props), content))) 43 if markup.startsWith("simp_trace_") => // FIXME proper comparison of string constants 44 (props, props) match { 45 case (Text(text), Parent(parent)) => 46 Some((markup, Data(serial, markup, text, parent, props, content))) 47 case _ => None 48 } 49 case _ => None 50 } 51 } 52 53 54 /* replies to the prover */ 55 56 case class Answer private[Simplifier_Trace](val name: String, val string: String) 57 58 object Answer 59 { 60 object step 61 { 62 val skip = Answer("skip", "Skip") 63 val continue = Answer("continue", "Continue") 64 val continue_trace = Answer("continue_trace", "Continue (with full trace)") 65 val continue_passive = Answer("continue_passive", "Continue (without asking)") 66 val continue_disable = Answer("continue_disable", "Continue (without any trace)") 67 68 val all = List(continue, continue_trace, continue_passive, continue_disable, skip) 69 } 70 71 object hint_fail 72 { 73 val exit = Answer("exit", "Exit") 74 val redo = Answer("redo", "Redo") 75 76 val all = List(redo, exit) 77 } 78 } 79 80 val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all 81 82 83 /* GUI interaction */ 84 85 case object Event 86 87 88 /* manager thread */ 89 90 private case class Handle_Results( 91 session: Session, id: Document_ID.Command, results: Command.Results, slot: Promise[Context]) 92 private case class Generate_Trace(results: Command.Results, slot: Promise[Trace]) 93 private case class Cancel(serial: Long) 94 private object Clear_Memory 95 case class Reply(session: Session, serial: Long, answer: Answer) 96 97 case class Question(data: Item.Data, answers: List[Answer]) 98 99 case class Context( 100 last_serial: Long = 0L, 101 questions: SortedMap[Long, Question] = SortedMap.empty) 102 { 103 def +(q: Question): Context = 104 copy(questions = questions + ((q.data.serial, q))) 105 106 def -(s: Long): Context = 107 copy(questions = questions - s) 108 109 def with_serial(s: Long): Context = 110 copy(last_serial = Math.max(last_serial, s)) 111 } 112 113 case class Trace(entries: List[Item.Data]) 114 115 case class Index(text: String, content: XML.Body) 116 117 object Index 118 { 119 def of_data(data: Item.Data): Index = 120 Index(data.text, data.content) 121 } 122 123 def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context = 124 { 125 val slot = Future.promise[Context] 126 manager.send(Handle_Results(session, id, results, slot)) 127 slot.join 128 } 129 130 def generate_trace(results: Command.Results): Trace = 131 { 132 val slot = Future.promise[Trace] 133 manager.send(Generate_Trace(results, slot)) 134 slot.join 135 } 136 137 def clear_memory() = 138 manager.send(Clear_Memory) 139 140 def send_reply(session: Session, serial: Long, answer: Answer) = 141 manager.send(Reply(session, serial, answer)) 142 143 def make_manager: Consumer_Thread[Any] = 144 { 145 var contexts = Map.empty[Document_ID.Command, Context] 146 147 var memory_children = Map.empty[Long, Set[Long]] 148 var memory = Map.empty[Index, Answer] 149 150 def find_question(serial: Long): Option[(Document_ID.Command, Question)] = 151 contexts collectFirst { 152 case (id, context) if context.questions contains serial => 153 (id, context.questions(serial)) 154 } 155 156 def do_cancel(serial: Long, id: Document_ID.Command) 157 { 158 // To save memory, we could try to remove empty contexts at this point. 159 // However, if a new serial gets attached to the same command_id after we deleted 160 // its context, its last_serial counter will start at 0 again, and we'll think the 161 // old serials are actually new 162 contexts += (id -> (contexts(id) - serial)) 163 } 164 165 def do_reply(session: Session, serial: Long, answer: Answer) 166 { 167 session.protocol_command( 168 "Simplifier_Trace.reply", Value.Long(serial), answer.name) 169 } 170 171 Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)( 172 consume = (arg: Any) => 173 { 174 arg match { 175 case Handle_Results(session, id, results, slot) => 176 var new_context = contexts.getOrElse(id, Context()) 177 var new_serial = new_context.last_serial 178 179 for ((serial, result) <- results.iterator if serial > new_context.last_serial) 180 { 181 result match { 182 case Item(markup, data) => 183 memory_children += 184 (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial)) 185 186 markup match { 187 188 case Markup.SIMP_TRACE_STEP => 189 val index = Index.of_data(data) 190 memory.get(index) match { 191 case Some(answer) if data.memory => 192 do_reply(session, serial, answer) 193 case _ => 194 new_context += Question(data, Answer.step.all) 195 } 196 197 case Markup.SIMP_TRACE_HINT => 198 data.props match { 199 case Success(false) => 200 results.get(data.parent) match { 201 case Some(Item(Markup.SIMP_TRACE_STEP, _)) => 202 new_context += Question(data, Answer.hint_fail.all) 203 case _ => 204 // unknown, better send a default reply 205 do_reply(session, data.serial, Answer.hint_fail.exit) 206 } 207 case _ => 208 } 209 210 case Markup.SIMP_TRACE_IGNORE => 211 // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP' 212 // entry, and that that 'STEP' entry is about to be replayed. Hence, we need 213 // to selectively purge the replies which have been memorized, going down from 214 // the parent to all leaves. 215 216 @tailrec 217 def purge(queue: Vector[Long]): Unit = 218 queue match { 219 case s +: rest => 220 for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s)) 221 memory -= Index.of_data(data) 222 val children = memory_children.getOrElse(s, Set.empty) 223 memory_children -= s 224 purge(rest ++ children.toVector) 225 case _ => 226 } 227 228 purge(Vector(data.parent)) 229 230 case _ => 231 } 232 233 case _ => 234 } 235 236 new_serial = serial 237 } 238 239 new_context = new_context.with_serial(new_serial) 240 contexts += (id -> new_context) 241 slot.fulfill(new_context) 242 243 case Generate_Trace(results, slot) => 244 // Since there are potentially lots of trace messages, we do not cache them here again. 245 // Instead, everytime the trace is being requested, we re-assemble it based on the 246 // current results. 247 248 val items = 249 results.iterator.collect { case (_, Item(_, data)) => data }.toList 250 251 slot.fulfill(Trace(items)) 252 253 case Cancel(serial) => 254 find_question(serial) match { 255 case Some((id, _)) => 256 do_cancel(serial, id) 257 case None => 258 } 259 260 case Clear_Memory => 261 memory_children = Map.empty 262 memory = Map.empty 263 264 case Reply(session, serial, answer) => 265 find_question(serial) match { 266 case Some((id, Question(data, _))) => 267 if (data.markup == Markup.SIMP_TRACE_STEP && data.memory) 268 { 269 val index = Index.of_data(data) 270 memory += (index -> answer) 271 } 272 do_cancel(serial, id) 273 case None => 274 Output.warning("send_reply: unknown serial " + serial) 275 } 276 277 do_reply(session, serial, answer) 278 session.trace_events.post(Event) 279 } 280 true 281 }, 282 finish = () => contexts = Map.empty 283 ) 284 } 285 286 private val manager_variable = Synchronized[Option[Consumer_Thread[Any]]](None) 287 288 def manager: Consumer_Thread[Any] = 289 manager_variable.value match { 290 case Some(thread) if thread.is_active => thread 291 case _ => error("Bad Simplifier_Trace.manager thread") 292 } 293 294 295 /* protocol handler */ 296 297 class Handler extends Session.Protocol_Handler 298 { 299 try { manager } 300 catch { case ERROR(_) => manager_variable.change(_ => Some(make_manager)) } 301 302 override def exit() = 303 { 304 manager.send(Clear_Memory) 305 manager.shutdown() 306 manager_variable.change(_ => None) 307 } 308 309 private def cancel(msg: Prover.Protocol_Output): Boolean = 310 msg.properties match { 311 case Markup.Simp_Trace_Cancel(serial) => 312 manager.send(Cancel(serial)) 313 true 314 case _ => 315 false 316 } 317 318 val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel _) 319 } 320} 321