# [isabelle-dev] Printing terms for debugging (Re: implicit beta normalization in the pretty-printer)

Alexander Krauss krauss at in.tum.de
Wed Jan 18 16:47:43 CET 2012

```On 01/18/2012 03:34 PM, Ondřej Kunčar wrote:
> It's a bit annoying if you want to do
> debugging on the ML level and you have to inspect every term by
> inspecting its ML representation (which is really tedious for larger
> terms).

This is a common problem, and everybody has come up with private hacks.
Mine goes roughly like this:

theory Dollar
imports Main
begin

consts dollar :: "('a::{} => 'b::{}) => 'a => 'b" (infixl "\$" 50)
consts box :: "'a::{} => 'a"
notation (output) box ("_")

ML {*
fun mk_dollar s t =
let
val sT as Type (_, [tT, resT]) = fastype_of s
in
Const (@{const_name box}, resT --> resT) \$
(Const (@{const_name dollar}, sT --> tT --> resT) \$ s \$ t)
end;

fun dollarize (s \$ t) = mk_dollar (dollarize s) (dollarize t)
| dollarize (Abs (x, T, b)) = Abs (x, T, dollarize b)
| dollarize t = t;

fun raw_print ctxt = writeln o Syntax.string_of_term ctxt o dollarize;
*}

ML {*
map (raw_print @{context})
[@{term "(\<lambda>x ((y,z),w). P)"},
@{term "x + y + z"},
@{term "{f x | x. P x }"},
@{term "(\<lambda>x. x)"} \$ @{term a},
@{term "(\<lambda>x. f x)"},
@{term "5::nat"}];
*}

end

Alex

```