src/Pure/Tools/simplifier_trace.ML
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 63806 c54a53ef1873
child 67147 dea94b1aabc3
permissions -rw-r--r--
tuned signature;
     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 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
    12 end
    13 
    14 structure Simplifier_Trace: SIMPLIFIER_TRACE =
    15 struct
    16 
    17 (** context data **)
    18 
    19 datatype mode = Disabled | Normal | Full
    20 
    21 fun merge_modes Disabled m = m
    22   | merge_modes Normal Full = Full
    23   | merge_modes Normal _ = Normal
    24   | merge_modes Full _ = Full
    25 
    26 val empty_breakpoints =
    27   (Item_Net.init (op aconv) single,
    28    Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm))
    29 
    30 fun 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 
    34 structure 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 
    64 val get_data = Data.get o Context.Proof
    65 val put_data = Context.proof_map o Data.put
    66 
    67 val 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 
    74 val get_breakpoints = #breakpoints o get_data
    75 
    76 fun 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 
    86 fun add_term_breakpoint term =
    87   map_breakpoints (apfst (Item_Net.update term))
    88 
    89 fun 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 
    96 fun 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 
   116 fun 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 
   133 fun 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 
   140 val futures =
   141   Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table)
   142 
   143 
   144 
   145 (** markup **)
   146 
   147 fun output_result (id, data) =
   148   Output.result (Markup.serial_properties id) [data]
   149 
   150 val parentN = "parent"
   151 val textN = "text"
   152 val memoryN = "memory"
   153 val successN = "success"
   154 
   155 type payload =
   156   {props: Properties.T,
   157    pretty: Pretty.T}
   158 
   159 fun empty_payload () : payload =
   160   {props = [], pretty = Pretty.str ""}
   161 
   162 fun 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 
   196 fun 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 
   204 fun 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 
   217 type data = {term: term, thm: thm, unconditional: bool, ctxt: Proof.context, rrule: rrule}
   218 
   219 fun 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 
   291 fun 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 
   315 fun 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 
   360 fun 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 
   374 fun 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 
   397 val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
   398 
   399 val _ = Theory.setup
   400   (Simplifier.set_trace_ops
   401     {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" depth term,
   402      trace_apply = simp_apply})
   403 
   404 val _ =
   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 
   422 val mode_parser =
   423   Scan.optional
   424     (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full"))
   425     "normal"
   426 
   427 val interactive_parser =
   428   Scan.optional (Args.$$$ "interactive" >> K true) false
   429 
   430 val memory_parser =
   431   Scan.optional (Args.$$$ "no_memory" >> K false) true
   432 
   433 val depth_parser =
   434   Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10
   435 
   436 val config_parser =
   437   (interactive_parser -- mode_parser -- depth_parser -- memory_parser) >>
   438     (fn (((interactive, mode), depth), memory) => config mode interactive depth memory)
   439 
   440 val _ = Theory.setup
   441   (Attrib.setup @{binding simp_break}
   442     (Scan.repeat Args.term_pattern >> breakpoint)
   443     "declaration of a simplifier breakpoint" #>
   444    Attrib.setup @{binding simp_trace_new} (Scan.lift config_parser)
   445     "simplifier trace configuration")
   446 
   447 end