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;
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 section \<open>Debugging facilities for code generated towards Isabelle/ML\<close>
     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_printing
    33   constant trace \<rightharpoonup> (Eval) "Output.tracing"
    34 | constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
    35 | constant timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
    36 
    37 code_reserved Eval Output Timing
    38 
    39 hide_const (open) trace tracing flush flushing timing
    40 
    41 end
    42