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

[Ulf Norell]

On Fri, Jun 17, 2016 at 9:03 PM, Ernesto Copello <ecopello at gmail.com> wrote:

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

Yes and no. The new functions can indeed only be called at compile time.
The old function could in principle be called at runtime, but none of the
compilers actually implemented them.


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

If I'm not completely mistaken the reify function is not intended to be run
at runtime, but as part of the tactic. Thus, when reimplementing Auto in
Agda 2.5.1 it should most likely get the type Proof → TC AgTerm.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160618/9a450cf9/attachment.html