author | wenzelm |
Wed, 17 Jun 2015 11:03:05 +0200 | |
changeset 60500 | 903bb1495239 |
parent 58881 | b9556a055632 |
child 61115 | 3a4400985780 |
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 |
|
60500 | 3 |
section \<open>Debugging facilities for code generated towards Isabelle/ML\<close> |
48427
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" |
60500 | 34 |
| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close> |
52435
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 |