2
$\begingroup$

In Coq, if I am unsure how a definition foo is defined, I can use the command Print foo. to inspect what foo looks like. If I am not satisfied with this, I can also build a dummy goal, say Goal foo = foo. and then use tactics such as unfold to gradually unroll the definition of foo (say I do first unfold foo., then I see another term bar so I can unfold bar., and so forth).

Is it possible to perform a similar task in Agda? I am aware of the ability to "normalize a term" (C-c C-n), and I could also look at the source Agda definition, but in my case I would very much like to inspect the body of a definition after elaboration, but before any form of normalization.

I also considered using reflection, in particular the getDefinition operation, but unfortunately this gives a value of type Definition only under the type-checking monad, and as far as I can tell there is no direct way to inspect this value.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ Note that top level pattern-matching functions are not match expressions like in Coq, they are their own thing, which is roughly regarded as postulated constants together with equality rules, and can't be "expanded". $\endgroup$
    – Trebor ♦
    Commented May 17, 2023 at 3:26
  • $\begingroup$ You are right, there is not really an all-encompassing notion of "term" as in Coq. But as far as I can tell the "Definition" type available in meta-programming corresponds to these postulated constants, so probably this is what I want to inspect. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented May 17, 2023 at 8:47

2 Answers 2

Reset to default
2
$\begingroup$

  1. What are you meaning by elaboration in this context? If you just want macros to be expanded, then C-c C-m will do what you want: you can give a term, and it will elaborate it (without normalizing it) and use it to fill the given hole. You might need to refine afterwards, I can't remember.

  2. To print TC values, you can use the debugPrint function, or for more heavy-duty things, you can use the Reflection external interface to e.g. write terms to files or do other logging. For either of these you probably want to use the functions in Reflection.AST.Show

Improve this answer
$\endgroup$
1
  • $\begingroup$ Basically, I have a top-level definition foo and I want to look at what the corresponding Definition built by Agda from it looks like. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented May 17, 2023 at 8:49
1
$\begingroup$

Here is a non-answer. Compile the master-sexp branch of my Agda s-expression extension, run agda with --sexp option and enjoy the glory of the internal representation in the generated .sexp file. (In Emacs, pp-buffer is your friend.)

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.