[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

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

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

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"}];



More information about the isabelle-dev mailing list