[Agda-dev] Agda Compiler Alterations Guide :: Notes

[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).

To elaborate further on what I'm really trying to accomplish, consider:

   record SingleSortedAlgebra : Set₁ where
     field
      Carrier : Set
      _⊕_ : Carrier → Carrier → Carrier

One of my aims is to introduce construct “fields-of”:

   record SingleSortedAlgebraWithConstant : Set₁ where
     fields-of SingleSortedAlgebra renaming (_⊕_ to _⟨$⟩_)
     field
       ε : Carrier

Which should have the same net result as:

   record SingleSortedAlgebraWithConstant : Set₁ where
     field
      Carrier : Set
      _⟨$⟩_ : Carrier → Carrier → Carrier
     ε : Carrier

I have been unsuccessful in locating any documentation to help me achieve
such changes to the Agda compiler. If you know of any, please send them my way.

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
silly1 where`
could no longer type check with module name and file name errors; even though
the file name was silly1.agda.

My steps and code can be found at https://github.com/alhassy/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