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!)
: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.
When flattening the `SimpleDocTree` created from a `SimpleDocStream`, the
first part of a concatenated doc was sometimes dropped, depending on the
result of the recursive call to `flatten`.
Previously, parameter block reused the same syntax as in Idris1:
```
parameters (v1 : t1, … , vn : tn)
```
Unfortunately this syntax presents some issues:
- It does not allow to declare implicit parameters
- It does not allow to specify which multiplicity to use
- It is inconsistent with the syntax used for named arguments elsewhere
in the language.
This change fixes those three problems by borrowing the syntax for
declaring type parameters in records:
```
parameters (v1 : t2) (v2 : t2) … (vn : tn)
```
It also enables other features like multiple declarations of arguments
with the same type:
```
parameters (v1, v2 : Type)
```
The previous names were a holdover from when these functions were a part
of `RefC.compileExpr`. The new names more accurately reflect their usage
in this context.
