There is an argument that, for import public, this should be automatic
(that is, the publicly imported things should be reexported with the
parent namespace). I decided not to do this, because another use of
import public which we do a lot in the Idris 2 code base is purely as a
convenience, where we still expect things to be in their original
namespace.
Also, where there's a choice between things being explicit and implicit,
I prefer to err on the side of explicit now.
So, if what you really want in an API is to reexport, you can do that,
but explicitly.
The ports are rather straight forward and I have purposefully written
the documentation to be beginner friendly.
Note, I have diverged from Idris1 over the naming of the projection
functions to make them consistent with `Pair` and `DPair`.
Apparently the concrete syntax is controversial ("{apples}"
vs. "$oranges"), so I'm just adding a simple DYI version until we
agree on a concrete syntax
This involves updating the bootstrap code since it needs a fix in
interface resolution. It shouldn't affect the Idris2-boot build though,
since it's in the libraries not the Idris2 source.
It's worth delaying in case doing some more work (and some more
interface resolution) can make the type more concrete. This makes
test linear011 work more smoothly, and will help with this sort of
program in general.
A better way, later, would be to try elaborating and delay only if the
type is not yet known. We have the facilities, but it's too fiddly for
me to want to implement it right now...
We need to check below top level too, since there could be holes that
we're happy to resolve by searching. The linearity test added
illustrates a place where this is needed.
Doing this is awkward, for a number of reasons, including 'pure' not
being linear in its argument - there's no guarantee it'll be used
linearly after all - and lack of multiplicity polymorphism. Fortunately
the user doesn't have to know about the ugliness underneath!
We can look at ways to make it less horrible later :). For now, this is
starting to look like something that allows us to write linear protocols
without too much extra machinery on top of IO.
Conditional variables with timeout in Chez didn't work, so changed to a
consistent meaning of the timeout (microseconds). Also fix linearity of
unsafePerformIO.
