Surprisingly, this doesn't affect performance - it shows up as about the
same in the profile. But more importantly, it ports more directly to
Idris 2, which can't guarantee that 'strTail' doesn't allocate at
runtime, so using a List Char here is much more efficient.
This probably points to the need for better string primitives. Later...
Trying to keep both up to date - apologies if I'm missed anyone. I got
the list from the git logs, but feel free to edit yourself in or out as
you prefer.
Back ends can still shortcut these and use their own primitives, but
doing things this way gives consistent behaviour between the simple IO
primitives and file IO, and allow us to use stdin/stdout consistently
(e.g. to flush stdout).
This also fixes the behaviour of 'replWith' to be consistent with the
Idris 1 version.
System mostly calls C now, except for getting command line arguments,
which may be too back end dependent so maybe we should think of another
approach here later.
I've also added some windows support headers (taken straight from the
rts/Idris 1) but I have no way to test, and the Makefile doesn't build
them. Please can someone who is familiar with windows fix this? Thanks!
This removes the need for some external primitives, and allows the
details to be shared between all the backends (plus we don't have to do
things a certain way just because Scheme chooses to)
A big cost in IO heavy programs is io_bind, and we can often inline it
away and turn it into just sequencing operations. Things have to be
lined up right to do that though - ideally, case inlining and the
newtype optimisation will know just a little bit more to be able to do
it automatically, but for now, the inliner treats io_bind as a special
case.
Also do another round of inlining, since lots more things can become
inlinable (io_bind especially, becoming fully applied to the %World)
after the first pass.
It's slightly different wrt to file reading and writing, and now
requires the created buffer to be explicitly freed (since unlike Idris 1
the run time can't be told to manage C values) but this makes the buffer
code more portable by not requiring it to run via scheme.
Performance appears more or less the same as before.
This can be quite effective at removing runtime overhead when just using
an overloaded method directly. It is, however, still quite limited (only
works on top level interfaces, so no inlining of parents, e.g. like X a
=> X (List a), and sometimes generating the transform rules fails for
reasons I haven't worked out yet).
This is experimental, I might change the way this works at any point,
but it's a nice improvement for now.
I haven't yet worked out a nice way to test these automatically...
Also note that:
- only the types of the LHS and RHS are checked (and must be the same,
like in a normal pattern matching clause) so there's no attempt to
ensure that the rules are "safe". Possibly later, they should require an
equality proof?
- There is no attempt to ensure the rules are confluent or terminating,
but there is a termination threshold on apply the rules (currently set
at 5 cycles, but maybe should be configurable)
This isn't strictly right yet (there should be no newline on the last
lie if there was no newline in the input file) but it puts the behaviour
back to what it was before fGetLine was changed to discard it.
This needs revisiting...
