瞭解Agda的unquoteDecl

我想了解Agda的內置反射機制，所以我決定寫一個簡單的函數，它需要一個標識符的字符串，引用類型和引用的術語，並簡單地定義一個術語具有給定字符串標識符的給定類型。因此，我寫了下面：瞭解Agda的unquoteDecl

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是一種不透明的。 Appaently聲明的形式應該

unquoteDecl x_1 x_2 ... x_n = m

其中x_i是Name S的，和m的類型是TC \top，所以也許我所試圖做的是沒有實際可能的，但我還是不明白這是如何機制的作品：如果m必須是TC ⊤類型，因此不能是名稱x_1 x_2 ... x_n的函數，我不明白如何使用unquoteDecl根本不可能將任何新名稱帶入範圍！

所以，總結一下：

是否可以定義像我這樣的功能使用阿格達的反射機制，這樣我可以使用String爭論帶來新的名稱爲範圍？我想是這樣的：

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

編譯通過什麼樣的機制能夠m利用名稱x_1 ... x_n的（即我可以實際使用新的名稱，「測試」）

，如果沒有，？與文檔相反，m實際上是否具有類似List Name → TC ⊤的類型？

來源

2017-03-31 Nathan BeDell

請在這些類型的職位import語句列表。 – gallais

根據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)

來源

2017-04-01 12:03:13 gallais

瞭解Agda的unquoteDecl

回答

相關問題