agda - 理解 Agda 中的 unquoteDecl

Question

我试图理解 Agda 的内置反射机制，所以我决定编写一个简单的函数，它接受一个字符串作为标识符，
一个带引号的类型和一个带引号的术语，并用给定的字符串标识符简单地定义给定类型的术语。因此，我写了以下内容:

testDefineName' : String → TC Type → TC Term → TC ⊤
testDefineName' s t a =
   bindTC (freshName s)
     (λ n → bindTC t
     (λ t' → bindTC a
     (λ a' → (bindTC (declareDef (arg (arg-info visible relevant) n) t')
     (λ _ → defineFun n ((clause [] a') ∷ []))))))

unquoteDecl = (testDefineName' "test" (quoteTC ℕ) (quoteTC zero))

这种类型检查，但是，当我尝试在其他地方使用“测试”时，我得到了 Not in scope: test错误。

documentation为 unquoteDecl有点不透明。显然声明应该是这样的形式

unquoteDecl x_1 x_2 ... x_n = m

哪里 x_i是 Name s 和 m有类型 TC \top ，所以也许我试图做的实际上是不可能的，但我仍然不明白这个机制是如何工作的:if m必须是 TC ⊤ 类型，因此不能是名称 x_1 x_2 ... x_n 的函数，我不知道如何使用 unquoteDecl 将任何新名称带入范围内根本!

所以，总结一下:

是否可以使用 Agda 的反射机制定义像我这样的函数，以便我可以使用 String 将新名称带入作用域？争论？我想要的是这样的:

<boilerplate code for unquoting> testDefineName' "test" (quoteTC ℕ) (quoteTC zero)
test' : ℕ
test' = test

编译(即我实际上可以使用新名称“test”)

如果没有，通过什么机制可以 m使用名称 x_1 ... x_n ?可以 m实际上有一个像 List Name → TC ⊤ 这样的类型，与文档相反？

Answer 1

基于 the way Ulf uses unquoteDecl ，我的印象是您需要在 LHS 上列出将扩大范围的名称。

您设置的问题在于您不知道 Name当您从 String 生成一个新的时并且无法获得它AFAIK。我的印象是freshName只应该用于从策略内部生成内部名称。

如果您制作 testDefineName'拿个 Name而不是 String然后一切正常:

testDefineName' : Name → TC Type → TC Term → TC ⊤
testDefineName' n t a = bindTC t
               $ λ t' → bindTC a
               $ λ a' → bindTC (declareDef (arg (arg-info visible relevant) n) t')
               $ λ _  → defineFun n ((clause [] a') ∷ [])

unquoteDecl test = testDefineName' test (quoteTC ℕ) (quoteTC zero)