library theories for debugging and parallel computing using code generation towards Isabelle/ML
1 (* Author: Florian Haftmann, TU Muenchen *)
3 header {* Debugging facilities for code generated towards Isabelle/ML *}
9 definition trace :: "String.literal \<Rightarrow> unit" where
10 [simp]: "trace s = ()"
12 definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
13 [simp]: "tracing s = id"
16 "tracing s = (let u = trace s in id)"
19 definition flush :: "'a \<Rightarrow> unit" where
20 [simp]: "flush x = ()"
22 definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
23 [simp]: "flushing x = id"
25 lemma [code, code_unfold]:
26 "flushing x = (let u = flush x in id)"
29 definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
30 [simp]: "timing s f x = f x"
32 code_const trace and flush and timing
33 (Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg")
35 code_reserved Eval Output PolyML Timing
37 hide_const (open) trace tracing flush flushing timing