[Agda] Agda Compiler Alterations Guide

[Musa Al-hassy]

Thank-you for the hints Jesper,

I've made my changes within the repo https://github.com/alhassy/agda
Where I'm trying to replace the keyword "module" with "mmodule".

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 to introduce construct “fields-of”:

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

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.

Thanks for any help,

Musa

On Mon, Oct 1, 2018 at 11:03 AM Jesper Cockx <Jesper at sikanda.be> wrote:
>
> 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