"no_memory" option for the simplifier trace to bypass memoization
authorLars Hupel <lars.hupel@mytum.de>
Tue Feb 11 11:30:33 2014 +0100 (2014-02-11 ago)
changeset 5539036550a4eac5e
parent 55389 33f833231fa2
child 55391 eae296b5ef33
"no_memory" option for the simplifier trace to bypass memoization
src/Pure/PIDE/markup.scala
src/Pure/Tools/simplifier_trace.ML
src/Pure/Tools/simplifier_trace.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Feb 11 09:29:46 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Feb 11 11:30:33 2014 +0100
     1.3 @@ -399,6 +399,9 @@
     1.4    val SUCCESS = "success"
     1.5    val Success = new Properties.Boolean(SUCCESS)
     1.6  
     1.7 +  val MEMORY = "memory"
     1.8 +  val Memory = new Properties.Boolean(MEMORY)
     1.9 +
    1.10    val CANCEL_SIMP_TRACE = "simp_trace_cancel"
    1.11    object Cancel_Simp_Trace
    1.12    {
    1.13 @@ -454,6 +457,10 @@
    1.14  
    1.15      case class Data(serial: Long, markup: String, text: String,
    1.16                      parent: Long, props: Properties.T, content: XML.Body)
    1.17 +    {
    1.18 +      def memory: Boolean =
    1.19 +        Memory.unapply(props) getOrElse true
    1.20 +    }
    1.21  
    1.22    }
    1.23  
     2.1 --- a/src/Pure/Tools/simplifier_trace.ML	Tue Feb 11 09:29:46 2014 +0100
     2.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Tue Feb 11 11:30:33 2014 +0100
     2.3 @@ -37,6 +37,7 @@
     2.4       depth: int,
     2.5       mode: mode,
     2.6       interactive: bool,
     2.7 +     memory: bool,
     2.8       parent: int,
     2.9       breakpoints: term Item_Net.T * rrule Item_Net.T}
    2.10    val empty =
    2.11 @@ -44,29 +45,33 @@
    2.12       depth = 0,
    2.13       mode = Disabled,
    2.14       interactive = false,
    2.15 +     memory = true,
    2.16       parent = 0,
    2.17       breakpoints = empty_breakpoints}
    2.18    val extend = I
    2.19    fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1,
    2.20 -              breakpoints = breakpoints1, ...}: T,
    2.21 +              memory = memory1, breakpoints = breakpoints1, ...}: T,
    2.22               {max_depth = max_depth2, mode = mode2, interactive = interactive2,
    2.23 -              breakpoints = breakpoints2, ...}: T) =
    2.24 +              memory = memory2, breakpoints = breakpoints2, ...}: T) =
    2.25      {max_depth = Int.max (max_depth1, max_depth2),
    2.26       depth = 0,
    2.27       mode = merge_modes mode1 mode2,
    2.28       interactive = interactive1 orelse interactive2,
    2.29 +     memory = memory1 andalso memory2,
    2.30       parent = 0,
    2.31       breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T
    2.32  )
    2.33  
    2.34  fun map_breakpoints f_term f_thm =
    2.35 -  Data.map (fn {max_depth, depth, mode, interactive, parent, breakpoints = (term_bs, thm_bs)} =>
    2.36 -    {max_depth = max_depth,
    2.37 -     depth = depth,
    2.38 -     mode = mode,
    2.39 -     interactive = interactive,
    2.40 -     parent = parent,
    2.41 -     breakpoints = (f_term term_bs, f_thm thm_bs)})
    2.42 +  Data.map
    2.43 +    (fn {max_depth, depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} =>
    2.44 +      {max_depth = max_depth,
    2.45 +       depth = depth,
    2.46 +       mode = mode,
    2.47 +       interactive = interactive,
    2.48 +       memory = memory,
    2.49 +       parent = parent,
    2.50 +       breakpoints = (f_term term_bs, f_thm thm_bs)})
    2.51  
    2.52  fun add_term_breakpoint term =
    2.53    map_breakpoints (Item_Net.update term) I
    2.54 @@ -94,7 +99,7 @@
    2.55  
    2.56  (** config and attributes **)
    2.57  
    2.58 -fun config raw_mode interactive max_depth =
    2.59 +fun config raw_mode interactive max_depth memory =
    2.60    let
    2.61      val mode = case raw_mode of
    2.62        "normal" => Normal
    2.63 @@ -106,6 +111,7 @@
    2.64         depth = depth,
    2.65         mode = mode,
    2.66         interactive = interactive,
    2.67 +       memory = memory,
    2.68         parent = parent,
    2.69         breakpoints = breakpoints})
    2.70    in Thm.declaration_attribute (K update) end
    2.71 @@ -129,6 +135,7 @@
    2.72  val serialN = "serial"
    2.73  val parentN = "parent"
    2.74  val textN = "text"
    2.75 +val memoryN = "memory"
    2.76  val successN = "success"
    2.77  
    2.78  val logN = "simp_trace_log"
    2.79 @@ -148,7 +155,7 @@
    2.80  
    2.81  fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
    2.82    let
    2.83 -    val {max_depth, depth, mode, interactive, parent, ...} = Data.get (Context.Proof ctxt)
    2.84 +    val {max_depth, depth, mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt)
    2.85  
    2.86      val eligible =
    2.87        case mode of
    2.88 @@ -165,6 +172,7 @@
    2.89          val {props = more_props, pretty} = payload ()
    2.90          val props =
    2.91            [(textN, text),
    2.92 +           (memoryN, Markup.print_bool memory),
    2.93             (parentN, Markup.print_int parent)]
    2.94          val data =
    2.95            Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty])
    2.96 @@ -235,7 +243,7 @@
    2.97          {props = [], pretty = pretty}
    2.98        end
    2.99  
   2.100 -    val {max_depth, depth, mode, interactive, breakpoints, ...} =
   2.101 +    val {max_depth, depth, mode, interactive, memory, breakpoints, ...} =
   2.102        Data.get (Context.Proof ctxt)
   2.103  
   2.104      fun mk_promise result =
   2.105 @@ -247,6 +255,7 @@
   2.106             depth = depth,
   2.107             mode = mode',
   2.108             interactive = interactive',
   2.109 +           memory = memory,
   2.110             parent = result_id,
   2.111             breakpoints = breakpoints} (Context.Proof ctxt) |>
   2.112            Context.the_proof
   2.113 @@ -276,13 +285,15 @@
   2.114        {props = [],
   2.115         pretty = Syntax.pretty_term ctxt term}
   2.116  
   2.117 -    val {max_depth, depth, mode, interactive, breakpoints, ...} = Data.get (Context.Proof ctxt)
   2.118 +    val {max_depth, depth, mode, interactive, memory, breakpoints, ...} =
   2.119 +      Data.get (Context.Proof ctxt)
   2.120  
   2.121      fun put result_id = Data.put
   2.122        {max_depth = max_depth,
   2.123         depth = depth + 1,
   2.124         mode = if depth >= max_depth then Disabled else mode,
   2.125         interactive = interactive,
   2.126 +       memory = memory,
   2.127         parent = result_id,
   2.128         breakpoints = breakpoints} (Context.Proof ctxt)
   2.129  
   2.130 @@ -356,7 +367,7 @@
   2.131  
   2.132  (** setup **)
   2.133  
   2.134 -fun simp_if_continue args ctxt cont =
   2.135 +fun simp_apply args ctxt cont =
   2.136    let
   2.137      val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args
   2.138      val data =
   2.139 @@ -374,7 +385,7 @@
   2.140            case res of
   2.141              NONE =>
   2.142                if Future.join (indicate_failure data ctxt') then
   2.143 -                simp_if_continue args ctxt cont
   2.144 +                simp_apply args ctxt cont
   2.145                else
   2.146                  NONE
   2.147            | SOME (thm, _) =>
   2.148 @@ -388,7 +399,7 @@
   2.149  val _ = Theory.setup
   2.150    (Simplifier.set_trace_ops
   2.151      {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term,
   2.152 -     trace_apply = simp_if_continue})
   2.153 +     trace_apply = simp_apply})
   2.154  
   2.155  val _ =
   2.156    Isabelle_Process.protocol_command "Document.simp_trace_reply"
   2.157 @@ -417,12 +428,15 @@
   2.158  val interactive_parser: bool parser =
   2.159    Scan.optional (Args.$$$ "interactive" >> K true) false
   2.160  
   2.161 +val memory_parser: bool parser =
   2.162 +  Scan.optional (Args.$$$ "no_memory" >> K false) true
   2.163 +
   2.164  val depth_parser =
   2.165    Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10
   2.166  
   2.167  val config_parser =
   2.168 -  (interactive_parser -- mode_parser -- depth_parser) >>
   2.169 -    (fn ((interactive, mode), depth) => config mode interactive depth)
   2.170 +  (interactive_parser -- mode_parser -- depth_parser -- memory_parser) >>
   2.171 +    (fn (((interactive, mode), depth), memory) => config mode interactive depth memory)
   2.172  
   2.173  val _ = Theory.setup
   2.174    (Attrib.setup @{binding break_term}
     3.1 --- a/src/Pure/Tools/simplifier_trace.scala	Tue Feb 11 09:29:46 2014 +0100
     3.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Tue Feb 11 11:30:33 2014 +0100
     3.3 @@ -150,10 +150,10 @@
     3.4                    case STEP =>
     3.5                      val index = Index.of_data(data)
     3.6                      memory.get(index) match {
     3.7 -                      case None =>
     3.8 +                      case Some(answer) if data.memory =>
     3.9 +                        do_reply(session, serial, answer)
    3.10 +                      case _ =>
    3.11                          new_context += Question(data, Answer.step.all, Answer.step.default)
    3.12 -                      case Some(answer) =>
    3.13 -                        do_reply(session, serial, answer)
    3.14                      }
    3.15  
    3.16                    case HINT =>
    3.17 @@ -232,7 +232,7 @@
    3.18          case Reply(session, serial, answer) =>
    3.19            find_question(serial) match {
    3.20              case Some((id, Question(data, _, _))) =>
    3.21 -              if (data.markup == Markup.Simp_Trace_Item.STEP)
    3.22 +              if (data.markup == Markup.Simp_Trace_Item.STEP && data.memory)
    3.23                {
    3.24                  val index = Index.of_data(data)
    3.25                  memory += (index -> answer)