src/Pure/Tools/simplifier_trace.scala
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 66461 0b55fbc51f76
permissions -rw-r--r--
tuned signature;
wenzelm@54730
     1
/*  Title:      Pure/Tools/simplifier_trace.scala
lars@55316
     2
    Author:     Lars Hupel
wenzelm@54730
     3
wenzelm@54730
     4
Interactive Simplifier trace.
wenzelm@54730
     5
*/
wenzelm@54730
     6
wenzelm@54730
     7
package isabelle
wenzelm@54730
     8
wenzelm@55553
     9
lars@55316
    10
import scala.annotation.tailrec
lars@55316
    11
import scala.collection.immutable.SortedMap
lars@55316
    12
wenzelm@54730
    13
wenzelm@54730
    14
object Simplifier_Trace
wenzelm@54730
    15
{
wenzelm@55553
    16
  /* trace items from the prover */
lars@55316
    17
wenzelm@55553
    18
  val TEXT = "text"
wenzelm@55553
    19
  val Text = new Properties.String(TEXT)
wenzelm@55553
    20
wenzelm@55553
    21
  val PARENT = "parent"
wenzelm@55553
    22
  val Parent = new Properties.Long(PARENT)
wenzelm@55553
    23
wenzelm@55553
    24
  val SUCCESS = "success"
wenzelm@55553
    25
  val Success = new Properties.Boolean(SUCCESS)
wenzelm@55553
    26
wenzelm@55553
    27
  val MEMORY = "memory"
wenzelm@55553
    28
  val Memory = new Properties.Boolean(MEMORY)
wenzelm@55553
    29
wenzelm@55553
    30
  object Item
wenzelm@55553
    31
  {
wenzelm@55553
    32
    case class Data(
wenzelm@55553
    33
      serial: Long, markup: String, text: String,
wenzelm@55553
    34
      parent: Long, props: Properties.T, content: XML.Body)
wenzelm@55553
    35
    {
wenzelm@55553
    36
      def memory: Boolean = Memory.unapply(props) getOrElse true
wenzelm@55553
    37
    }
wenzelm@55553
    38
wenzelm@55553
    39
    def unapply(tree: XML.Tree): Option[(String, Data)] =
wenzelm@55553
    40
      tree match {
wenzelm@55553
    41
        case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)),
wenzelm@55553
    42
          List(XML.Elem(Markup(markup, props), content)))
wenzelm@55553
    43
        if markup.startsWith("simp_trace_") =>  // FIXME proper comparison of string constants
wenzelm@55553
    44
          (props, props) match {
wenzelm@55553
    45
            case (Text(text), Parent(parent)) =>
wenzelm@55553
    46
              Some((markup, Data(serial, markup, text, parent, props, content)))
wenzelm@55553
    47
            case _ => None
wenzelm@55553
    48
          }
wenzelm@55553
    49
        case _ => None
wenzelm@55553
    50
      }
wenzelm@55553
    51
  }
lars@55316
    52
lars@55316
    53
lars@55316
    54
  /* replies to the prover */
lars@55316
    55
lars@55316
    56
  case class Answer private[Simplifier_Trace](val name: String, val string: String)
lars@55316
    57
lars@55316
    58
  object Answer
lars@55316
    59
  {
lars@55316
    60
    object step
lars@55316
    61
    {
lars@55316
    62
      val skip = Answer("skip", "Skip")
lars@55316
    63
      val continue = Answer("continue", "Continue")
lars@55316
    64
      val continue_trace = Answer("continue_trace", "Continue (with full trace)")
lars@55316
    65
      val continue_passive = Answer("continue_passive", "Continue (without asking)")
lars@55316
    66
      val continue_disable = Answer("continue_disable", "Continue (without any trace)")
lars@55316
    67
lars@55316
    68
      val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
lars@55316
    69
    }
lars@55316
    70
lars@55316
    71
    object hint_fail
lars@55316
    72
    {
lars@55316
    73
      val exit = Answer("exit", "Exit")
lars@55316
    74
      val redo = Answer("redo", "Redo")
lars@55316
    75
lars@55316
    76
      val all = List(redo, exit)
lars@55316
    77
    }
lars@55316
    78
  }
lars@55316
    79
wenzelm@55555
    80
  val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all
