如何检查与特定名称关联的 agda 术语是否依赖于 hole？

Question

出于脚本的目的，我想查询 agda 编译器有关 agda 源文件中函数定义的信息。我想请教一个问题：X命名的函数是依赖空洞的，还是不依赖空洞的？（即它是 "completed proof"，还是 "proof in progress"）。其中 X 是源文件中函数的名称。

例如，拿下面的例子源文件：

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

我希望能够确定（在我的脚本中），pf2 是否依赖于任何漏洞？在这种情况下，答案是否定的。

或者，假设该文件类似于：

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

现在上面提出的问题的答案是"yes"：pf2是不完整的，因为它依赖于一个洞（间接地，通过引理1）。

我知道我可以找到问题的答案：这个agda源文件中是否有任何函数依赖漏洞。当我们运行 agda compiler on a source file时，如果有"unsolved interaction metas"则return状态为1，如果一切完成则状态为0。但是我想知道源文件中的特定函数（按名称）是否具有 "unsolved interaction metas".

的详细信息

有什么办法吗？

我查看了agda交互模式的源代码（agda-mode emacs代码使用的接口），但似乎大多数为交互模式定义的命令依赖于字符范围而不是符号，所以我还没有找到从交互模式获取这些信息的方法。

编辑：根据 user3237465 的评论，我研究了使用反射来解决这个问题。看起来它可以工作，但重写存在问题。例如，假设我们在 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

如果我输入 C-c C-n 并输入 quoteTC pf3，它会输出 quoteTC (trans ?0 (sym q1))。这就是我想要的，因为它表明证明取决于一个漏洞。

另一方面，如果我输入 C-c C-n 并输入 quoteTC pf2，它会输出 quoteTC (pf2 | x | q1)。所以规范化过程似乎看不到重写。

有谁知道是否有办法解决这个问题？

EDIT2：使用 user3237465 的宏对 pf2 进行规范化是：

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

这个答案是关于使用反射来解决问题的。

你的尝试中缺少的东西是使用 getDefinition 来查看定义的函数。

这是一个使用 agda-prelude (https://github.com/UlfNorell/agda-prelude) 的完整示例，因为我没有时间用标准库来解决这个问题（reader 的练习）。

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

我们需要跟踪我们已经查看过的名称以避免在递归函数上循环，所以让我们使用状态 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

不幸的是，我们无法说服终止检查器只能定义有限数量的函数，所以让我们作弊吧。如果我们运行超出深度，则不作弊选项将设置深度限制和 return true（或不知道）。

{-# 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

我无法抗拒对 checkName 使用 do-notation，因为它使代码更漂亮。如果你不是从 github 构建最新的 Agda，你可以使用注释代码：

  -- 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

使用 anyMetas 函数，我们可以定义一个宏，使用一个名称和 returning 一个布尔值来指示该名称是否依赖于元数据。

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

你的测试用例现在通过了

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

如何检查与特定名称关联的 agda 术语是否依赖于 hole？

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

emacs

agda

agda-mode