[Agda] Debugging Agda's syntaxes

[Ulf Norell]

On Mon, May 17, 2010 at 8:55 PM, David Haguenauer <haguenad at iro.umontreal.ca
> wrote:

> * Ulf Norell <ulfn at chalmers.se>, 2010-04-27 21:24:20 Tue:
> > On Tue, Apr 27, 2010 at 9:07 PM, David Haguenauer <
> haguenad at iro.umontreal.ca
> > > wrote:
> > > [...] I wish I were able to print my Agda code at different stages of
> > > translation.
> >
> > [...] 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.
>
> As a followup question: I'm attempting to pretty-print from within
> module ConcreteToAbstract, in function concreteToAbstract (because
> that seemed to be a good place). I can't really tell how to get a TCM
> there; is there a way to get a (possibly dummy) one, or should I print
> from somewhere else?
>

The scope monad used by concreteToAbstract is actually TCM, so you
can just call TCM functions as they are.

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