Theory Debug

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Debugging facilities for code generated towards Isabelle/ML›

theory Debug
imports Main
begin

context
begin

qualified definition trace :: "String.literal ⇒ unit" where
  [simp]: "trace s = ()"

qualified definition tracing :: "String.literal ⇒ 'a ⇒ 'a" where
  [simp]: "tracing s = id"

lemma [code]:
  "tracing s = (let u = trace s in id)"
  by simp

qualified definition flush :: "'a ⇒ unit" where
  [simp]: "flush x = ()"

qualified definition flushing :: "'a ⇒ 'b ⇒ 'b" where
  [simp]: "flushing x = id"

lemma [code, code_unfold]:
  "flushing x = (let u = flush x in id)"
  by simp

qualified definition timing :: "String.literal ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" where
  [simp]: "timing s f x = f x"

end

code_printing
  constant Debug.trace ⇀ (Eval) "Output.tracing"
| constant Debug.flush ⇀ (Eval) "Output.tracing/ (@{make'_string} _)" ― ‹note indirection via antiquotation›
| constant Debug.timing ⇀ (Eval) "Timing.timeap'_msg"

code_reserved Eval Output Timing

end