[Agda-dev] Re: Epic back-end support

[Ulf Norell]

I think it would be worth the effort having a separate intermediate
language for compilation.
The internal syntax is used all over the place so it's awkward to change,
and I'm sure there
are things you'd like to do to the intermediate language that doesn't quite
fit in internal
syntax.

/ Ulf

On Tue, Mar 31, 2015 at 12:11 PM, Philipp Hausmann <
p.hausmann at students.uu.nl> wrote:

> On 03/31/2015 09:41 AM, Nils Anders Danielsson wrote:
> > On 2015-03-30 10:53, Ulf Norell wrote:
> >> I'd be ok with dropping Epic support. I don't think anyone is using
> >> it, but maybe polling the list would be a good idea just in case.
> >
> > I think it would be a good idea to keep the (more or less)
> > backend-independent optimisations, preferably in a separate,
> > backend-independent pass.
> >
> > Philipp, you ported at least one of these optimisations (smashing) to
> > the new UHC backend. Can you inform us about exactly what has been
> > ported?
> >
>
> I have ported Smashing to the UHC backend, but this still has some bugs.
> I have not ported
> any of the other optimisations so far.
>
> Making the optimisations backend-independent sounds like a good idea.
> That leaves the question where
> exactly the optimisations should go.
>
> I think implementing some of these optimisations in Agda's Internal
> Syntax should be possible. But in the long
> term it may be better to use a new dependently typed Core language
> tailored specifically towards optimisation and compilation.
> E.g. the case trees in Agda's Internal Syntax are a bit unhandy too when
> compiling.
> On the other hand, this would add another intermediate language...
>
> I think it could also be helpful if the result of these optimisations
> could be (optionally) type-checked, to provide some sanity check. If I
> remember correctly,
> GHC can do that with GHC Core.
>
> Philipp
> _______________________________________________
> 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/20150331/22d015d2/attachment.html