<div dir="ltr"><div dir="ltr"><div>Hi Musa,</div><div><br></div><div>What you're trying to do is currently not possible because of limitations of Agda's scope checker: it scope checks the <i>complete</i> file before any typechecking can happen or any reflection code is run, so any names generated through reflection appear 'too late' to be in scope. <br></div><div><br></div><div>For the same reason it's not possible to generate data/record types from reflection directly, since the scope checker wouldn't know about the constructor/field names. It is however already possible to generate the <i>types</i> of the constructors or fields through reflection.</div><div><br></div><div>I've also been annoyed by the lack of a good reflection tutorial in the past, but so far I haven't found the time yet to write something up. So the best way to learn more about reflection is by reading the documentation and looking at examples, e.g. my <a href="https://github.com/jespercockx/ataca">ataca</a> library. I think there's definitely an audience for a good proper tutorial like the one you're writing. Perhaps if you agree we could link to it from the list of tutorials at <a href="https://agda.readthedocs.io/en/v2.6.0/getting-started/tutorial-list.html">https://agda.readthedocs.io/en/v2.6.0/getting-started/tutorial-list.html</a> and/or from the reflection documentation.</div><div><br></div><div>-- Jesper<br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, May 16, 2019 at 10:10 PM Musa Al-hassy <<a href="mailto:alhassm@mcmaster.ca">alhassm@mcmaster.ca</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Dear Agda Community,<br><br>When I attempt to unquote a declaration where a `Name` is not provided, but instead created using `freshName`,<div>the resulting function is not in scope. I want to create functions based on lists of terms, so the option of passing</div><div>in names is not ideal.</div><div><br></div><div>Here is the current scenerario ---a minimal example is below, and attached.<br><br><div><div>{- Works, but is undesirable }</div><div>unquoteDecl identity = ⋯make the identity function⋯</div><div><br></div><div>{- Desirable but "identity" is not in scope. -}</div><div>unquoteDecl = do η ← freshName "identity"</div><div> ⋯make the identity function⋯</div></div><div><br></div>Moreover, regarding reflection is it possible to unquote a datatype or a record declaration?</div><div>Does anyone have any documentation on how to use the /current/,<br>or a /recent/, version of Agda's reflection mechanism.</div><div>( My personal notes can be found here: <br> <a href="https://github.com/alhassy/gentle-intro-to-reflection" target="_blank">https://github.com/alhassy/gentle-intro-to-reflection</a> )<br><br>Best regards,<br><br>Musa Al-hassy<br><br><div>------------------------------------------------------------------------</div><div>module tangled where</div><div><br></div><div>open import Relation.Binary.PropositionalEquality hiding ([_])</div><div>open import Data.List as List</div><div>open import Reflection</div><div>open import Data.Nat</div><div>open import Data.Unit</div><div><br></div><div>_>>=_ : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B</div><div>_>>=_ = bindTC</div><div>_>>_ : ∀ {a b} {A : Set a} {B : Set b} → TC A → TC B → TC B</div><div>_>>_ = λ p q → p >>= (λ _ → q)</div><div><br></div><div>{- 𝓋isible 𝓇elevant 𝒶rgument -}</div><div>𝓋𝓇𝒶 : {A : Set} → A → Arg A</div><div>𝓋𝓇𝒶 = arg (arg-info visible relevant)</div><div><br></div><div>unquoteDecl</div><div> = do η ← freshName "identity"</div><div> τ ← quoteTC (∀ {A : Set} → A → A)</div><div> declareDef (𝓋𝓇𝒶 η) τ</div><div> defineFun η [ clause [ 𝓋𝓇𝒶 (var "x") ] (var 0 []) ]</div><div><br></div><div>{-</div><div>-- “identity” is not in scope!?</div><div>_ : ∀ {x : ℕ} → identity x ≡ x</div><div>_ = refl</div><div>-}<br></div><div><br></div></div></div></div></div></div>
</div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>