[Agda] Agda Compiler Alterations Guide

[Musa Al-hassy]

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