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