lars@55316
    81
lars@55316
    82
lars@55316
    83
  /* GUI interaction */
lars@55316
    84
lars@55316
    85
  case object Event
lars@55316
    86
lars@55316
    87
wenzelm@56718
    88
  /* manager thread */
lars@55316
    89
wenzelm@56717
    90
  private case class Handle_Results(
wenzelm@56718
    91
    session: Session, id: Document_ID.Command, results: Command.Results, slot: Promise[Context])
wenzelm@56718
    92
  private case class Generate_Trace(results: Command.Results, slot: Promise[Trace])
lars@55316
    93
  private case class Cancel(serial: Long)
lars@55316
    94
  private object Clear_Memory
lars@55316
    95
  case class Reply(session: Session, serial: Long, answer: Answer)
lars@55316
    96
wenzelm@57593
    97
  case class Question(data: Item.Data, answers: List[Answer])
lars@55316
    98
lars@55316
    99
  case class Context(
lars@55316
   100
    last_serial: Long = 0L,
wenzelm@56717
   101
    questions: SortedMap[Long, Question] = SortedMap.empty)
lars@55316
   102
  {
lars@55316
   103
    def +(q: Question): Context =
lars@55316
   104
      copy(questions = questions + ((q.data.serial, q)))
lars@55316
   105
lars@55316
   106
    def -(s: Long): Context =
lars@55316
   107
      copy(questions = questions - s)
lars@55316
   108
lars@55316
   109
    def with_serial(s: Long): Context =
lars@55316
   110
      copy(last_serial = Math.max(last_serial, s))
lars@55316
   111
  }
lars@55316
   112
wenzelm@55553
   113
  case class Trace(entries: List[Item.Data])
lars@55316
   114
lars@55316
   115
  case class Index(text: String, content: XML.Body)
lars@55316
   116
lars@55316
   117
  object Index
lars@55316
   118
  {
wenzelm@55553
   119
    def of_data(data: Item.Data): Index =
lars@55316
   120
      Index(data.text, data.content)
lars@55316
   121
  }
lars@55316
   122
lars@55316
   123
  def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context =
wenzelm@56718
   124
  {
wenzelm@56718
   125
    val slot = Future.promise[Context]
wenzelm@56718
   126
    manager.send(Handle_Results(session, id, results, slot))
wenzelm@56718
   127
    slot.join
wenzelm@56718
   128
  }
lars@55316
   129
lars@55316
   130
  def generate_trace(results: Command.Results): Trace =
wenzelm@56718
   131
  {
wenzelm@56718
   132
    val slot = Future.promise[Trace]
wenzelm@56718
   133
    manager.send(Generate_Trace(results, slot))
wenzelm@56718
   134
    slot.join
wenzelm@56718
   135
  }
lars@55316
   136
lars@55316
   137
  def clear_memory() =
wenzelm@56718
   138
    manager.send(Clear_Memory)
lars@55316
   139
lars@55316
   140
  def send_reply(session: Session, serial: Long, answer: Answer) =
wenzelm@56718
   141
    manager.send(Reply(session, serial, answer))
lars@55316
   142
wenzelm@66461
   143
  def make_manager: Consumer_Thread[Any] =
