src/Pure/Tools/simplifier_trace.ML
author Lars Hupel <lars.hupel@mytum.de>
Tue Feb 11 11:30:33 2014 +0100 (2014-02-11)
changeset 55390 36550a4eac5e
parent 55335 8192d3acadbe
child 55552 e4907b74a347
permissions -rw-r--r--
"no_memory" option for the simplifier trace to bypass memoization
wenzelm@54730
     1
(*  Title:      Pure/Tools/simplifier_trace.ML
lars@55316
     2
    Author:     Lars Hupel
wenzelm@54730
     3
wenzelm@54730
     4
Interactive Simplifier trace.
wenzelm@54730
     5
*)
wenzelm@54730
     6
wenzelm@54730
     7
signature SIMPLIFIER_TRACE =
wenzelm@54730
     8
sig
lars@55316
     9
  val add_term_breakpoint: term -> Context.generic -> Context.generic
lars@55316
    10
  val add_thm_breakpoint: thm -> Context.generic -> Context.generic
wenzelm@54730
    11
end
wenzelm@54730
    12
wenzelm@54730
    13
structure Simplifier_Trace: SIMPLIFIER_TRACE =
wenzelm@54730
    14
struct
wenzelm@54730
    15
lars@55316
    16
(** background data **)
lars@55316
    17
lars@55316
    18
datatype mode = Disabled | Normal | Full
lars@55316
    19
lars@55316
    20
fun merge_modes Disabled m = m
lars@55316
    21
  | merge_modes Normal Full = Full
lars@55316
    22
  | merge_modes Normal _ = Normal
lars@55316
    23
  | merge_modes Full _ = Full
lars@55316
    24
lars@55316
    25
val empty_breakpoints =
lars@55316
    26
  (Item_Net.init (op =) single (* FIXME equality on terms? *),
lars@55316
    27
   Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm))
lars@55316
    28
lars@55316
    29
fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) =
lars@55316
    30
  (Item_Net.merge (term_bs1, term_bs2),
lars@55316
    31
   Item_Net.merge (thm_bs1, thm_bs2))
lars@55316
    32
lars@55316
    33
structure Data = Generic_Data
lars@55316
    34
(
lars@55316
    35
  type T =
lars@55316
    36
    {max_depth: int,
lars@55316
    37
     depth: int,
lars@55316
    38
     mode: mode,
lars@55316
    39
     interactive: bool,
lars@55390
    40
     memory: bool,
lars@55316
    41
     parent: int,
lars@55316
    42
     breakpoints: term Item_Net.T * rrule Item_Net.T}
lars@55316
    43
  val empty =
lars@55316
    44
    {max_depth = 10,
lars@55316
    45
     depth = 0,
lars@55316
    46
     mode = Disabled,
lars@55316
    47
     interactive = false,
lars@55390
    48
     memory = true,
lars@55316
    49
     parent = 0,
lars@55316
    50
     breakpoints = empty_breakpoints}
lars@55316
    51
  val extend = I
lars@55316
    52
  fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1,
lars@55390
    53
              memory = memory1, breakpoints = breakpoints1, ...}: T,
lars@55316
    54
             {max_depth = max_depth2, mode = mode2, interactive = interactive2,
lars@55390
    55
              memory = memory2, breakpoints = breakpoints2, ...}: T) =
lars@55316
    56
    {max_depth = Int.max (max_depth1, max_depth2),
lars@55316
    57
     depth = 0,
lars@55316
    58
     mode = merge_modes mode1 mode2,
lars@55316
    59
     interactive = interactive1 orelse interactive2,
lars@55390
    60
     memory = memory1 andalso memory2,
lars@55316
    61
     parent = 0,
lars@55335
    62
     breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T
lars@55316
    63
)
lars@55316
    64
lars@55316
    65
fun map_breakpoints f_term f_thm =
lars@55390
    66
  Data.map
lars@55390
    67
    (fn {max_depth, depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} =>
lars@55390
    68
      {max_depth = max_depth,
lars@55390
    69
       depth = depth,
lars@55390
    70
       mode = mode,
lars@55390
    71
       interactive = interactive,
lars@55390
    72
       memory = memory,
lars@55390
    73
       parent = parent,
lars@55390
    74
       breakpoints = (f_term term_bs, f_thm thm_bs)})
lars@55316
    75
lars@55316
    76
fun add_term_breakpoint term =
lars@55316
    77
  map_breakpoints (Item_Net.update term) I
lars@55316
    78
lars@55316
    79
