<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Hi and welcome to the Agda community!</div><div><br></div><div>We have the following sources to get familiar with the Agda codebase:</div><div><br></div><div>- The HACKING file (<a href="https://github.com/agda/agda/blob/master/HACKING">https://github.com/agda/agda/blob/master/HACKING</a>) gives some general tips & best practices for developing Agda.</div><div>- Some documentation on the wiki on bugfixing (<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=DevelopersManual.BugFixing">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=DevelopersManual.BugFixing</a>).</div><div>- The agda-dev mailing list (<a href="https://lists.chalmers.se/mailman/listinfo/agda-dev">https://lists.chalmers.se/mailman/listinfo/agda-dev</a>)</div><div>- Coming to one of the Agda meetings to learn about the codebase and get first-hand help (next Agda meeting is in two weeks in Nottingham!).</div><div><br></div><div>If you're working on a concrete feature, it's also a good idea to create an issue on github to let other people know you're working on this and possibly get some help.</div><div><br></div><div>Concretely for your goal of adding new declarations, Agda already has a feature for unquoting function definitions (see <a href="https://agda.readthedocs.io/en/v2.5.4.1/language/reflection.html#declarations">https://agda.readthedocs.io/en/v2.5.4.1/language/reflection.html#declarations</a>), but not for data/record types. This has been a feature on the wishlist for a while, so it would be nice to have someone working on it!</div><div><br></div><div>I'm not sure what's going wrong with the changes you tried in the parser -- maybe you can create a fork of Agda on your own github so we can take a look at the code?</div><div><br></div><div>Best regards,</div><div>Jesper<br></div></div><div dir="ltr"><div><br></div><div><br></div></div></div></div></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Oct 1, 2018 at 4:45 PM Musa Al-hassy <<a href="mailto:alhassm@mcmaster.ca" target="_blank">alhassm@mcmaster.ca</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Agda Community,<br>
<br>
Does anyone have notes, or knows how to, or can provide a guide<br>
to making alterations to the Agda compiler.<br>
<br>
I would like to experiment with adding record declaration combinators.<br>
In general, I am trying to add some meta-programming features that<br>
would generate new declarations based on existing declarations,<br>
somewhat like Haskell's deriving (or deriving-via).<br>
<br>
I have been trying to make super simple changes, like aliases for keywords,<br>
and have been unsuccessful for some time.<br>
<br>
In particular, to make an observable change I wanted the compiler<br>
to accept the keyword `mmodule` in place of the existing `module` keyword.<br>
I grep'd for "module" in the agda source, including in the alex and happy files,<br>
prepended the strings with an extra `m`, then re-compiled and re-built<br>
everything.<br>
The result was a broken agda sytem: A file containing only `mmodule silly where`<br>
could no longer type check with module name and file name errors; even though<br>
the file name was silly.agda.<br>
<br>
My current aim is to provide renaming of record fields, that would provide<br>
an isomorphic record declaration but with some fields renamed, as a starting<br>
point. [I am well aware of Agda's renaming features when opening a module;<br>
this is different, as it is about generating new declarations].<br>
<br>
Any advice would be appreciated --any existing notes would be immensely helpful!<br>
<br>
Best regards,<br>
<br>
Musa Al-hassy<br>
_______________________________________________<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>