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