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