fun add_thm_breakpoint thm context =
lars@55316
    80
  let
lars@55316
    81
    val rrules = mk_rrules (Context.proof_of context) [thm]
lars@55316
    82
  in
lars@55316
    83
    map_breakpoints I (fold Item_Net.update rrules) context
lars@55316
    84
  end
lars@55316
    85
lars@55316
    86
fun is_breakpoint (term, rrule) context =
lars@55316
    87
  let
lars@55316
    88
    val {breakpoints, ...} = Data.get context
lars@55316
    89
lars@55316
    90
    fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term)
lars@55316
    91
    val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term)
lars@55316
    92
lars@55316
    93
    val {thm = thm, ...} = rrule
lars@55316
    94
    val thm_matches = exists (eq_rrule o pair rrule)
lars@55316
    95
      (Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm))
lars@55316
    96
  in
lars@55316
    97
    (term_matches, thm_matches)
lars@55316
    98
  end
lars@55316
    99
lars@55316
   100
(** config and attributes **)
lars@55316
   101
lars@55390
   102
fun config raw_mode interactive max_depth memory =
lars@55316
   103
  let
lars@55316
   104
    val mode = case raw_mode of
lars@55316
   105
      "normal" => Normal
lars@55316
   106
    | "full" => Full
lars@55316
   107
    | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)
lars@55316
   108
lars@55316
   109
    val update = Data.map (fn {depth, parent, breakpoints, ...} =>
lars@55316
   110
      {max_depth = max_depth,
lars@55316
   111
       depth = depth,
lars@55316
   112
       mode = mode,
lars@55316
   113
       interactive = interactive,
lars@55390
   114
       memory = memory,
lars@55316
   115
       parent = parent,
lars@55316
   116
       breakpoints = breakpoints})
lars@55316
   117
  in Thm.declaration_attribute (K update) end
lars@55316
   118
lars@55316
   119
fun term_breakpoint terms =
lars@55316
   120
  Thm.declaration_attribute (K (fold add_term_breakpoint terms))
lars@55316
   121
lars@55316
   122
val thm_breakpoint =
lars@55316
   123
  Thm.declaration_attribute add_thm_breakpoint
lars@55316
   124
lars@55316
   125
(** tracing state **)
lars@55316
   126
lars@55316
   127
val futures =
lars@55316
   128
  Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table)
lars@55316
   129
lars@55316
   130
(** markup **)
lars@55316
   131
lars@55316
   132
fun output_result (id, data) =
lars@55316
   133
  Output.result (Markup.serial_properties id) data
lars@55316
   134
lars@55316
   135
val serialN = "serial"
lars@55316
   136
val parentN = "parent"
lars@55316
   137
val textN = "text"
lars@55390
   138
val memoryN = "memory"
lars@55316
   139
val successN = "success"
lars@55316
   140
lars@55316
   141
val logN = "simp_trace_log"
lars@55316
   142
val stepN = "simp_trace_step"
lars@55316
   143
val recurseN = "simp_trace_recurse"
lars@55316
   144
val hintN = "simp_trace_hint"
lars@55316
   145
val ignoreN = "simp_trace_ignore"
lars@55316
   146
lars@55316
   147
val cancelN = "simp_trace_cancel"
lars@55316
   148
lars@55316
   149
type payload =
lars@55316
   150
  {props: Properties.T,
lars@55316
   151
   pretty: Pretty.T}
lars@55316
   152
lars@55316
   153
fun empty_payload () : payload =
lars@55316
   154
  {props = [], pretty = Pretty.str ""}
lars@55316
   155
lars@55316
   156
fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
lars@55316
   157
  let
lars@55390
   158
    val {max_depth, depth, mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt)
lars@55316
   159
lars@55316
   160
    val eligible =
lars@55316
   161
      case mode of
lars@55316
   162
        Disabled => false
lars@55316
   163
      | Normal => triggered
lars@55316
   164
      | Full => true
lars@55316
   165
lars@55316
   166
    val markup' = if markup = stepN andalso not interactive then logN else markup
lars@55316
   167
  in
lars@55316
   168
    if not eligible orelse depth > max_depth then
lars@55316
   169
      NONE
lars@55316
   170
    else
lars@55316
   171
      let
lars@55316
   172
        val {props = more_props, pretty} = payload ()
lars@55316
   173
        val props =
lars@55316
   174
          [(textN, text),
lars@55390
   175
           (memoryN, Markup.print_bool memory),
lars@55316
   176
           (parentN, Markup.print_int parent)]
lars@55316
   177
        val data =
