[Agda] Agda Compiler Alterations Guide

[Jesper Cockx]

Hi and welcome to the Agda community!

We have the following sources to get familiar with the Agda codebase:

- The HACKING file (https://github.com/agda/agda/blob/master/HACKING) gives
some general tips & best practices for developing Agda.
- Some documentation on the wiki on bugfixing (
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=DevelopersManual.BugFixing
).
- The agda-dev mailing list (
https://lists.chalmers.se/mailman/listinfo/agda-dev)
- 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!).

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.

Concretely for your goal of adding new declarations, Agda already has a
feature for unquoting function definitions (see
https://agda.readthedocs.io/en/v2.5.4.1/language/reflection.html#declarations),
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!

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?

Best regards,
Jesper



On Mon, Oct 1, 2018 at 4:45 PM Musa Al-hassy <alhassm at mcmaster.ca> wrote:

> Dear Agda Community,
>
> Does anyone have notes, or knows how to, or can provide a guide
> to making alterations to the Agda compiler.
>
> I would like to experiment with adding record declaration combinators.
> In general, I am trying to add some meta-programming features that
> would generate new declarations based on existing declarations,
> somewhat like Haskell's deriving (or deriving-via).
>
> I have been trying to make super simple changes, like aliases for keywords,
> and have been unsuccessful for some time.
>
> In particular, to make an observable change I wanted the compiler
> to accept the keyword `mmodule` in place of the existing `module` keyword.
> I grep'd for "module" in the agda source, including in the alex and happy
> files,
> prepended the strings with an extra `m`, then re-compiled and re-built
> everything.
> The result was a broken agda sytem: A file containing only `mmodule silly
> where`
> could no longer type check with module name and file name errors; even
> though
> the file name was silly.agda.
>
> My current aim is to provide renaming of record fields, that would provide
> an isomorphic record declaration but with some fields renamed, as a
> starting
> point. [I am well aware of Agda's renaming features when opening a module;
> this is different, as it is about generating new declarations].
>
> Any advice would be appreciated --any existing notes would be immensely
> helpful!
>
> Best regards,
>
> Musa Al-hassy
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181001/ae0d96d4/attachment.html>