# HG changeset patch # User Lars Hupel # Date 1391504699 0 # Node ID 885500f4aa6a570fd046e96c3348a92d75cc94af # Parent 54b0352fb46d10ef342e30b4f5c288ad1eba9954 interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state diff -r 54b0352fb46d -r 885500f4aa6a CONTRIBUTORS --- a/CONTRIBUTORS Tue Feb 04 01:35:48 2014 +0100 +++ b/CONTRIBUTORS Tue Feb 04 09:04:59 2014 +0000 @@ -6,6 +6,9 @@ Contributions to this Isabelle version -------------------------------------- +* January 2014: Lars Hupel, TUM + An improved, interactive simplifier trace with integration into the + Isabelle/jEdit Prover IDE. Contributions to Isabelle2013-1 ------------------------------- diff -r 54b0352fb46d -r 885500f4aa6a NEWS --- a/NEWS Tue Feb 04 01:35:48 2014 +0100 +++ b/NEWS Tue Feb 04 09:04:59 2014 +0000 @@ -37,6 +37,10 @@ process, without requiring old-fashioned command-line invocation of "isabelle jedit -m MODE". +* New panel: Simplifier trace. Provides an interactive view of the +simplification process, enabled by the newly-introduced +"simplifier_trace" declaration. + *** Pure *** diff -r 54b0352fb46d -r 885500f4aa6a src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Tue Feb 04 09:04:59 2014 +0000 @@ -273,7 +273,8 @@ /* messages */ - val Serial = new Properties.Long("serial") + val SERIAL = "serial" + val Serial = new Properties.Long(SERIAL) val MESSAGE = "message" @@ -386,6 +387,76 @@ case _ => None } } + + /* simplifier trace */ + + val TEXT = "text" + val Text = new Properties.String(TEXT) + + val PARENT = "parent" + val Parent = new Properties.Long(PARENT) + + val SUCCESS = "success" + val Success = new Properties.Boolean(SUCCESS) + + val CANCEL_SIMP_TRACE = "simp_trace_cancel" + object Cancel_Simp_Trace + { + def unapply(props: Properties.T): Option[Long] = + props match { + case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id) + case _ => None + } + } + + val SIMP_TRACE = "simp_trace" + object Simp_Trace + { + def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] = + tree match { + case XML.Elem(Markup(SIMP_TRACE, props), _) => + (props, props) match { + case (Serial(serial), Name(name)) => + Simplifier_Trace.all_answers.find(_.name == name).map((serial, _)) + case _ => + None + } + case _ => + None + } + } + + /* trace items from the prover */ + + object Simp_Trace_Item + { + + def unapply(tree: XML.Tree): Option[(String, Data)] = + tree match { + case XML.Elem(Markup(RESULT, Serial(serial)), List( + XML.Elem(Markup(markup, props), content) + )) if markup.startsWith("simp_trace_") => + (props, props) match { + case (Text(text), Parent(parent)) => + Some((markup, Data(serial, markup, text, parent, props, content))) + case _ => + None + } + case _ => + None + } + + val LOG = "simp_trace_log" + val STEP = "simp_trace_step" + val RECURSE = "simp_trace_recurse" + val HINT = "simp_trace_hint" + val IGNORE = "simp_trace_ignore" + + case class Data(serial: Long, markup: String, text: String, + parent: Long, props: Properties.T, content: XML.Body) + + } + } diff -r 54b0352fb46d -r 885500f4aa6a src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Pure/System/session.scala Tue Feb 04 09:04:59 2014 +0000 @@ -139,7 +139,7 @@ val syslog_messages = new Event_Bus[Isabelle_Process.Output] val raw_output_messages = new Event_Bus[Isabelle_Process.Output] val all_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck - + val trace_events = new Event_Bus[Simplifier_Trace.Event.type] /** buffered command changes (delay_first discipline) **/ diff -r 54b0352fb46d -r 885500f4aa6a src/Pure/Tools/simplifier_trace.ML --- a/src/Pure/Tools/simplifier_trace.ML Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Pure/Tools/simplifier_trace.ML Tue Feb 04 09:04:59 2014 +0000 @@ -1,38 +1,435 @@ (* Title: Pure/Tools/simplifier_trace.ML - Author: Lars Hupel, TU Muenchen + Author: Lars Hupel Interactive Simplifier trace. *) signature SIMPLIFIER_TRACE = sig - val simp_trace_test: bool Config.T + val add_term_breakpoint: term -> Context.generic -> Context.generic + val add_thm_breakpoint: thm -> Context.generic -> Context.generic end structure Simplifier_Trace: SIMPLIFIER_TRACE = struct -(* Simplifier trace operations *) +(** background data **) + +datatype mode = Disabled | Normal | Full + +fun merge_modes Disabled m = m + | merge_modes Normal Full = Full + | merge_modes Normal _ = Normal + | merge_modes Full _ = Full + +val empty_breakpoints = + (Item_Net.init (op =) single (* FIXME equality on terms? *), + Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm)) + +fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) = + (Item_Net.merge (term_bs1, term_bs2), + Item_Net.merge (thm_bs1, thm_bs2)) + +structure Data = Generic_Data +( + type T = + {max_depth: int, + depth: int, + mode: mode, + interactive: bool, + parent: int, + breakpoints: term Item_Net.T * rrule Item_Net.T} + val empty = + {max_depth = 10, + depth = 0, + mode = Disabled, + interactive = false, + parent = 0, + breakpoints = empty_breakpoints} + val extend = I + fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1, + breakpoints = breakpoints1, ...}, + {max_depth = max_depth2, mode = mode2, interactive = interactive2, + breakpoints = breakpoints2, ...}) = + {max_depth = Int.max (max_depth1, max_depth2), + depth = 0, + mode = merge_modes mode1 mode2, + interactive = interactive1 orelse interactive2, + parent = 0, + breakpoints = merge_breakpoints (breakpoints1, breakpoints2)} +) + +fun map_breakpoints f_term f_thm = + Data.map (fn {max_depth, depth, mode, interactive, parent, breakpoints = (term_bs, thm_bs)} => + {max_depth = max_depth, + depth = depth, + mode = mode, + interactive = interactive, + parent = parent, + breakpoints = (f_term term_bs, f_thm thm_bs)}) + +fun add_term_breakpoint term = + map_breakpoints (Item_Net.update term) I + +fun add_thm_breakpoint thm context = + let + val rrules = mk_rrules (Context.proof_of context) [thm] + in + map_breakpoints I (fold Item_Net.update rrules) context + end + +fun is_breakpoint (term, rrule) context = + let + val {breakpoints, ...} = Data.get context + + fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term) + val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term) + + val {thm = thm, ...} = rrule + val thm_matches = exists (eq_rrule o pair rrule) + (Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm)) + in + (term_matches, thm_matches) + end + +(** config and attributes **) + +fun config raw_mode interactive max_depth = + let + val mode = case raw_mode of + "normal" => Normal + | "full" => Full + | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode) + + val update = Data.map (fn {depth, parent, breakpoints, ...} => + {max_depth = max_depth, + depth = depth, + mode = mode, + interactive = interactive, + parent = parent, + breakpoints = breakpoints}) + in Thm.declaration_attribute (K update) end + +fun term_breakpoint terms = + Thm.declaration_attribute (K (fold add_term_breakpoint terms)) + +val thm_breakpoint = + Thm.declaration_attribute add_thm_breakpoint + +(** tracing state **) + +val futures = + Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table) + +(** markup **) + +fun output_result (id, data) = + Output.result (Markup.serial_properties id) data + +val serialN = "serial" +val parentN = "parent" +val textN = "text" +val successN = "success" + +val logN = "simp_trace_log" +val stepN = "simp_trace_step" +val recurseN = "simp_trace_recurse" +val hintN = "simp_trace_hint" +val ignoreN = "simp_trace_ignore" + +val cancelN = "simp_trace_cancel" + +type payload = + {props: Properties.T, + pretty: Pretty.T} + +fun empty_payload () : payload = + {props = [], pretty = Pretty.str ""} + +fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt = + let + val {max_depth, depth, mode, interactive, parent, ...} = Data.get (Context.Proof ctxt) + + val eligible = + case mode of + Disabled => false + | Normal => triggered + | Full => true + + val markup' = if markup = stepN andalso not interactive then logN else markup + in + if not eligible orelse depth > max_depth then + NONE + else + let + val {props = more_props, pretty} = payload () + val props = + [(textN, text), + (parentN, Markup.print_int parent)] + val data = + Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty]) + in + SOME (serial (), data) + end + end + +(** tracing output **) + +fun send_request (result_id, content) = + let + fun break () = + (Output.protocol_message + [(Markup.functionN, cancelN), + (serialN, Markup.print_int result_id)] + ""; + Synchronized.change futures (Inttab.delete_safe result_id)) + val promise = Future.promise break : string future + in + Synchronized.change futures (Inttab.update_new (result_id, promise)); + output_result (result_id, content); + promise + end + + +fun step {term, thm, unconditional, ctxt, rrule} = + let + val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt) + + val {name, ...} = rrule + val term_triggered = not (null matching_terms) -val simp_trace_test = - Attrib.setup_config_bool @{binding simp_trace_test} (K false) + val text = + if unconditional then + "Apply rewrite rule?" + else + "Apply conditional rewrite rule?" + + fun payload () = + let + (* FIXME pretty printing via Proof_Context.pretty_fact *) + val pretty_thm = Pretty.block + [Pretty.str ("Instance of " ^ name ^ ":"), + Pretty.brk 1, + Syntax.pretty_term ctxt (Thm.prop_of thm)] + + val pretty_term = Pretty.block + [Pretty.str "Trying to rewrite:", + Pretty.brk 1, + Syntax.pretty_term ctxt term] + + val pretty_matchings = + let + val items = map (Pretty.item o single o Syntax.pretty_term ctxt) matching_terms + in + if not (null matching_terms) then + [Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))] + else + [] + end + + val pretty = + Pretty.chunks ([pretty_thm, pretty_term] @ pretty_matchings) + in + {props = [], pretty = pretty} + end + + val {max_depth, depth, mode, interactive, breakpoints, ...} = + Data.get (Context.Proof ctxt) + + fun mk_promise result = + let + val result_id = #1 result + + fun put mode' interactive' = Data.put + {max_depth = max_depth, + depth = depth, + mode = mode', + interactive = interactive', + parent = result_id, + breakpoints = breakpoints} (Context.Proof ctxt) |> + Context.the_proof + + fun to_response "skip" = NONE + | to_response "continue" = SOME (put mode true) + | to_response "continue_trace" = SOME (put Full true) + | to_response "continue_passive" = SOME (put mode false) + | to_response "continue_disable" = SOME (put Disabled false) + | to_response _ = raise Fail "Simplifier_Trace.step: invalid message" + in + if not interactive then + (output_result result; Future.value (SOME (put mode false))) + else + Future.map to_response (send_request result) + end + + in + case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of + NONE => Future.value (SOME ctxt) + | SOME res => mk_promise res + end + +fun recurse text term ctxt = + let + fun payload () = + {props = [], + pretty = Syntax.pretty_term ctxt term} + + val {max_depth, depth, mode, interactive, breakpoints, ...} = Data.get (Context.Proof ctxt) + + fun put result_id = Data.put + {max_depth = max_depth, + depth = depth + 1, + mode = if depth >= max_depth then Disabled else mode, + interactive = interactive, + parent = result_id, + breakpoints = breakpoints} (Context.Proof ctxt) + + val context' = + case mk_generic_result recurseN text true payload ctxt of + NONE => + put 0 + | SOME res => + (output_result res; put (#1 res)) + in Context.the_proof context' end + +fun indicate_failure {term, ctxt, thm, rrule, ...} ctxt' = + let + fun payload () = + let + val {name, ...} = rrule + val pretty_thm = + (* FIXME pretty printing via Proof_Context.pretty_fact *) + Pretty.block + [Pretty.str ("In an instance of " ^ name ^ ":"), + Pretty.brk 1, + Syntax.pretty_term ctxt (Thm.prop_of thm)] + + val pretty_term = + Pretty.block + [Pretty.str "Was trying to rewrite:", + Pretty.brk 1, + Syntax.pretty_term ctxt term] + + val pretty = + Pretty.chunks [pretty_thm, pretty_term] + in + {props = [(successN, "false")], pretty = pretty} + end + + val {interactive, ...} = Data.get (Context.Proof ctxt) + val {parent, ...} = Data.get (Context.Proof ctxt') + + fun mk_promise result = + let + val result_id = #1 result + + fun to_response "exit" = + false + | to_response "redo" = + (Option.app output_result + (mk_generic_result ignoreN "Ignore" true empty_payload ctxt'); + true) + | to_response _ = + raise Fail "Simplifier_Trace.indicate_failure: invalid message" + in + if not interactive then + (output_result result; Future.value false) + else + Future.map to_response (send_request result) + end + in + case mk_generic_result hintN "Step failed" true payload ctxt' of + NONE => Future.value false + | SOME res => mk_promise res + end + +fun indicate_success thm ctxt = + let + fun payload () = + {props = [(successN, "true")], + pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)} + in + Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt) + end + +(** setup **) + +fun simp_if_continue args ctxt cont = + let + val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args + val data = + {term = term, + unconditional = unconditional, + ctxt = ctxt, + thm = thm, + rrule = rrule} + in + case Future.join (step data) of + NONE => + NONE + | SOME ctxt' => + let val res = cont ctxt' in + case res of + NONE => + if Future.join (indicate_failure data ctxt') then + simp_if_continue args ctxt cont + else + NONE + | SOME (thm, _) => + (indicate_success thm ctxt'; + res) + end + end + +val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" val _ = Theory.setup (Simplifier.set_trace_ops - {trace_invoke = fn {depth, term} => fn ctxt => - (if Config.get ctxt simp_trace_test then - tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^ - Syntax.string_of_term ctxt term) - else (); ctxt), - trace_apply = fn args => fn ctxt => fn cont => - (if Config.get ctxt simp_trace_test then - tracing ("Simplifier " ^ @{make_string} args) - else (); cont ctxt)}) + {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term, + trace_apply = simp_if_continue}) + +val _ = + Isabelle_Process.protocol_command "Document.simp_trace_reply" + (fn [s, r] => + let + val serial = Markup.parse_int s + fun lookup_delete tab = + (Inttab.lookup tab serial, Inttab.delete_safe serial tab) + fun apply_result (SOME promise) = Future.fulfill promise r + | apply_result NONE = () (* FIXME handle protocol failure, just like in active.ML? *) + in + (Synchronized.change_result futures lookup_delete |> apply_result) + handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn + end) + +(** attributes **) + +val pat_parser = + Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic +val mode_parser: string parser = + Scan.optional + (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full")) + "normal" -(* PIDE protocol *) +val interactive_parser: bool parser = + Scan.optional (Args.$$$ "interactive" >> K true) false + +val depth_parser = + Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10 + +val config_parser = + (interactive_parser -- mode_parser -- depth_parser) >> + (fn ((interactive, mode), depth) => config mode interactive depth) -val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" +val _ = Theory.setup + (Attrib.setup @{binding break_term} + ((Scan.repeat1 pat_parser) >> term_breakpoint) + "declaration of a term breakpoint" #> + Attrib.setup @{binding break_thm} + (Scan.succeed thm_breakpoint) + "declaration of a theorem breakpoint" #> + Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser) + "simplifier trace configuration") end - diff -r 54b0352fb46d -r 885500f4aa6a src/Pure/Tools/simplifier_trace.scala --- a/src/Pure/Tools/simplifier_trace.scala Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Pure/Tools/simplifier_trace.scala Tue Feb 04 09:04:59 2014 +0000 @@ -1,18 +1,279 @@ /* Title: Pure/Tools/simplifier_trace.scala - Author: Lars Hupel, TU Muenchen + Author: Lars Hupel Interactive Simplifier trace. */ package isabelle +import scala.actors.Actor._ +import scala.annotation.tailrec +import scala.collection.immutable.SortedMap + object Simplifier_Trace { - /* PIDE protocol */ + + import Markup.Simp_Trace_Item + + + /* replies to the prover */ + + case class Answer private[Simplifier_Trace](val name: String, val string: String) + + object Answer + { + + object step + { + val skip = Answer("skip", "Skip") + val continue = Answer("continue", "Continue") + val continue_trace = Answer("continue_trace", "Continue (with full trace)") + val continue_passive = Answer("continue_passive", "Continue (without asking)") + val continue_disable = Answer("continue_disable", "Continue (without any trace)") + + val default = skip + val all = List(continue, continue_trace, continue_passive, continue_disable, skip) + } + + object hint_fail + { + val exit = Answer("exit", "Exit") + val redo = Answer("redo", "Redo") + + val default = exit + val all = List(redo, exit) + } + + } + + val all_answers = Answer.step.all ++ Answer.hint_fail.all + + + /* GUI interaction */ + + case object Event + + + /* manager actor */ + + private case class Handle_Results(session: Session, id: Document_ID.Command, results: Command.Results) + private case class Generate_Trace(results: Command.Results) + private case class Cancel(serial: Long) + private object Clear_Memory + private object Stop + case class Reply(session: Session, serial: Long, answer: Answer) + + case class Question(data: Simp_Trace_Item.Data, answers: List[Answer], default_answer: Answer) + + case class Context( + last_serial: Long = 0L, + questions: SortedMap[Long, Question] = SortedMap.empty + ) + { + + def +(q: Question): Context = + copy(questions = questions + ((q.data.serial, q))) + + def -(s: Long): Context = + copy(questions = questions - s) + + def with_serial(s: Long): Context = + copy(last_serial = Math.max(last_serial, s)) + + } + + case class Trace(entries: List[Simp_Trace_Item.Data]) + + case class Index(text: String, content: XML.Body) + + object Index + { + def of_data(data: Simp_Trace_Item.Data): Index = + Index(data.text, data.content) + } + + def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context = + (manager !? Handle_Results(session, id, results)).asInstanceOf[Context] + + def generate_trace(results: Command.Results): Trace = + (manager !? Generate_Trace(results)).asInstanceOf[Trace] + + def clear_memory() = + manager ! Clear_Memory + + def send_reply(session: Session, serial: Long, answer: Answer) = + manager ! Reply(session, serial, answer) + + private val manager = actor { + var contexts = Map.empty[Document_ID.Command, Context] + + var memory_children = Map.empty[Long, Set[Long]] + var memory = Map.empty[Index, Answer] + + def find_question(serial: Long): Option[(Document_ID.Command, Question)] = + contexts collectFirst { + case (id, context) if context.questions contains serial => + (id, context.questions(serial)) + } + + def do_cancel(serial: Long, id: Document_ID.Command) + { + // To save memory, we could try to remove empty contexts at this point. + // However, if a new serial gets attached to the same command_id after we deleted + // its context, its last_serial counter will start at 0 again, and we'll think the + // old serials are actually new + contexts += (id -> (contexts(id) - serial)) + } + + def do_reply(session: Session, serial: Long, answer: Answer) + { + session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name) + } + + loop { + react { + case Handle_Results(session, id, results) => + var new_context = contexts.getOrElse(id, Context()) + var new_serial = new_context.last_serial + + for ((serial, result) <- results.entries if serial > new_context.last_serial) + { + result match { + case Simp_Trace_Item(markup, data) => + import Simp_Trace_Item._ + + memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial)) + + markup match { + + case STEP => + val index = Index.of_data(data) + memory.get(index) match { + case None => + new_context += Question(data, Answer.step.all, Answer.step.default) + case Some(answer) => + do_reply(session, serial, answer) + } + + case HINT => + data.props match { + case Markup.Success(false) => + results.get(data.parent) match { + case Some(Simp_Trace_Item(STEP, _)) => + new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default) + case _ => + // unknown, better send a default reply + do_reply(session, data.serial, Answer.hint_fail.default) + } + case _ => + } + + case IGNORE => + // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP' + // entry, and that that 'STEP' entry is about to be replayed. Hence, we need + // to selectively purge the replies which have been memorized, going down from + // the parent to all leaves. + + @tailrec + def purge(queue: Vector[Long]): Unit = + queue match { + case s +: rest => + for (Simp_Trace_Item(STEP, data) <- results.get(s)) + memory -= Index.of_data(data) + val children = memory_children.getOrElse(s, Set.empty) + memory_children -= s + purge(rest ++ children.toVector) + case _ => + } + + purge(Vector(data.parent)) + + case _ => + } + + case _ => + } + + new_serial = serial + } + + new_context = new_context.with_serial(new_serial) + contexts += (id -> new_context) + reply(new_context) + + case Generate_Trace(results) => + // Since there are potentially lots of trace messages, we do not cache them here again. + // Instead, everytime the trace is being requested, we re-assemble it based on the + // current results. + + val items = + for { (_, Simp_Trace_Item(_, data)) <- results.entries } + yield data + + reply(Trace(items.toList)) + + case Cancel(serial) => + find_question(serial) match { + case Some((id, _)) => + do_cancel(serial, id) + case None => + System.err.println("handle_cancel: unknown serial " + serial) + } + + case Clear_Memory => + memory_children = Map.empty + memory = Map.empty + + case Stop => + contexts = Map.empty + exit("Simplifier_Trace: manager actor stopped") + + case Reply(session, serial, answer) => + find_question(serial) match { + case Some((id, Question(data, _, _))) => + if (data.markup == Markup.Simp_Trace_Item.STEP) + { + val index = Index.of_data(data) + memory += (index -> answer) + } + do_cancel(serial, id) + case None => + System.err.println("send_reply: unknown serial " + serial) + } + + do_reply(session, serial, answer) + session.trace_events.event(Event) + + case bad => + System.err.println("context_manager: bad message " + bad) + } + } + } + + + /* protocol handler */ class Handler extends Session.Protocol_Handler { - val functions = Map.empty[String, (Session.Prover, Isabelle_Process.Protocol_Output) => Boolean] + private def cancel( + prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = + msg.properties match { + case Markup.Cancel_Simp_Trace(serial) => + manager ! Cancel(serial) + true + case _ => + false + } + + override def stop(prover: Session.Prover) = + { + manager ! Clear_Memory + manager ! Stop + } + + val functions = Map( + Markup.CANCEL_SIMP_TRACE -> cancel _) } + } diff -r 54b0352fb46d -r 885500f4aa6a src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Pure/raw_simplifier.ML Tue Feb 04 09:04:59 2014 +0000 @@ -17,6 +17,7 @@ val simp_trace: bool Config.T type cong_name = bool * string type rrule + val mk_rrules: Proof.context -> thm list -> rrule list val eq_rrule: rrule * rrule -> bool type proc type solver @@ -571,6 +572,12 @@ fun extract_safe_rrules ctxt thm = maps (orient_rrule ctxt) (extract_rews ctxt [thm]); +fun mk_rrules ctxt thms = + let + val rews = extract_rews ctxt thms + val raw_rrules = flat (map (mk_rrule ctxt) rews) + in map mk_rrule2 raw_rrules end + (* add/del rules explicitly *) @@ -588,7 +595,6 @@ fun add_simp thm ctxt = ctxt addsimps [thm]; fun del_simp thm ctxt = ctxt delsimps [thm]; - (* congs *) local @@ -814,7 +820,7 @@ type trace_ops = {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context, - trace_apply: {unconditional: bool, term: term, thm: thm, name: string} -> + trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} -> Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option}; structure Trace_Ops = Theory_Data @@ -919,8 +925,9 @@ val eta_thm = Thm.eta_conversion t; val eta_t' = Thm.rhs_of eta_thm; val eta_t = term_of eta_t'; - fun rew {thm, name, lhs, elhs, extra, fo, perm} = + fun rew rrule = let + val {thm, name, lhs, elhs, extra, fo, perm} = rrule val prop = Thm.prop_of thm; val (rthm, elhs') = if maxt = ~1 orelse not extra then (thm, elhs) @@ -932,7 +939,7 @@ val prop' = Thm.prop_of thm'; val unconditional = (Logic.count_prems prop' = 0); val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop'); - val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', name = name}; + val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule}; in if perm andalso not (termless (rhs', lhs')) then diff -r 54b0352fb46d -r 885500f4aa6a src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Feb 04 09:04:59 2014 +0000 @@ -39,6 +39,8 @@ "src/rich_text_area.scala" "src/scala_console.scala" "src/sledgehammer_dockable.scala" + "src/simplifier_trace_dockable.scala" + "src/simplifier_trace_window.scala" "src/symbols_dockable.scala" "src/syslog_dockable.scala" "src/text_overview.scala" diff -r 54b0352fb46d -r 885500f4aa6a src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Tools/jEdit/src/Isabelle.props Tue Feb 04 09:04:59 2014 +0000 @@ -37,6 +37,7 @@ isabelle.protocol-panel \ isabelle.raw-output-panel \ isabelle.sledgehammer-panel \ + isabelle.simp-trace-panel \ isabelle.symbols-panel \ isabelle.syslog-panel \ isabelle.theories-panel \ @@ -47,6 +48,7 @@ isabelle.output-panel.label=Output panel isabelle.protocol-panel.label=Protocol panel isabelle.raw-output-panel.label=Raw Output panel +isabelle.simp-trace-panel.label=Simplifier trace panel isabelle.sledgehammer-panel.label=Sledgehammer panel isabelle.symbols-panel.label=Symbols panel isabelle.syslog-panel.label=Syslog panel @@ -59,6 +61,7 @@ isabelle-info.title=Info isabelle-monitor.title=Monitor isabelle-output.title=Output +isabelle-simp-trace.title=Simplifier trace isabelle-protocol.title=Protocol isabelle-raw-output.title=Raw Output isabelle-documentation.title=Documentation diff -r 54b0352fb46d -r 885500f4aa6a src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Tools/jEdit/src/actions.xml Tue Feb 04 09:04:59 2014 +0000 @@ -42,6 +42,11 @@ wm.addDockableWindow("isabelle-raw-output"); + + + wm.addDockableWindow("isabelle-simp-trace"); + + wm.addDockableWindow("isabelle-protocol"); @@ -147,4 +152,4 @@ isabelle.jedit.Isabelle.input_bsup(textArea); - \ No newline at end of file + diff -r 54b0352fb46d -r 885500f4aa6a src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Tools/jEdit/src/active.scala Tue Feb 04 09:04:59 2014 +0000 @@ -61,6 +61,9 @@ else text_area.setSelectedText(text) } + case Markup.Simp_Trace(serial, answer) => + Simplifier_Trace.send_reply(PIDE.session, serial, answer) + case Protocol.Dialog(id, serial, result) => model.session.dialog_result(id, serial, result) @@ -72,4 +75,3 @@ } } } - diff -r 54b0352fb46d -r 885500f4aa6a src/Tools/jEdit/src/dockables.xml --- a/src/Tools/jEdit/src/dockables.xml Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Tools/jEdit/src/dockables.xml Tue Feb 04 09:04:59 2014 +0000 @@ -41,4 +41,7 @@ new isabelle.jedit.Symbols_Dockable(view, position); - \ No newline at end of file + + new isabelle.jedit.Simplifier_Trace_Dockable(view, position); + + diff -r 54b0352fb46d -r 885500f4aa6a src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Feb 04 09:04:59 2014 +0000 @@ -81,6 +81,12 @@ case _ => None } + def docked_simplifier_trace(view: View): Option[Simplifier_Trace_Dockable] = + wm(view).getDockableWindow("isabelle-simp-trace") match { + case dockable: Simplifier_Trace_Dockable => Some(dockable) + case _ => None + } + def docked_protocol(view: View): Option[Protocol_Dockable] = wm(view).getDockableWindow("isabelle-protocol") match { case dockable: Protocol_Dockable => Some(dockable) diff -r 54b0352fb46d -r 885500f4aa6a src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Tue Feb 04 09:04:59 2014 +0000 @@ -189,6 +189,7 @@ isabelle-output.height=174 isabelle-output.width=412 isabelle-sledgehammer.dock-position=bottom +isabelle-simp-trace.dock-position=bottom isabelle-symbols.dock-position=bottom isabelle-theories.dock-position=right isabelle.complete.label=Complete Isabelle text diff -r 54b0352fb46d -r 885500f4aa6a src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Tue Feb 04 01:35:48 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Tue Feb 04 09:04:59 2014 +0000 @@ -270,7 +270,7 @@ private val active_include = - Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG) + Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE) def active(range: Text.Range): Option[Text.Info[XML.Elem]] = snapshot.select_markup(range, Some(active_include), command_state => @@ -281,7 +281,8 @@ case Text.Info(info_range, elem) => if (elem.name == Markup.BROWSER || elem.name == Markup.GRAPHVIEW || - elem.name == Markup.SENDBACK) + elem.name == Markup.SENDBACK || + elem.name == Markup.SIMP_TRACE) Some(Text.Info(snapshot.convert(info_range), elem)) else None }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None } diff -r 54b0352fb46d -r 885500f4aa6a src/Tools/jEdit/src/simplifier_trace_dockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 04 09:04:59 2014 +0000 @@ -0,0 +1,222 @@ +/* Title: Tools/jEdit/src/simplifier_trace_dockable.scala + Author: Lars Hupel + +Dockable window with interactive simplifier trace. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.actors.Actor._ + +import scala.swing.{Button, CheckBox, Orientation, Separator} +import scala.swing.event.ButtonClicked + +import java.awt.BorderLayout +import java.awt.event.{ComponentEvent, ComponentAdapter} + +import org.gjt.sp.jedit.View + +class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position) +{ + Swing_Thread.require() + + /* component state -- owned by Swing thread */ + + private var current_snapshot = Document.State.init.snapshot() + private var current_state = Command.empty.init_state + private var current_id = 0L + private var do_update = true + private var do_auto_reply = false + + + private val text_area = new Pretty_Text_Area(view) + set_content(text_area) + + private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.Tree = + { + val data = question.data + + def make_button(answer: Simplifier_Trace.Answer): XML.Tree = + XML.Wrapped_Elem( + Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)), + Nil, + List(XML.Text(answer.string)) + ) + + def make_block(body: XML.Body): XML.Body = + List(Pretty.Block(0, body)) + + val all = Pretty.separate( + XML.Text(data.text) :: + data.content ::: + make_block(Library.separate(XML.Text(", "), question.answers map make_button)) + ) + + XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(all))) + } + + private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context) + { + Swing_Thread.require() + val questions = context.questions.values + if (do_auto_reply && !questions.isEmpty) + { + questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer)) + handle_update(do_update) + } + else + { + val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut)) + text_area.update(snapshot, Command.Results.empty, contents) + do_paint() + } + } + + private def show_trace() + { + val trace = Simplifier_Trace.generate_trace(current_state.results) + new Simplifier_Trace_Window(view, current_snapshot, trace) + } + + private def do_paint() + { + Swing_Thread.later { + text_area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round) + } + } + + private def update_contents() + { + set_context( + current_snapshot, + Simplifier_Trace.handle_results(PIDE.session, current_id, current_state.results) + ) + } + + private def handle_resize() + { + do_paint() + } + + private def handle_update(follow: Boolean) + { + val (new_snapshot, new_state, new_id) = + PIDE.editor.current_node_snapshot(view) match { + case Some(snapshot) => + if (follow && !snapshot.is_outdated) { + PIDE.editor.current_command(view, snapshot) match { + case Some(cmd) => + (snapshot, snapshot.state.command_state(snapshot.version, cmd), cmd.id) + case None => + (Document.State.init.snapshot(), Command.empty.init_state, 0L) + } + } + else (current_snapshot, current_state, current_id) + case None => (current_snapshot, current_state, current_id) + } + + current_snapshot = new_snapshot + current_state = new_state + current_id = new_id + update_contents() + } + + + /* main actor */ + + private val main_actor = actor { + loop { + react { + case _: Session.Global_Options => + Swing_Thread.later { handle_resize() } + case changed: Session.Commands_Changed => + Swing_Thread.later { handle_update(do_update) } + case Session.Caret_Focus => + Swing_Thread.later { handle_update(do_update) } + case Simplifier_Trace.Event => + Swing_Thread.later { handle_update(do_update) } + case bad => System.err.println("Simplifier_Trace_Dockable: ignoring bad message " + bad) + } + } + } + + override def init() + { + Swing_Thread.require() + + PIDE.session.global_options += main_actor + PIDE.session.commands_changed += main_actor + PIDE.session.caret_focus += main_actor + PIDE.session.trace_events += main_actor + handle_update(true) + } + + override def exit() + { + Swing_Thread.require() + + PIDE.session.global_options -= main_actor + PIDE.session.commands_changed -= main_actor + PIDE.session.caret_focus -= main_actor + PIDE.session.trace_events -= main_actor + delay_resize.revoke() + } + + + /* resize */ + + private val delay_resize = + Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + + addComponentListener(new ComponentAdapter { + override def componentResized(e: ComponentEvent) { delay_resize.invoke() } + override def componentShown(e: ComponentEvent) { delay_resize.invoke() } + }) + + + /* controls */ + + private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)( + new CheckBox("Auto update") { + selected = do_update + reactions += { + case ButtonClicked(_) => + do_update = this.selected + handle_update(do_update) + } + }, + new Button("Update") { + reactions += { + case ButtonClicked(_) => + handle_update(true) + } + }, + new Separator(Orientation.Vertical), + new CheckBox("Auto reply") { + selected = do_auto_reply + reactions += { + case ButtonClicked(_) => + do_auto_reply = this.selected + handle_update(do_update) + } + }, + new Separator(Orientation.Vertical), + new Button("Show trace") { + reactions += { + case ButtonClicked(_) => + show_trace() + } + }, + new Button("Clear memory") { + reactions += { + case ButtonClicked(_) => + Simplifier_Trace.clear_memory() + } + } + ) + + add(controls.peer, BorderLayout.NORTH) +} diff -r 54b0352fb46d -r 885500f4aa6a src/Tools/jEdit/src/simplifier_trace_window.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 04 09:04:59 2014 +0000 @@ -0,0 +1,237 @@ +/* Title: Tools/jEdit/src/simplifier_trace_window.scala + Author: Lars Hupel + +Trace window with tree-style view of the simplifier trace. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.annotation.tailrec + +import scala.collection.immutable.SortedMap + +import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField} +import scala.swing.event.{Key, KeyPressed} + +import scala.util.matching.Regex + +import java.awt.BorderLayout +import java.awt.event.{ComponentEvent, ComponentAdapter} + +import javax.swing.SwingUtilities + +import org.gjt.sp.jedit.View + +private object Simplifier_Trace_Window +{ + + import Markup.Simp_Trace_Item + + sealed trait Trace_Tree + { + var children: SortedMap[Long, Elem_Tree] = SortedMap.empty + val serial: Long + val parent: Option[Trace_Tree] + var hints: List[Simp_Trace_Item.Data] + def set_interesting(): Unit + } + + final class Root_Tree(val serial: Long) extends Trace_Tree + { + val parent = None + val hints = Nil + def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints") + def set_interesting() = () + + def format(regex: Option[Regex]): XML.Body = + Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut)) + } + + final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree + { + val serial = data.serial + var hints = List.empty[Simp_Trace_Item.Data] + var interesting: Boolean = false + + def set_interesting(): Unit = + if (!interesting) + { + interesting = true + parent match { + case Some(p) => + p.set_interesting() + case None => + } + } + + def format(regex: Option[Regex]): (Boolean, XML.Tree) = + { + def format_child(child: Elem_Tree): Option[XML.Tree] = child.format(regex) match { + case (false, _) => + None + case (true, res) => + Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res))) + } + + def format_hint(data: Simp_Trace_Item.Data): XML.Tree = + Pretty.block(Pretty.separate( + XML.Text(data.text) :: + data.content + )) + + def body_contains(regex: Regex, body: XML.Body): Boolean = + body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined) + + val children_bodies: XML.Body = + children.values.filter(_.interesting).flatMap(format_child).toList + + lazy val hint_bodies: XML.Body = + hints.reverse.map(format_hint) + + val eligible = regex match { + case None => + true + case Some(r) => + body_contains(r, data.content) || hints.exists(h => body_contains(r, h.content)) + } + + val all = + if (eligible) + XML.Text(data.text) :: data.content ::: children_bodies ::: hint_bodies + else + XML.Text(data.text) :: children_bodies + + val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all)))) + + (eligible || children_bodies != Nil, res) + } + } + + @tailrec + def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit = + rest match { + case Nil => + () + case head :: tail => + lookup.get(head.parent) match { + case Some(parent) => + if (head.markup == Simp_Trace_Item.HINT) + { + parent.hints ::= head + walk_trace(tail, lookup) + } + else if (head.markup == Simp_Trace_Item.IGNORE) + { + parent.parent match { + case None => + System.err.println("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent) + case Some(tree) => + tree.children -= head.parent + walk_trace(tail, lookup) // FIXME discard from lookup + } + } + else + { + val entry = new Elem_Tree(head, Some(parent)) + parent.children += ((head.serial, entry)) + if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG) + entry.set_interesting() + walk_trace(tail, lookup + (head.serial -> entry)) + } + + case None => + System.err.println("Simplifier_Trace_Window: unknown parent " + head.parent) + } + } + +} + +class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame +{ + + import Simplifier_Trace_Window._ + + Swing_Thread.require() + + val area = new Pretty_Text_Area(view) + + size = new Dimension(500, 500) + contents = new BorderPanel { + layout(Component.wrap(area)) = BorderPanel.Position.Center + } + + private val tree = trace.entries.headOption match { + case Some(first) => + val tree = new Root_Tree(first.parent) + walk_trace(trace.entries, Map(first.parent -> tree)) + tree + case None => + new Root_Tree(0) + } + + do_update(None) + open() + do_paint() + + def do_update(regex: Option[Regex]) + { + val xml = tree.format(regex) + area.update(snapshot, Command.Results.empty, xml) + } + + def do_paint() + { + Swing_Thread.later { + area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round) + } + } + + def handle_resize() + { + do_paint() + } + + + /* resize */ + + private val delay_resize = + Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + + peer.addComponentListener(new ComponentAdapter { + override def componentResized(e: ComponentEvent) { delay_resize.invoke() } + override def componentShown(e: ComponentEvent) { delay_resize.invoke() } + }) + + + /* controls */ + + val use_regex = new CheckBox("Regex") + + private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)( + new Label { + text = "Search" + }, + new TextField(30) { + listenTo(keys) + reactions += { + case KeyPressed(_, Key.Enter, 0, _) => + val input = text.trim + val regex = + if (input.isEmpty) + None + else if (use_regex.selected) + Some(input.r) + else + Some(java.util.regex.Pattern.quote(input).r) + do_update(regex) + do_paint() + } + }, + use_regex + ) + + peer.add(controls.peer, BorderLayout.NORTH) +}