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