lars@55316
   178
          Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty])
lars@55316
   179
      in
lars@55316
   180
        SOME (serial (), data)
lars@55316
   181
      end
lars@55316
   182
  end
lars@55316
   183
lars@55316
   184
(** tracing output **)
lars@55316
   185
lars@55316
   186
fun send_request (result_id, content) =
lars@55316
   187
  let
lars@55316
   188
    fun break () =
lars@55316
   189
      (Output.protocol_message
lars@55316
   190
         [(Markup.functionN, cancelN),
lars@55316
   191
          (serialN, Markup.print_int result_id)]
lars@55316
   192
         "";
lars@55316
   193
       Synchronized.change futures (Inttab.delete_safe result_id))
lars@55316
   194
    val promise = Future.promise break : string future
lars@55316
   195
  in
lars@55316
   196
    Synchronized.change futures (Inttab.update_new (result_id, promise));
lars@55316
   197
    output_result (result_id, content);
lars@55316
   198
    promise
lars@55316
   199
  end
lars@55316
   200
lars@55316
   201
lars@55335
   202
type data = {term: term, thm: thm, unconditional: bool, ctxt: Proof.context, rrule: rrule}
lars@55335
   203
lars@55335
   204
fun step ({term, thm, unconditional, ctxt, rrule}: data) =
lars@55316
   205
  let
lars@55316
   206
    val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt)
lars@55316
   207
lars@55316
   208
    val {name, ...} = rrule
lars@55316
   209
    val term_triggered = not (null matching_terms)
wenzelm@54730
   210
lars@55316
   211
    val text =
lars@55316
   212
      if unconditional then
lars@55316
   213
        "Apply rewrite rule?"
lars@55316
   214
      else
lars@55316
   215
        "Apply conditional rewrite rule?"
lars@55316
   216
lars@55316
   217
    fun payload () =
lars@55316
   218
      let
lars@55316
   219
        (* FIXME pretty printing via Proof_Context.pretty_fact *)
lars@55316
   220
        val pretty_thm = Pretty.block
lars@55316
   221
          [Pretty.str ("Instance of " ^ name ^ ":"),
lars@55316
   222
           Pretty.brk 1,
lars@55316
   223
           Syntax.pretty_term ctxt (Thm.prop_of thm)]
lars@55316
   224
lars@55316
   225
        val pretty_term = Pretty.block
lars@55316
   226
          [Pretty.str "Trying to rewrite:",
lars@55316
   227
           Pretty.brk 1,
lars@55316
   228
           Syntax.pretty_term ctxt term]
lars@55316
   229
lars@55316
   230
        val pretty_matchings =
lars@55316
   231
          let
lars@55316
   232
            val items = map (Pretty.item o single o Syntax.pretty_term ctxt) matching_terms
lars@55316
   233
          in
lars@55316
   234
            if not (null matching_terms) then
lars@55316
   235
              [Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))]
lars@55316
   236
            else
lars@55316
   237
              []
lars@55316
   238
          end
lars@55316
   239
lars@55316
   240
        val pretty =
lars@55316
   241
          Pretty.chunks ([pretty_thm, pretty_term] @ pretty_matchings)
lars@55316
   242
      in
lars@55316
   243
        {props = [], pretty = pretty}
lars@55316
   244
      end
lars@55316
   245
lars@55390
   246
    val {max_depth, depth, mode, interactive, memory, breakpoints, ...} =
lars@55316
   247
      Data.get (Context.Proof ctxt)
lars@55316
   248
lars@55316
   249
    fun mk_promise result =
lars@55316
   250
      let
lars@55316
   251
        val result_id = #1 result
lars@55316
   252
lars@55316
   253
        fun put mode' interactive' = Data.put
lars@55316
   254
          {max_depth = max_depth,
lars@55316
   255
           depth = depth,
lars@55316
   256
           mode = mode',
lars@55316
   257
           interactive = interactive',
lars@55390
   258
           memory = memory,
lars@55316
   259
           parent = result_id,
lars@55316
   260
           breakpoints = breakpoints} (Context.Proof ctxt) |>
lars@55316
   261
          Context.the_proof
lars@55316
   262
lars@55316
   263
        fun to_response "skip" = NONE
lars@55316
   264
          | to_response "continue" = SOME (put mode true)
lars@55316
   265
          | to_response "continue_trace" = SOME (put Full true)
lars@55316
   266
          | to_response "continue_passive" = SOME (put mode false)
lars@55316
   267
          | to_response "continue_disable" = SOME (put Disabled false)
