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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
