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...
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.
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.
Flags can now be set on implementations too, where the flags get passed
to each of the methods in the implementation. We might want something a
bit more fine grained than this later. Also some small changes to the
way inlining lets is done in the compiler.
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.
e.g. in a C file. This means we don't accidentally treat things as
empty, since previously we just defined these as empty types, but that
broke coverage checking. Fixes#240
We never inspect it, so it carries no information - it just needs to be
there as a token to make sure that IO operations run at the right time.
So, IORes can be a newtype now and therefore optimised away.
This prevents display of shadowed names from case blocks/where clauses
that are now unusable. It does mean that constraint arguments aren't
displayed, unless given an explicit name - this may not be good, since
we might want to know which constraints are in scope, so it may yet need
a little tweaking.
This is the result of running the command:
$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +
I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
Functions can be declared as %foreign with a list of calling
conventions, which a backend will work through until it finds one it can
understand. Currently implemented only in Chez backend. If this works
out, I'll implement it for Racket too, and remove the old primitive
functions.
There's a bit more boiler plate here than before, but it has the benefit
of being more extensible and portable between different back ends.
Some examples, pending proper documentation:
%foreign "C:puts,libc" "scheme:display"
putline : String -> PrimIO ()
%foreign "C:exp, libm.so.6, math.h"
fexp : Double -> Double
%foreign "C:initscr, ncurses_glue.so, ncurses.h"
prim_initscr : PrimIO ()
This is part of what we used to have in Enum but I think it's better to
separate the two. Added implementations for Nat, and anything in
Integral/Ord/Neg, so that we get range syntax (at least when its
implemeted) for the most useful cases.
Elaborate via either === (homogeneous equality) or ~=~ (heterogeneous
equality) both of which are synonyms for Equal. This is to get the Idris
1 behaviour that equality is homogeneous by default to reduce the need
for type annotations, but heterogeneous if that doesn't work.
This has shown up a problem with 'case' which is hard to fix - since it
works by generating a function with the appropriate type, it's hard to
ensure that let bindings computational behaviour is propagated while
maintaining appropriate dependencies between arguments and keeping the
let so that it only evaluates once. So, I've disabled the computational
behaviour of 'let' inside case blocks. I hope this isn't a big
inconvenience (there are workarounds if it's ever needed, anyway).
