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