src/Pure/Tools/simplifier_trace.scala
author wenzelm
Fri Apr 25 13:29:56 2014 +0200 (2014-04-25)
changeset 56718 096139bcfadd
parent 56717 d96b10ec397c
child 56782 433cf57550fa
permissions -rw-r--r--
replaced manager Actor by Consumer_Thread, which is lazy to defer its start to actual Handler init time;
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 default = skip
lars@55316
    69
      val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
lars@55316
    70
    }
lars@55316
    71
lars@55316
    72
    object hint_fail
lars@55316
    73
    {
lars@55316
    74
      val exit = Answer("exit", "Exit")
lars@55316
    75
      val redo = Answer("redo", "Redo")
lars@55316
    76
lars@55316
    77
      val default = exit
lars@55316
    78
      val all = List(redo, exit)
lars@55316
    79
    }
lars@55316
    80
  }
lars@55316
    81
wenzelm@55555
    82
  val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all
lars@55316
    83
wenzelm@55553
    84
  object Active
wenzelm@55553
    85
  {
wenzelm@55553
    86
    def unapply(tree: XML.Tree): Option[(Long, Answer)] =
wenzelm@55553
    87
      tree match {
wenzelm@55553
    88
        case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) =>
wenzelm@55553
    89
          (props, props) match {
wenzelm@55553
    90
            case (Markup.Serial(serial), Markup.Name(name)) =>
wenzelm@55553
    91
              all_answers.find(_.name == name).map((serial, _))
wenzelm@55553
    92
            case _ => None
wenzelm@55553
    93
          }
wenzelm@55553
    94
        case _ => None
wenzelm@55553
    95
      }
wenzelm@55553
    96
  }
wenzelm@55553
    97
lars@55316
    98
lars@55316
    99
  /* GUI interaction */
lars@55316
   100
lars@55316
   101
  case object Event
lars@55316
   102
lars@55316
   103
wenzelm@56718
   104
  /* manager thread */
lars@55316
   105
wenzelm@56717
   106
  private case class Handle_Results(
wenzelm@56718
   107
    session: Session, id: Document_ID.Command, results: Command.Results, slot: Promise[Context])
wenzelm@56718
   108
  private case class Generate_Trace(results: Command.Results, slot: Promise[Trace])
lars@55316
   109
  private case class Cancel(serial: Long)
lars@55316
   110
  private object Clear_Memory
lars@55316
   111
  case class Reply(session: Session, serial: Long, answer: Answer)
lars@55316
   112
wenzelm@55553
   113
  case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
lars@55316
   114
lars@55316
   115
  case class Context(
lars@55316
   116
    last_serial: Long = 0L,
wenzelm@56717
   117
    questions: SortedMap[Long, Question] = SortedMap.empty)
lars@55316
   118
  {
lars@55316
   119
    def +(q: Question): Context =
lars@55316
   120
      copy(questions = questions + ((q.data.serial, q)))
lars@55316
   121
lars@55316
   122
    def -(s: Long): Context =
lars@55316
   123
      copy(questions = questions - s)
lars@55316
   124
lars@55316
   125
    def with_serial(s: Long): Context =
lars@55316
   126
      copy(last_serial = Math.max(last_serial, s))
lars@55316
   127
  }
lars@55316
   128
wenzelm@55553
   129
  case class Trace(entries: List[Item.Data])
lars@55316
   130
lars@55316
   131
  case class Index(text: String, content: XML.Body)
lars@55316
   132
lars@55316
   133
  object Index
lars@55316
   134
  {
wenzelm@55553
   135
    def of_data(data: Item.Data): Index =
lars@55316
   136
      Index(data.text, data.content)
lars@55316
   137
  }
lars@55316
   138
lars@55316
   139
  def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context =
wenzelm@56718
   140
  {
wenzelm@56718
   141
    val slot = Future.promise[Context]
wenzelm@56718
   142
    manager.send(Handle_Results(session, id, results, slot))
wenzelm@56718
   143
    slot.join
wenzelm@56718
   144
  }
lars@55316
   145
lars@55316
   146
  def generate_trace(results: Command.Results): Trace =
wenzelm@56718
   147
  {
wenzelm@56718
   148
    val slot = Future.promise[Trace]
wenzelm@56718
   149
    manager.send(Generate_Trace(results, slot))
wenzelm@56718
   150
    slot.join
wenzelm@56718
   151
  }
lars@55316
   152
lars@55316
   153
  def clear_memory() =
wenzelm@56718
   154
    manager.send(Clear_Memory)
lars@55316
   155
