--- a/src/Pure/Tools/simplifier_trace.ML Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Tue Feb 04 09:04:59 2014 +0000
@@ -1,38 +1,435 @@
(* Title: Pure/Tools/simplifier_trace.ML
- Author: Lars Hupel, TU Muenchen
+ Author: Lars Hupel
Interactive Simplifier trace.
*)
signature SIMPLIFIER_TRACE =
sig
- val simp_trace_test: bool Config.T
+ val add_term_breakpoint: term -> Context.generic -> Context.generic
+ val add_thm_breakpoint: thm -> Context.generic -> Context.generic
end
structure Simplifier_Trace: SIMPLIFIER_TRACE =
struct
-(* Simplifier trace operations *)
+(** background data **)
+
+datatype mode = Disabled | Normal | Full
+
+fun merge_modes Disabled m = m
+ | merge_modes Normal Full = Full
+ | merge_modes Normal _ = Normal
+ | merge_modes Full _ = Full
+
+val empty_breakpoints =
+ (Item_Net.init (op =) single (* FIXME equality on terms? *),
+ Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm))
+
+fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) =
+ (Item_Net.merge (term_bs1, term_bs2),
+ Item_Net.merge (thm_bs1, thm_bs2))
+
+structure Data = Generic_Data
+(
+ type T =
+ {max_depth: int,
+ depth: int,
+ mode: mode,
+ interactive: bool,
+ parent: int,
+ breakpoints: term Item_Net.T * rrule Item_Net.T}
+ val empty =
+ {max_depth = 10,
+ depth = 0,
+ mode = Disabled,
+ interactive = false,
+ parent = 0,
+ breakpoints = empty_breakpoints}
+ val extend = I
+ fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1,
+ breakpoints = breakpoints1, ...},
+ {max_depth = max_depth2, mode = mode2, interactive = interactive2,
+ breakpoints = breakpoints2, ...}) =
+ {max_depth = Int.max (max_depth1, max_depth2),
+ depth = 0,
+ mode = merge_modes mode1 mode2,
+ interactive = interactive1 orelse interactive2,
+ parent = 0,
+ breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}
+)
+
+fun map_breakpoints f_term f_thm =
+ Data.map (fn {max_depth, depth, mode, interactive, parent, breakpoints = (term_bs, thm_bs)} =>
+ {max_depth = max_depth,
+ depth = depth,
+ mode = mode,
+ interactive = interactive,
+ parent = parent,
+ breakpoints = (f_term term_bs, f_thm thm_bs)})
+
+fun add_term_breakpoint term =
+ map_breakpoints (Item_Net.update term) I
+
+fun add_thm_breakpoint thm context =
+ let
+ val rrules = mk_rrules (Context.proof_of context) [thm]
+ in
+ map_breakpoints I (fold Item_Net.update rrules) context
+ end
+
+fun is_breakpoint (term, rrule) context =
+ let
+ val {breakpoints, ...} = Data.get context
+
+ fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term)
+ val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term)
+
+ val {thm = thm, ...} = rrule
+ val thm_matches = exists (eq_rrule o pair rrule)
+ (Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm))
+ in
+ (term_matches, thm_matches)
+ end
+
+(** config and attributes **)
+
+fun config raw_mode interactive max_depth =
+ let
+ val mode = case raw_mode of
+ "normal" => Normal
+ | "full" => Full
+ | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)
+
+ val update = Data.map (fn {depth, parent, breakpoints, ...} =>
+ {max_depth = max_depth,
+ depth = depth,
+ mode = mode,
+ interactive = interactive,
+ parent = parent,
+ breakpoints = breakpoints})
+ in Thm.declaration_attribute (K update) end
+
+fun term_breakpoint terms =
+ Thm.declaration_attribute (K (fold add_term_breakpoint terms))
+
+val thm_breakpoint =
+ Thm.declaration_attribute add_thm_breakpoint
+
+(** tracing state **)
+
+val futures =
+ Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table)
+
+(** markup **)
+
+fun output_result (id, data) =
+ Output.result (Markup.serial_properties id) data
+
+val serialN = "serial"
+val parentN = "parent"
+val textN = "text"
+val successN = "success"
+
+val logN = "simp_trace_log"
+val stepN = "simp_trace_step"
+val recurseN = "simp_trace_recurse"
+val hintN = "simp_trace_hint"
+val ignoreN = "simp_trace_ignore"
+
+val cancelN = "simp_trace_cancel"
+
+type payload =
+ {props: Properties.T,
+ pretty: Pretty.T}
+
+fun empty_payload () : payload =
+ {props = [], pretty = Pretty.str ""}
+
+fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
+ let
+ val {max_depth, depth, mode, interactive, parent, ...} = Data.get (Context.Proof ctxt)
+
+ val eligible =
+ case mode of
+ Disabled => false
+ | Normal => triggered
+ | Full => true
+
+ val markup' = if markup = stepN andalso not interactive then logN else markup
+ in
+ if not eligible orelse depth > max_depth then
+ NONE
+ else
+ let
+ val {props = more_props, pretty} = payload ()
+ val props =
+ [(textN, text),
+ (parentN, Markup.print_int parent)]
+ val data =
+ Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty])
+ in
+ SOME (serial (), data)
+ end
+ end
+
+(** tracing output **)
+
+fun send_request (result_id, content) =
+ let
+ fun break () =
+ (Output.protocol_message
+ [(Markup.functionN, cancelN),
+ (serialN, Markup.print_int result_id)]
+ "";
+ Synchronized.change futures (Inttab.delete_safe result_id))
+ val promise = Future.promise break : string future
+ in
+ Synchronized.change futures (Inttab.update_new (result_id, promise));
+ output_result (result_id, content);
+ promise
+ end
+
+
+fun step {term, thm, unconditional, ctxt, rrule} =
+ let
+ val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt)
+
+ val {name, ...} = rrule
+ val term_triggered = not (null matching_terms)
-val simp_trace_test =
- Attrib.setup_config_bool @{binding simp_trace_test} (K false)
+ val text =
+ if unconditional then
+ "Apply rewrite rule?"
+ else
+ "Apply conditional rewrite rule?"
+
+ fun payload () =
+ let
+ (* FIXME pretty printing via Proof_Context.pretty_fact *)
+ val pretty_thm = Pretty.block
+ [Pretty.str ("Instance of " ^ name ^ ":"),
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt (Thm.prop_of thm)]
+
+ val pretty_term = Pretty.block
+ [Pretty.str "Trying to rewrite:",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt term]
+
+ val pretty_matchings =
+ let
+ val items = map (Pretty.item o single o Syntax.pretty_term ctxt) matching_terms
+ in
+ if not (null matching_terms) then
+ [Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))]
+ else
+ []
+ end
+
+ val pretty =
+ Pretty.chunks ([pretty_thm, pretty_term] @ pretty_matchings)
+ in
+ {props = [], pretty = pretty}
+ end
+
+ val {max_depth, depth, mode, interactive, breakpoints, ...} =
+ Data.get (Context.Proof ctxt)
+
+ fun mk_promise result =
+ let
+ val result_id = #1 result
+
+ fun put mode' interactive' = Data.put
+ {max_depth = max_depth,
+ depth = depth,
+ mode = mode',
+ interactive = interactive',
+ parent = result_id,
+ breakpoints = breakpoints} (Context.Proof ctxt) |>
+ Context.the_proof
+
+ fun to_response "skip" = NONE
+ | to_response "continue" = SOME (put mode true)
+ | to_response "continue_trace" = SOME (put Full true)
+ | to_response "continue_passive" = SOME (put mode false)
+ | to_response "continue_disable" = SOME (put Disabled false)
+ | to_response _ = raise Fail "Simplifier_Trace.step: invalid message"
+ in
+ if not interactive then
+ (output_result result; Future.value (SOME (put mode false)))
+ else
+ Future.map to_response (send_request result)
+ end
+
+ in
+ case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of
+ NONE => Future.value (SOME ctxt)
+ | SOME res => mk_promise res
+ end
+
+fun recurse text term ctxt =
+ let
+ fun payload () =
+ {props = [],
+ pretty = Syntax.pretty_term ctxt term}
+
+ val {max_depth, depth, mode, interactive, breakpoints, ...} = Data.get (Context.Proof ctxt)
+
+ fun put result_id = Data.put
+ {max_depth = max_depth,
+ depth = depth + 1,
+ mode = if depth >= max_depth then Disabled else mode,
+ interactive = interactive,
+ parent = result_id,
+ breakpoints = breakpoints} (Context.Proof ctxt)
+
+ val context' =
+ case mk_generic_result recurseN text true payload ctxt of
+ NONE =>
+ put 0
+ | SOME res =>
+ (output_result res; put (#1 res))
+ in Context.the_proof context' end
+
+fun indicate_failure {term, ctxt, thm, rrule, ...} ctxt' =
+ let
+ fun payload () =
+ let
+ val {name, ...} = rrule
+ val pretty_thm =
+ (* FIXME pretty printing via Proof_Context.pretty_fact *)
+ Pretty.block
+ [Pretty.str ("In an instance of " ^ name ^ ":"),
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt (Thm.prop_of thm)]
+
+ val pretty_term =
+ Pretty.block
+ [Pretty.str "Was trying to rewrite:",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt term]
+
+ val pretty =
+ Pretty.chunks [pretty_thm, pretty_term]
+ in
+ {props = [(successN, "false")], pretty = pretty}
+ end
+
+ val {interactive, ...} = Data.get (Context.Proof ctxt)
+ val {parent, ...} = Data.get (Context.Proof ctxt')
+
+ fun mk_promise result =
+ let
+ val result_id = #1 result
+
+ fun to_response "exit" =
+ false
+ | to_response "redo" =
+ (Option.app output_result
+ (mk_generic_result ignoreN "Ignore" true empty_payload ctxt');
+ true)
+ | to_response _ =
+ raise Fail "Simplifier_Trace.indicate_failure: invalid message"
+ in
+ if not interactive then
+ (output_result result; Future.value false)
+ else
+ Future.map to_response (send_request result)
+ end
+ in
+ case mk_generic_result hintN "Step failed" true payload ctxt' of
+ NONE => Future.value false
+ | SOME res => mk_promise res
+ end
+
+fun indicate_success thm ctxt =
+ let
+ fun payload () =
+ {props = [(successN, "true")],
+ pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)}
+ in
+ Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt)
+ end
+
+(** setup **)
+
+fun simp_if_continue args ctxt cont =
+ let
+ val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args
+ val data =
+ {term = term,
+ unconditional = unconditional,
+ ctxt = ctxt,
+ thm = thm,
+ rrule = rrule}
+ in
+ case Future.join (step data) of
+ NONE =>
+ NONE
+ | SOME ctxt' =>
+ let val res = cont ctxt' in
+ case res of
+ NONE =>
+ if Future.join (indicate_failure data ctxt') then
+ simp_if_continue args ctxt cont
+ else
+ NONE
+ | SOME (thm, _) =>
+ (indicate_success thm ctxt';
+ res)
+ end
+ end
+
+val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
val _ = Theory.setup
(Simplifier.set_trace_ops
- {trace_invoke = fn {depth, term} => fn ctxt =>
- (if Config.get ctxt simp_trace_test then
- tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^
- Syntax.string_of_term ctxt term)
- else (); ctxt),
- trace_apply = fn args => fn ctxt => fn cont =>
- (if Config.get ctxt simp_trace_test then
- tracing ("Simplifier " ^ @{make_string} args)
- else (); cont ctxt)})
+ {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term,
+ trace_apply = simp_if_continue})
+
+val _ =
+ Isabelle_Process.protocol_command "Document.simp_trace_reply"
+ (fn [s, r] =>
+ let
+ val serial = Markup.parse_int s
+ fun lookup_delete tab =
+ (Inttab.lookup tab serial, Inttab.delete_safe serial tab)
+ fun apply_result (SOME promise) = Future.fulfill promise r
+ | apply_result NONE = () (* FIXME handle protocol failure, just like in active.ML? *)
+ in
+ (Synchronized.change_result futures lookup_delete |> apply_result)
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn
+ end)
+
+(** attributes **)
+
+val pat_parser =
+ Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic
+val mode_parser: string parser =
+ Scan.optional
+ (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full"))
+ "normal"
-(* PIDE protocol *)
+val interactive_parser: bool parser =
+ Scan.optional (Args.$$$ "interactive" >> K true) false
+
+val depth_parser =
+ Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10
+
+val config_parser =
+ (interactive_parser -- mode_parser -- depth_parser) >>
+ (fn ((interactive, mode), depth) => config mode interactive depth)
-val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
+val _ = Theory.setup
+ (Attrib.setup @{binding break_term}
+ ((Scan.repeat1 pat_parser) >> term_breakpoint)
+ "declaration of a term breakpoint" #>
+ Attrib.setup @{binding break_thm}
+ (Scan.succeed thm_breakpoint)
+ "declaration of a theorem breakpoint" #>
+ Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
+ "simplifier trace configuration")
end
-