<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jun 17, 2016 at 9:03 PM, Ernesto Copello <span dir="ltr">&lt;<a href="mailto:ecopello@gmail.com" target="_blank">ecopello@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div><div><div><div><div><div><div>Hi all,<br><br></div>I am studying the Reflection mechanism in Agda, and I have the following questions.<br><br></div>I have the impression that the following functions have been removed in Agda 2.5.1:<br><br>type : Name → Type<br>definition : Name → Definition<br><br></div>And they have been replaced with the following ones:<br><br></div>getType : Name → TC Type<br></div>getDefinition : Name → TC Definition<br><br></div>Am I right ? <br><br>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 ?<br></div></div></blockquote><div><br></div><div>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.</div><div><div> <br></div></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div><br></div>If my previous inference is right then the following code, extracted from <a href="https://github.com/pepijnkokke/AutoInAgda/blob/master/src/Auto/Core.agda" target="_blank">https://github.com/pepijnkokke/AutoInAgda/blob/master/src/Auto/Core.agda</a> project, could not be implemented in Agda 2.5.1, because definition is called with a variable whose value is know at runtime  ?<br><br><div dir="ltr">-- function which reifies untyped proof terms (from the</div><div dir="ltr">-- `ProofSearch` module) to untyped Agda terms.</div><div dir="ltr">mutual</div><div dir="ltr">reify : Proof → AgTerm</div><div dir="ltr">reify (con (var i) ps) = var i []</div><div dir="ltr">reify (con (name n) ps) with definition n</div><div dir="ltr">... | function x = def n (reifyChildren ps)</div><div dir="ltr">... | constructor′ = con n (reifyChildren ps)</div><div dir="ltr">... | data-type x = unknown</div><div dir="ltr">... | record′ x = unknown</div><div dir="ltr">... | axiom = unknown</div><div dir="ltr">... | primitive′ = unknown</div><div><br></div><div><div><div><div><div>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.<br></div></div></div></div></div></div></blockquote><div><br></div><div>If I&#39;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.</div><div><br></div><div>/ Ulf</div></div></div></div>