* Update strings.rst
For some reasons the code blocks which are not set as 'idris' are not displayed in the readthedocs rendering.
* Update overloadedlit.rst
* Update overloadedlit.rst
* Abandon ambiguity resolution on undefined name
This has finally annoyed me enough to do something about it. If we get a
"no such variable" error there's no point exploring other branches.
* Removes spaces from test file
One day I'll update the linter to ignore test files. We should really
accept literally anything as a possiblity for test files, even if
removing the spaces is tidier.
* Reset context before throwing in 'successful'
Although I don't think this is strictly necessary for a fatal error, we
should still for the sake of tidiness reset the state when backtracking.
* Move Context into its own file
Just the core definition - this is so that we have access to it in
Core.Core, for inclusion in error messages, to save normalisation of
terms in errors until we actually show them.
* Normalise errors on display, not when they arise
This can save a lot of time in ambiguity resolution if the errors are
complicated, because the errors might never be displayed if it's in an
abandoned branch.
This involves lifting 'Context' out of Core.Context, because we need to
store it in Error, which is needed by Core, which in turn is needed in
Core.Context.
Also moved a couple of test caes from ttimp to idris2, so that the
errors get rendered properly and won't need updating unnecessarily. In
fact all of the ttimp tests - which were just part of the initial
scaffolding - are probably now subsumed by the idris2 tests.
* Add new coverage001 test files
If they don't, we can't turn them into patterns to match on, and we end
up looping. Possibly we could throw a different and maybe more
informative error instead of just making an unmatchable pattern.
Fixes#1895
* Split Normalise into three files
Evaluation, Quoting, and Conversion checking are distinct steps, and I'm
about to add some variations to quoting so better to reorganise a bit.
* Add a Quote mode that limits size of result
Sometimes normalising an expression is a good idea because it makes
things smaler, and sometimes it isnt, because it doesn't. We can't tell
in advance which situation we're in, but we can try speculatively
normalising something. This is good for case types and hole types - we
generally want the normal form, but if that's expensive, we should stop.
So, quote is now able to give up if it passes a certain size threshold
for stuck applications. By experimentation, it seems that up to 10
doesn't hurt too much, but beyond that it's better not to normalise at
all.
* Add the new normalise files
integerToNat is only equal to `believe_me` at runtime, not at compile
time. You'd believe it cannot be a problem given that the implementation
of `Cast` is not exported but the REPL reduces everything.
* Refactored the annotations to be more uniform
* KindedNames now carry both a fullName and a rawName
(useful in the HTML backend where we use the fullName for links)
* Removed the ad-hoc handling of qualified names in the html backend
