It's disappointing to have to do this, but I think necessary because
various issue reports have shown it to be unsound (at least as far as
inference goes) and, at the very least, confusing. This patch brings us
back to the basic rules of QTT.
On the one hand, this makes the 1 multiplicity less useful, because it
means we can't flag arguments as being used exactly once which would be
useful for optimisation purposes as well as precision in the type. On
the other hand, it removes some complexity (and a hack) from
unification, and has the advantage of being correct! Also, I still
consider the 1 multiplicity an experiment.
We can still do interesting things like protocol state tracking, which
is my primary motivation at least.
Ideally, if the 1 multiplicity is going to be more generall useful,
we'll need some kind of way of doing multiplicity polymorphism in the
future. I don't think subtyping is the way (I've pretty much always come
to regret adding some form of subtyping).
Fixes#73 (and maybe some others).
- Added initial implementations for terms and values
- Error messages converted to pretty printer
- Colorization for error messages
- Color and console width option both as command line and repl command
This is partly to tidy things up, but also a good test for 'import as'.
Requires some internal changes since there are parts of reflection,
unelaboration and a compiler hack that rely on where things are in the
Prelude.
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.
unelabBinder was losing information for the purpose of displaying names
nicely. This is typically wanted but when working with elabortation it's
useful to have all the information you can get. Things like record field
names would be lost when querying with GetType but are now retained.
Clash in a reflection test due to conflicting merges. I'd like to find a
way to make the internally generated numbers not matter here (and
elsewhere) but I don't see an obvious way.
helps with readability since these, especially named-IPi, come up a lot
didn't change everything that could need it like PiInfo or BindMode
PiInfo rarely has DefImplicit (so far) and BindMode hasn't come up a lot (so far)
reduced indentation for TTImp Show implementation
So the type of Elab now gives the expected type that's being elaborated
to, meaning that we can run 'check' in the middle of scripts and use the
result.
Instead of merely generating a locally unique name, use the existing
code for generating a new unique variable name in the unifier, which is
therefore globally unique.
