Как проверить, основывается ли термин agda, связанный с конкретным именем, на дыре?

Question

Для целей сценария я хотел бы запросить agda-компилятор об определении функции в исходном файле agda. Я хотел бы задать вопрос: функция, названная X, полагается на дыру или нет? (т.е. это "законченное доказательство" или "доказательство в процессе"). Где 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

Теперь ответ на поставленный выше вопрос - "да": pf2 неполный, потому что он опирается на дыру (косвенно, через лемму 1).

Я знаю, что могу найти ответ на вопрос: есть ли в этом исходном файле agda какие-либо функции, использующие дыры. Когда мы запускаем agda-компилятор для исходного файла, возвращаемое состояние будет равно 1, если есть "нерешенные мета взаимодействия", и состояние будет 0, если все будет выполнено. Однако я хотел бы знать детальную информацию о том, имеет ли конкретная функция (по имени) в исходном файле "неразрешенные мета-ды взаимодействия".

Есть какой-либо способ сделать это?

Я просмотрел исходный код для режима взаимодействия agda (интерфейс, используемый кодом emacs режима agda), но кажется, что большинство команд, определенных для режима взаимодействия, основаны на символьных диапазонах, а не на символах, поэтому я не нашел способ получить эту информацию из режима взаимодействия.

РЕДАКТИРОВАТЬ: на основе комментария 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

Если я наберу Cc Cn и введите quoteTC pf3, это выводит quoteTC (trans ?0 (sym q1)), Это то, что я хотел, потому что это указывает на то, что доказательство зависит от дыры.

С другой стороны, если я наберу Cc Cn и введу quoteTC pf2, это выводит quoteTC (pf2 | x | q1), Таким образом, кажется, что процесс нормализации не может видеть прошлое переписать.

Кто-нибудь знает, есть ли способ обойти это?

EDIT2: нормализация pf2 с использованием макроса user3237465:

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), потому что у меня нет времени, чтобы выяснить это со стандартной библиотекой (упражнение для читателя).

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

Нам нужно отслеживать, какие имена мы уже просмотрели, чтобы избежать зацикливания рекурсивных функций, поэтому давайте использовать монаду состояний.

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

К сожалению, мы не сможем убедить средство проверки завершения в том, что может быть только конечное число определенных функций, поэтому давайте обманем. Опция no-cheat - установить предел глубины и вернуть 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 так как это делает код намного приятнее. Если вы не собираете последнюю версию Agda из github, вы можете использовать закомментированный код:

  -- 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 С помощью функции мы можем определить макрос, принимающий имя и возвращающий логическое значение, указывающее, зависит ли имя от мета.

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