<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><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> <span>-- function which reifies untyped proof terms (from the</span>
      
      
        <table><tbody><tr><td>  <span>-- `ProofSearch` module) to untyped Agda terms.</span></td>
      </tr>
      <tr>
        </tr></tbody></table><table><tbody><tr><td>  <span>mutual</span></td>
      </tr>
      <tr>
        </tr></tbody></table><table><tbody><tr><td>    <span>reify</span> <span>:</span> Proof <span>→</span> AgTerm</td>
      </tr>
      <tr>
        </tr></tbody></table><table><tbody><tr><td>    reify (con (var i) ps) <span>=</span> var i []</td>
      </tr>
      <tr>
        </tr></tbody></table><table><tbody><tr><td>    reify (con (name n) ps) with definition n</td>
      </tr>
      <tr>
        </tr></tbody></table><table><tbody><tr><td>    ... | function x    <span>=</span> def n (reifyChildren ps)</td>
      </tr>
      <tr>
        </tr></tbody></table><table><tbody><tr><td>    ... | <span>constructor</span>′  <span>=</span> con n (reifyChildren ps)</td>
      </tr>
      <tr>
        </tr></tbody></table><table><tbody><tr><td>    ... | data-type x   <span>=</span> unknown</td>
      </tr>
      <tr>
        </tr></tbody></table><table><tbody><tr><td>    ... | <span>record</span>′ x     <span>=</span> unknown</td>
      </tr>
      <tr>
        </tr></tbody></table><table><tbody><tr><td>    ... | axiom         <span>=</span> unknown</td>
      </tr>
      <tr>
        </tr></tbody></table>    ... | primitive′    <span>=</span> unknown<br><div><div><br><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><br>
Thank you in advance,<br><br><br></div><div><br></div></div></div></div></div></div>