src/HOL/Library/Debug.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 61115 3a4400985780
permissions -rw-r--r--
isabelle update_cartouches;
haftmann@48427
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@48427
     2
wenzelm@60500
     3
section \<open>Debugging facilities for code generated towards Isabelle/ML\<close>
haftmann@48427
     4
haftmann@48427
     5
theory Debug
haftmann@48427
     6
imports Main
haftmann@48427
     7
begin
haftmann@48427
     8
haftmann@48427
     9
definition trace :: "String.literal \<Rightarrow> unit" where
haftmann@48427
    10
  [simp]: "trace s = ()"
haftmann@48427
    11
haftmann@48427
    12
definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
haftmann@48427
    13
  [simp]: "tracing s = id"
haftmann@48427
    14
haftmann@48427
    15
lemma [code]:
haftmann@48427
    16
  "tracing s = (let u = trace s in id)"
haftmann@48427
    17
  by simp
haftmann@48427
    18
haftmann@48427
    19
definition flush :: "'a \<Rightarrow> unit" where
haftmann@48427
    20
  [simp]: "flush x = ()"
haftmann@48427
    21
haftmann@48427
    22
definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
haftmann@48427
    23
  [simp]: "flushing x = id"
haftmann@48427
    24
haftmann@48427
    25
lemma [code, code_unfold]:
haftmann@48427
    26
  "flushing x = (let u = flush x in id)"
haftmann@48427
    27
  by simp
haftmann@48427
    28
haftmann@48427
    29
definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
haftmann@48427
    30
  [simp]: "timing s f x = f x"
haftmann@48427
    31
haftmann@52435
    32
code_printing
haftmann@52435
    33
  constant trace \<rightharpoonup> (Eval) "Output.tracing"
wenzelm@60500
    34
| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
haftmann@52435
    35
| constant timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
haftmann@48427
    36
haftmann@52435
    37
code_reserved Eval Output Timing
haftmann@48427
    38
haftmann@48427
    39
hide_const (open) trace tracing flush flushing timing
haftmann@48427
    40
haftmann@48427
    41
end
haftmann@48427
    42