1/*  Title:      Pure/Tools/simplifier_trace.scala
2    Author:     Lars Hupel
3
4Interactive Simplifier trace.
5*/
6
7package isabelle
8
9
10import scala.annotation.tailrec
11import scala.collection.immutable.SortedMap
12
13
14object 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}
321