アッダのunquoteDeclを理解する

Question

私はAgdaの反射メカニズムを理解しようとしていますので、識別子の文字列を引用し、引用された型と引用された用語を持つ単純な関数を書くことにしました。指定された文字列識別子を持つ指定された型の私は他の場所で「テスト」を使用しようとすると、私はNot in scope: testエラーを取得し、このタイプのチェックが

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

、しかし：したがって、私は次のように書きました。

unquoteDeclのdocumentationは不透明です。 Appaently宣言は、フォームx_iがName sは

unquoteDecl x_1 x_2 ... x_n = m 

のものでなければならない、と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 

がm名x_1 ... x_nを利用することができますどのようなメカニズムによって

とされていない場合を、（すなわち、私は実際に新しい名前、「テスト」を使用することができます）コンパイルする：何かのように私は何をしたいのですか？ mは実際にはドキュメントに反してList Name → TC ⊤のようなタイプがありますか？

Answer 1

the way Ulf uses unquoteDeclに基づいて、スコープを拡張する予定の名前をLHSにリストする必要があるという印象があります。

設定の問題はStringから新しいものを生成し、AFAIKを取得する方法がないため、Nameがわからないことです。私は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)