[Agda] Reflection: type-definition vs. getType and getDefinitions functions.

[Ernesto Copello]

Hi all,

I am studying the Reflection mechanism in Agda, and I have the following
questions.

I have the impression that the following functions have been removed in
Agda 2.5.1:

type : Name → Type
definition : Name → Definition

And they have been replaced with the following ones:

getType : Name → TC Type
getDefinition : Name → TC Definition

Am I right ?

If I am right, could I also infer that getType and getDefinition can only
been called in a macro, so in compile time as macros runs the TC monad ?
Whereas previous type and definition can be called anywhere, including
runtime ?

If my previous inference is right then the following code, extracted from
https://github.com/pepijnkokke/AutoInAgda/blob/master/src/Auto/Core.agda
project, could not be implemented in Agda 2.5.1, because definition is
called with a variable whose value is know at runtime  ?

-- function which reifies untyped proof terms (from the
-- `ProofSearch` module) to untyped Agda terms.
mutual
reify : Proof → AgTerm
reify (con (var i) ps) = var i []
reify (con (name n) ps) with definition n
... | function x = def n (reifyChildren ps)
... | constructor′ = con n (reifyChildren ps)
... | data-type x = unknown
... | record′ x = unknown
... | axiom = unknown
... | primitive′ = unknown

Although, If this function can not be implemented in Agda 2.5.1 I think
this is no so dramatic, I belive definition function call could be avoided
storing more information in constructor con when Proof terms are created.

Thank you in advance,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160617/d58e448d/attachment.html