wenzelm@56718
   144
  {
lars@55316
   145
    var contexts = Map.empty[Document_ID.Command, Context]
lars@55316
   146
lars@55316
   147
    var memory_children = Map.empty[Long, Set[Long]]
lars@55316
   148
    var memory = Map.empty[Index, Answer]
lars@55316
   149
lars@55316
   150
    def find_question(serial: Long): Option[(Document_ID.Command, Question)] =
lars@55316
   151
      contexts collectFirst {
lars@55316
   152
        case (id, context) if context.questions contains serial =>
lars@55316
   153
          (id, context.questions(serial))
lars@55316
   154
      }
lars@55316
   155
lars@55316
   156
    def do_cancel(serial: Long, id: Document_ID.Command)
lars@55316
   157
    {
lars@55316
   158
      // To save memory, we could try to remove empty contexts at this point.
lars@55316
   159
      // However, if a new serial gets attached to the same command_id after we deleted
lars@55316
   160
      // its context, its last_serial counter will start at 0 again, and we'll think the
lars@55316
   161
      // old serials are actually new
lars@55316
   162
      contexts += (id -> (contexts(id) - serial))
lars@55316
   163
    }
lars@55316
   164
lars@55316
   165
    def do_reply(session: Session, serial: Long, answer: Answer)
lars@55316
   166
    {
wenzelm@56717
   167
      session.protocol_command(
wenzelm@63805
   168
        "Simplifier_Trace.reply", Value.Long(serial), answer.name)
lars@55316
   169
    }
lars@55316
   170
wenzelm@56718
   171
    Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)(
wenzelm@56718
   172
      consume = (arg: Any) =>
wenzelm@56718
   173
      {
wenzelm@56718
   174
        arg match {
wenzelm@56718
   175
          case Handle_Results(session, id, results, slot) =>
wenzelm@56718
   176
            var new_context = contexts.getOrElse(id, Context())
wenzelm@56718
   177
            var new_serial = new_context.last_serial
lars@55316
   178
wenzelm@56718
   179
            for ((serial, result) <- results.iterator if serial > new_context.last_serial)
wenzelm@56718
   180
            {
wenzelm@56718
   181
              result match {
wenzelm@56718
   182
                case Item(markup, data) =>
wenzelm@56718
   183
                  memory_children +=
wenzelm@56718
   184
                    (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
lars@55316
   185
wenzelm@56718
   186
                  markup match {
lars@55316
   187
wenzelm@56718
   188
                    case Markup.SIMP_TRACE_STEP =>
wenzelm@56718
   189
                      val index = Index.of_data(data)
wenzelm@56718
   190
                      memory.get(index) match {
wenzelm@56718
   191
                        case Some(answer) if data.memory =>
wenzelm@56718
   192
                          do_reply(session, serial, answer)
wenzelm@56718
   193
                        case _ =>
wenzelm@57593
   194
                          new_context += Question(data, Answer.step.all)
wenzelm@56718
   195
                      }
lars@55316
   196
wenzelm@56718
   197
                    case Markup.SIMP_TRACE_HINT =>
wenzelm@56718
   198
                      data.props match {
wenzelm@56718
   199
                        case Success(false) =>
wenzelm@56718
   200
                          results.get(data.parent) match {
wenzelm@56718
   201
                            case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
wenzelm@57593
   202
                              new_context += Question(data, Answer.hint_fail.all)
wenzelm@56718
   203
                            case _ =>
wenzelm@56718
   204
                              // unknown, better send a default reply
wenzelm@57593
   205
                              do_reply(session, data.serial, Answer.hint_fail.exit)
wenzelm@56718
   206
                          }
lars@55316
   207
                        case _ =>
lars@55316
   208
                      }
lars@55316
   209
wenzelm@56718
   210
                    case Markup.SIMP_TRACE_IGNORE =>
wenzelm@56718
   211
                      // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
wenzelm@56718
   212
                      // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
wenzelm@56718
   213
                      // to selectively purge the replies which have been memorized, going down from
wenzelm@56718
   214
                      // the parent to all leaves.
lars@55316
   215
wenzelm@56718
   216
                      @tailrec
wenzelm@56718
   217
                      def purge(queue: Vector[Long]): Unit =
wenzelm@56718
   218
                        queue match {
wenzelm@56718
   219
                          case s +: rest =>
wenzelm@56718
   220
                            for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
wenzelm@56718
   221
                              memory -= Index.of_data(data)
wenzelm@56718
   222
                            val children = memory_children.getOrElse(s, Set.empty)
wenzelm@56718
   223
                            memory_children -= s
wenzelm@56718
   224
                            purge(rest ++ children.toVector)
wenzelm@56718
   225
                          case _ =>
wenzelm@56718
   226
                        }
lars@55316
   227
wenzelm@56718
   228
                      purge(Vector(data.parent))
wenzelm@56718
   229
wenzelm@56718
   230
                    case _ =>
wenzelm@56718
   231
                  }
wenzelm@56718
   232
wenzelm@56718
   233
                case _ =>
wenzelm@56718
   234
              }
wenzelm@56718
   235
wenzelm@56718
   236
              new_serial = serial
lars@55316
   237
            }
lars@55316
   238
wenzelm@56718
   239
            new_context = new_context.with_serial(new_serial)
wenzelm@56718
   240
            contexts += (id -> new_context)
wenzelm@56718
   241
            slot.fulfill(new_context)
lars@55316
   242
wenzelm@56718
   243
          case Generate_Trace(results, slot) =>
wenzelm@56718
   244
            // Since there are potentially lots of trace messages, we do not cache them here again.
wenzelm@56718
   245
            // Instead, everytime the trace is being requested, we re-assemble it based on the
wenzelm@56718
   246
            // current results.
lars@55316
   247
wenzelm@56718
   248
            val items =
wenzelm@57593
   249
              results.iterator.collect { case (_, Item(_, data)) => data }.toList
lars@55316
   250
wenzelm@56718
   251
            slot.fulfill(Trace(items))
lars@55316
   252
wenzelm@56718
   253
          case Cancel(serial) =>
wenzelm@56718
   254
            find_question(serial) match {
wenzelm@56718
   255
              case Some((id, _)) =>
wenzelm@56718
   256
                do_cancel(serial, id)
wenzelm@56718
   257
              case None =>
wenzelm@56718
   258
            }
lars@55316
   259
wenzelm@56718
   260
          case Clear_Memory =>
wenzelm@56718
   261
            memory_children = Map.empty
wenzelm@56718
   262
            memory = Map.empty
lars@55316
   263
wenzelm@56718
   264
          case Reply(session, serial, answer) =>
wenzelm@56718
   265
            find_question(serial) match {
wenzelm@57593
   266
              case Some((id, Question(data, _))) =>
wenzelm@56718
   267
                if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
wenzelm@56718
   268
                {
wenzelm@56718
   269
                  val index = Index.of_data(data)
wenzelm@56718
   270
                  memory += (index -> answer)
wenzelm@56718
   271
                }
wenzelm@56718
   272
                do_cancel(serial, id)
wenzelm@56718
   273
              case None =>
wenzelm@56782
   274
                Output.warning("send_reply: unknown serial " + serial)
wenzelm@56718
   275
            }
lars@55316
   276
wenzelm@56718
   277
            do_reply(session, serial, answer)
wenzelm@56718
   278
            session.trace_events.post(Event)
wenzelm@56718
   279
        }
wenzelm@56718
   280
        true
wenzelm@56718
   281
      },
wenzelm@56718
   282
      finish = () => contexts = Map.empty
wenzelm@56718
   283
    )
lars@55316
   284
  }
