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

[Alexander Krauss]

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