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

[Philipp Hausmann]

I guess the main problem now is that adding an intermediate language for
compilation and optimisations will be quite a bit of work. I don't think any
of the existing intermediate languages in
Agda (Internal Syntax, Epic AST, UHC AST,...) can be reused as-is.

I probably don't have enough time to make any real progress on this
in the near future. I will write down my ideas and will make
some experiments, but don't expect anything usable from me soon...
If anybody wants this done rather sooner than later, they probably
have to take a go at it themselves.

Philipp


On 03/31/2015 12:22 PM, Ulf Norell wrote:
> 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 <mailto: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 <mailto: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/20150402/9bfe390d/attachment.html