[Agda] How do I check whether an agda term associated with a specific name relies on hole?

[Anthony Cantor]

Hi, I'm hoping somebody can help me with my Agda question on stack
overflow.

https://stackoverflow.com/questions/47193486/how-do-i-check-whether-an-
agda-term-associated-with-a-specific-name-relies-on-ho?noredirect=1

If anybody has any insight on my issue, especially any knowledge about
whether the reflection library can normalize a term past a rewrite,
please let me know (either by email or on stack overflow). The text of
the SO question [1] is copied inline below for convenience.

Thanks for any help anybody can provide!

[1]
For the purpose of a script I would like to query the agda compiler
about the definition of a function in an agda source file. I would like
to ask the question: does the function named by **X** rely on a hole,
or not? (i.e. is it a "completed proof", or is it a "proof in
progress"). Where **X** is the name of the function in the source file.

For example, take the following example source file:

    open import Relation.Binary.PropositionalEquality
    
    postulate
      A : Set
      x : A
      y : A
      z : A  
      q1 : x ≡ y
      q2 : y ≡ z
    
    pf1 : x ≡ z
    pf1 = trans q1 q2 
    
    pf2 : z ≡ x
    pf2 rewrite q1 | q2 = refl

I would like to be able to determine (in my script), does `pf2` rely on
any holes? In this case the answer is no.

Alternatively, suppose that file were something like:

    open import Relation.Binary.PropositionalEquality
    
    postulate
      A : Set
      x : A
      y : A
      z : A  
      q1 : x ≡ y
      q2 : y ≡ z
    
    pf1 : x ≡ z
    pf1 = trans q1 q2 

    lemma1 : z ≡ y
    lemma1 = {!!}

    pf2 : z ≡ x
    pf2 rewrite q1 = lemma1
Now the answer to the question posed above is "yes": `pf2` is
incomplete because it relies on a hole (indirectly, through lemma1).

I know that I can find out the answer to the question: are there
**any** functions in this agda source file that rely on holes. When we
run the agda compiler on a source file, the return status will be 1 if
there are "unsolved interaction metas", and the status will be 0 if
everything is completed. However I would like to know the granular
information of whether a **particular** function (by name) within a
source file has "unsolved interaction metas".

Is there any way to do this?

I looked through the source code for the interaction mode of agda (the
interface used by the agda-mode emacs code), but it seems most of the
commands defined for the interaction mode rely on character ranges
rather than symbols, so I haven't found a way to get this information
from interaction mode.

EDIT: based on user3237465's comment, I looked into using reflection to
solve this issue. It seems like it could work but there is an issue
with rewrites. For example, suppose we have the following file loaded
in emacs:

    open import Relation.Binary.PropositionalEquality
    open import Agda.Builtin.Reflection
    
    postulate
      A : Set
      x : A
      y : A
      z : A  
      q1 : x ≡ y
      q2 : y ≡ z
    
    pf1 : x ≡ z
    pf1 = trans q1 q2 
    
    lemma1 : z ≡ y
    lemma1 = {!!}
    
    pf2 : z ≡ x
    pf2 rewrite q1 = lemma1
    
    pf3 : z ≡ x
    pf3 = trans lemma1 (sym q1)
    
    -- user3237465 suggested this macro.
    -- unfortunately, normalizing `test`
    -- using this macro still doesn't show
    -- information about the contents of
    -- lemma1
    macro
      actualQuote : Term -> Term -> TC _
      actualQuote term hole =
        bindTC (normalise term) λ nterm ->
        bindTC (quoteTC nterm) (unify hole)
    
    test = actualQuote pf2
    test2 = actualQuote pf3
    test3 = actualQuote pf1


If I type C-c C-n and enter `quoteTC pf3`, it outputs `quoteTC (trans
?0 (sym q1))`. This is what I wanted because it indicates that a the
proof depends on a hole.

On the other hand, if I type C-c C-n and enter `quoteTC pf2`, it
outputs `quoteTC (pf2 | x | q1)`. So it appears that the normalization
process can't see past a rewrite.

Does anyone know if there is a way around this?

EDIT2: the normalization of pf2 using user3237465's macro is:

    def (quote .test4.rewrite-20)
    (arg (arg-info visible relevant)
     (def (quote x) .Agda.Builtin.List.List.[])
     .Agda.Builtin.List.List.∷
     arg (arg-info visible relevant)
     (def (quote q1) .Agda.Builtin.List.List.[])
     .Agda.Builtin.List.List.∷ .Agda.Builtin.List.List.[])