* Add field for universe level to TType
This doesn't do anything yet, other than introduce new universe
variables whenever we introduce a new type, but it's the first step
towards checking the universe hierarchy. Next step is to add constraints
when checking pi, unifying/converting types, and when adding data
constructors.
* TTC version increment
Thought I'd done this, but apparently I didn't save the file. Oops!
* Add structure for universe constraints
* Fix display of ambiguity errors
We need to store the Context in errors at the point where the error
occurs, or we might get some nonsense in the message. There's still a
couple of places in Error where we don't do this right. This fixes one
of them, and improves a few messages in the process.
* 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
While the discussion about how to refactor test framework is not
finished (#1654), make this change: move `rm -rf build` in the
beginning of the test. For these reasons:
* it is useful to inspect the contents of the `build` directory
especially after the test failure
* if build crashes mid-test (e.g. process killed), next run should
not be affected by the `build` directory from the previous run
We already did this, but missed a few cases due to the way arguments are
elaborated. So now, when checking an LHS, we don't allow LHS argument
types to be inferred from the pattern, but rather they must be inferred
from elsewhere. To do this, we keep track of the constraints which would
be solved when inferring the type, and make sure they don't solve any
new metavariables. Fixes#1510, and also now gets the error location
right as a bonus!
Why:
* To implement robust cross-project go-to-definition in LSP
i.e you can jump to definition of any global name coming
from library dependencies, as well as from the local project files.
What it does:
* Modify `FC`s to carry `ModuleIdent` for .idr sources,
file name for .ipkg sources or nothing for interactive runs.
* Add `--install-with-src` to install the source code alongside
the ttc binaries. The source is installed into the same directory
as the corresponding ttc file. Installed sources are made read-only.
* As we install the sources pinned to the related ttc files we gain
the versioning of sources for free.
This saves a lot of unnecessary exploring of size change graphs, which
can get over the top quite quickly if there's complex mutual
definitions, or even just a single function with an interesting variety
of recursive calls.
Fixes#1365Fixes#1277Fixes#645
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.
This adds new `Int8`, `Int16`, `Int32` and `Int64` data types
to the compiler, thus working towards properly specified integer
types as discussed in #1048.
In addition, the following changes / corrections are made:
* Support casts from `Char`, `String`, and `Double` to all integer
types (and back). This fixes#1270.
* Make sure that all casts to limited-precision integers are properly
bounds checked (this was not the case so far for casts from `String`
and `Double` to `Int`)
* Add a thorough set of tests to make sure all bounds checks work
correctly for all supported casts and arithmetic operations
We've always just used 0, which isn't correct if the function is going
to be used in a runtime pattern match. Now calculate correctly so that
we're explicit about which type level variables are used at runtime.
This might cause some programs to fail to compile, if they use functions
that calculate Pi types. The solution is to make those functions
explicitly 0 multiplicity. If that doesn't work, you may have been
accidentally trying to use compile-time only data at run time!
Fixes#1163
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
Including appropriate casts, and Num/Eq/Ord/Show implementations.
Also includes new primitives in Data.Buffer, and calls to foreign
functions in C as 'unsigned'.
Can't export a type which refers to a private name. This has caught a
couple of visibility errors in the libraries, code and tests, so they've
been updated too.
This is mostly to make it easier to write linear function types without
having to invent names for everything, which might be noisy. Also it
improves the display of linear function types when the name isn't used
in the scope.
Still a couple of things to resolve in coverage and totality checking
before we can switch on %default, so don't expect quite the right
behaviour just yet. More progress though!
Also working on this has caught a few totality errors in the Idris 2
code base that Idris 1 missed... so these are fixed on the way.
