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

[Musa Al-hassy]

Going to the language's Implementors meeting --on a whole other
continent-- seems rather unreasonable to obtain
minimal direction on altering the compiler. I want to work on the
compiler, but I don't have superfluous funds.

Once again, I appeal to the community: Surely someone has jotted down some messy
notes on how to make alterations; anything helps, such as how the
system is interconnected
or where a reasonable place to begin and work from!

Honestly, anything helps!

This is an opportunity to get some manual made for others to contribute.
People have things on the Agda ``wish list'', and people like me might realise
them if guiding manuals were in-place.

On Tue, Oct 2, 2018 at 10:19 AM Andreas Abel <abela at chalmers.se> wrote:
>
>  > Does anyone have notes, or knows how to, or can provide a guide
>  > to making alterations to the Agda compiler.
>
> Well, we know how to, but have not anything written down.  The Agda
> meeting is a place for getting insider information.
>
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXVIII
>
>  > My steps and code can be found at https://github.com/alhassy/agda
>
> I commented here:
> https://github.com/alhassy/agda/commit/6043e77e4a72518711f5f808fb4eb593cbf0bb7c#commitcomment-30735013
>
> On 02/10/18 15:15, Musa Al-hassy 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).
> >
> > 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
> > _______________________________________________
> > Agda-dev mailing list
> > Agda-dev at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda-dev
> >
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www.cse.chalmers.se/~abela/