src/HOL/Library/Debug.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (19 months ago)
changeset 67951 655aa11359dc
parent 61585 a9599d3d7610
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
     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 context
    10 begin
    11 
    12 qualified definition trace :: "String.literal \<Rightarrow> unit" where
    13   [simp]: "trace s = ()"
    14 
    15 qualified definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
    16   [simp]: "tracing s = id"
    17 
    18 lemma [code]:
    19   "tracing s = (let u = trace s in id)"
    20   by simp
    21 
    22 qualified definition flush :: "'a \<Rightarrow> unit" where
    23   [simp]: "flush x = ()"
    24 
    25 qualified definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
    26   [simp]: "flushing x = id"
    27 
    28 lemma [code, code_unfold]:
    29   "flushing x = (let u = flush x in id)"
    30   by simp
    31 
    32 qualified definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    33   [simp]: "timing s f x = f x"
    34 
    35 end
    36 
    37 code_printing
    38   constant Debug.trace \<rightharpoonup> (Eval) "Output.tracing"
    39 | constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" \<comment> \<open>note indirection via antiquotation\<close>
    40 | constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
    41 
    42 code_reserved Eval Output Timing
    43 
    44 end
    45