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

[Guillaume Brunerie]

One suggestion would be that you browse the commit history on github, look
at the commits that are touching the same parts of Agda that you're
interested in, and try to understand the changes made by the author of the
commit.
You will most likely learn a lot in this way.

Den tis 2 okt. 2018 18:15Musa Al-hassy <alhassy at gmail.com> skrev:

> 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/
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20181002/fd8f1c9a/attachment.html>