This means we can eliminate unused definitions from the generated code.
As usual, this doesn't make the generated code any faster, or the chez
compilation, but it's still good for tidiness and it does make the
generated scheme smaller.
Don't just have a placeholder. While this doesn't have a huge effect (if
any) on performance, it does generate smaller output for Chez to
process, and is tidier. Perhaps it's good for other back ends too, ones
that don't optimise as much as Chez does.
Only doing named functions, not higher order functions. HOFs may be
worth doing too, if we can, since this could remove lambdas and make
fewer closures.
The increment in TTC Version is necessary because otherwise there could
be inconsistencies between libraries and clients erasure properties.
WebKit seems to throw away any sequence of spaces between inline tags.
All affected places I found could be fixed by replacing single space
characters with the character U+2002 ("EN Space"), which means
almost the same thing as "normal space" (i.e. it breaks/wraps text and
has approximately the same width) but is not discarded by WebKit when
parsing the document.
If this should come up in a different place, a more thorough solution
might be needed (e.g. modifying `htmlEscape` to replace all spaces).
Checking the log categories isn't cheap because it involves parsing a
string. So, record whether we've ever set a log level. If we haven't,
there's no point in checking the string. This reduces overhead and saves
a few seconds in typechecking the Idris code base - also means we don't
have to worry so much about adding more logging if we feel we need it!
We've had these for a while, used for interface specialisation, but
they're not yet used anywhere else or properly documented. We should
document them soon, but for now, it's a useful performance boost to
always use the fast versions of pack/unpack/concat at runtime.
Also moves a couple to the prelude, to ensure that the fast versions are
defined in the same place as the 'normal' version so that the
transformation will always fire (that is, no need to import Data.String
for the transformation to work).
If set, when compiling this generates an executable which generates
profiling data. Currently supported by Racket and Chez, other backends
silently ignore it.
If all branches in a case block are a lambda, lift the lambda out. In
many cases, this can save creating a closure then evaluating it
immediately, because the function is already applied to the extra
argument.
This happens in particular with IO based code, where the extra argument
is the world token. One place where this transformation has a big effect
is 'evalRef' so the evaluator is now a bit faster (about 20% on the
small benchmark I tried it on - but no guarantees that's going to happen
on other examples!)
Since we have the locally overloaded `prettyTerm`, we can move most
functions in the `REPL` module back to `IdrisAnn`, reducing the overall
size of the PR.
:ti does the same thing as :t, but shows the type as if showimplicits
were set. The value of REPLOpt.ShowImplicits is unchanged.
:opts shows the current values of the options that can be set or unset
with :set/:unset. (This already existed in REPLCmd.GetOpts, idk why it
just wasn't in Parser.parserCommandsForHelp.)
Also fixed the spacing of the help message.
