理解 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))

此类型检查，但是，当我尝试在其他地方使用 "test" 时，我收到 Not in scope: test 错误。

unquoteDecl 的 documentation 有点不透明。 Appaently声明应该是

的形式

unquoteDecl x_1 x_2 ... x_n = m

其中 x_i 是 Name，而 m 的类型是 TC \top，所以也许我试图做的实际上是不可能的，但我仍然不明白这个机制是如何工作的：如果 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)

理解 Agda 中的 unquoteDecl

Understanding unquoteDecl in Agda

agda