We can erase things of type %World, which opens up more possibilities of
newtype and helps optimise IO, but we need to be sure that the side
effecting operations aren't optimised away as a result because we no
longer have to inspect the newtype. Therefore, if optimising away a case
analysis on a newtype with a %World deleted, add a let binding for the
scrutinee of the case, and flag it as non-inlinable.
It's not actually used as part of any compilation pipeline yet, and I've
only tested it by eyeballing the output, but it'll be useful soon, and
it's good for it to be available to any new back ends that might need
it. It will need some optimisation.
That is, really erase the argument position rather than just putting
'erased there. It doesn't make a huge difference to the generated scheme
performance, but since we can always do this for constructors, we might
as well.
This improves runtime performance a bit since it avoids creating some
unnecessary closures (and is a preliminary step to lambda lifting, which
might help for some back ends).
Not calculating the needed space correctly, so sometimes not expanding
the buffer enough! This cause buffer data to be corrupted, leading to
issues like #114.
If IO operations don't return an updated world token, the inliner might
think they're not used at all. So if this turns out to be an overhead,
we'll have to work out another way of eliding it.
Or, more accurately, by not doing a thing that's a waste of time. After
evaluating a local, if the result isn't applied to a stack, there's no
more reduction to do, so stop there.
Still go to the explicit named representation afterwards, since that's
an easier API for a code generator, and by then the names are guaranteed
unique.
(without adding syntax for them)
Somewhat of a surgical change, changing the AST and elaboration to
support it
Seems to pass all tests (including Frex)
Changes in `Idris/Desugar.idr` seem to be a bit challenging for the
type-checker in do-blocks, so I added type annotations.
Hopefully we could remove them in `idris2sh`.
The `isLet` check is essentially the disjunction of the `Maybe Bool`
and the function looking up the value to check whether it is a `Let`.
But:
* `getBinder` does the same lookup & then dispatches on Let
* the non-let cases in both branches of the if-then-else are equal
So we can actually get rid of that `isLet` and it should compute the
same result. We still use the `Maybe Bool` to potentially avoid running
`getBinder` if we already know the local value is not a let.
Instead of essentially interleaving the proof that `reverseOnto`
and ̀`reverse _ ++ _` are equivalent, we embrace `reverseOnto` and
perform a single rewrite at the end.
Apologies to anyone who's working on a back end independently!
You can still use CExp for now, but I'm shortly going to try using
NamedCExp in inlining, to save the fairly large cost of maintaining the
de Bruijn indices when going under binders.
Names are kept unique in the translation, so you can assume you don't
need to worry about them.
Use a variant of MkVar which has the name in the type and therefore
means it can be erased to a newtype, so just an Integer. Then use
'insertNames' rather than repeatedly thinning.
A bit of reorganisation to ensure that the context membership proofs are
erased. It's only a small overhead in general to keep the proofs, but
there are places where it's really noticeable, particularly when
compiling large programs.
