<div dir="ltr">My answer on SO: <a href="https://stackoverflow.com/a/47295996/1802306">https://stackoverflow.com/a/47295996/1802306</a><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Nov 14, 2017 at 7:18 PM, Anthony Cantor <span dir="ltr"><<a href="mailto:anthony-cantor@uiowa.edu" target="_blank">anthony-cantor@uiowa.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi, I'm hoping somebody can help me with my Agda question on stack<br>
overflow.<br>
<br>
<a href="https://stackoverflow.com/questions/47193486/how-do-i-check-whether-an-
agda-term-associated-with-a-specific-name-relies-on-ho?noredirect=1" rel="noreferrer" target="_blank">https://stackoverflow.com/<wbr>questions/47193486/how-do-i-<wbr>check-whether-an-<br>
agda-term-associated-with-a-<wbr>specific-name-relies-on-ho?<wbr>noredirect=1</a><br>
<br>
If anybody has any insight on my issue, especially any knowledge about<br>
whether the reflection library can normalize a term past a rewrite,<br>
please let me know (either by email or on stack overflow). The text of<br>
the SO question [1] is copied inline below for convenience.<br>
<br>
Thanks for any help anybody can provide!<br>
<br>
[1]<br>
For the purpose of a script I would like to query the agda compiler<br>
about the definition of a function in an agda source file. I would like<br>
to ask the question: does the function named by **X** rely on a hole,<br>
or not? (i.e. is it a "completed proof", or is it a "proof in<br>
progress"). Where **X** is the name of the function in the source file.<br>
<br>
For example, take the following example source file:<br>
<br>
open import Relation.Binary.<wbr>PropositionalEquality<br>
<br>
postulate<br>
A : Set<br>
x : A<br>
y : A<br>
z : A <br>
q1 : x ≡ y<br>
q2 : y ≡ z<br>
<br>
pf1 : x ≡ z<br>
pf1 = trans q1 q2 <br>
<br>
pf2 : z ≡ x<br>
pf2 rewrite q1 | q2 = refl<br>
<br>
I would like to be able to determine (in my script), does `pf2` rely on<br>
any holes? In this case the answer is no.<br>
<br>
Alternatively, suppose that file were something like:<br>
<br>
open import Relation.Binary.<wbr>PropositionalEquality<br>
<br>
postulate<br>
A : Set<br>
x : A<br>
y : A<br>
z : A <br>
q1 : x ≡ y<br>
q2 : y ≡ z<br>
<br>
pf1 : x ≡ z<br>
pf1 = trans q1 q2 <br>
<br>
lemma1 : z ≡ y<br>
lemma1 = {!!}<br>
<br>
pf2 : z ≡ x<br>
pf2 rewrite q1 = lemma1<br>
Now the answer to the question posed above is "yes": `pf2` is<br>
incomplete because it relies on a hole (indirectly, through lemma1).<br>
<br>
I know that I can find out the answer to the question: are there<br>
**any** functions in this agda source file that rely on holes. When we<br>
run the agda compiler on a source file, the return status will be 1 if<br>
there are "unsolved interaction metas", and the status will be 0 if<br>
everything is completed. However I would like to know the granular<br>
information of whether a **particular** function (by name) within a<br>
source file has "unsolved interaction metas".<br>
<br>
Is there any way to do this?<br>
<br>
I looked through the source code for the interaction mode of agda (the<br>
interface used by the agda-mode emacs code), but it seems most of the<br>
commands defined for the interaction mode rely on character ranges<br>
rather than symbols, so I haven't found a way to get this information<br>
from interaction mode.<br>
<br>
EDIT: based on user3237465's comment, I looked into using reflection to<br>
solve this issue. It seems like it could work but there is an issue<br>
with rewrites. For example, suppose we have the following file loaded<br>
in emacs:<br>
<br>
open import Relation.Binary.<wbr>PropositionalEquality<br>
open import Agda.Builtin.Reflection<br>
<br>
postulate<br>
A : Set<br>
x : A<br>
y : A<br>
z : A <br>
q1 : x ≡ y<br>
q2 : y ≡ z<br>
<br>
pf1 : x ≡ z<br>
pf1 = trans q1 q2 <br>
<br>
lemma1 : z ≡ y<br>
lemma1 = {!!}<br>
<br>
pf2 : z ≡ x<br>
pf2 rewrite q1 = lemma1<br>
<br>
pf3 : z ≡ x<br>
pf3 = trans lemma1 (sym q1)<br>
<br>
-- user3237465 suggested this macro.<br>
-- unfortunately, normalizing `test`<br>
-- using this macro still doesn't show<br>
-- information about the contents of<br>
-- lemma1<br>
macro<br>
actualQuote : Term -> Term -> TC _<br>
actualQuote term hole =<br>
bindTC (normalise term) λ nterm -><br>
bindTC (quoteTC nterm) (unify hole)<br>
<br>
test = actualQuote pf2<br>
test2 = actualQuote pf3<br>
test3 = actualQuote pf1<br>
<br>
<br>
If I type C-c C-n and enter `quoteTC pf3`, it outputs `quoteTC (trans<br>
?0 (sym q1))`. This is what I wanted because it indicates that a the<br>
proof depends on a hole.<br>
<br>
On the other hand, if I type C-c C-n and enter `quoteTC pf2`, it<br>
outputs `quoteTC (pf2 | x | q1)`. So it appears that the normalization<br>
process can't see past a rewrite.<br>
<br>
Does anyone know if there is a way around this?<br>
<br>
EDIT2: the normalization of pf2 using user3237465's macro is:<br>
<br>
def (quote .test4.rewrite-20)<br>
(arg (arg-info visible relevant)<br>
(def (quote x) .Agda.Builtin.List.List.[])<br>
.Agda.Builtin.List.List.∷<br>
arg (arg-info visible relevant)<br>
(def (quote q1) .Agda.Builtin.List.List.[])<br>
.Agda.Builtin.List.List.∷ .Agda.Builtin.List.List.[])<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>