tuned
authorLars Hupel <lars.hupel@mytum.de>
Thu Mar 06 17:55:39 2014 +0100 (2014-03-06)
changeset 559465163ed3a38f5
parent 55945 e96383acecf9
child 55965 0c2c61a87a7d
tuned
src/Pure/Tools/simplifier_trace.ML
     1.1 --- a/src/Pure/Tools/simplifier_trace.ML	Thu Mar 06 15:40:33 2014 +0100
     1.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Thu Mar 06 17:55:39 2014 +0100
     1.3 @@ -34,7 +34,6 @@
     1.4  (
     1.5    type T =
     1.6      {max_depth: int,
     1.7 -     depth: int,
     1.8       mode: mode,
     1.9       interactive: bool,
    1.10       memory: bool,
    1.11 @@ -42,7 +41,6 @@
    1.12       breakpoints: term Item_Net.T * rrule Item_Net.T}
    1.13    val empty =
    1.14      {max_depth = 10,
    1.15 -     depth = 0,
    1.16       mode = Disabled,
    1.17       interactive = false,
    1.18       memory = true,
    1.19 @@ -55,7 +53,6 @@
    1.20       {max_depth = max_depth2, mode = mode2, interactive = interactive2,
    1.21        memory = memory2, breakpoints = breakpoints2, ...}: T) =
    1.22      {max_depth = Int.max (max_depth1, max_depth2),
    1.23 -     depth = 0,
    1.24       mode = merge_modes mode1 mode2,
    1.25       interactive = interactive1 orelse interactive2,
    1.26       memory = memory1 andalso memory2,
    1.27 @@ -65,9 +62,8 @@
    1.28  
    1.29  fun map_breakpoints f_term f_thm =
    1.30    Data.map
    1.31 -    (fn {max_depth, depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} =>
    1.32 +    (fn {max_depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} =>
    1.33        {max_depth = max_depth,
    1.34 -       depth = depth,
    1.35         mode = mode,
    1.36         interactive = interactive,
    1.37         memory = memory,
    1.38 @@ -110,9 +106,8 @@
    1.39        | "full" => Full
    1.40        | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode))
    1.41  
    1.42 -    val update = Data.map (fn {depth, parent, breakpoints, ...} =>
    1.43 +    val update = Data.map (fn {parent, breakpoints, ...} =>
    1.44        {max_depth = max_depth,
    1.45 -       depth = depth,
    1.46         mode = mode,
    1.47         interactive = interactive,
    1.48         memory = memory,
    1.49 @@ -154,7 +149,7 @@
    1.50  
    1.51  fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
    1.52    let
    1.53 -    val {max_depth, depth, mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt)
    1.54 +    val {mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt)
    1.55  
    1.56      val eligible =
    1.57        (case mode of
    1.58 @@ -167,7 +162,7 @@
    1.59        then Markup.simp_trace_logN
    1.60        else markup
    1.61    in
    1.62 -    if not eligible orelse depth > max_depth then NONE
    1.63 +    if not eligible then NONE
    1.64      else
    1.65        let
    1.66          val {props = more_props, pretty} = payload ()
    1.67 @@ -240,7 +235,7 @@
    1.68          {props = [], pretty = pretty}
    1.69        end
    1.70  
    1.71 -    val {max_depth, depth, mode, interactive, memory, breakpoints, ...} =
    1.72 +    val {max_depth, mode, interactive, memory, breakpoints, ...} =
    1.73        Data.get (Context.Proof ctxt)
    1.74  
    1.75      fun mk_promise result =
    1.76 @@ -249,7 +244,6 @@
    1.77  
    1.78          fun put mode' interactive' = Data.put
    1.79            {max_depth = max_depth,
    1.80 -           depth = depth,
    1.81             mode = mode',
    1.82             interactive = interactive',
    1.83             memory = memory,
    1.84 @@ -276,18 +270,17 @@
    1.85      | SOME res => mk_promise res)
    1.86    end
    1.87  
    1.88 -fun recurse text term ctxt =
    1.89 +fun recurse text depth term ctxt =
    1.90    let
    1.91      fun payload () =
    1.92        {props = [],
    1.93         pretty = Syntax.pretty_term ctxt term}
    1.94  
    1.95 -    val {max_depth, depth, mode, interactive, memory, breakpoints, ...} =
    1.96 +    val {max_depth, mode, interactive, memory, breakpoints, ...} =
    1.97        Data.get (Context.Proof ctxt)
    1.98  
    1.99      fun put result_id = Data.put
   1.100        {max_depth = max_depth,
   1.101 -       depth = depth + 1,
   1.102         mode = if depth >= max_depth then Disabled else mode,
   1.103         interactive = interactive,
   1.104         memory = memory,
   1.105 @@ -325,12 +318,9 @@
   1.106        end
   1.107  
   1.108      val {interactive, ...} = Data.get (Context.Proof ctxt)
   1.109 -    val {parent, ...} = Data.get (Context.Proof ctxt')
   1.110  
   1.111      fun mk_promise result =
   1.112        let
   1.113 -        val result_id = #1 result
   1.114 -
   1.115          fun to_response "exit" = false
   1.116            | to_response "redo" =
   1.117                (Option.app output_result
   1.118 @@ -389,7 +379,7 @@
   1.119  
   1.120  val _ = Theory.setup
   1.121    (Simplifier.set_trace_ops
   1.122 -    {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term,
   1.123 +    {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" depth term,
   1.124       trace_apply = simp_apply})
   1.125  
   1.126  val _ =