[Agda] Debugging Agda's syntaxes

[Ulf Norell]

On Tue, Apr 27, 2010 at 9:07 PM, David Haguenauer <haguenad at iro.umontreal.ca
> wrote:

> 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.
>

Pretty printing for the Concrete syntax is defined in
Agda.Syntax.Concrete.Pretty.
Abstract syntax can be pretty printed using
Agda.Syntax.Abstract.Pretty.prettyA
and Internal syntax with Agda.TypeChecking.Pretty.prettyTCM. The pretty
printers for Abstract and Internal syntax run in the type checking monad,
since
they use the current scope to figure out how to print things.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100427/f0a08b21/attachment.html