Theory Tracing

theory Tracing
  imports
    "../heap_monad/Heap_Main"
    "HOL-Library.Code_Target_Numeral"
    Show.Show_Instances
begin

text ‹NB:
  A more complete solution could be built by using the following entry:
  🌐‹https://www.isa-afp.org/entries/Show.html›.
›

definition writeln :: "String.literal ⇒ unit" where
  "writeln = (λ s. ())"

code_printing
  constant writeln ⇀ (SML) "writeln _"

definition trace where
  "trace s x = (let a = writeln s in x)"

lemma trace_alt_def[simp]:
  "trace s x = (λ _. x) (writeln s)"
  unfolding trace_def by simp

definition (in heap_mem_defs) checkmem_trace ::
  "('k ⇒ String.literal) ⇒ 'k ⇒ (unit ⇒ 'v Heap) ⇒ 'v Heap"
  where
  "checkmem_trace trace_key param calc ≡
    Heap_Monad.bind (lookup param) (λ x.
    case x of
      Some x ⇒ trace (STR ''Hit '' + trace_key param) (return x)
    | None ⇒ trace (STR ''Miss ''  + trace_key param)
       Heap_Monad.bind (calc ()) (λ x.
        Heap_Monad.bind (update param x) (λ _.
        return x
      )
    )
  )
  "

lemma (in heap_mem_defs) checkmem_checkmem_trace:
  "checkmem param calc = checkmem_trace trace_key param (λ_. calc)"
  unfolding checkmem_trace_def checkmem_def trace_alt_def ..

definition nat_to_string :: "nat ⇒ String.literal" where
  "nat_to_string x = String.implode (show x)"

definition nat_pair_to_string :: "nat × nat ⇒ String.literal" where
  "nat_pair_to_string x = String.implode (show x)"

value "show (3 :: nat)"

paragraph ‹Code Setup›

lemmas [code] =
  heap_mem_defs.checkmem_trace_def

lemmas [code_unfold] =
  heap_mem_defs.checkmem_checkmem_trace[where trace_key = nat_to_string]
  heap_mem_defs.checkmem_checkmem_trace[where trace_key = nat_pair_to_string]

end