src/Pure/PIDE/protocol.scala
author wenzelm
Thu Apr 03 14:54:17 2014 +0200 (2014-04-03)
changeset 56387 d92eb5c3960d
parent 56372 fadb0fef09d7
child 56395 0546e036d1c0
permissions -rw-r--r--
more general prover operations;
     1 /*  Title:      Pure/PIDE/protocol.scala
     2     Author:     Makarius
     3 
     4 Protocol message formats for interactive proof documents.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object 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         val body = YXML.parse_body(text)
    20         Some(pair(long, list(pair(long, list(long))))(body))
    21       }
    22       catch {
    23         case ERROR(_) => None
    24         case _: XML.Error => None
    25       }
    26   }
    27 
    28   object Removed
    29   {
    30     def unapply(text: String): Option[List[Document_ID.Version]] =
    31       try {
    32         import XML.Decode._
    33         Some(list(long)(YXML.parse_body(text)))
    34       }
    35       catch {
    36         case ERROR(_) => None
    37         case _: XML.Error => None
    38       }
    39   }
    40 
    41 
    42   /* command status */
    43 
    44   object Status
    45   {
    46     def make(markup_iterator: Iterator[Markup]): Status =
    47     {
    48       var touched = false
    49       var accepted = false
    50       var failed = false
    51       var forks = 0
    52       var runs = 0
    53       for (markup <- markup_iterator) {
    54         markup.name match {
    55           case Markup.ACCEPTED => accepted = true
    56           case Markup.FORKED => touched = true; forks += 1
    57           case Markup.JOINED => forks -= 1
    58           case Markup.RUNNING => touched = true; runs += 1
    59           case Markup.FINISHED => runs -= 1
    60           case Markup.FAILED => failed = true
    61           case _ =>
    62         }
    63       }
    64       Status(touched, accepted, failed, forks, runs)
    65     }
    66 
    67     val empty = make(Iterator.empty)
    68 
    69     def merge(status_iterator: Iterator[Status]): Status =
    70       if (status_iterator.hasNext) {
    71         val status0 = status_iterator.next
    72         (status0 /: status_iterator)(_ + _)
    73       }
    74       else empty
    75   }
    76 
    77   sealed case class Status(
    78     private val touched: Boolean,
    79     private val accepted: Boolean,
    80     private val failed: Boolean,
    81     forks: Int,
    82     runs: Int)
    83   {
    84     def + (that: Status): Status =
    85       Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
    86         forks + that.forks, runs + that.runs)
    87 
    88     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
    89     def is_running: Boolean = runs != 0
    90     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    91     def is_failed: Boolean = failed
    92   }
    93 
    94   val command_status_elements =
    95     Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    96       Markup.FINISHED, Markup.FAILED)
    97 
    98   val status_elements =
    99     command_status_elements + Markup.WARNING + Markup.ERROR
   100 
   101 
   102   /* command timing */
   103 
   104   object Command_Timing
   105   {
   106     def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
   107       props match {
   108         case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
   109           (args, args) match {
   110             case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
   111             case _ => None
   112           }
   113         case _ => None
   114       }
   115   }
   116 
   117 
   118   /* node status */
   119 
   120   sealed case class Node_Status(
   121     unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int)
   122   {
   123     def total: Int = unprocessed + running + finished + warned + failed
   124   }
   125 
   126   def node_status(
   127     state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
   128   {
   129     var unprocessed = 0
   130     var running = 0
   131     var finished = 0
   132     var warned = 0
   133     var failed = 0
   134     for (command <- node.commands.iterator) {
   135       val states = state.command_states(version, command)
   136       val status = Status.merge(states.iterator.map(_.protocol_status))
   137 
   138       if (status.is_running) running += 1
   139       else if (status.is_finished) {
   140         val warning = states.exists(st => st.results.iterator.exists(p => is_warning(p._2)))
   141         if (warning) warned += 1 else finished += 1
   142       }
   143       else if (status.is_failed) failed += 1
   144       else unprocessed += 1
   145     }
   146     Node_Status(unprocessed, running, finished, warned, failed)
   147   }
   148 
   149 
   150   /* node timing */
   151 
   152   sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
   153 
   154   val empty_node_timing = Node_Timing(0.0, Map.empty)
   155 
   156   def node_timing(
   157     state: Document.State,
   158     version: Document.Version,
   159     node: Document.Node,
   160     threshold: Double): Node_Timing =
   161   {
   162     var total = 0.0
   163     var commands = Map.empty[Command, Double]
   164     for {
   165       command <- node.commands.iterator
   166       st <- state.command_states(version, command)
   167     } {
   168       val command_timing =
   169         (0.0 /: st.status)({
   170           case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
   171           case (timing, _) => timing
   172         })
   173       total += command_timing
   174       if (command_timing >= threshold) commands += (command -> command_timing)
   175     }
   176     Node_Timing(total, commands)
   177   }
   178 
   179 
   180   /* result messages */
   181 
   182   private val clean_elements =
   183     Document.Elements(Markup.REPORT, Markup.NO_REPORT)
   184 
   185   def clean_message(body: XML.Body): XML.Body =
   186     body filter {
   187       case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
   188       case XML.Elem(Markup(name, _), _) => !clean_elements(name)
   189       case _ => true
   190     } map {
   191       case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
   192       case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts))
   193       case t => t
   194     }
   195 
   196   def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
   197     body flatMap {
   198       case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
   199         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
   200       case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
   201         List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
   202       case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
   203       case XML.Elem(_, ts) => message_reports(props, ts)
   204       case XML.Text(_) => Nil
   205     }
   206 
   207 
   208   /* specific messages */
   209 
   210   def is_inlined(msg: XML.Tree): Boolean =
   211     !(is_result(msg) || is_tracing(msg) || is_state(msg))
   212 
   213   def is_result(msg: XML.Tree): Boolean =
   214     msg match {
   215       case XML.Elem(Markup(Markup.RESULT, _), _) => true
   216       case _ => false
   217     }
   218 
   219   def is_tracing(msg: XML.Tree): Boolean =
   220     msg match {
   221       case XML.Elem(Markup(Markup.TRACING, _), _) => true
   222       case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true
   223       case _ => false
   224     }
   225 
   226   def is_writeln_markup(msg: XML.Tree, name: String): Boolean =
   227     msg match {
   228       case XML.Elem(Markup(Markup.WRITELN, _),
   229         List(XML.Elem(markup, _))) => markup.name == name
   230       case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
   231         List(XML.Elem(markup, _))) => markup.name == name
   232       case _ => false
   233     }
   234 
   235   def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
   236   def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
   237 
   238   def is_warning(msg: XML.Tree): Boolean =
   239     msg match {
   240       case XML.Elem(Markup(Markup.WARNING, _), _) => true
   241       case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
   242       case _ => false
   243     }
   244 
   245   def is_error(msg: XML.Tree): Boolean =
   246     msg match {
   247       case XML.Elem(Markup(Markup.ERROR, _), _) => true
   248       case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
   249       case _ => false
   250     }
   251 
   252 
   253   /* dialogs */
   254 
   255   object Dialog_Args
   256   {
   257     def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] =
   258       (props, props, props) match {
   259         case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
   260           Some((id, serial, result))
   261         case _ => None
   262       }
   263   }
   264 
   265   object Dialog
   266   {
   267     def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] =
   268       tree match {
   269         case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
   270           Some((id, serial, result))
   271         case _ => None
   272       }
   273   }
   274 
   275   object Dialog_Result
   276   {
   277     def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem =
   278     {
   279       val props = Position.Id(id) ::: Markup.Serial(serial)
   280       XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
   281     }
   282 
   283     def unapply(tree: XML.Tree): Option[String] =
   284       tree match {
   285         case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
   286         case _ => None
   287       }
   288   }
   289 
   290 
   291   /* reported positions */
   292 
   293   private val position_elements =
   294     Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
   295 
   296   def message_positions(
   297     valid_id: Document_ID.Generic => Boolean,
   298     chunk: Command.Chunk,
   299     message: XML.Elem): Set[Text.Range] =
   300   {
   301     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
   302       props match {
   303         case Position.Reported(id, file_name, symbol_range)
   304         if valid_id(id) && file_name == chunk.file_name =>
   305           chunk.incorporate(symbol_range) match {
   306             case Some(range) => set + range
   307             case _ => set
   308           }
   309         case _ => set
   310       }
   311 
   312     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
   313       tree match {
   314         case XML.Wrapped_Elem(Markup(name, props), _, body) =>
   315           body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
   316         case XML.Elem(Markup(name, props), body) =>
   317           body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
   318         case XML.Text(_) => set
   319       }
   320 
   321     val set = positions(Set.empty, message)
   322     if (set.isEmpty) elem_positions(message.markup.properties, set)
   323     else set
   324   }
   325 }
   326 
   327 
   328 trait Protocol extends Prover
   329 {
   330   /* options */
   331 
   332   def options(opts: Options): Unit =
   333     protocol_command("Prover.options", YXML.string_of_body(opts.encode))
   334 
   335 
   336   /* interned items */
   337 
   338   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
   339     protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
   340 
   341   def define_command(command: Command): Unit =
   342   {
   343     val blobs_yxml =
   344     { import XML.Encode._
   345       val encode_blob: T[Command.Blob] =
   346         variant(List(
   347           { case Exn.Res((a, b)) =>
   348               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
   349           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
   350       YXML.string_of_body(list(encode_blob)(command.blobs))
   351     }
   352     protocol_command("Document.define_command",
   353       Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
   354   }
   355 
   356 
   357   /* execution */
   358 
   359   def discontinue_execution(): Unit =
   360     protocol_command("Document.discontinue_execution")
   361 
   362   def cancel_exec(id: Document_ID.Exec): Unit =
   363     protocol_command("Document.cancel_exec", Document_ID(id))
   364 
   365 
   366   /* document versions */
   367 
   368   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
   369     edits: List[Document.Edit_Command])
   370   {
   371     val edits_yxml =
   372     { import XML.Encode._
   373       def id: T[Command] = (cmd => long(cmd.id))
   374       def encode_edit(name: Document.Node.Name)
   375           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
   376         variant(List(
   377           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
   378           { case Document.Node.Deps(header) =>
   379               val master_dir = Isabelle_System.posix_path(name.master_dir)
   380               val imports = header.imports.map(_.node)
   381               val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
   382               (Nil,
   383                 pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
   384                   pair(list(pair(Encode.string,
   385                     option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
   386                   list(Encode.string)))))(
   387                 (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
   388           { case Document.Node.Perspective(a, b, c) =>
   389               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
   390                 list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
   391       def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
   392       {
   393         val (name, edit) = node_edit
   394         pair(string, encode_edit(name))(name.node, edit)
   395       })
   396       YXML.string_of_body(encode_edits(edits)) }
   397     protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
   398   }
   399 
   400   def remove_versions(versions: List[Document.Version])
   401   {
   402     val versions_yxml =
   403       { import XML.Encode._
   404         YXML.string_of_body(list(long)(versions.map(_.id))) }
   405     protocol_command("Document.remove_versions", versions_yxml)
   406   }
   407 
   408 
   409   /* dialog via document content */
   410 
   411   def dialog_result(serial: Long, result: String): Unit =
   412     protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
   413 }