src/HOL/Library/Debug.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 52435 6646bb548c6b
child 58881 b9556a055632
permissions -rw-r--r--
more simplification rules on unary and binary minus
haftmann@48427
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@48427
     2
haftmann@48427
     3
header {* Debugging facilities for code generated towards Isabelle/ML *}
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"
haftmann@52435
    34
| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- {* note indirection via antiquotation *}
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