lars@55316
   268
          | to_response _ = raise Fail "Simplifier_Trace.step: invalid message"
lars@55316
   269
      in
lars@55316
   270
        if not interactive then
lars@55316
   271
          (output_result result; Future.value (SOME (put mode false)))
lars@55316
   272
        else
lars@55316
   273
          Future.map to_response (send_request result)
lars@55316
   274
      end
lars@55316
   275
lars@55316
   276
  in
lars@55316
   277
    case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of
lars@55316
   278
      NONE => Future.value (SOME ctxt)
lars@55316
   279
    | SOME res => mk_promise res
lars@55316
   280
  end
lars@55316
   281
lars@55316
   282
fun recurse text term ctxt =
lars@55316
   283
  let
lars@55316
   284
    fun payload () =
lars@55316
   285
      {props = [],
lars@55316
   286
       pretty = Syntax.pretty_term ctxt term}
lars@55316
   287
lars@55390
   288
    val {max_depth, depth, mode, interactive, memory, breakpoints, ...} =
lars@55390
   289
      Data.get (Context.Proof ctxt)
lars@55316
   290
lars@55316
   291
    fun put result_id = Data.put
lars@55316
   292
      {max_depth = max_depth,
lars@55316
   293
       depth = depth + 1,
lars@55316
   294
       mode = if depth >= max_depth then Disabled else mode,
lars@55316
   295
       interactive = interactive,
lars@55390
   296
       memory = memory,
lars@55316
   297
       parent = result_id,
lars@55316
   298
       breakpoints = breakpoints} (Context.Proof ctxt)
lars@55316
   299
lars@55316
   300
    val context' =
lars@55316
   301
      case mk_generic_result recurseN text true payload ctxt of
lars@55316
   302
        NONE =>
lars@55316
   303
          put 0
lars@55316
   304
      | SOME res =>
