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