src/HOL/Library/Debug.thy
author Andreas Lochbihler
Wed Feb 27 10:33:30 2013 +0100 (2013-02-27)
changeset 51288 be7e9a675ec9
parent 48427 571cb1df0768
child 51929 5e8a0b8bb070
permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
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@48427
    32
code_const trace and flush and timing
haftmann@48427
    33
  (Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg")
haftmann@48427
    34
haftmann@48427
    35
code_reserved Eval Output PolyML Timing
haftmann@48427
    36
haftmann@48427
    37
hide_const (open) trace tracing flush flushing timing
haftmann@48427
    38
haftmann@48427
    39
end
haftmann@48427
    40