<br><div class="gmail_quote">On Tue, Apr 27, 2010 at 9:07 PM, David Haguenauer <span dir="ltr"><<a href="mailto:haguenad@iro.umontreal.ca">haguenad@iro.umontreal.ca</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi,<br>
<br>
Reading Agda's source code, I see that the intermediate language<br>
"Internal" (as defined in src/full/Agda/Syntax/Internal.hs) is made of<br>
datatypes that implement Show, whereas languages "Abstract" and<br>
"Concrete" are not.<br>
<br>
I wish I were able to print my Agda code at different stages of<br>
translation. Is there a standard way to do that? (I do not mind having<br>
to alter Agda's code.)<br>
<br>
As an example of what I would like to do, calling O'Caml's top level<br>
with undocumented option -dparsetree will cause each sentence to be<br>
pretty-printed in intermediate form before being evaluated.<br></blockquote><div><br></div><div>Pretty printing for the Concrete syntax is defined in Agda.Syntax.Concrete.Pretty.</div><div>Abstract syntax can be pretty printed using Agda.Syntax.Abstract.Pretty.prettyA</div>
<div>and Internal syntax with Agda.TypeChecking.Pretty.prettyTCM. The pretty</div><div>printers for Abstract and Internal syntax run in the type checking monad, since</div><div>they use the current scope to figure out how to print things.</div>
<div><br></div><div>/ Ulf</div></div>