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