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