lars@55316
   305
          (output_result res; put (#1 res))
lars@55316
   306
  in Context.the_proof context' end
lars@55316
   307
lars@55335
   308
fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' =
lars@55316
   309
  let
lars@55316
   310
    fun payload () =
lars@55316
   311
      let
lars@55316
   312
        val {name, ...} = rrule
lars@55316
   313
        val pretty_thm =
lars@55316
   314
          (* FIXME pretty printing via Proof_Context.pretty_fact *)
lars@55316
   315
          Pretty.block
lars@55316
   316
            [Pretty.str ("In an instance of " ^ name ^ ":"),
lars@55316
   317
             Pretty.brk 1,
lars@55316
   318
             Syntax.pretty_term ctxt (Thm.prop_of thm)]
lars@55316
   319
lars@55316
   320
        val pretty_term =
lars@55316
   321
          Pretty.block
lars@55316
   322
            [Pretty.str "Was trying to rewrite:",
lars@55316
   323
             Pretty.brk 1,
lars@55316
   324
             Syntax.pretty_term ctxt term]
lars@55316
   325
lars@55316
   326
        val pretty =
lars@55316
   327
          Pretty.chunks [pretty_thm, pretty_term]
lars@55316
   328
      in
lars@55316
   329
        {props = [(successN, "false")], pretty = pretty}
lars@55316
   330
      end
lars@55316
   331
lars@55316
   332
    val {interactive, ...} = Data.get (Context.Proof ctxt)
lars@55316
   333
    val {parent, ...} = Data.get (Context.Proof ctxt')
lars@55316
   334
lars@55316
   335
    fun mk_promise result =
lars@55316
   336
      let
lars@55316
   337
        val result_id = #1 result
lars@55316
   338
lars@55316
   339
        fun to_response "exit" =
lars@55316
   340
              false
lars@55316
   341
          | to_response "redo" =
lars@55316
   342
              (Option.app output_result
lars@55316
   343
                (mk_generic_result ignoreN "Ignore" true empty_payload ctxt');
lars@55316
   344
               true)
lars@55316
   345
          | to_response _ =
lars@55316
   346
              raise Fail "Simplifier_Trace.indicate_failure: invalid message"
lars@55316
   347
      in
lars@55316
   348
        if not interactive then
lars@55316
   349
          (output_result result; Future.value false)
lars@55316
   350
        else
lars@55316
   351
          Future.map to_response (send_request result)
lars@55316
   352
      end
lars@55316
   353
  in
lars@55316
   354
    case mk_generic_result hintN "Step failed" true payload ctxt' of
lars@55316
   355
      NONE => Future.value false
lars@55316
   356
    | SOME res => mk_promise res
lars@55316
   357
  end
lars@55316
   358
lars@55316
   359
fun indicate_success thm ctxt =
lars@55316
   360
  let
lars@55316
   361
    fun payload () =
lars@55316
   362
      {props = [(successN, "true")],
lars@55316
   363
       pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)}
lars@55316
   364
  in
lars@55316
   365
    Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt)
lars@55316
   366
  end
lars@55316
   367
lars@55316
   368
(** setup **)
lars@55316
   369
lars@55390
   370
fun simp_apply args ctxt cont =
lars@55316
   371
  let
lars@55316
   372
    val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args
lars@55316
   373
    val data =
lars@55316
   374
      {term = term,
lars@55316
   375
       unconditional = unconditional,
lars@55316
   376
       ctxt = ctxt,
lars@55316
   377
       thm = thm,
lars@55316
   378
       rrule = rrule}
lars@55316
   379
  in
lars@55316
   380
    case Future.join (step data) of
lars@55316
   381
      NONE =>
lars@55316
   382
        NONE
lars@55316
   383
    | SOME ctxt' =>
lars@55316
   384
        let val res = cont ctxt' in
lars@55316
   385
          case res of
lars@55316
   386
            NONE =>
lars@55316
   387
              if Future.join (indicate_failure data ctxt') then
lars@55390
   388
                simp_apply args ctxt cont
lars@55316
   389
              else
lars@55316
   390
                NONE
lars@55316
   391
          | SOME (thm, _) =>
lars@55316
   392
              (indicate_success thm ctxt';
lars@55316
   393
               res)
lars@55316
   394
        end
lars@55316
   395
  end
lars@55316
   396
lars@55316
   397
val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
wenzelm@54730
   398
wenzelm@54730
   399
val _ = Theory.setup
wenzelm@54731
   400
  (Simplifier.set_trace_ops
lars@55316
   401
    {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term,
lars@55390
   402
     trace_apply = simp_apply})
lars@55316
   403
lars@55316
   404
val _ =
lars@55316
   405
  Isabelle_Process.protocol_command "Document.simp_trace_reply"
lars@55316
   406
    (fn [s, r] =>
lars@55316
   407
      let
lars@55316
   408
        val serial = Markup.parse_int s
lars@55316
   409
        fun lookup_delete tab =
lars@55316
   410
          (Inttab.lookup tab serial, Inttab.delete_safe serial tab)
lars@55316
   411
        fun apply_result (SOME promise) = Future.fulfill promise r
lars@55316
   412
          | apply_result NONE = () (* FIXME handle protocol failure, just like in active.ML? *)
lars@55316
   413
      in
lars@55316
   414
        (Synchronized.change_result futures lookup_delete |> apply_result)
lars@55316
   415
          handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn
lars@55316
   416
      end)
lars@55316
   417
lars@55316
   418
(** attributes **)
lars@55316
   419
lars@55316
   420
val pat_parser =
lars@55316
   421
  Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic
wenzelm@54730
   422
lars@55316
   423
val mode_parser: string parser =
lars@55316
   424
  Scan.optional
lars@55316
   425
    (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full"))
lars@55316
   426
    "normal"
wenzelm@54730
   427
lars@55316
   428
val interactive_parser: bool parser =
lars@55316
   429
  Scan.optional (Args.$$$ "interactive" >> K true) false
lars@55316
   430
lars@55390
   431
val memory_parser: bool parser =
lars@55390
   432
  Scan.optional (Args.$$$ "no_memory" >> K false) true
lars@55390
   433
lars@55316
   434
val depth_parser =
lars@55316
   435
  Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10
lars@55316
   436
lars@55316
   437
val config_parser =
lars@55390
   438
  (interactive_parser -- mode_parser -- depth_parser -- memory_parser) >>
lars@55390
   439
    (fn (((interactive, mode), depth), memory) => config mode interactive depth memory)
wenzelm@54730
   440
lars@55316
   441
val _ = Theory.setup
lars@55316
   442
  (Attrib.setup @{binding break_term}
lars@55316
   443
    ((Scan.repeat1 pat_parser) >> term_breakpoint)
lars@55316
   444
    "declaration of a term breakpoint" #>
lars@55316
   445
   Attrib.setup @{binding break_thm}
lars@55316
   446
    (Scan.succeed thm_breakpoint)
lars@55316
   447
    "declaration of a theorem breakpoint" #>
lars@55316
   448
   Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
lars@55316
   449
    "simplifier trace configuration")
wenzelm@54730
   450
wenzelm@54730
   451
end