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

[Philipp Hausmann]

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