Clever Geek Handbook

Understanding unquoteDecl in Agda

I'm trying to understand that Agda is built in reflection mechanisms, so I decided to write a simple function that takes a string for an identifier, a quoted type and a quoted term, and simply defines a term of a given type with a given string identifier. Thus, I wrote the following:

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

This type checks, but when I try to use "test" elsewhere, I get an error Not in scope: test

.

the documentation for unquoteDecl

is opaque. The applause should look like

unquoteDecl x_1 x_2 ... x_n = m

where x_i

is Name

s, and m

has a type TC \top

, so maybe what I'm trying to do is actually impossible, but I still don't understand how this mechanism works: if it m

must have a type TC ⊀

and therefore cannot be a name function x_1 x_2 ... x_n

, I don't see how it is possible to add any new names to the scope using unquoteDecl

at all!

So, to summarize:

Is it possible to define a function like mine using Agda's reflection mechanism so that I can inject new names into scope using an argument String

? I want something like:

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

to compile (ie I can actually use the new name, "test")

and if not, what mechanism can the m

names be used x_1 ... x_n

? Can it m

be of a type List Name β†’ TC ⊀

, contrary to the documentation?

+3


source to share


1 answer


Based on the way Ulf uses itunquoteDecl

, I get the impression that you need to list on the LHS the names that go to expand the scope.

The problem with your setup is that you don't know Name

as you are creating a new one from String

and can't grab it AFAIK. I was under the impression that freshName

it is intended to be used only to create internal names within tactics.



If you do testDefineName'

take Name

and not String

, then everything will work:

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


source






More articles: