(* Author: Florian Haftmann, TU Muenchen *)
header {* Debugging facilities for code generated towards Isabelle/ML *}
theory Debug
imports Main
begin
definition trace :: "String.literal \<Rightarrow> unit" where
[simp]: "trace s = ()"
definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
[simp]: "tracing s = id"
lemma [code]:
"tracing s = (let u = trace s in id)"
by simp
definition flush :: "'a \<Rightarrow> unit" where
[simp]: "flush x = ()"
definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
[simp]: "flushing x = id"
lemma [code, code_unfold]:
"flushing x = (let u = flush x in id)"
by simp
definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
[simp]: "timing s f x = f x"
code_const trace and flush and timing
(* FIXME proper @{make_string} instead of PolyML.makestring?!?! *)
(Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg")
code_reserved Eval Output PolyML Timing
hide_const (open) trace tracing flush flushing timing
end