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

Question

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.[])

Answer 1

This answer is about using reflection to solve the problem.

The thing missing from your attempt is using getDefinition to look inside defined functions.

Here's a complete example using agda-prelude (https://github.com/UlfNorell/agda-prelude) because I don't have time to figure out to do this with the standard library (exercise for the reader).

open import Prelude
open import Tactic.Reflection
open import Control.Monad.State
open import Container.Traversable

We need to keep track of which names we have already looked inside to avoid looping on recursive functions, so let's use a state monad.

M = StateT (List Name) TC

runM : {A : Set} → M A → TC A
runM m = fst <$> runStateT m []

isVisited : Name → M Bool
isVisited x = gets (elem x)

setVisited : Name → M ⊤
setVisited x = _ <$ modify (x ∷_)

anyM : {A : Set} → (A → M Bool) → List A → M Bool
anyM p xs = foldr _||_ false <$> traverse p xs

Unfortunately we're not going to be able to convince the termination checker that there can only be a finite number of defined functions, so let's cheat. The no-cheat option would be to set a depth limit and return true (or dont-know) if we run out of depth.

{-# TERMINATING #-}
anyMetas : Term → M Bool

checkClause : Clause → M Bool
checkClause (clause ps t) = anyMetas t
checkClause (absurd-clause ps) = return false

checkName : Name → M Bool
checkName f = do
  false ← isVisited f
    where true → return false
  function cs ← lift (getDefinition f)
    where _ → return false
  anyM checkClause cs

I couldn't resist using do-notation for checkName since it makes the code so much nicer. If you're not building the latest Agda from github, you can use the commented code:

  -- caseM isVisited f of λ where
  --   true → return false
  --   false → setVisited f >>
  --     (caseM lift (getDefinition f) of λ where
  --       (function cs) → anyM checkClause cs
  --       _ → return false)

 

anyMetaArgs = anyM (anyMetas ∘ unArg)

checkSort : Sort → M Bool
checkSort (set t) = anyMetas t
checkSort (lit n) = return false
checkSort unknown = return false

anyMetas (var x args) = anyMetaArgs args
anyMetas (con c args) = anyMetaArgs args
anyMetas (def f args) = (| checkName f || anyMetaArgs args |)
anyMetas (lam v t) = anyMetas (unAbs t)
anyMetas (pat-lam cs args) = (| anyM checkClause cs || anyMetaArgs args |)
anyMetas (pi a b) = (| anyMetas (unArg a) || anyMetas (unAbs b) |)
anyMetas (agda-sort s) = checkSort s
anyMetas (lit l) = return false
anyMetas (meta x x₁) = return true
anyMetas unknown = return false

With the anyMetas function we can define a macro taking a name and returning a boolean indicating if the name depends on a meta.

macro
  dependsOnMeta? : Name → Term → TC ⊤
  dependsOnMeta? x hole = unify hole =<< quoteTC =<< runM (anyMetas (def x []))

Your test case now goes through

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)

test1 : dependsOnMeta? pf1 ≡ false
test1 = refl

test2 : dependsOnMeta? pf2 ≡ true
test2 = refl

test3 : dependsOnMeta? pf3 ≡ true
test3 = refl