1/* Title: Pure/PIDE/protocol.scala 2 Author: Makarius 3 4Protocol message formats for interactive proof documents. 5*/ 6 7package isabelle 8 9 10object Protocol 11{ 12 /* document editing */ 13 14 object Assign_Update 15 { 16 def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] = 17 try { 18 import XML.Decode._ 19 Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text))) 20 } 21 catch { 22 case ERROR(_) => None 23 case _: XML.Error => None 24 } 25 } 26 27 object Removed 28 { 29 def unapply(text: String): Option[List[Document_ID.Version]] = 30 try { 31 import XML.Decode._ 32 Some(list(long)(Symbol.decode_yxml(text))) 33 } 34 catch { 35 case ERROR(_) => None 36 case _: XML.Error => None 37 } 38 } 39 40 41 /* consolidation status */ 42 43 def maybe_consolidated(markups: List[Markup]): Boolean = 44 { 45 var touched = false 46 var forks = 0 47 var runs = 0 48 for (markup <- markups) { 49 markup.name match { 50 case Markup.FORKED => touched = true; forks += 1 51 case Markup.JOINED => forks -= 1 52 case Markup.RUNNING => touched = true; runs += 1 53 case Markup.FINISHED => runs -= 1 54 case _ => 55 } 56 } 57 touched && forks == 0 && runs == 0 58 } 59 60 61 /* command status */ 62 63 object Status 64 { 65 def make(markup_iterator: Iterator[Markup]): Status = 66 { 67 var touched = false 68 var accepted = false 69 var warned = false 70 var failed = false 71 var forks = 0 72 var runs = 0 73 for (markup <- markup_iterator) { 74 markup.name match { 75 case Markup.ACCEPTED => accepted = true 76 case Markup.FORKED => touched = true; forks += 1 77 case Markup.JOINED => forks -= 1 78 case Markup.RUNNING => touched = true; runs += 1 79 case Markup.FINISHED => runs -= 1 80 case Markup.WARNING | Markup.LEGACY => warned = true 81 case Markup.FAILED | Markup.ERROR => failed = true 82 case _ => 83 } 84 } 85 Status(touched, accepted, warned, failed, forks, runs) 86 } 87 88 val empty = make(Iterator.empty) 89 90 def merge(status_iterator: Iterator[Status]): Status = 91 if (status_iterator.hasNext) { 92 val status0 = status_iterator.next 93 (status0 /: status_iterator)(_ + _) 94 } 95 else empty 96 } 97 98 sealed case class Status( 99 private val touched: Boolean, 100 private val accepted: Boolean, 101 private val warned: Boolean, 102 private val failed: Boolean, 103 forks: Int, 104 runs: Int) 105 { 106 def + (that: Status): Status = 107 Status( 108 touched || that.touched, 109 accepted || that.accepted, 110 warned || that.warned, 111 failed || that.failed, 112 forks + that.forks, 113 runs + that.runs) 114 115 def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0)) 116 def is_running: Boolean = runs != 0 117 def is_warned: Boolean = warned 118 def is_failed: Boolean = failed 119 def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0 120 } 121 122 val proper_status_elements = 123 Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING, 124 Markup.FINISHED, Markup.FAILED) 125 126 val liberal_status_elements = 127 proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR 128 129 130 /* command timing */ 131 132 object Command_Timing 133 { 134 def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] = 135 props match { 136 case Markup.COMMAND_TIMING :: args => 137 (args, args) match { 138 case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing)) 139 case _ => None 140 } 141 case _ => None 142 } 143 } 144 145 146 /* theory timing */ 147 148 object Theory_Timing 149 { 150 def unapply(props: Properties.T): Option[(String, isabelle.Timing)] = 151 props match { 152 case Markup.THEORY_TIMING :: args => 153 (args, args) match { 154 case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing)) 155 case _ => None 156 } 157 case _ => None 158 } 159 } 160 161 162 /* node status */ 163 164 sealed case class Node_Status( 165 unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, 166 initialized: Boolean, consolidated: Boolean) 167 { 168 def ok: Boolean = failed == 0 169 def total: Int = unprocessed + running + warned + failed + finished 170 171 def json: JSON.Object.T = 172 JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed, 173 "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished, 174 "initialized" -> initialized, "consolidated" -> consolidated) 175 } 176 177 def node_status( 178 state: Document.State, 179 version: Document.Version, 180 name: Document.Node.Name): Node_Status = 181 { 182 val node = version.nodes(name) 183 184 var unprocessed = 0 185 var running = 0 186 var warned = 0 187 var failed = 0 188 var finished = 0 189 for (command <- node.commands.iterator) { 190 val states = state.command_states(version, command) 191 val status = Status.merge(states.iterator.map(_.protocol_status)) 192 193 if (status.is_running) running += 1 194 else if (status.is_failed) failed += 1 195 else if (status.is_warned) warned += 1 196 else if (status.is_finished) finished += 1 197 else unprocessed += 1 198 } 199 val initialized = state.node_initialized(version, name) 200 val consolidated = state.node_consolidated(version, name) 201 202 Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated) 203 } 204 205 206 /* node timing */ 207 208 sealed case class Node_Timing(total: Double, commands: Map[Command, Double]) 209 210 val empty_node_timing = Node_Timing(0.0, Map.empty) 211 212 def node_timing( 213 state: Document.State, 214 version: Document.Version, 215 node: Document.Node, 216 threshold: Double): Node_Timing = 217 { 218 var total = 0.0 219 var commands = Map.empty[Command, Double] 220 for { 221 command <- node.commands.iterator 222 st <- state.command_states(version, command) 223 } { 224 val command_timing = 225 (0.0 /: st.status)({ 226 case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds 227 case (timing, _) => timing 228 }) 229 total += command_timing 230 if (command_timing >= threshold) commands += (command -> command_timing) 231 } 232 Node_Timing(total, commands) 233 } 234 235 236 /* result messages */ 237 238 def is_result(msg: XML.Tree): Boolean = 239 msg match { 240 case XML.Elem(Markup(Markup.RESULT, _), _) => true 241 case _ => false 242 } 243 244 def is_tracing(msg: XML.Tree): Boolean = 245 msg match { 246 case XML.Elem(Markup(Markup.TRACING, _), _) => true 247 case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true 248 case _ => false 249 } 250 251 def is_state(msg: XML.Tree): Boolean = 252 msg match { 253 case XML.Elem(Markup(Markup.STATE, _), _) => true 254 case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true 255 case _ => false 256 } 257 258 def is_information(msg: XML.Tree): Boolean = 259 msg match { 260 case XML.Elem(Markup(Markup.INFORMATION, _), _) => true 261 case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true 262 case _ => false 263 } 264 265 def is_writeln(msg: XML.Tree): Boolean = 266 msg match { 267 case XML.Elem(Markup(Markup.WRITELN, _), _) => true 268 case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true 269 case _ => false 270 } 271 272 def is_warning(msg: XML.Tree): Boolean = 273 msg match { 274 case XML.Elem(Markup(Markup.WARNING, _), _) => true 275 case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true 276 case _ => false 277 } 278 279 def is_legacy(msg: XML.Tree): Boolean = 280 msg match { 281 case XML.Elem(Markup(Markup.LEGACY, _), _) => true 282 case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true 283 case _ => false 284 } 285 286 def is_error(msg: XML.Tree): Boolean = 287 msg match { 288 case XML.Elem(Markup(Markup.ERROR, _), _) => true 289 case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true 290 case _ => false 291 } 292 293 def is_inlined(msg: XML.Tree): Boolean = 294 !(is_result(msg) || is_tracing(msg) || is_state(msg)) 295 296 def is_exported(msg: XML.Tree): Boolean = 297 is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg) 298 299 300 /* breakpoints */ 301 302 object ML_Breakpoint 303 { 304 def unapply(tree: XML.Tree): Option[Long] = 305 tree match { 306 case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint) 307 case _ => None 308 } 309 } 310 311 312 /* dialogs */ 313 314 object Dialog_Args 315 { 316 def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] = 317 (props, props, props) match { 318 case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) => 319 Some((id, serial, result)) 320 case _ => None 321 } 322 } 323 324 object Dialog 325 { 326 def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] = 327 tree match { 328 case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) => 329 Some((id, serial, result)) 330 case _ => None 331 } 332 } 333 334 object Dialog_Result 335 { 336 def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem = 337 { 338 val props = Position.Id(id) ::: Markup.Serial(serial) 339 XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result))) 340 } 341 342 def unapply(tree: XML.Tree): Option[String] = 343 tree match { 344 case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result) 345 case _ => None 346 } 347 } 348} 349 350 351trait Protocol 352{ 353 /* protocol commands */ 354 355 def protocol_command_bytes(name: String, args: Bytes*): Unit 356 def protocol_command(name: String, args: String*): Unit 357 358 359 /* options */ 360 361 def options(opts: Options): Unit = 362 protocol_command("Prover.options", Symbol.encode_yxml(opts.encode)) 363 364 365 /* session base */ 366 367 private def encode_table(table: List[(String, String)]): String = 368 { 369 import XML.Encode._ 370 Symbol.encode_yxml(list(pair(string, string))(table)) 371 } 372 373 private def encode_list(lst: List[String]): String = 374 { 375 import XML.Encode._ 376 Symbol.encode_yxml(list(string)(lst)) 377 } 378 379 private def encode_sessions(lst: List[(String, Position.T)]): String = 380 { 381 import XML.Encode._ 382 Symbol.encode_yxml(list(pair(string, properties))(lst)) 383 } 384 385 def session_base(resources: Resources) 386 { 387 val base = resources.session_base.standard_path 388 protocol_command("Prover.init_session_base", 389 encode_sessions(base.known.sessions.toList), 390 encode_list(base.doc_names), 391 encode_table(base.global_theories.toList), 392 encode_list(base.loaded_theories.keys), 393 encode_table(base.dest_known_theories)) 394 } 395 396 397 /* interned items */ 398 399 def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit = 400 protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes) 401 402 def define_command(command: Command) 403 { 404 val blobs_yxml = 405 { 406 import XML.Encode._ 407 val encode_blob: T[Command.Blob] = 408 variant(List( 409 { case Exn.Res((a, b)) => 410 (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, 411 { case Exn.Exn(e) => (Nil, string(Exn.message(e))) })) 412 413 Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) 414 } 415 416 val toks = command.span.content 417 val toks_yxml = 418 { 419 import XML.Encode._ 420 val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) 421 Symbol.encode_yxml(list(encode_tok)(toks)) 422 } 423 424 protocol_command("Document.define_command", 425 (Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml :: 426 toks.map(tok => Symbol.encode(tok.source))): _*) 427 } 428 429 430 /* execution */ 431 432 def discontinue_execution(): Unit = 433 protocol_command("Document.discontinue_execution") 434 435 def cancel_exec(id: Document_ID.Exec): Unit = 436 protocol_command("Document.cancel_exec", Document_ID(id)) 437 438 439 /* document versions */ 440 441 def update(old_id: Document_ID.Version, new_id: Document_ID.Version, 442 edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name]) 443 { 444 val edits_yxml = 445 { 446 import XML.Encode._ 447 def id: T[Command] = (cmd => long(cmd.id)) 448 def encode_edit(name: Document.Node.Name) 449 : T[Document.Node.Edit[Command.Edit, Command.Perspective]] = 450 variant(List( 451 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, 452 { case Document.Node.Deps(header) => 453 val master_dir = File.standard_url(name.master_dir) 454 val imports = header.imports.map({ case (a, _) => a.node }) 455 val keywords = 456 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) }) 457 (Nil, 458 pair(string, pair(string, pair(list(string), pair(list(pair(string, 459 pair(pair(string, list(string)), list(string)))), list(string)))))( 460 (master_dir, (name.theory, (imports, (keywords, header.errors)))))) }, 461 { case Document.Node.Perspective(a, b, c) => 462 (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), 463 list(pair(id, pair(string, list(string))))(c.dest)) })) 464 def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => 465 { 466 val (name, edit) = node_edit 467 pair(string, encode_edit(name))(name.node, edit) 468 }) 469 Symbol.encode_yxml(encode_edits(edits)) 470 } 471 472 val consolidate_yxml = 473 { 474 import XML.Encode._ 475 Symbol.encode_yxml(list(string)(consolidate.map(_.node))) 476 } 477 478 protocol_command( 479 "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate_yxml) 480 } 481 482 def remove_versions(versions: List[Document.Version]) 483 { 484 val versions_yxml = 485 { import XML.Encode._ 486 Symbol.encode_yxml(list(long)(versions.map(_.id))) } 487 protocol_command("Document.remove_versions", versions_yxml) 488 } 489 490 491 /* dialog via document content */ 492 493 def dialog_result(serial: Long, result: String): Unit = 494 protocol_command("Document.dialog_result", Value.Long(serial), result) 495} 496