[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
More information about the isabelle-dev
mailing list