lars@55316
   156
  def send_reply(session: Session, serial: Long, answer: Answer) =
wenzelm@56718
   157
    manager.send(Reply(session, serial, answer))
lars@55316
   158
wenzelm@56718
   159
  private lazy val manager: Consumer_Thread[Any] =
wenzelm@56718
   160
  {
lars@55316
   161
    var contexts = Map.empty[Document_ID.Command, Context]
lars@55316
   162
lars@55316
   163
    var memory_children = Map.empty[Long, Set[Long]]
lars@55316
   164
    var memory = Map.empty[Index, Answer]
lars@55316
   165
lars@55316
   166
    def find_question(serial: Long): Option[(Document_ID.Command, Question)] =
lars@55316
   167
      contexts collectFirst {
lars@55316
   168
        case (id, context) if context.questions contains serial =>
lars@55316
   169
          (id, context.questions(serial))
lars@55316
   170
      }
lars@55316
   171
lars@55316
   172
    def do_cancel(serial: Long, id: Document_ID.Command)
lars@55316
   173
    {
lars@55316
   174
      // To save memory, we could try to remove empty contexts at this point.
lars@55316
   175
      // However, if a new serial gets attached to the same command_id after we deleted
lars@55316
   176
      // its context, its last_serial counter will start at 0 again, and we'll think the
lars@55316
   177
      // old serials are actually new
lars@55316
   178
      contexts += (id -> (contexts(id) - serial))
lars@55316
   179
    }
lars@55316
   180
lars@55316
   181
    def do_reply(session: Session, serial: Long, answer: Answer)
lars@55316
   182
    {
wenzelm@56717
   183
      session.protocol_command(
wenzelm@56717
   184
        "Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
lars@55316
   185
    }
lars@55316
   186
wenzelm@56718
   187
    Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)(
wenzelm@56718
   188
      consume = (arg: Any) =>
wenzelm@56718
   189
      {
wenzelm@56718
   190
        arg match {
wenzelm@56718
   191
          case Handle_Results(session, id, results, slot) =>
wenzelm@56718
   192
            var new_context = contexts.getOrElse(id, Context())
wenzelm@56718
   193
            var new_serial = new_context.last_serial
lars@55316
   194
wenzelm@56718
   195
            for ((serial, result) <- results.iterator if serial > new_context.last_serial)
wenzelm@56718
   196
            {
wenzelm@56718
   197
              result match {
wenzelm@56718
   198
                case Item(markup, data) =>
wenzelm@56718
   199
                  memory_children +=
wenzelm@56718
   200
                    (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
lars@55316
   201
wenzelm@56718
   202
                  markup match {
lars@55316
   203
wenzelm@56718
   204
                    case Markup.SIMP_TRACE_STEP =>
wenzelm@56718
   205
                      val index = Index.of_data(data)
wenzelm@56718
   206
                      memory.get(index) match {
wenzelm@56718
   207
                        case Some(answer) if data.memory =>
wenzelm@56718
   208
                          do_reply(session, serial, answer)
wenzelm@56718
   209
                        case _ =>
wenzelm@56718
   210
                          new_context += Question(data, Answer.step.all, Answer.step.default)
wenzelm@56718
   211
                      }
lars@55316
   212
wenzelm@56718
   213
                    case Markup.SIMP_TRACE_HINT =>
wenzelm@56718
   214
                      data.props match {
wenzelm@56718
   215
                        case Success(false) =>
wenzelm@56718
   216
                          results.get(data.parent) match {
wenzelm@56718
   217
                            case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
wenzelm@56718
   218
                              new_context +=
wenzelm@56718
   219
                                Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
wenzelm@56718
   220
                            case _ =>
wenzelm@56718
   221
                              // unknown, better send a default reply
wenzelm@56718
   222
                              do_reply(session, data.serial, Answer.hint_fail.default)
wenzelm@56718
   223
                          }
lars@55316
   224
                        case _ =>
lars@55316
   225
                      }
lars@55316
   226
wenzelm@56718
   227
                    case Markup.SIMP_TRACE_IGNORE =>
wenzelm@56718
   228
                      // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
wenzelm@56718
   229
                      // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
wenzelm@56718
   230
                      // to selectively purge the replies which have been memorized, going down from
wenzelm@56718
   231
                      // the parent to all leaves.
lars@55316
   232
wenzelm@56718
   233
                      @tailrec
wenzelm@56718
   234
                      def purge(queue: Vector[Long]): Unit =
wenzelm@56718
   235
                        queue match {
wenzelm@56718
   236
                          case s +: rest =>
wenzelm@56718
   237
                            for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
wenzelm@56718
   238
                              memory -= Index.of_data(data)
wenzelm@56718
   239
                            val children = memory_children.getOrElse(s, Set.empty)
wenzelm@56718
   240
                            memory_children -= s
wenzelm@56718
   241
                            purge(rest ++ children.toVector)
wenzelm@56718
   242
                          case _ =>
wenzelm@56718
   243
                        }
lars@55316
   244
wenzelm@56718
   245
                      purge(Vector(data.parent))
wenzelm@56718
   246
wenzelm@56718
   247
                    case _ =>
wenzelm@56718
   248
                  }
wenzelm@56718
   249
wenzelm@56718
   250
                case _ =>
wenzelm@56718
   251
              }
wenzelm@56718
   252
wenzelm@56718
   253
              new_serial = serial
lars@55316
   254
            }
lars@55316
   255
wenzelm@56718
   256
            new_context = new_context.with_serial(new_serial)
wenzelm@56718
   257
            contexts += (id -> new_context)
wenzelm@56718
   258
            slot.fulfill(new_context)
lars@55316
   259
wenzelm@56718
   260
          case Generate_Trace(results, slot) =>
wenzelm@56718
   261
            // Since there are potentially lots of trace messages, we do not cache them here again.
wenzelm@56718
   262
            // Instead, everytime the trace is being requested, we re-assemble it based on the
wenzelm@56718
   263
            // current results.
lars@55316
   264
wenzelm@56718
   265
            val items =
wenzelm@56718
   266
              (for { (_, Item(_, data)) <- results.iterator }
wenzelm@56718
   267
                yield data).toList
lars@55316
   268
wenzelm@56718
   269
            slot.fulfill(Trace(items))
lars@55316
   270
wenzelm@56718
   271
          case Cancel(serial) =>
wenzelm@56718
   272
            find_question(serial) match {
wenzelm@56718
   273
              case Some((id, _)) =>
wenzelm@56718
   274
                do_cancel(serial, id)
wenzelm@56718
   275
              case None =>
wenzelm@56718
   276
            }
lars@55316
   277
wenzelm@56718
   278
          case Clear_Memory =>
wenzelm@56718
   279
            memory_children = Map.empty
wenzelm@56718
   280
            memory = Map.empty
lars@55316
   281
wenzelm@56718
   282
          case Reply(session, serial, answer) =>
wenzelm@56718
   283
            find_question(serial) match {
wenzelm@56718
   284
              case Some((id, Question(data, _, _))) =>
wenzelm@56718
   285
                if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
wenzelm@56718
   286
                {
wenzelm@56718
   287
                  val index = Index.of_data(data)
wenzelm@56718
   288
                  memory += (index -> answer)
wenzelm@56718
   289
                }
wenzelm@56718
   290
                do_cancel(serial, id)
wenzelm@56718
   291
              case None =>
wenzelm@56718
   292
                System.err.println("send_reply: unknown serial " + serial)
wenzelm@56718
   293
            }
lars@55316
   294
wenzelm@56718
   295
            do_reply(session, serial, answer)
wenzelm@56718
   296
            session.trace_events.post(Event)
wenzelm@56718
   297
        }
wenzelm@56718
   298
        true
wenzelm@56718
   299
      },
wenzelm@56718
   300
      finish = () => contexts = Map.empty
wenzelm@56718
   301
    )
lars@55316
   302
  }
lars@55316
   303
lars@55316
   304
lars@55316
   305
  /* protocol handler */
wenzelm@54730
   306
wenzelm@54730
   307
  class Handler extends Session.Protocol_Handler
wenzelm@54730
   308
  {
wenzelm@56718
   309
    assert(manager.is_active)
wenzelm@56718
   310
wenzelm@56387
   311
    private def cancel(prover: Prover, msg: Prover.Protocol_Output): Boolean =
lars@55316
   312
      msg.properties match {
wenzelm@55553
   313
        case Markup.Simp_Trace_Cancel(serial) =>
wenzelm@56718
   314
          manager.send(Cancel(serial))
lars@55316
   315
          true
lars@55316
   316
        case _ =>
lars@55316
   317
          false
lars@55316
   318
      }
lars@55316
   319
wenzelm@56387
   320
    override def stop(prover: Prover) =
lars@55316
   321
    {
wenzelm@56718
   322
      manager.send(Clear_Memory)
wenzelm@56718
   323
      manager.shutdown()
lars@55316
   324
    }
lars@55316
   325
wenzelm@55553
   326
    val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _)
wenzelm@54730
   327
  }
wenzelm@54730
   328
}