src/Pure/Tools/simplifier_trace.scala
author Lars Hupel <lars.hupel@mytum.de>
Tue Feb 04 09:04:59 2014 +0000 (2014-02-04)
changeset 55316 885500f4aa6a
parent 54730 de2d99b459b3
child 55390 36550a4eac5e
permissions -rw-r--r--
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
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
lars@55316
     9
import scala.actors.Actor._
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
{
lars@55316
    16
lars@55316
    17
  import Markup.Simp_Trace_Item
lars@55316
    18
lars@55316
    19
lars@55316
    20
  /* replies to the prover */
lars@55316
    21
lars@55316
    22
  case class Answer private[Simplifier_Trace](val name: String, val string: String)
lars@55316
    23
lars@55316
    24
  object Answer
lars@55316
    25
  {
lars@55316
    26
lars@55316
    27
    object step
lars@55316
    28
    {
lars@55316
    29
      val skip = Answer("skip", "Skip")
lars@55316
    30
      val continue = Answer("continue", "Continue")
lars@55316
    31
      val continue_trace = Answer("continue_trace", "Continue (with full trace)")
lars@55316
    32
      val continue_passive = Answer("continue_passive", "Continue (without asking)")
lars@55316
    33
      val continue_disable = Answer("continue_disable", "Continue (without any trace)")
lars@55316
    34
lars@55316
    35
      val default = skip
lars@55316
    36
      val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
lars@55316
    37
    }
lars@55316
    38
lars@55316
    39
    object hint_fail
lars@55316
    40
    {
lars@55316
    41
      val exit = Answer("exit", "Exit")
lars@55316
    42
      val redo = Answer("redo", "Redo")
lars@55316
    43
lars@55316
    44
      val default = exit
lars@55316
    45
      val all = List(redo, exit)
lars@55316
    46
    }
lars@55316
    47
lars@55316
    48
  }
lars@55316
    49
lars@55316
    50
  val all_answers = Answer.step.all ++ Answer.hint_fail.all
lars@55316
    51
lars@55316
    52
lars@55316
    53
  /* GUI interaction */
lars@55316
    54
lars@55316
    55
  case object Event
lars@55316
    56
lars@55316
    57
lars@55316
    58
  /* manager actor */
lars@55316
    59
lars@55316
    60
  private case class Handle_Results(session: Session, id: Document_ID.Command, results: Command.Results)
lars@55316
    61
  private case class Generate_Trace(results: Command.Results)
lars@55316
    62
  private case class Cancel(serial: Long)
lars@55316
    63
  private object Clear_Memory
lars@55316
    64
  private object Stop
lars@55316
    65
  case class Reply(session: Session, serial: Long, answer: Answer)
lars@55316
    66
lars@55316
    67
  case class Question(data: Simp_Trace_Item.Data, answers: List[Answer], default_answer: Answer)
lars@55316
    68
lars@55316
    69
  case class Context(
lars@55316
    70
    last_serial: Long = 0L,
lars@55316
    71
    questions: SortedMap[Long, Question] = SortedMap.empty
lars@55316
    72
  )
lars@55316
    73
  {
lars@55316
    74
lars@55316
    75
    def +(q: Question): Context =
lars@55316
    76
      copy(questions = questions + ((q.data.serial, q)))
lars@55316
    77
lars@55316
    78
    def -(s: Long): Context =
lars@55316
    79
      copy(questions = questions - s)
lars@55316
    80
lars@55316
    81
    def with_serial(s: Long): Context =
lars@55316
    82
      copy(last_serial = Math.max(last_serial, s))
lars@55316
    83
lars@55316
    84
  }
lars@55316
    85
lars@55316
    86
  case class Trace(entries: List[Simp_Trace_Item.Data])
lars@55316
    87
lars@55316
    88
  case class Index(text: String, content: XML.Body)
lars@55316
    89
lars@55316
    90
  object Index
lars@55316
    91
  {
lars@55316
    92
    def of_data(data: Simp_Trace_Item.Data): Index =
lars@55316
    93
      Index(data.text, data.content)
lars@55316
    94
  }
lars@55316
    95
lars@55316
    96
  def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context =
lars@55316
    97
    (manager !? Handle_Results(session, id, results)).asInstanceOf[Context]
lars@55316
    98
lars@55316
    99
  def generate_trace(results: Command.Results): Trace =
lars@55316
   100
    (manager !? Generate_Trace(results)).asInstanceOf[Trace]
lars@55316
   101
lars@55316
   102
  def clear_memory() =
lars@55316
   103
    manager ! Clear_Memory
lars@55316
   104
lars@55316
   105
  def send_reply(session: Session, serial: Long, answer: Answer) =
lars@55316
   106
    manager ! Reply(session, serial, answer)
lars@55316
   107
lars@55316
   108
  private val manager = actor {
lars@55316
   109
    var contexts = Map.empty[Document_ID.Command, Context]
lars@55316
   110
lars@55316
   111
    var memory_children = Map.empty[Long, Set[Long]]
lars@55316
   112
    var memory = Map.empty[Index, Answer]
lars@55316
   113
lars@55316
   114
    def find_question(serial: Long): Option[(Document_ID.Command, Question)] =
lars@55316
   115
      contexts collectFirst {
lars@55316
   116
        case (id, context) if context.questions contains serial =>
lars@55316
   117
          (id, context.questions(serial))
lars@55316
   118
      }
lars@55316
   119
lars@55316
   120
    def do_cancel(serial: Long, id: Document_ID.Command)
lars@55316
   121
    {
lars@55316
   122
      // To save memory, we could try to remove empty contexts at this point.
lars@55316
   123
      // However, if a new serial gets attached to the same command_id after we deleted
lars@55316
   124
      // its context, its last_serial counter will start at 0 again, and we'll think the
lars@55316
   125
      // old serials are actually new
lars@55316
   126
      contexts += (id -> (contexts(id) - serial))
lars@55316
   127
    }
lars@55316
   128
lars@55316
   129
    def do_reply(session: Session, serial: Long, answer: Answer)
lars@55316
   130
    {
lars@55316
   131
      session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name)
lars@55316
   132
    }
lars@55316
   133
lars@55316
   134
    loop {
lars@55316
   135
      react {
lars@55316
   136
        case Handle_Results(session, id, results) =>
lars@55316
   137
          var new_context = contexts.getOrElse(id, Context())
lars@55316
   138
          var new_serial = new_context.last_serial
lars@55316
   139
lars@55316
   140
          for ((serial, result) <- results.entries if serial > new_context.last_serial)
lars@55316
   141
          {
lars@55316
   142
            result match {
lars@55316
   143
              case Simp_Trace_Item(markup, data) =>
lars@55316
   144
                import Simp_Trace_Item._
lars@55316
   145
lars@55316
   146
                memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
lars@55316
   147
lars@55316
   148
                markup match {
lars@55316
   149
lars@55316
   150
                  case STEP =>
lars@55316
   151
                    val index = Index.of_data(data)
lars@55316
   152
                    memory.get(index) match {
lars@55316
   153
                      case None =>
lars@55316
   154
                        new_context += Question(data, Answer.step.all, Answer.step.default)
lars@55316
   155
                      case Some(answer) =>
lars@55316
   156
                        do_reply(session, serial, answer)
lars@55316
   157
                    }
lars@55316
   158
lars@55316
   159
                  case HINT =>
lars@55316
   160
                    data.props match {
lars@55316
   161
                      case Markup.Success(false) =>
lars@55316
   162
                        results.get(data.parent) match {
lars@55316
   163
                          case Some(Simp_Trace_Item(STEP, _)) =>
lars@55316
   164
                            new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
lars@55316
   165
                          case _ =>
lars@55316
   166
                            // unknown, better send a default reply
lars@55316
   167
                            do_reply(session, data.serial, Answer.hint_fail.default)
lars@55316
   168
                        }
lars@55316
   169
                      case _ =>
lars@55316
   170
                    }
lars@55316
   171
lars@55316
   172
                  case IGNORE =>
lars@55316
   173
                    // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
lars@55316
   174
                    // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
lars@55316
   175
                    // to selectively purge the replies which have been memorized, going down from
lars@55316
   176
                    // the parent to all leaves.
lars@55316
   177
lars@55316
   178
                    @tailrec
lars@55316
   179
                    def purge(queue: Vector[Long]): Unit =
lars@55316
   180
                      queue match {
lars@55316
   181
                        case s +: rest =>
lars@55316
   182
                          for (Simp_Trace_Item(STEP, data) <- results.get(s))
lars@55316
   183
                            memory -= Index.of_data(data)
lars@55316
   184
                          val children = memory_children.getOrElse(s, Set.empty)
lars@55316
   185
                          memory_children -= s
lars@55316
   186
                          purge(rest ++ children.toVector)
lars@55316
   187
                        case _ =>
lars@55316
   188
                      }
lars@55316
   189
lars@55316
   190
                    purge(Vector(data.parent))
lars@55316
   191
lars@55316
   192
                  case _ =>
lars@55316
   193
                }
lars@55316
   194
lars@55316
   195
              case _ =>
lars@55316
   196
            }
lars@55316
   197
lars@55316
   198
            new_serial = serial
lars@55316
   199
          }
lars@55316
   200
lars@55316
   201
          new_context = new_context.with_serial(new_serial)
lars@55316
   202
          contexts += (id -> new_context)
lars@55316
   203
          reply(new_context)
lars@55316
   204
lars@55316
   205
        case Generate_Trace(results) =>
lars@55316
   206
          // Since there are potentially lots of trace messages, we do not cache them here again.
lars@55316
   207
          // Instead, everytime the trace is being requested, we re-assemble it based on the
lars@55316
   208
          // current results.
lars@55316
   209
lars@55316
   210
          val items =
lars@55316
   211
            for { (_, Simp_Trace_Item(_, data)) <- results.entries }
lars@55316
   212
              yield data
lars@55316
   213
lars@55316
   214
          reply(Trace(items.toList))
lars@55316
   215
lars@55316
   216
        case Cancel(serial) =>
lars@55316
   217
          find_question(serial) match {
lars@55316
   218
            case Some((id, _)) =>
lars@55316
   219
              do_cancel(serial, id)
lars@55316
   220
            case None =>
lars@55316
   221
              System.err.println("handle_cancel: unknown serial " + serial)
lars@55316
   222
          }
lars@55316
   223
lars@55316
   224
        case Clear_Memory =>
lars@55316
   225
          memory_children = Map.empty
lars@55316
   226
          memory = Map.empty
lars@55316
   227
lars@55316
   228
        case Stop =>
lars@55316
   229
          contexts = Map.empty
lars@55316
   230
          exit("Simplifier_Trace: manager actor stopped")
lars@55316
   231
lars@55316
   232
        case Reply(session, serial, answer) =>
lars@55316
   233
          find_question(serial) match {
lars@55316
   234
            case Some((id, Question(data, _, _))) =>
lars@55316
   235
              if (data.markup == Markup.Simp_Trace_Item.STEP)
lars@55316
   236
              {
lars@55316
   237
                val index = Index.of_data(data)
lars@55316
   238
                memory += (index -> answer)
lars@55316
   239
              }
lars@55316
   240
              do_cancel(serial, id)
lars@55316
   241
            case None =>
lars@55316
   242
              System.err.println("send_reply: unknown serial " + serial)
lars@55316
   243
          }
lars@55316
   244
lars@55316
   245
          do_reply(session, serial, answer)
lars@55316
   246
          session.trace_events.event(Event)
lars@55316
   247
lars@55316
   248
        case bad =>
lars@55316
   249
          System.err.println("context_manager: bad message " + bad)
lars@55316
   250
      }
lars@55316
   251
    }
lars@55316
   252
  }
lars@55316
   253
lars@55316
   254
lars@55316
   255
  /* protocol handler */
wenzelm@54730
   256
wenzelm@54730
   257
  class Handler extends Session.Protocol_Handler
wenzelm@54730
   258
  {
lars@55316
   259
    private def cancel(
lars@55316
   260
      prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
lars@55316
   261
      msg.properties match {
lars@55316
   262
        case Markup.Cancel_Simp_Trace(serial) =>
lars@55316
   263
          manager ! Cancel(serial)
lars@55316
   264
          true
lars@55316
   265
        case _ =>
lars@55316
   266
          false
lars@55316
   267
      }
lars@55316
   268
lars@55316
   269
    override def stop(prover: Session.Prover) =
lars@55316
   270
    {
lars@55316
   271
      manager ! Clear_Memory
lars@55316
   272
      manager ! Stop
lars@55316
   273
    }
lars@55316
   274
lars@55316
   275
    val functions = Map(
lars@55316
   276
      Markup.CANCEL_SIMP_TRACE -> cancel _)
wenzelm@54730
   277
  }
lars@55316
   278
wenzelm@54730
   279
}