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

[Ulf Norell]

My answer on SO: https://stackoverflow.com/a/47295996/1802306

/ Ulf

On Tue, Nov 14, 2017 at 7:18 PM, Anthony Cantor <anthony-cantor at uiowa.edu>
wrote:

> 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.[])
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171114/5fdd276f/attachment-0001.html>