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