[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

[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

Post by 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
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by Jesper Cockx
Hi and welcome to the Agda community!
- 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

Post by 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
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda