We do this during desugaring because elaboration may insert valid
`?` values on the LHS (e.g. when elaborating things that cannot be
pattern-matched on and should be checked to be forced).
Write small integers out as 1 byte, not 8, at the cost of writing larger
integers out in 9 bytes. Most integers fit in 1 byte, since it's string
and list lengths from user-written code.
This saves writing the same strings over and over again in the body of a
definition. At the cost of a traversal on reading and writing the ttcs,
there is a good bit less to write out.
We don't need to write the current namespace every single time! This
won't work as well if there's namespaces in the file, so it needs
refining a bit, but this reduces loading time anyway.
Where 'small' means they don't refer to other metavariables, except
right at the top level, and they don't go beyond a certain small depth,
arrived at by experimenting.
We already did a bit of this, but only for depth 0. The effect of this
is that we don't need to save out lots of metavariables, so ttc loading
is faster. This takes about 8s off the Idris build time!
Sometimes we have to re-read, if we've previously imported and then
imported public, but on the second read we don't need to read the whole
thing, just the header.
With the new representation of postponed problems, this is now either
not worth doing, or much more expensive than just having another crack
at the problem anyway. So let's not calculate it.
This makes the libraries built a couple of seconds quicker for me, and I
have one example where a program that previously took minutes now type
checks in seconds...
Might revisit this later, if it turns out to be a potential source of
optimisations, but it'll need to be done an entirely different way.
We stored them as equations between terms, I think because terms are
easy to re-evaluate with new information, and because I thought we might
want to save them out. It's not usually a problem to do that. However...
Going back and forth between terms and values can be expensive if
we're stuck in the middle of a complicated unification problem, the like
of which can turn up a lot if your types are complicated. So, we need to
be able to handle this.
Now store the postponed problems as NF, rather than Term, and add a
fuction to resume evaluating a NF with an updated context.
Authored by @stefan-hoeck
Stefan also says "Please note: The fix is quick and dirty. I plan to
open an new issue about the state of the JS backend soonish, since the
whole code requires some cleanup and documentation."
This means we can add things to the main context rather than the staging
context, if the 'branch' is always bracketed with a 'commit'. It doesn't
make a huge difference, but it is at least tidy!
On FreeBSD, the versionless `libc.so` file is a (text-based) linker
script and can not be loaded dynamically at runtime. Instead of
hardcoding the libc version "7" for FreeBSD we can just skip the load
completely, since libc is already implicitly loaded by the Chez runtime.