lars@55316
   285
wenzelm@66461
   286
  private val manager_variable = Synchronized[Option[Consumer_Thread[Any]]](None)
wenzelm@66461
   287
wenzelm@66461
   288
  def manager: Consumer_Thread[Any] =
wenzelm@66461
   289
    manager_variable.value match {
wenzelm@66461
   290
      case Some(thread) if thread.is_active => thread
wenzelm@66461
   291
      case _ => error("Bad Simplifier_Trace.manager thread")
wenzelm@66461
   292
    }
wenzelm@66461
   293
lars@55316
   294
lars@55316
   295
  /* protocol handler */
wenzelm@54730
   296
wenzelm@54730
   297
  class Handler extends Session.Protocol_Handler
wenzelm@54730
   298
  {
wenzelm@66461
   299
    try { manager }
wenzelm@66461
   300
    catch { case ERROR(_) => manager_variable.change(_ => Some(make_manager)) }
wenzelm@56718
   301
wenzelm@65220
   302
    override def exit() =
wenzelm@65220
   303
    {
wenzelm@65220
   304
      manager.send(Clear_Memory)
wenzelm@65220
   305
      manager.shutdown()
wenzelm@66461
   306
      manager_variable.change(_ => None)
wenzelm@65220
   307
    }
wenzelm@65220
   308
wenzelm@65219
   309
    private def cancel(msg: Prover.Protocol_Output): Boolean =
lars@55316
   310
      msg.properties match {
wenzelm@55553
   311
        case Markup.Simp_Trace_Cancel(serial) =>
wenzelm@56718
   312
          manager.send(Cancel(serial))
lars@55316
   313
          true
lars@55316
   314
        case _ =>
lars@55316
   315
          false
lars@55316
   316
      }
lars@55316
   317
wenzelm@65219
   318
    val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel _)
wenzelm@54730
   319
  }
wenzelm@54730
   320
}