Don't get too excited yet - I want this in so that it doesn't get too
out of sync, but I still have to think about exactly how it's going to
work in practice.
This means it abstracts over the value syntactically, rather than by
value, and can significantly speed up elaboration where large types are
involved, at a cost of being less general. Try it if "with" is slow.
There are more flags we want on with (well, at least one: "proof")
building Chez Scheme locally from source and
improve formatting of first paragraphs
```
Compiling idris2_app/idris2-boot.ss with output to
idris2_app/idris2-boot.so
Exception: attempt to reference unbound identifier
make-thread-parameter at line 171, char 30 of idris2_app/idris2-boot.ss
```
As patterns weren't getting propagated to local definitions, due to a
combination of being stored as let bindings and being part of a pattern
scrutinee. The solution removes the computation behaviour, but that is
consistent with the way let works everywhere else.
(If we do as patterns as let bindings, the way case and locals elaborate
mean that the value gets recomputed. Fixing this would require changing
the way the core works, and I'm not going to do that for a while.)
The required totality of interface methods is now only affected if
there's an explicit modifier on the method. This allows us to set
%default total on the Prelude, which is a good thing to do anyway,
without also requiring that every implementation of the interface in the
prelude has to be total, which would potentially be a pain.
Another good affect is that it speeds up totality checking elsewhere
because totality checking is done lazily, and so with the total flag set
we know in advance that prelude functions are total.
On second thoughts, and after further experimentation, better to recheck
the metavariable if it arises in linearity checking, because the type
could be very big and in general will be much bigger than the
definition. If this turns out to be a performance issue later, we can
revisit it.
In this case, it's only needed to ensure the dictionaries are inlined
when checking recursive methods, so can be unset once we're done, to
save excessive inlining when totality checking later.
It's a small performance hit, but not as big as it used to be because we
don't load everything any more. This is necessary because saved
metavariables might turn up during evaluation, and then be needed in the
final linearity check. Another way is to check them again if this
happens, but there's a risk that might be even more expensive (and
saving the type is much safter anyway).
This wouldn't have got caught since the merge that caused the problem
was checked before I pushed the patch that made import work right! So
hopefully this'll sort it.
- %inline in a few places, which helps especially when it's known at
compile time whether something consumes
- a little bit of reordering so that the most likely alternative is
tried first
- (not really much effect, but...) use fastPack from the Prelude for
building tokens
If we're going to use assert_total. we might as well not have the
distinction between empty and non empty results, which only makes the
code harder to follow.
Also there's some kind of issue which seems to mean the token list can't
be erased if we do that. I will investigate if I can make a smaller
example.
This was taking too long, and adding too many things, because it was
going too deep in the name of having everything accessible at the REPL
and for the compiler. So, it's done a bit differently now, only chasing
everything on a "full" load (i.e., final load at the REPL)
This has some effects:
+ As systems get bigger, load time gets better (on my machine, checking
Idris.Main now takes 52s from scratch, down from 76s)
+ You might find import errors that you didn't previously get, because
things were being imported that shouldn't have been. The new way is
correct!
An unfortunate effect is that sometimes you end up getting "undefined
name" errors even if you didn't explicitly use the name, because
sometimes a module uses a name from another module in a type, which then
gets exported, and eventually needs to be reduced. This mostly happens
because there is a compile time check that should be done which I
haven't implemented yet. That is, public export definitions should only
be allowed to use names that are also public export. I'll get to this
soon.
As it was in Idris1 being able to override some, or introduce new, options to an Idris IPKG is beneficial. For example, generate code for multiple codegens from a single source.
Overridable options are:
+ `--quiet`
+ `--verbose`
+ `--timing`
+ `--dumpcases <file>`
+ `--dumplifted <file>`
+ `--dumpvmcode <file>`
+ `--debug-elab-check`
