# HG changeset patch # User Lars Hupel # Date 1392114633 -3600 # Node ID 36550a4eac5eb551ed086927d9decfa567d9b7ae # Parent 33f833231fa2c7af80991885e479ae1993f25d0b "no_memory" option for the simplifier trace to bypass memoization diff -r 33f833231fa2 -r 36550a4eac5e src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Feb 11 09:29:46 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Tue Feb 11 11:30:33 2014 +0100 @@ -399,6 +399,9 @@ val SUCCESS = "success" val Success = new Properties.Boolean(SUCCESS) + val MEMORY = "memory" + val Memory = new Properties.Boolean(MEMORY) + val CANCEL_SIMP_TRACE = "simp_trace_cancel" object Cancel_Simp_Trace { @@ -454,6 +457,10 @@ case class Data(serial: Long, markup: String, text: String, parent: Long, props: Properties.T, content: XML.Body) + { + def memory: Boolean = + Memory.unapply(props) getOrElse true + } } diff -r 33f833231fa2 -r 36550a4eac5e src/Pure/Tools/simplifier_trace.ML --- a/src/Pure/Tools/simplifier_trace.ML Tue Feb 11 09:29:46 2014 +0100 +++ b/src/Pure/Tools/simplifier_trace.ML Tue Feb 11 11:30:33 2014 +0100 @@ -37,6 +37,7 @@ depth: int, mode: mode, interactive: bool, + memory: bool, parent: int, breakpoints: term Item_Net.T * rrule Item_Net.T} val empty = @@ -44,29 +45,33 @@ depth = 0, mode = Disabled, interactive = false, + memory = true, parent = 0, breakpoints = empty_breakpoints} val extend = I fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1, - breakpoints = breakpoints1, ...}: T, + memory = memory1, breakpoints = breakpoints1, ...}: T, {max_depth = max_depth2, mode = mode2, interactive = interactive2, - breakpoints = breakpoints2, ...}: T) = + memory = memory2, breakpoints = breakpoints2, ...}: T) = {max_depth = Int.max (max_depth1, max_depth2), depth = 0, mode = merge_modes mode1 mode2, interactive = interactive1 orelse interactive2, + memory = memory1 andalso memory2, parent = 0, breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T ) 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)}) + Data.map + (fn {max_depth, depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} => + {max_depth = max_depth, + depth = depth, + mode = mode, + interactive = interactive, + memory = memory, + parent = parent, + breakpoints = (f_term term_bs, f_thm thm_bs)}) fun add_term_breakpoint term = map_breakpoints (Item_Net.update term) I @@ -94,7 +99,7 @@ (** config and attributes **) -fun config raw_mode interactive max_depth = +fun config raw_mode interactive max_depth memory = let val mode = case raw_mode of "normal" => Normal @@ -106,6 +111,7 @@ depth = depth, mode = mode, interactive = interactive, + memory = memory, parent = parent, breakpoints = breakpoints}) in Thm.declaration_attribute (K update) end @@ -129,6 +135,7 @@ val serialN = "serial" val parentN = "parent" val textN = "text" +val memoryN = "memory" val successN = "success" val logN = "simp_trace_log" @@ -148,7 +155,7 @@ 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 {max_depth, depth, mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt) val eligible = case mode of @@ -165,6 +172,7 @@ val {props = more_props, pretty} = payload () val props = [(textN, text), + (memoryN, Markup.print_bool memory), (parentN, Markup.print_int parent)] val data = Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty]) @@ -235,7 +243,7 @@ {props = [], pretty = pretty} end - val {max_depth, depth, mode, interactive, breakpoints, ...} = + val {max_depth, depth, mode, interactive, memory, breakpoints, ...} = Data.get (Context.Proof ctxt) fun mk_promise result = @@ -247,6 +255,7 @@ depth = depth, mode = mode', interactive = interactive', + memory = memory, parent = result_id, breakpoints = breakpoints} (Context.Proof ctxt) |> Context.the_proof @@ -276,13 +285,15 @@ {props = [], pretty = Syntax.pretty_term ctxt term} - val {max_depth, depth, mode, interactive, breakpoints, ...} = Data.get (Context.Proof ctxt) + val {max_depth, depth, mode, interactive, memory, 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, + memory = memory, parent = result_id, breakpoints = breakpoints} (Context.Proof ctxt) @@ -356,7 +367,7 @@ (** setup **) -fun simp_if_continue args ctxt cont = +fun simp_apply args ctxt cont = let val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args val data = @@ -374,7 +385,7 @@ case res of NONE => if Future.join (indicate_failure data ctxt') then - simp_if_continue args ctxt cont + simp_apply args ctxt cont else NONE | SOME (thm, _) => @@ -388,7 +399,7 @@ val _ = Theory.setup (Simplifier.set_trace_ops {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term, - trace_apply = simp_if_continue}) + trace_apply = simp_apply}) val _ = Isabelle_Process.protocol_command "Document.simp_trace_reply" @@ -417,12 +428,15 @@ val interactive_parser: bool parser = Scan.optional (Args.$$$ "interactive" >> K true) false +val memory_parser: bool parser = + Scan.optional (Args.$$$ "no_memory" >> K false) true + 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) + (interactive_parser -- mode_parser -- depth_parser -- memory_parser) >> + (fn (((interactive, mode), depth), memory) => config mode interactive depth memory) val _ = Theory.setup (Attrib.setup @{binding break_term} diff -r 33f833231fa2 -r 36550a4eac5e src/Pure/Tools/simplifier_trace.scala --- a/src/Pure/Tools/simplifier_trace.scala Tue Feb 11 09:29:46 2014 +0100 +++ b/src/Pure/Tools/simplifier_trace.scala Tue Feb 11 11:30:33 2014 +0100 @@ -150,10 +150,10 @@ case STEP => val index = Index.of_data(data) memory.get(index) match { - case None => + case Some(answer) if data.memory => + do_reply(session, serial, answer) + case _ => new_context += Question(data, Answer.step.all, Answer.step.default) - case Some(answer) => - do_reply(session, serial, answer) } case HINT => @@ -232,7 +232,7 @@ case Reply(session, serial, answer) => find_question(serial) match { case Some((id, Question(data, _, _))) => - if (data.markup == Markup.Simp_Trace_Item.STEP) + if (data.markup == Markup.Simp_Trace_Item.STEP && data.memory) { val index = Index.of_data(data) memory += (index -> answer)