src/HOL/Library/Debug.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 61585 a9599d3d7610
permissions -rw-r--r--
executable domain membership checks
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
wenzelm@61115
     9
context
wenzelm@61115
    10
begin
wenzelm@61115
    11
wenzelm@61115
    12
qualified definition trace :: "String.literal \<Rightarrow> unit" where
haftmann@48427
    13
  [simp]: "trace s = ()"
haftmann@48427
    14
wenzelm@61115
    15
qualified definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
haftmann@48427
    16
  [simp]: "tracing s = id"
haftmann@48427
    17
haftmann@48427
    18
lemma [code]:
haftmann@48427
    19
  "tracing s = (let u = trace s in id)"
haftmann@48427
    20
  by simp
haftmann@48427
    21
wenzelm@61115
    22
qualified definition flush :: "'a \<Rightarrow> unit" where
haftmann@48427
    23
  [simp]: "flush x = ()"
haftmann@48427
    24
wenzelm@61115
    25
qualified definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
haftmann@48427
    26
  [simp]: "flushing x = id"
haftmann@48427
    27
haftmann@48427
    28
lemma [code, code_unfold]:
haftmann@48427
    29
  "flushing x = (let u = flush x in id)"
haftmann@48427
    30
  by simp
haftmann@48427
    31
wenzelm@61115
    32
qualified definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
haftmann@48427
    33
  [simp]: "timing s f x = f x"
haftmann@48427
    34
wenzelm@61115
    35
end
wenzelm@61115
    36
haftmann@52435
    37
code_printing
wenzelm@61115
    38
  constant Debug.trace \<rightharpoonup> (Eval) "Output.tracing"
wenzelm@61585
    39
| constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" \<comment> \<open>note indirection via antiquotation\<close>
wenzelm@61115
    40
| constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
haftmann@48427
    41
haftmann@52435
    42
code_reserved Eval Output Timing
haftmann@48427
    43
haftmann@48427
    44
end
haftmann@48427
    45