author | blanchet |
Thu, 06 Mar 2014 15:40:33 +0100 | |
changeset 55945 | e96383acecf9 |
parent 52435 | 6646bb548c6b |
child 58881 | b9556a055632 |
permissions | -rw-r--r-- |
48427
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
1 |
(* Author: Florian Haftmann, TU Muenchen *) |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
2 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
3 |
header {* Debugging facilities for code generated towards Isabelle/ML *} |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
4 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
5 |
theory Debug |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
6 |
imports Main |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
7 |
begin |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
8 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
9 |
definition trace :: "String.literal \<Rightarrow> unit" where |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
10 |
[simp]: "trace s = ()" |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
11 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
12 |
definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
13 |
[simp]: "tracing s = id" |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
14 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
15 |
lemma [code]: |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
16 |
"tracing s = (let u = trace s in id)" |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
17 |
by simp |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
18 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
19 |
definition flush :: "'a \<Rightarrow> unit" where |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
20 |
[simp]: "flush x = ()" |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
21 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
22 |
definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
23 |
[simp]: "flushing x = id" |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
24 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
25 |
lemma [code, code_unfold]: |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
26 |
"flushing x = (let u = flush x in id)" |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
27 |
by simp |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
28 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
29 |
definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
30 |
[simp]: "timing s f x = f x" |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
31 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51929
diff
changeset
|
32 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51929
diff
changeset
|
33 |
constant trace \<rightharpoonup> (Eval) "Output.tracing" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51929
diff
changeset
|
34 |
| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- {* note indirection via antiquotation *} |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51929
diff
changeset
|
35 |
| constant timing \<rightharpoonup> (Eval) "Timing.timeap'_msg" |
48427
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
36 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51929
diff
changeset
|
37 |
code_reserved Eval Output Timing |
48427
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
38 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
39 |
hide_const (open) trace tracing flush flushing timing |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
40 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
41 |
end |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
42 |