interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
1.1 --- a/CONTRIBUTORS Tue Feb 04 01:35:48 2014 +0100
1.2 +++ b/CONTRIBUTORS Tue Feb 04 09:04:59 2014 +0000
1.3 @@ -6,6 +6,9 @@
1.4 Contributions to this Isabelle version
1.5 --------------------------------------
1.6
1.7 +* January 2014: Lars Hupel, TUM
1.8 + An improved, interactive simplifier trace with integration into the
1.9 + Isabelle/jEdit Prover IDE.
1.10
1.11 Contributions to Isabelle2013-1
1.12 -------------------------------
2.1 --- a/NEWS Tue Feb 04 01:35:48 2014 +0100
2.2 +++ b/NEWS Tue Feb 04 09:04:59 2014 +0000
2.3 @@ -37,6 +37,10 @@
2.4 process, without requiring old-fashioned command-line invocation of
2.5 "isabelle jedit -m MODE".
2.6
2.7 +* New panel: Simplifier trace. Provides an interactive view of the
2.8 +simplification process, enabled by the newly-introduced
2.9 +"simplifier_trace" declaration.
2.10 +
2.11
2.12 *** Pure ***
2.13
3.1 --- a/src/Pure/PIDE/markup.scala Tue Feb 04 01:35:48 2014 +0100
3.2 +++ b/src/Pure/PIDE/markup.scala Tue Feb 04 09:04:59 2014 +0000
3.3 @@ -273,7 +273,8 @@
3.4
3.5 /* messages */
3.6
3.7 - val Serial = new Properties.Long("serial")
3.8 + val SERIAL = "serial"
3.9 + val Serial = new Properties.Long(SERIAL)
3.10
3.11 val MESSAGE = "message"
3.12
3.13 @@ -386,6 +387,76 @@
3.14 case _ => None
3.15 }
3.16 }
3.17 +
3.18 + /* simplifier trace */
3.19 +
3.20 + val TEXT = "text"
3.21 + val Text = new Properties.String(TEXT)
3.22 +
3.23 + val PARENT = "parent"
3.24 + val Parent = new Properties.Long(PARENT)
3.25 +
3.26 + val SUCCESS = "success"
3.27 + val Success = new Properties.Boolean(SUCCESS)
3.28 +
3.29 + val CANCEL_SIMP_TRACE = "simp_trace_cancel"
3.30 + object Cancel_Simp_Trace
3.31 + {
3.32 + def unapply(props: Properties.T): Option[Long] =
3.33 + props match {
3.34 + case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
3.35 + case _ => None
3.36 + }
3.37 + }
3.38 +
3.39 + val SIMP_TRACE = "simp_trace"
3.40 + object Simp_Trace
3.41 + {
3.42 + def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] =
3.43 + tree match {
3.44 + case XML.Elem(Markup(SIMP_TRACE, props), _) =>
3.45 + (props, props) match {
3.46 + case (Serial(serial), Name(name)) =>
3.47 + Simplifier_Trace.all_answers.find(_.name == name).map((serial, _))
3.48 + case _ =>
3.49 + None
3.50 + }
3.51 + case _ =>
3.52 + None
3.53 + }
3.54 + }
3.55 +
3.56 + /* trace items from the prover */
3.57 +
3.58 + object Simp_Trace_Item
3.59 + {
3.60 +
3.61 + def unapply(tree: XML.Tree): Option[(String, Data)] =
3.62 + tree match {
3.63 + case XML.Elem(Markup(RESULT, Serial(serial)), List(
3.64 + XML.Elem(Markup(markup, props), content)
3.65 + )) if markup.startsWith("simp_trace_") =>
3.66 + (props, props) match {
3.67 + case (Text(text), Parent(parent)) =>
3.68 + Some((markup, Data(serial, markup, text, parent, props, content)))
3.69 + case _ =>
3.70 + None
3.71 + }
3.72 + case _ =>
3.73 + None
3.74 + }
3.75 +
3.76 + val LOG = "simp_trace_log"
3.77 + val STEP = "simp_trace_step"
3.78 + val RECURSE = "simp_trace_recurse"
3.79 + val HINT = "simp_trace_hint"
3.80 + val IGNORE = "simp_trace_ignore"
3.81 +
3.82 + case class Data(serial: Long, markup: String, text: String,
3.83 + parent: Long, props: Properties.T, content: XML.Body)
3.84 +
3.85 + }
3.86 +
3.87 }
3.88
3.89
4.1 --- a/src/Pure/System/session.scala Tue Feb 04 01:35:48 2014 +0100
4.2 +++ b/src/Pure/System/session.scala Tue Feb 04 09:04:59 2014 +0000
4.3 @@ -139,7 +139,7 @@
4.4 val syslog_messages = new Event_Bus[Isabelle_Process.Output]
4.5 val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
4.6 val all_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
4.7 -
4.8 + val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
4.9
4.10
4.11 /** buffered command changes (delay_first discipline) **/
5.1 --- a/src/Pure/Tools/simplifier_trace.ML Tue Feb 04 01:35:48 2014 +0100
5.2 +++ b/src/Pure/Tools/simplifier_trace.ML Tue Feb 04 09:04:59 2014 +0000
5.3 @@ -1,38 +1,435 @@
5.4 (* Title: Pure/Tools/simplifier_trace.ML
5.5 - Author: Lars Hupel, TU Muenchen
5.6 + Author: Lars Hupel
5.7
5.8 Interactive Simplifier trace.
5.9 *)
5.10
5.11 signature SIMPLIFIER_TRACE =
5.12 sig
5.13 - val simp_trace_test: bool Config.T
5.14 + val add_term_breakpoint: term -> Context.generic -> Context.generic
5.15 + val add_thm_breakpoint: thm -> Context.generic -> Context.generic
5.16 end
5.17
5.18 structure Simplifier_Trace: SIMPLIFIER_TRACE =
5.19 struct
5.20
5.21 -(* Simplifier trace operations *)
5.22 +(** background data **)
5.23
5.24 -val simp_trace_test =
5.25 - Attrib.setup_config_bool @{binding simp_trace_test} (K false)
5.26 +datatype mode = Disabled | Normal | Full
5.27 +
5.28 +fun merge_modes Disabled m = m
5.29 + | merge_modes Normal Full = Full
5.30 + | merge_modes Normal _ = Normal
5.31 + | merge_modes Full _ = Full
5.32 +
5.33 +val empty_breakpoints =
5.34 + (Item_Net.init (op =) single (* FIXME equality on terms? *),
5.35 + Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm))
5.36 +
5.37 +fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) =
5.38 + (Item_Net.merge (term_bs1, term_bs2),
5.39 + Item_Net.merge (thm_bs1, thm_bs2))
5.40 +
5.41 +structure Data = Generic_Data
5.42 +(
5.43 + type T =
5.44 + {max_depth: int,
5.45 + depth: int,
5.46 + mode: mode,
5.47 + interactive: bool,
5.48 + parent: int,
5.49 + breakpoints: term Item_Net.T * rrule Item_Net.T}
5.50 + val empty =
5.51 + {max_depth = 10,
5.52 + depth = 0,
5.53 + mode = Disabled,
5.54 + interactive = false,
5.55 + parent = 0,
5.56 + breakpoints = empty_breakpoints}
5.57 + val extend = I
5.58 + fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1,
5.59 + breakpoints = breakpoints1, ...},
5.60 + {max_depth = max_depth2, mode = mode2, interactive = interactive2,
5.61 + breakpoints = breakpoints2, ...}) =
5.62 + {max_depth = Int.max (max_depth1, max_depth2),
5.63 + depth = 0,
5.64 + mode = merge_modes mode1 mode2,
5.65 + interactive = interactive1 orelse interactive2,
5.66 + parent = 0,
5.67 + breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}
5.68 +)
5.69 +
5.70 +fun map_breakpoints f_term f_thm =
5.71 + Data.map (fn {max_depth, depth, mode, interactive, parent, breakpoints = (term_bs, thm_bs)} =>
5.72 + {max_depth = max_depth,
5.73 + depth = depth,
5.74 + mode = mode,
5.75 + interactive = interactive,
5.76 + parent = parent,
5.77 + breakpoints = (f_term term_bs, f_thm thm_bs)})
5.78 +
5.79 +fun add_term_breakpoint term =
5.80 + map_breakpoints (Item_Net.update term) I
5.81 +
5.82 +fun add_thm_breakpoint thm context =
5.83 + let
5.84 + val rrules = mk_rrules (Context.proof_of context) [thm]
5.85 + in
5.86 + map_breakpoints I (fold Item_Net.update rrules) context
5.87 + end
5.88 +
5.89 +fun is_breakpoint (term, rrule) context =
5.90 + let
5.91 + val {breakpoints, ...} = Data.get context
5.92 +
5.93 + fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term)
5.94 + val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term)
5.95 +
5.96 + val {thm = thm, ...} = rrule
5.97 + val thm_matches = exists (eq_rrule o pair rrule)
5.98 + (Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm))
5.99 + in
5.100 + (term_matches, thm_matches)
5.101 + end
5.102 +
5.103 +(** config and attributes **)
5.104 +
5.105 +fun config raw_mode interactive max_depth =
5.106 + let
5.107 + val mode = case raw_mode of
5.108 + "normal" => Normal
5.109 + | "full" => Full
5.110 + | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)
5.111 +
5.112 + val update = Data.map (fn {depth, parent, breakpoints, ...} =>
5.113 + {max_depth = max_depth,
5.114 + depth = depth,
5.115 + mode = mode,
5.116 + interactive = interactive,
5.117 + parent = parent,
5.118 + breakpoints = breakpoints})
5.119 + in Thm.declaration_attribute (K update) end
5.120 +
5.121 +fun term_breakpoint terms =
5.122 + Thm.declaration_attribute (K (fold add_term_breakpoint terms))
5.123 +
5.124 +val thm_breakpoint =
5.125 + Thm.declaration_attribute add_thm_breakpoint
5.126 +
5.127 +(** tracing state **)
5.128 +
5.129 +val futures =
5.130 + Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table)
5.131 +
5.132 +(** markup **)
5.133 +
5.134 +fun output_result (id, data) =
5.135 + Output.result (Markup.serial_properties id) data
5.136 +
5.137 +val serialN = "serial"
5.138 +val parentN = "parent"
5.139 +val textN = "text"
5.140 +val successN = "success"
5.141 +
5.142 +val logN = "simp_trace_log"
5.143 +val stepN = "simp_trace_step"
5.144 +val recurseN = "simp_trace_recurse"
5.145 +val hintN = "simp_trace_hint"
5.146 +val ignoreN = "simp_trace_ignore"
5.147 +
5.148 +val cancelN = "simp_trace_cancel"
5.149 +
5.150 +type payload =
5.151 + {props: Properties.T,
5.152 + pretty: Pretty.T}
5.153 +
5.154 +fun empty_payload () : payload =
5.155 + {props = [], pretty = Pretty.str ""}
5.156 +
5.157 +fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
5.158 + let
5.159 + val {max_depth, depth, mode, interactive, parent, ...} = Data.get (Context.Proof ctxt)
5.160 +
5.161 + val eligible =
5.162 + case mode of
5.163 + Disabled => false
5.164 + | Normal => triggered
5.165 + | Full => true
5.166 +
5.167 + val markup' = if markup = stepN andalso not interactive then logN else markup
5.168 + in
5.169 + if not eligible orelse depth > max_depth then
5.170 + NONE
5.171 + else
5.172 + let
5.173 + val {props = more_props, pretty} = payload ()
5.174 + val props =
5.175 + [(textN, text),
5.176 + (parentN, Markup.print_int parent)]
5.177 + val data =
5.178 + Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty])
5.179 + in
5.180 + SOME (serial (), data)
5.181 + end
5.182 + end
5.183 +
5.184 +(** tracing output **)
5.185 +
5.186 +fun send_request (result_id, content) =
5.187 + let
5.188 + fun break () =
5.189 + (Output.protocol_message
5.190 + [(Markup.functionN, cancelN),
5.191 + (serialN, Markup.print_int result_id)]
5.192 + "";
5.193 + Synchronized.change futures (Inttab.delete_safe result_id))
5.194 + val promise = Future.promise break : string future
5.195 + in
5.196 + Synchronized.change futures (Inttab.update_new (result_id, promise));
5.197 + output_result (result_id, content);
5.198 + promise
5.199 + end
5.200 +
5.201 +
5.202 +fun step {term, thm, unconditional, ctxt, rrule} =
5.203 + let
5.204 + val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt)
5.205 +
5.206 + val {name, ...} = rrule
5.207 + val term_triggered = not (null matching_terms)
5.208 +
5.209 + val text =
5.210 + if unconditional then
5.211 + "Apply rewrite rule?"
5.212 + else
5.213 + "Apply conditional rewrite rule?"
5.214 +
5.215 + fun payload () =
5.216 + let
5.217 + (* FIXME pretty printing via Proof_Context.pretty_fact *)
5.218 + val pretty_thm = Pretty.block
5.219 + [Pretty.str ("Instance of " ^ name ^ ":"),
5.220 + Pretty.brk 1,
5.221 + Syntax.pretty_term ctxt (Thm.prop_of thm)]
5.222 +
5.223 + val pretty_term = Pretty.block
5.224 + [Pretty.str "Trying to rewrite:",
5.225 + Pretty.brk 1,
5.226 + Syntax.pretty_term ctxt term]
5.227 +
5.228 + val pretty_matchings =
5.229 + let
5.230 + val items = map (Pretty.item o single o Syntax.pretty_term ctxt) matching_terms
5.231 + in
5.232 + if not (null matching_terms) then
5.233 + [Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))]
5.234 + else
5.235 + []
5.236 + end
5.237 +
5.238 + val pretty =
5.239 + Pretty.chunks ([pretty_thm, pretty_term] @ pretty_matchings)
5.240 + in
5.241 + {props = [], pretty = pretty}
5.242 + end
5.243 +
5.244 + val {max_depth, depth, mode, interactive, breakpoints, ...} =
5.245 + Data.get (Context.Proof ctxt)
5.246 +
5.247 + fun mk_promise result =
5.248 + let
5.249 + val result_id = #1 result
5.250 +
5.251 + fun put mode' interactive' = Data.put
5.252 + {max_depth = max_depth,
5.253 + depth = depth,
5.254 + mode = mode',
5.255 + interactive = interactive',
5.256 + parent = result_id,
5.257 + breakpoints = breakpoints} (Context.Proof ctxt) |>
5.258 + Context.the_proof
5.259 +
5.260 + fun to_response "skip" = NONE
5.261 + | to_response "continue" = SOME (put mode true)
5.262 + | to_response "continue_trace" = SOME (put Full true)
5.263 + | to_response "continue_passive" = SOME (put mode false)
5.264 + | to_response "continue_disable" = SOME (put Disabled false)
5.265 + | to_response _ = raise Fail "Simplifier_Trace.step: invalid message"
5.266 + in
5.267 + if not interactive then
5.268 + (output_result result; Future.value (SOME (put mode false)))
5.269 + else
5.270 + Future.map to_response (send_request result)
5.271 + end
5.272 +
5.273 + in
5.274 + case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of
5.275 + NONE => Future.value (SOME ctxt)
5.276 + | SOME res => mk_promise res
5.277 + end
5.278 +
5.279 +fun recurse text term ctxt =
5.280 + let
5.281 + fun payload () =
5.282 + {props = [],
5.283 + pretty = Syntax.pretty_term ctxt term}
5.284 +
5.285 + val {max_depth, depth, mode, interactive, breakpoints, ...} = Data.get (Context.Proof ctxt)
5.286 +
5.287 + fun put result_id = Data.put
5.288 + {max_depth = max_depth,
5.289 + depth = depth + 1,
5.290 + mode = if depth >= max_depth then Disabled else mode,
5.291 + interactive = interactive,
5.292 + parent = result_id,
5.293 + breakpoints = breakpoints} (Context.Proof ctxt)
5.294 +
5.295 + val context' =
5.296 + case mk_generic_result recurseN text true payload ctxt of
5.297 + NONE =>
5.298 + put 0
5.299 + | SOME res =>
5.300 + (output_result res; put (#1 res))
5.301 + in Context.the_proof context' end
5.302 +
5.303 +fun indicate_failure {term, ctxt, thm, rrule, ...} ctxt' =
5.304 + let
5.305 + fun payload () =
5.306 + let
5.307 + val {name, ...} = rrule
5.308 + val pretty_thm =
5.309 + (* FIXME pretty printing via Proof_Context.pretty_fact *)
5.310 + Pretty.block
5.311 + [Pretty.str ("In an instance of " ^ name ^ ":"),
5.312 + Pretty.brk 1,
5.313 + Syntax.pretty_term ctxt (Thm.prop_of thm)]
5.314 +
5.315 + val pretty_term =
5.316 + Pretty.block
5.317 + [Pretty.str "Was trying to rewrite:",
5.318 + Pretty.brk 1,
5.319 + Syntax.pretty_term ctxt term]
5.320 +
5.321 + val pretty =
5.322 + Pretty.chunks [pretty_thm, pretty_term]
5.323 + in
5.324 + {props = [(successN, "false")], pretty = pretty}
5.325 + end
5.326 +
5.327 + val {interactive, ...} = Data.get (Context.Proof ctxt)
5.328 + val {parent, ...} = Data.get (Context.Proof ctxt')
5.329 +
5.330 + fun mk_promise result =
5.331 + let
5.332 + val result_id = #1 result
5.333 +
5.334 + fun to_response "exit" =
5.335 + false
5.336 + | to_response "redo" =
5.337 + (Option.app output_result
5.338 + (mk_generic_result ignoreN "Ignore" true empty_payload ctxt');
5.339 + true)
5.340 + | to_response _ =
5.341 + raise Fail "Simplifier_Trace.indicate_failure: invalid message"
5.342 + in
5.343 + if not interactive then
5.344 + (output_result result; Future.value false)
5.345 + else
5.346 + Future.map to_response (send_request result)
5.347 + end
5.348 + in
5.349 + case mk_generic_result hintN "Step failed" true payload ctxt' of
5.350 + NONE => Future.value false
5.351 + | SOME res => mk_promise res
5.352 + end
5.353 +
5.354 +fun indicate_success thm ctxt =
5.355 + let
5.356 + fun payload () =
5.357 + {props = [(successN, "true")],
5.358 + pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)}
5.359 + in
5.360 + Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt)
5.361 + end
5.362 +
5.363 +(** setup **)
5.364 +
5.365 +fun simp_if_continue args ctxt cont =
5.366 + let
5.367 + val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args
5.368 + val data =
5.369 + {term = term,
5.370 + unconditional = unconditional,
5.371 + ctxt = ctxt,
5.372 + thm = thm,
5.373 + rrule = rrule}
5.374 + in
5.375 + case Future.join (step data) of
5.376 + NONE =>
5.377 + NONE
5.378 + | SOME ctxt' =>
5.379 + let val res = cont ctxt' in
5.380 + case res of
5.381 + NONE =>
5.382 + if Future.join (indicate_failure data ctxt') then
5.383 + simp_if_continue args ctxt cont
5.384 + else
5.385 + NONE
5.386 + | SOME (thm, _) =>
5.387 + (indicate_success thm ctxt';
5.388 + res)
5.389 + end
5.390 + end
5.391 +
5.392 +val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
5.393
5.394 val _ = Theory.setup
5.395 (Simplifier.set_trace_ops
5.396 - {trace_invoke = fn {depth, term} => fn ctxt =>
5.397 - (if Config.get ctxt simp_trace_test then
5.398 - tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^
5.399 - Syntax.string_of_term ctxt term)
5.400 - else (); ctxt),
5.401 - trace_apply = fn args => fn ctxt => fn cont =>
5.402 - (if Config.get ctxt simp_trace_test then
5.403 - tracing ("Simplifier " ^ @{make_string} args)
5.404 - else (); cont ctxt)})
5.405 + {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term,
5.406 + trace_apply = simp_if_continue})
5.407
5.408 +val _ =
5.409 + Isabelle_Process.protocol_command "Document.simp_trace_reply"
5.410 + (fn [s, r] =>
5.411 + let
5.412 + val serial = Markup.parse_int s
5.413 + fun lookup_delete tab =
5.414 + (Inttab.lookup tab serial, Inttab.delete_safe serial tab)
5.415 + fun apply_result (SOME promise) = Future.fulfill promise r
5.416 + | apply_result NONE = () (* FIXME handle protocol failure, just like in active.ML? *)
5.417 + in
5.418 + (Synchronized.change_result futures lookup_delete |> apply_result)
5.419 + handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn
5.420 + end)
5.421
5.422 -(* PIDE protocol *)
5.423 +(** attributes **)
5.424
5.425 -val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
5.426 +val pat_parser =
5.427 + Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic
5.428 +
5.429 +val mode_parser: string parser =
5.430 + Scan.optional
5.431 + (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full"))
5.432 + "normal"
5.433 +
5.434 +val interactive_parser: bool parser =
5.435 + Scan.optional (Args.$$$ "interactive" >> K true) false
5.436 +
5.437 +val depth_parser =
5.438 + Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10
5.439 +
5.440 +val config_parser =
5.441 + (interactive_parser -- mode_parser -- depth_parser) >>
5.442 + (fn ((interactive, mode), depth) => config mode interactive depth)
5.443 +
5.444 +val _ = Theory.setup
5.445 + (Attrib.setup @{binding break_term}
5.446 + ((Scan.repeat1 pat_parser) >> term_breakpoint)
5.447 + "declaration of a term breakpoint" #>
5.448 + Attrib.setup @{binding break_thm}
5.449 + (Scan.succeed thm_breakpoint)
5.450 + "declaration of a theorem breakpoint" #>
5.451 + Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
5.452 + "simplifier trace configuration")
5.453
5.454 end
5.455 -
6.1 --- a/src/Pure/Tools/simplifier_trace.scala Tue Feb 04 01:35:48 2014 +0100
6.2 +++ b/src/Pure/Tools/simplifier_trace.scala Tue Feb 04 09:04:59 2014 +0000
6.3 @@ -1,18 +1,279 @@
6.4 /* Title: Pure/Tools/simplifier_trace.scala
6.5 - Author: Lars Hupel, TU Muenchen
6.6 + Author: Lars Hupel
6.7
6.8 Interactive Simplifier trace.
6.9 */
6.10
6.11 package isabelle
6.12
6.13 +import scala.actors.Actor._
6.14 +import scala.annotation.tailrec
6.15 +import scala.collection.immutable.SortedMap
6.16 +
6.17
6.18 object Simplifier_Trace
6.19 {
6.20 - /* PIDE protocol */
6.21 +
6.22 + import Markup.Simp_Trace_Item
6.23 +
6.24 +
6.25 + /* replies to the prover */
6.26 +
6.27 + case class Answer private[Simplifier_Trace](val name: String, val string: String)
6.28 +
6.29 + object Answer
6.30 + {
6.31 +
6.32 + object step
6.33 + {
6.34 + val skip = Answer("skip", "Skip")
6.35 + val continue = Answer("continue", "Continue")
6.36 + val continue_trace = Answer("continue_trace", "Continue (with full trace)")
6.37 + val continue_passive = Answer("continue_passive", "Continue (without asking)")
6.38 + val continue_disable = Answer("continue_disable", "Continue (without any trace)")
6.39 +
6.40 + val default = skip
6.41 + val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
6.42 + }
6.43 +
6.44 + object hint_fail
6.45 + {
6.46 + val exit = Answer("exit", "Exit")
6.47 + val redo = Answer("redo", "Redo")
6.48 +
6.49 + val default = exit
6.50 + val all = List(redo, exit)
6.51 + }
6.52 +
6.53 + }
6.54 +
6.55 + val all_answers = Answer.step.all ++ Answer.hint_fail.all
6.56 +
6.57 +
6.58 + /* GUI interaction */
6.59 +
6.60 + case object Event
6.61 +
6.62 +
6.63 + /* manager actor */
6.64 +
6.65 + private case class Handle_Results(session: Session, id: Document_ID.Command, results: Command.Results)
6.66 + private case class Generate_Trace(results: Command.Results)
6.67 + private case class Cancel(serial: Long)
6.68 + private object Clear_Memory
6.69 + private object Stop
6.70 + case class Reply(session: Session, serial: Long, answer: Answer)
6.71 +
6.72 + case class Question(data: Simp_Trace_Item.Data, answers: List[Answer], default_answer: Answer)
6.73 +
6.74 + case class Context(
6.75 + last_serial: Long = 0L,
6.76 + questions: SortedMap[Long, Question] = SortedMap.empty
6.77 + )
6.78 + {
6.79 +
6.80 + def +(q: Question): Context =
6.81 + copy(questions = questions + ((q.data.serial, q)))
6.82 +
6.83 + def -(s: Long): Context =
6.84 + copy(questions = questions - s)
6.85 +
6.86 + def with_serial(s: Long): Context =
6.87 + copy(last_serial = Math.max(last_serial, s))
6.88 +
6.89 + }
6.90 +
6.91 + case class Trace(entries: List[Simp_Trace_Item.Data])
6.92 +
6.93 + case class Index(text: String, content: XML.Body)
6.94 +
6.95 + object Index
6.96 + {
6.97 + def of_data(data: Simp_Trace_Item.Data): Index =
6.98 + Index(data.text, data.content)
6.99 + }
6.100 +
6.101 + def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context =
6.102 + (manager !? Handle_Results(session, id, results)).asInstanceOf[Context]
6.103 +
6.104 + def generate_trace(results: Command.Results): Trace =
6.105 + (manager !? Generate_Trace(results)).asInstanceOf[Trace]
6.106 +
6.107 + def clear_memory() =
6.108 + manager ! Clear_Memory
6.109 +
6.110 + def send_reply(session: Session, serial: Long, answer: Answer) =
6.111 + manager ! Reply(session, serial, answer)
6.112 +
6.113 + private val manager = actor {
6.114 + var contexts = Map.empty[Document_ID.Command, Context]
6.115 +
6.116 + var memory_children = Map.empty[Long, Set[Long]]
6.117 + var memory = Map.empty[Index, Answer]
6.118 +
6.119 + def find_question(serial: Long): Option[(Document_ID.Command, Question)] =
6.120 + contexts collectFirst {
6.121 + case (id, context) if context.questions contains serial =>
6.122 + (id, context.questions(serial))
6.123 + }
6.124 +
6.125 + def do_cancel(serial: Long, id: Document_ID.Command)
6.126 + {
6.127 + // To save memory, we could try to remove empty contexts at this point.
6.128 + // However, if a new serial gets attached to the same command_id after we deleted
6.129 + // its context, its last_serial counter will start at 0 again, and we'll think the
6.130 + // old serials are actually new
6.131 + contexts += (id -> (contexts(id) - serial))
6.132 + }
6.133 +
6.134 + def do_reply(session: Session, serial: Long, answer: Answer)
6.135 + {
6.136 + session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name)
6.137 + }
6.138 +
6.139 + loop {
6.140 + react {
6.141 + case Handle_Results(session, id, results) =>
6.142 + var new_context = contexts.getOrElse(id, Context())
6.143 + var new_serial = new_context.last_serial
6.144 +
6.145 + for ((serial, result) <- results.entries if serial > new_context.last_serial)
6.146 + {
6.147 + result match {
6.148 + case Simp_Trace_Item(markup, data) =>
6.149 + import Simp_Trace_Item._
6.150 +
6.151 + memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
6.152 +
6.153 + markup match {
6.154 +
6.155 + case STEP =>
6.156 + val index = Index.of_data(data)
6.157 + memory.get(index) match {
6.158 + case None =>
6.159 + new_context += Question(data, Answer.step.all, Answer.step.default)
6.160 + case Some(answer) =>
6.161 + do_reply(session, serial, answer)
6.162 + }
6.163 +
6.164 + case HINT =>
6.165 + data.props match {
6.166 + case Markup.Success(false) =>
6.167 + results.get(data.parent) match {
6.168 + case Some(Simp_Trace_Item(STEP, _)) =>
6.169 + new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
6.170 + case _ =>
6.171 + // unknown, better send a default reply
6.172 + do_reply(session, data.serial, Answer.hint_fail.default)
6.173 + }
6.174 + case _ =>
6.175 + }
6.176 +
6.177 + case IGNORE =>
6.178 + // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
6.179 + // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
6.180 + // to selectively purge the replies which have been memorized, going down from
6.181 + // the parent to all leaves.
6.182 +
6.183 + @tailrec
6.184 + def purge(queue: Vector[Long]): Unit =
6.185 + queue match {
6.186 + case s +: rest =>
6.187 + for (Simp_Trace_Item(STEP, data) <- results.get(s))
6.188 + memory -= Index.of_data(data)
6.189 + val children = memory_children.getOrElse(s, Set.empty)
6.190 + memory_children -= s
6.191 + purge(rest ++ children.toVector)
6.192 + case _ =>
6.193 + }
6.194 +
6.195 + purge(Vector(data.parent))
6.196 +
6.197 + case _ =>
6.198 + }
6.199 +
6.200 + case _ =>
6.201 + }
6.202 +
6.203 + new_serial = serial
6.204 + }
6.205 +
6.206 + new_context = new_context.with_serial(new_serial)
6.207 + contexts += (id -> new_context)
6.208 + reply(new_context)
6.209 +
6.210 + case Generate_Trace(results) =>
6.211 + // Since there are potentially lots of trace messages, we do not cache them here again.
6.212 + // Instead, everytime the trace is being requested, we re-assemble it based on the
6.213 + // current results.
6.214 +
6.215 + val items =
6.216 + for { (_, Simp_Trace_Item(_, data)) <- results.entries }
6.217 + yield data
6.218 +
6.219 + reply(Trace(items.toList))
6.220 +
6.221 + case Cancel(serial) =>
6.222 + find_question(serial) match {
6.223 + case Some((id, _)) =>
6.224 + do_cancel(serial, id)
6.225 + case None =>
6.226 + System.err.println("handle_cancel: unknown serial " + serial)
6.227 + }
6.228 +
6.229 + case Clear_Memory =>
6.230 + memory_children = Map.empty
6.231 + memory = Map.empty
6.232 +
6.233 + case Stop =>
6.234 + contexts = Map.empty
6.235 + exit("Simplifier_Trace: manager actor stopped")
6.236 +
6.237 + case Reply(session, serial, answer) =>
6.238 + find_question(serial) match {
6.239 + case Some((id, Question(data, _, _))) =>
6.240 + if (data.markup == Markup.Simp_Trace_Item.STEP)
6.241 + {
6.242 + val index = Index.of_data(data)
6.243 + memory += (index -> answer)
6.244 + }
6.245 + do_cancel(serial, id)
6.246 + case None =>
6.247 + System.err.println("send_reply: unknown serial " + serial)
6.248 + }
6.249 +
6.250 + do_reply(session, serial, answer)
6.251 + session.trace_events.event(Event)
6.252 +
6.253 + case bad =>
6.254 + System.err.println("context_manager: bad message " + bad)
6.255 + }
6.256 + }
6.257 + }
6.258 +
6.259 +
6.260 + /* protocol handler */
6.261
6.262 class Handler extends Session.Protocol_Handler
6.263 {
6.264 - val functions = Map.empty[String, (Session.Prover, Isabelle_Process.Protocol_Output) => Boolean]
6.265 + private def cancel(
6.266 + prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
6.267 + msg.properties match {
6.268 + case Markup.Cancel_Simp_Trace(serial) =>
6.269 + manager ! Cancel(serial)
6.270 + true
6.271 + case _ =>
6.272 + false
6.273 + }
6.274 +
6.275 + override def stop(prover: Session.Prover) =
6.276 + {
6.277 + manager ! Clear_Memory
6.278 + manager ! Stop
6.279 + }
6.280 +
6.281 + val functions = Map(
6.282 + Markup.CANCEL_SIMP_TRACE -> cancel _)
6.283 }
6.284 +
6.285 }
7.1 --- a/src/Pure/raw_simplifier.ML Tue Feb 04 01:35:48 2014 +0100
7.2 +++ b/src/Pure/raw_simplifier.ML Tue Feb 04 09:04:59 2014 +0000
7.3 @@ -17,6 +17,7 @@
7.4 val simp_trace: bool Config.T
7.5 type cong_name = bool * string
7.6 type rrule
7.7 + val mk_rrules: Proof.context -> thm list -> rrule list
7.8 val eq_rrule: rrule * rrule -> bool
7.9 type proc
7.10 type solver
7.11 @@ -571,6 +572,12 @@
7.12 fun extract_safe_rrules ctxt thm =
7.13 maps (orient_rrule ctxt) (extract_rews ctxt [thm]);
7.14
7.15 +fun mk_rrules ctxt thms =
7.16 + let
7.17 + val rews = extract_rews ctxt thms
7.18 + val raw_rrules = flat (map (mk_rrule ctxt) rews)
7.19 + in map mk_rrule2 raw_rrules end
7.20 +
7.21
7.22 (* add/del rules explicitly *)
7.23
7.24 @@ -588,7 +595,6 @@
7.25 fun add_simp thm ctxt = ctxt addsimps [thm];
7.26 fun del_simp thm ctxt = ctxt delsimps [thm];
7.27
7.28 -
7.29 (* congs *)
7.30
7.31 local
7.32 @@ -814,7 +820,7 @@
7.33
7.34 type trace_ops =
7.35 {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
7.36 - trace_apply: {unconditional: bool, term: term, thm: thm, name: string} ->
7.37 + trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} ->
7.38 Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option};
7.39
7.40 structure Trace_Ops = Theory_Data
7.41 @@ -919,8 +925,9 @@
7.42 val eta_thm = Thm.eta_conversion t;
7.43 val eta_t' = Thm.rhs_of eta_thm;
7.44 val eta_t = term_of eta_t';
7.45 - fun rew {thm, name, lhs, elhs, extra, fo, perm} =
7.46 + fun rew rrule =
7.47 let
7.48 + val {thm, name, lhs, elhs, extra, fo, perm} = rrule
7.49 val prop = Thm.prop_of thm;
7.50 val (rthm, elhs') =
7.51 if maxt = ~1 orelse not extra then (thm, elhs)
7.52 @@ -932,7 +939,7 @@
7.53 val prop' = Thm.prop_of thm';
7.54 val unconditional = (Logic.count_prems prop' = 0);
7.55 val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
7.56 - val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', name = name};
7.57 + val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule};
7.58 in
7.59 if perm andalso not (termless (rhs', lhs'))
7.60 then
8.1 --- a/src/Tools/jEdit/lib/Tools/jedit Tue Feb 04 01:35:48 2014 +0100
8.2 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Feb 04 09:04:59 2014 +0000
8.3 @@ -39,6 +39,8 @@
8.4 "src/rich_text_area.scala"
8.5 "src/scala_console.scala"
8.6 "src/sledgehammer_dockable.scala"
8.7 + "src/simplifier_trace_dockable.scala"
8.8 + "src/simplifier_trace_window.scala"
8.9 "src/symbols_dockable.scala"
8.10 "src/syslog_dockable.scala"
8.11 "src/text_overview.scala"
9.1 --- a/src/Tools/jEdit/src/Isabelle.props Tue Feb 04 01:35:48 2014 +0100
9.2 +++ b/src/Tools/jEdit/src/Isabelle.props Tue Feb 04 09:04:59 2014 +0000
9.3 @@ -37,6 +37,7 @@
9.4 isabelle.protocol-panel \
9.5 isabelle.raw-output-panel \
9.6 isabelle.sledgehammer-panel \
9.7 + isabelle.simp-trace-panel \
9.8 isabelle.symbols-panel \
9.9 isabelle.syslog-panel \
9.10 isabelle.theories-panel \
9.11 @@ -47,6 +48,7 @@
9.12 isabelle.output-panel.label=Output panel
9.13 isabelle.protocol-panel.label=Protocol panel
9.14 isabelle.raw-output-panel.label=Raw Output panel
9.15 +isabelle.simp-trace-panel.label=Simplifier trace panel
9.16 isabelle.sledgehammer-panel.label=Sledgehammer panel
9.17 isabelle.symbols-panel.label=Symbols panel
9.18 isabelle.syslog-panel.label=Syslog panel
9.19 @@ -59,6 +61,7 @@
9.20 isabelle-info.title=Info
9.21 isabelle-monitor.title=Monitor
9.22 isabelle-output.title=Output
9.23 +isabelle-simp-trace.title=Simplifier trace
9.24 isabelle-protocol.title=Protocol
9.25 isabelle-raw-output.title=Raw Output
9.26 isabelle-documentation.title=Documentation
10.1 --- a/src/Tools/jEdit/src/actions.xml Tue Feb 04 01:35:48 2014 +0100
10.2 +++ b/src/Tools/jEdit/src/actions.xml Tue Feb 04 09:04:59 2014 +0000
10.3 @@ -42,6 +42,11 @@
10.4 wm.addDockableWindow("isabelle-raw-output");
10.5 </CODE>
10.6 </ACTION>
10.7 + <ACTION NAME="isabelle.simp-trace-panel">
10.8 + <CODE>
10.9 + wm.addDockableWindow("isabelle-simp-trace");
10.10 + </CODE>
10.11 + </ACTION>
10.12 <ACTION NAME="isabelle.protocol-panel">
10.13 <CODE>
10.14 wm.addDockableWindow("isabelle-protocol");
10.15 @@ -147,4 +152,4 @@
10.16 isabelle.jedit.Isabelle.input_bsup(textArea);
10.17 </CODE>
10.18 </ACTION>
10.19 -</ACTIONS>
10.20 \ No newline at end of file
10.21 +</ACTIONS>
11.1 --- a/src/Tools/jEdit/src/active.scala Tue Feb 04 01:35:48 2014 +0100
11.2 +++ b/src/Tools/jEdit/src/active.scala Tue Feb 04 09:04:59 2014 +0000
11.3 @@ -61,6 +61,9 @@
11.4 else text_area.setSelectedText(text)
11.5 }
11.6
11.7 + case Markup.Simp_Trace(serial, answer) =>
11.8 + Simplifier_Trace.send_reply(PIDE.session, serial, answer)
11.9 +
11.10 case Protocol.Dialog(id, serial, result) =>
11.11 model.session.dialog_result(id, serial, result)
11.12
11.13 @@ -72,4 +75,3 @@
11.14 }
11.15 }
11.16 }
11.17 -
12.1 --- a/src/Tools/jEdit/src/dockables.xml Tue Feb 04 01:35:48 2014 +0100
12.2 +++ b/src/Tools/jEdit/src/dockables.xml Tue Feb 04 09:04:59 2014 +0000
12.3 @@ -41,4 +41,7 @@
12.4 <DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
12.5 new isabelle.jedit.Symbols_Dockable(view, position);
12.6 </DOCKABLE>
12.7 -</DOCKABLES>
12.8 \ No newline at end of file
12.9 + <DOCKABLE NAME="isabelle-simp-trace" MOVABLE="TRUE">
12.10 + new isabelle.jedit.Simplifier_Trace_Dockable(view, position);
12.11 + </DOCKABLE>
12.12 +</DOCKABLES>
13.1 --- a/src/Tools/jEdit/src/isabelle.scala Tue Feb 04 01:35:48 2014 +0100
13.2 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Feb 04 09:04:59 2014 +0000
13.3 @@ -81,6 +81,12 @@
13.4 case _ => None
13.5 }
13.6
13.7 + def docked_simplifier_trace(view: View): Option[Simplifier_Trace_Dockable] =
13.8 + wm(view).getDockableWindow("isabelle-simp-trace") match {
13.9 + case dockable: Simplifier_Trace_Dockable => Some(dockable)
13.10 + case _ => None
13.11 + }
13.12 +
13.13 def docked_protocol(view: View): Option[Protocol_Dockable] =
13.14 wm(view).getDockableWindow("isabelle-protocol") match {
13.15 case dockable: Protocol_Dockable => Some(dockable)
14.1 --- a/src/Tools/jEdit/src/jEdit.props Tue Feb 04 01:35:48 2014 +0100
14.2 +++ b/src/Tools/jEdit/src/jEdit.props Tue Feb 04 09:04:59 2014 +0000
14.3 @@ -189,6 +189,7 @@
14.4 isabelle-output.height=174
14.5 isabelle-output.width=412
14.6 isabelle-sledgehammer.dock-position=bottom
14.7 +isabelle-simp-trace.dock-position=bottom
14.8 isabelle-symbols.dock-position=bottom
14.9 isabelle-theories.dock-position=right
14.10 isabelle.complete.label=Complete Isabelle text
15.1 --- a/src/Tools/jEdit/src/rendering.scala Tue Feb 04 01:35:48 2014 +0100
15.2 +++ b/src/Tools/jEdit/src/rendering.scala Tue Feb 04 09:04:59 2014 +0000
15.3 @@ -270,7 +270,7 @@
15.4
15.5
15.6 private val active_include =
15.7 - Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
15.8 + Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
15.9
15.10 def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
15.11 snapshot.select_markup(range, Some(active_include), command_state =>
15.12 @@ -281,7 +281,8 @@
15.13 case Text.Info(info_range, elem) =>
15.14 if (elem.name == Markup.BROWSER ||
15.15 elem.name == Markup.GRAPHVIEW ||
15.16 - elem.name == Markup.SENDBACK)
15.17 + elem.name == Markup.SENDBACK ||
15.18 + elem.name == Markup.SIMP_TRACE)
15.19 Some(Text.Info(snapshot.convert(info_range), elem))
15.20 else None
15.21 }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 04 09:04:59 2014 +0000
16.3 @@ -0,0 +1,222 @@
16.4 +/* Title: Tools/jEdit/src/simplifier_trace_dockable.scala
16.5 + Author: Lars Hupel
16.6 +
16.7 +Dockable window with interactive simplifier trace.
16.8 +*/
16.9 +
16.10 +package isabelle.jedit
16.11 +
16.12 +
16.13 +import isabelle._
16.14 +
16.15 +import scala.actors.Actor._
16.16 +
16.17 +import scala.swing.{Button, CheckBox, Orientation, Separator}
16.18 +import scala.swing.event.ButtonClicked
16.19 +
16.20 +import java.awt.BorderLayout
16.21 +import java.awt.event.{ComponentEvent, ComponentAdapter}
16.22 +
16.23 +import org.gjt.sp.jedit.View
16.24 +
16.25 +class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
16.26 +{
16.27 + Swing_Thread.require()
16.28 +
16.29 + /* component state -- owned by Swing thread */
16.30 +
16.31 + private var current_snapshot = Document.State.init.snapshot()
16.32 + private var current_state = Command.empty.init_state
16.33 + private var current_id = 0L
16.34 + private var do_update = true
16.35 + private var do_auto_reply = false
16.36 +
16.37 +
16.38 + private val text_area = new Pretty_Text_Area(view)
16.39 + set_content(text_area)
16.40 +
16.41 + private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.Tree =
16.42 + {
16.43 + val data = question.data
16.44 +
16.45 + def make_button(answer: Simplifier_Trace.Answer): XML.Tree =
16.46 + XML.Wrapped_Elem(
16.47 + Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)),
16.48 + Nil,
16.49 + List(XML.Text(answer.string))
16.50 + )
16.51 +
16.52 + def make_block(body: XML.Body): XML.Body =
16.53 + List(Pretty.Block(0, body))
16.54 +
16.55 + val all = Pretty.separate(
16.56 + XML.Text(data.text) ::
16.57 + data.content :::
16.58 + make_block(Library.separate(XML.Text(", "), question.answers map make_button))
16.59 + )
16.60 +
16.61 + XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(all)))
16.62 + }
16.63 +
16.64 + private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
16.65 + {
16.66 + Swing_Thread.require()
16.67 + val questions = context.questions.values
16.68 + if (do_auto_reply && !questions.isEmpty)
16.69 + {
16.70 + questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer))
16.71 + handle_update(do_update)
16.72 + }
16.73 + else
16.74 + {
16.75 + val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut))
16.76 + text_area.update(snapshot, Command.Results.empty, contents)
16.77 + do_paint()
16.78 + }
16.79 + }
16.80 +
16.81 + private def show_trace()
16.82 + {
16.83 + val trace = Simplifier_Trace.generate_trace(current_state.results)
16.84 + new Simplifier_Trace_Window(view, current_snapshot, trace)
16.85 + }
16.86 +
16.87 + private def do_paint()
16.88 + {
16.89 + Swing_Thread.later {
16.90 + text_area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
16.91 + }
16.92 + }
16.93 +
16.94 + private def update_contents()
16.95 + {
16.96 + set_context(
16.97 + current_snapshot,
16.98 + Simplifier_Trace.handle_results(PIDE.session, current_id, current_state.results)
16.99 + )
16.100 + }
16.101 +
16.102 + private def handle_resize()
16.103 + {
16.104 + do_paint()
16.105 + }
16.106 +
16.107 + private def handle_update(follow: Boolean)
16.108 + {
16.109 + val (new_snapshot, new_state, new_id) =
16.110 + PIDE.editor.current_node_snapshot(view) match {
16.111 + case Some(snapshot) =>
16.112 + if (follow && !snapshot.is_outdated) {
16.113 + PIDE.editor.current_command(view, snapshot) match {
16.114 + case Some(cmd) =>
16.115 + (snapshot, snapshot.state.command_state(snapshot.version, cmd), cmd.id)
16.116 + case None =>
16.117 + (Document.State.init.snapshot(), Command.empty.init_state, 0L)
16.118 + }
16.119 + }
16.120 + else (current_snapshot, current_state, current_id)
16.121 + case None => (current_snapshot, current_state, current_id)
16.122 + }
16.123 +
16.124 + current_snapshot = new_snapshot
16.125 + current_state = new_state
16.126 + current_id = new_id
16.127 + update_contents()
16.128 + }
16.129 +
16.130 +
16.131 + /* main actor */
16.132 +
16.133 + private val main_actor = actor {
16.134 + loop {
16.135 + react {
16.136 + case _: Session.Global_Options =>
16.137 + Swing_Thread.later { handle_resize() }
16.138 + case changed: Session.Commands_Changed =>
16.139 + Swing_Thread.later { handle_update(do_update) }
16.140 + case Session.Caret_Focus =>
16.141 + Swing_Thread.later { handle_update(do_update) }
16.142 + case Simplifier_Trace.Event =>
16.143 + Swing_Thread.later { handle_update(do_update) }
16.144 + case bad => System.err.println("Simplifier_Trace_Dockable: ignoring bad message " + bad)
16.145 + }
16.146 + }
16.147 + }
16.148 +
16.149 + override def init()
16.150 + {
16.151 + Swing_Thread.require()
16.152 +
16.153 + PIDE.session.global_options += main_actor
16.154 + PIDE.session.commands_changed += main_actor
16.155 + PIDE.session.caret_focus += main_actor
16.156 + PIDE.session.trace_events += main_actor
16.157 + handle_update(true)
16.158 + }
16.159 +
16.160 + override def exit()
16.161 + {
16.162 + Swing_Thread.require()
16.163 +
16.164 + PIDE.session.global_options -= main_actor
16.165 + PIDE.session.commands_changed -= main_actor
16.166 + PIDE.session.caret_focus -= main_actor
16.167 + PIDE.session.trace_events -= main_actor
16.168 + delay_resize.revoke()
16.169 + }
16.170 +
16.171 +
16.172 + /* resize */
16.173 +
16.174 + private val delay_resize =
16.175 + Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
16.176 +
16.177 + addComponentListener(new ComponentAdapter {
16.178 + override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
16.179 + override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
16.180 + })
16.181 +
16.182 +
16.183 + /* controls */
16.184 +
16.185 + private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
16.186 + new CheckBox("Auto update") {
16.187 + selected = do_update
16.188 + reactions += {
16.189 + case ButtonClicked(_) =>
16.190 + do_update = this.selected
16.191 + handle_update(do_update)
16.192 + }
16.193 + },
16.194 + new Button("Update") {
16.195 + reactions += {
16.196 + case ButtonClicked(_) =>
16.197 + handle_update(true)
16.198 + }
16.199 + },
16.200 + new Separator(Orientation.Vertical),
16.201 + new CheckBox("Auto reply") {
16.202 + selected = do_auto_reply
16.203 + reactions += {
16.204 + case ButtonClicked(_) =>
16.205 + do_auto_reply = this.selected
16.206 + handle_update(do_update)
16.207 + }
16.208 + },
16.209 + new Separator(Orientation.Vertical),
16.210 + new Button("Show trace") {
16.211 + reactions += {
16.212 + case ButtonClicked(_) =>
16.213 + show_trace()
16.214 + }
16.215 + },
16.216 + new Button("Clear memory") {
16.217 + reactions += {
16.218 + case ButtonClicked(_) =>
16.219 + Simplifier_Trace.clear_memory()
16.220 + }
16.221 + }
16.222 + )
16.223 +
16.224 + add(controls.peer, BorderLayout.NORTH)
16.225 +}
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 04 09:04:59 2014 +0000
17.3 @@ -0,0 +1,237 @@
17.4 +/* Title: Tools/jEdit/src/simplifier_trace_window.scala
17.5 + Author: Lars Hupel
17.6 +
17.7 +Trace window with tree-style view of the simplifier trace.
17.8 +*/
17.9 +
17.10 +package isabelle.jedit
17.11 +
17.12 +
17.13 +import isabelle._
17.14 +
17.15 +import scala.annotation.tailrec
17.16 +
17.17 +import scala.collection.immutable.SortedMap
17.18 +
17.19 +import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
17.20 +import scala.swing.event.{Key, KeyPressed}
17.21 +
17.22 +import scala.util.matching.Regex
17.23 +
17.24 +import java.awt.BorderLayout
17.25 +import java.awt.event.{ComponentEvent, ComponentAdapter}
17.26 +
17.27 +import javax.swing.SwingUtilities
17.28 +
17.29 +import org.gjt.sp.jedit.View
17.30 +
17.31 +private object Simplifier_Trace_Window
17.32 +{
17.33 +
17.34 + import Markup.Simp_Trace_Item
17.35 +
17.36 + sealed trait Trace_Tree
17.37 + {
17.38 + var children: SortedMap[Long, Elem_Tree] = SortedMap.empty
17.39 + val serial: Long
17.40 + val parent: Option[Trace_Tree]
17.41 + var hints: List[Simp_Trace_Item.Data]
17.42 + def set_interesting(): Unit
17.43 + }
17.44 +
17.45 + final class Root_Tree(val serial: Long) extends Trace_Tree
17.46 + {
17.47 + val parent = None
17.48 + val hints = Nil
17.49 + def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints")
17.50 + def set_interesting() = ()
17.51 +
17.52 + def format(regex: Option[Regex]): XML.Body =
17.53 + Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut))
17.54 + }
17.55 +
17.56 + final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree
17.57 + {
17.58 + val serial = data.serial
17.59 + var hints = List.empty[Simp_Trace_Item.Data]
17.60 + var interesting: Boolean = false
17.61 +
17.62 + def set_interesting(): Unit =
17.63 + if (!interesting)
17.64 + {
17.65 + interesting = true
17.66 + parent match {
17.67 + case Some(p) =>
17.68 + p.set_interesting()
17.69 + case None =>
17.70 + }
17.71 + }
17.72 +
17.73 + def format(regex: Option[Regex]): (Boolean, XML.Tree) =
17.74 + {
17.75 + def format_child(child: Elem_Tree): Option[XML.Tree] = child.format(regex) match {
17.76 + case (false, _) =>
17.77 + None
17.78 + case (true, res) =>
17.79 + Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
17.80 + }
17.81 +
17.82 + def format_hint(data: Simp_Trace_Item.Data): XML.Tree =
17.83 + Pretty.block(Pretty.separate(
17.84 + XML.Text(data.text) ::
17.85 + data.content
17.86 + ))
17.87 +
17.88 + def body_contains(regex: Regex, body: XML.Body): Boolean =
17.89 + body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
17.90 +
17.91 + val children_bodies: XML.Body =
17.92 + children.values.filter(_.interesting).flatMap(format_child).toList
17.93 +
17.94 + lazy val hint_bodies: XML.Body =
17.95 + hints.reverse.map(format_hint)
17.96 +
17.97 + val eligible = regex match {
17.98 + case None =>
17.99 + true
17.100 + case Some(r) =>
17.101 + body_contains(r, data.content) || hints.exists(h => body_contains(r, h.content))
17.102 + }
17.103 +
17.104 + val all =
17.105 + if (eligible)
17.106 + XML.Text(data.text) :: data.content ::: children_bodies ::: hint_bodies
17.107 + else
17.108 + XML.Text(data.text) :: children_bodies
17.109 +
17.110 + val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all))))
17.111 +
17.112 + (eligible || children_bodies != Nil, res)
17.113 + }
17.114 + }
17.115 +
17.116 + @tailrec
17.117 + def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
17.118 + rest match {
17.119 + case Nil =>
17.120 + ()
17.121 + case head :: tail =>
17.122 + lookup.get(head.parent) match {
17.123 + case Some(parent) =>
17.124 + if (head.markup == Simp_Trace_Item.HINT)
17.125 + {
17.126 + parent.hints ::= head
17.127 + walk_trace(tail, lookup)
17.128 + }
17.129 + else if (head.markup == Simp_Trace_Item.IGNORE)
17.130 + {
17.131 + parent.parent match {
17.132 + case None =>
17.133 + System.err.println("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
17.134 + case Some(tree) =>
17.135 + tree.children -= head.parent
17.136 + walk_trace(tail, lookup) // FIXME discard from lookup
17.137 + }
17.138 + }
17.139 + else
17.140 + {
17.141 + val entry = new Elem_Tree(head, Some(parent))
17.142 + parent.children += ((head.serial, entry))
17.143 + if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG)
17.144 + entry.set_interesting()
17.145 + walk_trace(tail, lookup + (head.serial -> entry))
17.146 + }
17.147 +
17.148 + case None =>
17.149 + System.err.println("Simplifier_Trace_Window: unknown parent " + head.parent)
17.150 + }
17.151 + }
17.152 +
17.153 +}
17.154 +
17.155 +class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
17.156 +{
17.157 +
17.158 + import Simplifier_Trace_Window._
17.159 +
17.160 + Swing_Thread.require()
17.161 +
17.162 + val area = new Pretty_Text_Area(view)
17.163 +
17.164 + size = new Dimension(500, 500)
17.165 + contents = new BorderPanel {
17.166 + layout(Component.wrap(area)) = BorderPanel.Position.Center
17.167 + }
17.168 +
17.169 + private val tree = trace.entries.headOption match {
17.170 + case Some(first) =>
17.171 + val tree = new Root_Tree(first.parent)
17.172 + walk_trace(trace.entries, Map(first.parent -> tree))
17.173 + tree
17.174 + case None =>
17.175 + new Root_Tree(0)
17.176 + }
17.177 +
17.178 + do_update(None)
17.179 + open()
17.180 + do_paint()
17.181 +
17.182 + def do_update(regex: Option[Regex])
17.183 + {
17.184 + val xml = tree.format(regex)
17.185 + area.update(snapshot, Command.Results.empty, xml)
17.186 + }
17.187 +
17.188 + def do_paint()
17.189 + {
17.190 + Swing_Thread.later {
17.191 + area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
17.192 + }
17.193 + }
17.194 +
17.195 + def handle_resize()
17.196 + {
17.197 + do_paint()
17.198 + }
17.199 +
17.200 +
17.201 + /* resize */
17.202 +
17.203 + private val delay_resize =
17.204 + Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
17.205 +
17.206 + peer.addComponentListener(new ComponentAdapter {
17.207 + override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
17.208 + override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
17.209 + })
17.210 +
17.211 +
17.212 + /* controls */
17.213 +
17.214 + val use_regex = new CheckBox("Regex")
17.215 +
17.216 + private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
17.217 + new Label {
17.218 + text = "Search"
17.219 + },
17.220 + new TextField(30) {
17.221 + listenTo(keys)
17.222 + reactions += {
17.223 + case KeyPressed(_, Key.Enter, 0, _) =>
17.224 + val input = text.trim
17.225 + val regex =
17.226 + if (input.isEmpty)
17.227 + None
17.228 + else if (use_regex.selected)
17.229 + Some(input.r)
17.230 + else
17.231 + Some(java.util.regex.Pattern.quote(input).r)
17.232 + do_update(regex)
17.233 + do_paint()
17.234 + }
17.235 + },
17.236 + use_regex
17.237 + )
17.238 +
17.239 + peer.add(controls.peer, BorderLayout.NORTH)
17.240 +}