1/*  Title:      Pure/PIDE/command.scala
2    Author:     Fabian Immler, TU Munich
3    Author:     Makarius
4
5Prover commands with accumulated results from execution.
6*/
7
8package isabelle
9
10
11import scala.collection.mutable
12import scala.collection.immutable.SortedMap
13
14
15object Command
16{
17  type Edit = (Option[Command], Option[Command])
18
19  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])]
20  type Blobs_Info = (List[Blob], Int)
21  val no_blobs: Blobs_Info = (Nil, -1)
22
23
24  /** accumulated results from prover **/
25
26  /* results */
27
28  object Results
29  {
30    type Entry = (Long, XML.Tree)
31    val empty: Results = new Results(SortedMap.empty)
32    def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
33    def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
34
35
36    /* XML data representation */
37
38    val encode: XML.Encode.T[Results] = (results: Results) =>
39    { import XML.Encode._; list(pair(long, tree))(results.rep.toList) }
40
41    val decode: XML.Decode.T[Results] = (body: XML.Body) =>
42    { import XML.Decode._; make(list(pair(long, tree))(body)) }
43  }
44
45  final class Results private(private val rep: SortedMap[Long, XML.Tree])
46  {
47    def is_empty: Boolean = rep.isEmpty
48    def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
49    def get(serial: Long): Option[XML.Tree] = rep.get(serial)
50    def iterator: Iterator[Results.Entry] = rep.iterator
51
52    def + (entry: Results.Entry): Results =
53      if (defined(entry._1)) this
54      else new Results(rep + entry)
55
56    def ++ (other: Results): Results =
57      if (this eq other) this
58      else if (rep.isEmpty) other
59      else (this /: other.iterator)(_ + _)
60
61    override def hashCode: Int = rep.hashCode
62    override def equals(that: Any): Boolean =
63      that match {
64        case other: Results => rep == other.rep
65        case _ => false
66      }
67    override def toString: String = iterator.mkString("Results(", ", ", ")")
68  }
69
70
71  /* exports */
72
73  object Exports
74  {
75    type Entry = (Long, Export.Entry)
76    val empty: Exports = new Exports(SortedMap.empty)
77    def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _)
78  }
79
80  final class Exports private(private val rep: SortedMap[Long, Export.Entry])
81  {
82    def is_empty: Boolean = rep.isEmpty
83    def iterator: Iterator[Exports.Entry] = rep.iterator
84
85    def + (entry: Exports.Entry): Exports =
86      if (rep.isDefinedAt(entry._1)) this
87      else new Exports(rep + entry)
88
89    def ++ (other: Exports): Exports =
90      if (this eq other) this
91      else if (rep.isEmpty) other
92      else (this /: other.iterator)(_ + _)
93
94    override def hashCode: Int = rep.hashCode
95    override def equals(that: Any): Boolean =
96      that match {
97        case other: Exports => rep == other.rep
98        case _ => false
99      }
100    override def toString: String = iterator.mkString("Exports(", ", ", ")")
101  }
102
103
104  /* markups */
105
106  object Markup_Index
107  {
108    val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default)
109  }
110
111  sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name)
112
113  object Markups
114  {
115    val empty: Markups = new Markups(Map.empty)
116    def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
117    def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
118
119
120    /* XML data representation */
121
122    def encode(source_length: Int): XML.Encode.T[Markups] = (markups: Markups) =>
123    {
124      import XML.Encode._
125
126      val markup_index: T[Markup_Index] = (index: Markup_Index) =>
127        pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name)
128
129      val markup_tree: T[Markup_Tree] =
130        _.to_XML(Text.Range(0, source_length), Symbol.spaces(source_length), Markup.Elements.full)
131
132      list(pair(markup_index, markup_tree))(markups.rep.toList)
133    }
134
135    val decode: XML.Decode.T[Markups] = (body: XML.Body) =>
136    {
137      import XML.Decode._
138
139      val markup_index: T[Markup_Index] = (body: XML.Body) =>
140      {
141        val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body)
142        Markup_Index(status, chunk_name)
143      }
144
145      (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _)
146    }
147  }
148
149  final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
150  {
151    def is_empty: Boolean = rep.isEmpty
152
153    def apply(index: Markup_Index): Markup_Tree =
154      rep.getOrElse(index, Markup_Tree.empty)
155
156    def add(index: Markup_Index, markup: Text.Markup): Markups =
157      new Markups(rep + (index -> (this(index) + markup)))
158
159    def + (entry: (Markup_Index, Markup_Tree)): Markups =
160    {
161      val (index, tree) = entry
162      new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full))))
163    }
164
165    def ++ (other: Markups): Markups =
166      if (this eq other) this
167      else if (rep.isEmpty) other
168      else (this /: other.rep.iterator)(_ + _)
169
170    def redirection_iterator: Iterator[Document_ID.Generic] =
171      for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
172        yield id
173
174    def redirect(other_id: Document_ID.Generic): Markups =
175    {
176      val rep1 =
177        (for {
178          (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator
179          if other_id == id
180        } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap
181      if (rep1.isEmpty) Markups.empty else new Markups(rep1)
182    }
183
184    override def hashCode: Int = rep.hashCode
185    override def equals(that: Any): Boolean =
186      that match {
187        case other: Markups => rep == other.rep
188        case _ => false
189      }
190    override def toString: String = rep.iterator.mkString("Markups(", ", ", ")")
191  }
192
193
194  /* state */
195
196  object State
197  {
198    def get_result(states: List[State], serial: Long): Option[XML.Tree] =
199      states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get)
200
201    def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] =
202      for {
203        serial <- Markup.Serial.unapply(props)
204        tree @ XML.Elem(_, body) <- get_result(states, serial)
205        if body.nonEmpty
206      } yield (serial -> tree)
207
208    def merge_results(states: List[State]): Results =
209      Results.merge(states.map(_.results))
210
211    def merge_exports(states: List[State]): Exports =
212      Exports.merge(states.map(_.exports))
213
214    def merge_markups(states: List[State]): Markups =
215      Markups.merge(states.map(_.markups))
216
217    def merge_markup(states: List[State], index: Markup_Index,
218        range: Text.Range, elements: Markup.Elements): Markup_Tree =
219      Markup_Tree.merge(states.map(_.markup(index)), range, elements)
220
221    def merge(command: Command, states: List[State]): State =
222      State(command, states.flatMap(_.status), merge_results(states),
223        merge_exports(states), merge_markups(states))
224
225
226    /* XML data representation */
227
228    val encode: XML.Encode.T[State] = (st: State) =>
229    {
230      import XML.Encode._
231
232      val command = st.command
233      val blobs_names = command.blobs_names.map(_.node)
234      val blobs_index = command.blobs_index
235      require(command.blobs_ok)
236
237      pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.encode,
238          pair(list(Markup.encode), pair(Results.encode, Markups.encode(command.source.length)))))))(
239        (command.id, (command.node_name.node, ((blobs_names, blobs_index), (command.span,
240          (st.status, (st.results, st.markups)))))))
241    }
242
243    def decode(node_name: String => Document.Node.Name): XML.Decode.T[State] = (body: XML.Body) =>
244    {
245      import XML.Decode._
246      val (id, (node, ((blobs_names, blobs_index), (span, (status, (results, markups)))))) =
247        pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.decode,
248          pair(list(Markup.decode), pair(Results.decode, Markups.decode))))))(body)
249
250      val blobs_info: Blobs_Info =
251        (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index)
252      val command = Command(id, node_name(node), blobs_info, span)
253      State(command, status, results, Exports.empty, markups)
254    }
255  }
256
257  sealed case class State(
258    command: Command,
259    status: List[Markup] = Nil,
260    results: Results = Results.empty,
261    exports: Exports = Exports.empty,
262    markups: Markups = Markups.empty)
263  {
264    def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
265    def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING)
266    def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
267
268    lazy val maybe_consolidated: Boolean =
269    {
270      var touched = false
271      var forks = 0
272      var runs = 0
273      for (markup <- status) {
274        markup.name match {
275          case Markup.FORKED => touched = true; forks += 1
276          case Markup.JOINED => forks -= 1
277          case Markup.RUNNING => touched = true; runs += 1
278          case Markup.FINISHED => runs -= 1
279          case _ =>
280        }
281      }
282      touched && forks == 0 && runs == 0
283    }
284
285    lazy val document_status: Document_Status.Command_Status =
286    {
287      val warnings =
288        if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2)))
289          List(Markup(Markup.WARNING, Nil))
290        else Nil
291      val errors =
292        if (results.iterator.exists(p => Protocol.is_error(p._2)))
293          List(Markup(Markup.ERROR, Nil))
294        else Nil
295      Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator)
296    }
297
298    def markup(index: Markup_Index): Markup_Tree = markups(index)
299
300    def redirect(other_command: Command): Option[State] =
301    {
302      val markups1 = markups.redirect(other_command.id)
303      if (markups1.is_empty) None
304      else Some(new State(other_command, markups = markups1))
305    }
306
307    private def add_status(st: Markup): State =
308      copy(status = st :: status)
309
310    private def add_result(entry: Results.Entry): State =
311      copy(results = results + entry)
312
313    def add_export(entry: Exports.Entry): Option[State] =
314      if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry))
315      else None
316
317    private def add_markup(
318      status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
319    {
320      val markups1 =
321        if (status || Document_Status.Command_Status.liberal_elements(m.info.name))
322          markups.add(Markup_Index(true, chunk_name), m)
323        else markups
324      copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
325    }
326
327    def accumulate(
328        self_id: Document_ID.Generic => Boolean,
329        other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
330        message: XML.Elem,
331        xml_cache: XML.Cache): State =
332      message match {
333        case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
334          (this /: msgs)((state, msg) =>
335            msg match {
336              case elem @ XML.Elem(markup, Nil) =>
337                state.
338                  add_status(markup).
339                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
340              case _ =>
341                Output.warning("Ignored status message: " + msg)
342                state
343            })
344
345        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
346          (this /: msgs)((state, msg) =>
347            {
348              def bad(): Unit = Output.warning("Ignored report message: " + msg)
349
350              msg match {
351                case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) =>
352
353                  val target =
354                    if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
355                      Some((chunk_name, command.chunks(chunk_name)))
356                    else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
357                    else None
358
359                  (target, atts) match {
360                    case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
361                      target_chunk.incorporate(symbol_range) match {
362                        case Some(range) =>
363                          val props = Position.purge(atts)
364                          val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
365                          state.add_markup(false, target_name, Text.Info(range, elem))
366                        case None => bad(); state
367                      }
368                    case _ =>
369                      // silently ignore excessive reports
370                      state
371                  }
372
373                case XML.Elem(Markup(name, atts), args)
374                if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
375                  val range = command.core_range
376                  val props = Position.purge(atts)
377                  val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
378                  state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem))
379
380                case _ => bad(); state
381              }
382            })
383        case XML.Elem(Markup(name, props), body) =>
384          props match {
385            case Markup.Serial(i) =>
386              val markup_message =
387                xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body))
388              val message_markup =
389                xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
390
391              var st = add_result(i -> markup_message)
392              if (Protocol.is_inlined(message)) {
393                for {
394                  (chunk_name, chunk) <- command.chunks.iterator
395                  range <- Protocol_Message.positions(
396                    self_id, command.span.position, chunk_name, chunk, message)
397                } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup))
398              }
399              st
400
401            case _ =>
402              Output.warning("Ignored message without serial number: " + message)
403              this
404          }
405      }
406  }
407
408
409
410  /** static content **/
411
412  /* make commands */
413
414  def apply(
415    id: Document_ID.Command,
416    node_name: Document.Node.Name,
417    blobs_info: Blobs_Info,
418    span: Command_Span.Span): Command =
419  {
420    val (source, span1) = span.compact_source
421    new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty)
422  }
423
424  val empty: Command =
425    Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty)
426
427  def unparsed(
428    id: Document_ID.Command,
429    source: String,
430    results: Results,
431    markup: Markup_Tree): Command =
432  {
433    val (source1, span1) = Command_Span.unparsed(source).compact_source
434    new Command(id, Document.Node.Name.empty, no_blobs, span1, source1, results, markup)
435  }
436
437  def text(source: String): Command =
438    unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
439
440  def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
441  {
442    val text = XML.content(body)
443    val markup = Markup_Tree.from_XML(body)
444    unparsed(id, text, results, markup)
445  }
446
447
448  /* perspective */
449
450  object Perspective
451  {
452    val empty: Perspective = Perspective(Nil)
453  }
454
455  sealed case class Perspective(commands: List[Command])  // visible commands in canonical order
456  {
457    def is_empty: Boolean = commands.isEmpty
458
459    def same(that: Perspective): Boolean =
460    {
461      val cmds1 = this.commands
462      val cmds2 = that.commands
463      require(!cmds1.exists(_.is_undefined))
464      require(!cmds2.exists(_.is_undefined))
465      cmds1.length == cmds2.length &&
466        (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
467    }
468  }
469
470
471  /* blobs: inlined errors and auxiliary files */
472
473  private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
474  {
475    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
476      toks match {
477        case (t1, i1) :: (t2, i2) :: rest =>
478          if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
479          else (t1, i1) :: clean((t2, i2) :: rest)
480        case _ => toks
481      }
482    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
483  }
484
485  private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
486    if (tokens.exists({ case (t, _) => t.is_command })) {
487      tokens.dropWhile({ case (t, _) => !t.is_command }).
488        collectFirst({ case (t, i) if t.is_embedded => (t.content, i) })
489    }
490    else None
491
492  def span_files(syntax: Outer_Syntax, span: Command_Span.Span): (List[String], Int) =
493    syntax.load_command(span.name) match {
494      case Some(exts) =>
495        find_file(clean_tokens(span.content)) match {
496          case Some((file, i)) =>
497            if (exts.isEmpty) (List(file), i)
498            else (exts.map(ext => file + "." + ext), i)
499          case None => (Nil, -1)
500        }
501      case None => (Nil, -1)
502    }
503
504  def blobs_info(
505    resources: Resources,
506    syntax: Outer_Syntax,
507    get_blob: Document.Node.Name => Option[Document.Blob],
508    can_import: Document.Node.Name => Boolean,
509    node_name: Document.Node.Name,
510    span: Command_Span.Span): Blobs_Info =
511  {
512    span.name match {
513      // inlined errors
514      case Thy_Header.THEORY =>
515        val reader = Scan.char_reader(Token.implode(span.content))
516        val imports_pos = resources.check_thy_reader(node_name, reader).imports_pos
517        val raw_imports =
518          try {
519            val read_imports = Thy_Header.read(reader, Token.Pos.none).imports
520            if (imports_pos.length == read_imports.length) read_imports else error("")
521          }
522          catch { case exn: Throwable => List.fill(imports_pos.length)("") }
523
524        val errors =
525          for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
526          yield {
527            val completion =
528              if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
529            val msg =
530              "Bad theory import " +
531                Markup.Path(import_name.node).markup(quote(import_name.toString)) +
532                Position.here(pos) + Completion.report_theories(pos, completion)
533            Exn.Exn(ERROR(msg)): Command.Blob
534          }
535        (errors, -1)
536
537      // auxiliary files
538      case _ =>
539        val (files, index) = span_files(syntax, span)
540        val blobs =
541          files.map(file =>
542            (Exn.capture {
543              val name = Document.Node.Name(resources.append(node_name, Path.explode(file)))
544              val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
545              (name, blob)
546            }).user_error)
547        (blobs, index)
548    }
549  }
550}
551
552
553final class Command private(
554    val id: Document_ID.Command,
555    val node_name: Document.Node.Name,
556    val blobs_info: Command.Blobs_Info,
557    val span: Command_Span.Span,
558    val source: String,
559    val init_results: Command.Results,
560    val init_markup: Markup_Tree)
561{
562  override def toString: String = id + "/" + span.kind.toString
563
564
565  /* classification */
566
567  def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span]
568  def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span
569
570  def is_undefined: Boolean = id == Document_ID.none
571  val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
572  val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
573
574  def potentially_initialized: Boolean = span.name == Thy_Header.THEORY
575
576
577  /* blobs */
578
579  def blobs: List[Command.Blob] = blobs_info._1
580  def blobs_index: Int = blobs_info._2
581
582  def blobs_ok: Boolean =
583    blobs.forall({ case Exn.Res(_) => true case _ => false })
584
585  def blobs_names: List[Document.Node.Name] =
586    for (Exn.Res((name, _)) <- blobs) yield name
587
588  def blobs_undefined: List[Document.Node.Name] =
589    for (Exn.Res((name, None)) <- blobs) yield name
590
591  def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] =
592    for (Exn.Res((name, Some((digest, _)))) <- blobs) yield (name, digest)
593
594  def blobs_changed(doc_blobs: Document.Blobs): Boolean =
595    blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false })
596
597
598  /* source chunks */
599
600  val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source)
601
602  val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
603    ((Symbol.Text_Chunk.Default -> chunk) ::
604      (for (Exn.Res((name, Some((_, file)))) <- blobs)
605        yield Symbol.Text_Chunk.File(name.node) -> file)).toMap
606
607  def length: Int = source.length
608  def range: Text.Range = chunk.range
609
610  val core_range: Text.Range =
611    Text.Range(0,
612      (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
613
614  def source(range: Text.Range): String = range.substring(source)
615
616
617  /* accumulated results */
618
619  val init_state: Command.State =
620    Command.State(this, results = init_results, markups = Command.Markups.init(init_markup))
621
622  val empty_state: Command.State = Command.State(this)
623}
624