author | wenzelm |
Sat, 11 May 2013 16:13:08 +0200 | |
changeset 51929 | 5e8a0b8bb070 |
parent 48427 | 571cb1df0768 |
child 52435 | 6646bb548c6b |
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 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
32 |
code_const trace and flush and timing |
51929 | 33 |
(* FIXME proper @{make_string} instead of PolyML.makestring?!?! *) |
48427
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
34 |
(Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg") |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
35 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
36 |
code_reserved Eval Output PolyML Timing |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
37 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
38 |
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
|
39 |
|
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
40 |
end |
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
diff
changeset
|
41 |