equal
deleted
inserted
replaced
|
1 (* Author: Florian Haftmann, TU Muenchen *) |
|
2 |
|
3 header {* Debugging facilities for code generated towards Isabelle/ML *} |
|
4 |
|
5 theory Debug |
|
6 imports Main |
|
7 begin |
|
8 |
|
9 definition trace :: "String.literal \<Rightarrow> unit" where |
|
10 [simp]: "trace s = ()" |
|
11 |
|
12 definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
13 [simp]: "tracing s = id" |
|
14 |
|
15 lemma [code]: |
|
16 "tracing s = (let u = trace s in id)" |
|
17 by simp |
|
18 |
|
19 definition flush :: "'a \<Rightarrow> unit" where |
|
20 [simp]: "flush x = ()" |
|
21 |
|
22 definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where |
|
23 [simp]: "flushing x = id" |
|
24 |
|
25 lemma [code, code_unfold]: |
|
26 "flushing x = (let u = flush x in id)" |
|
27 by simp |
|
28 |
|
29 definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
|
30 [simp]: "timing s f x = f x" |
|
31 |
|
32 code_const trace and flush and timing |
|
33 (Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg") |
|
34 |
|
35 code_reserved Eval Output PolyML Timing |
|
36 |
|
37 hide_const (open) trace tracing flush flushing timing |
|
38 |
|
39 end |
|
40 |