[Agda] Debugging Agda's syntaxes

[David Haguenauer]

Hi,

Reading Agda's source code, I see that the intermediate language
"Internal" (as defined in src/full/Agda/Syntax/Internal.hs) is made of
datatypes that implement Show, whereas languages "Abstract" and
"Concrete" are not.

I wish I were able to print my Agda code at different stages of
translation. Is there a standard way to do that? (I do not mind having
to alter Agda's code.)

As an example of what I would like to do, calling O'Caml's top level
with undocumented option -dparsetree will cause each sentence to be
pretty-printed in intermediate form before being evaluated.

-- 
Thanks,
David Haguenauer
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 254 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100427/c967d2e2/attachment.bin