The `if then else` syntax expects a block for the `then` and `else`
parts. Before this patch, the token `InterpEnd` was not a valid
follow up token to end a block. This adds `InterpEnd` as a closing
token for blocks, allowing `if then else` in interpolation slices
without additional parens.
Instead of having an arbitrary looking priority number, record explicit
reasons for the delay, which helps order them sensibly when rerunning
them. Mostly this allows us to choose which ones to rerun, where it
helps, and helps order things to get better error messages.
`testInDir dir ...` lists all directories in `dir` which contains
`run` files, and such directories are considered tests.
This is done to make test addition/maintenance cheaper.
Convert some test directories to `testInDir`, but not all of them
because
* some directories are listed in several test groups
* other directories are have some tests disabled
* add `nextDirEntry` which returns `Maybe String`, so `Nothing` on
the end of directory unlike `dirEntry` which returns unspecified error
on the end of directory
* `dirEntry` is deprecated now, but not removed because compiler depends on it
* native implementation of `dirEntry` is patched to explicitly reset `errno`
before the `readdir` call: without it end of directory and error were
indistinguishable
* test added
* Add trailing newline on non-empty list in unlines
There are several reasons to do that:
* a line in a text file is something which ends with newline,
and the last line is not special
* `unlines []` should be different from `unlines [""]`
* `unlines (a ++ b) = unlines a ++ unlines b`
* Haskell does it
* Change lines function behaviour
* Propagate 'do qualification' to inner bangs and comprehensions
* Minor
* Remove banner in test
* Move tests from reg045 to reg047
* Move mbNS from Desugar.idr to Name.idr, renaming it to mbApplyNS
The 'with' type and application need to treat the parameters with the
same plicity, but the application has just always treated them as
explicit since it never looked. It's easiest just to make them all
explicit, since this isn't a user visible type. Fixes#1695.
* add `strerror` function
* move `getErrno` to `System.Errno`
* use `strerror` in `Show FileError`
* on node there's no access to `strerror`, so `strerror` just converts the number to string
Ideally we'd have a complete incremental build in CI, but that could be
a bit fiddly to set up at the moment (updating bootstrap code might make
it easier). This tests that the basic facilities work, though - there's
a lot can go wrong even in a small test like this, trust me, I have made
those mistakes :).
This involves making 'unelab' aware of nested names so that it can
remove the parameters from names in the current block. It's a bit of a
hacky solution, but it is also the easiest one.
Ideally we'd build the getter types directly, rather than using unelab,
but that's one to save for another time.
Fixes#1482
Convert `App.Control.Exception` interface to an alias to `HasErr`.
Probably `Exception` interface need to be deprecated or removed.
Note similar problem exists with `PrimIO` calling `PrimIO, Exception`,
also need to be fixed.
Fix this scenario:
```
throwBoth : Has [Exception String, Exception Int] es => App es ()
throwOne : Has [Exception Int] es => App es Int
throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
```
With this commit it works, before this commit it failed with:
```
Error: While processing right hand side of throwOne. Can't find an implementation for Exception Int (String :: es).
TestException.idr:8:48--8:57
|
8 | throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
| ^^^^^^^^^
```
If it's solved by unification, expression search should just print the
unified value. In fact it almost did this, but wasn't reducing the holes
so the result was being rendered incorrectly.
This is set to 1 second by default. Usually if it hasn't found a result
by then, it never will, but given that we find the first batch of
results then sort them, the timeout also stops us fruitlessly searching
for more solutions.
Hopefully 1s is more than enough for CI too. There is a mechanism to
change the timeout (%search_timeout) so if it turns out that CI needs
longer in some cases, we can increase it there.
I haven't documented this yet, but proof/definition search needs
documenting in general. I'll get to that.
The timer mechanism may also be useful elsewhere - I'm considering it
for ambiguity warnings, because the ambiguity depth limit isn't working
very well for that.
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!
We need to fully evaluate, not just the public export names, otherwise
we don't pattern match properly and potentially generate catch all
patterns we don't mean.
Fixes#1537
* Add utility functions to treat All as a heterogeneous container
* Distinguish RefC Int and Bits types
* Change RefC Integers to be arbitrary precision
* Add RefC Bits maths operations
* Make RefC div and mod Euclidean
* Add RefC bit-ops tests
* Add RefC integer comparison tests
* Add RefC IntN support
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
- Fix off-by-one error in String reverse
- Correct order of arguments in strSubstr
- Actually use start index of strSubstr
- Reduce memory usage of strSubstr in case of overrunning string end
- Add fastPack/fastUnpack/fastConcat
- Use unsigned chars for character comparisons
- Fix generated C character encodings
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).
* Banners for test pools
* Summary with the list of failing tests at the end
* Option to write the list of failing tests to a file
* Option to read the list of tests to run from a file
* Using these two latest features to add a new make target to rerun precisely the tests that failed last time
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
Previously, parameter block reused the same syntax as in Idris1:
```
parameters (v1 : t1, … , vn : tn)
```
Unfortunately this syntax presents some issues:
- It does not allow to declare implicit parameters
- It does not allow to specify which multiplicity to use
- It is inconsistent with the syntax used for named arguments elsewhere
in the language.
This change fixes those three problems by borrowing the syntax for
declaring type parameters in records:
```
parameters (v1 : t2) (v2 : t2) … (vn : tn)
```
It also enables other features like multiple declarations of arguments
with the same type:
```
parameters (v1, v2 : Type)
```
Given we keep getting tripped up by this, here we go:
* Namespaces
* Data names
* Record names
* Data constructor names (except for operators)
* Record constructor names (except for operators)
* Interface constructor names (except for operators)
`.proj` and `proj` are identically defined but separate functions.
This patch fixes it by defining `.proj` only once, and adding `proj = (.proj)`
for every projection.
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
Now reporting an error if we can't find a package that satisfies the
constraints. The version number field can still be a string (as it used
to be) but will give a deprecation warning - and the old style version
string wasn't used anyway.
Version constraints can have an upper and/or lower bound, which can be
inclusive or not.
Add wrap on file end
use rust-style raw string syntax
use swift style syntax raw string
Update src/Parser/Support.idr
Co-authored-by: André Videla <andre.videla@gmail.com>
Escape line wrap
Resolve conflict
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).
Local hints need to reduce (just like global hints do) so we expand
their definition to the lifted name before applying them.
We're identifying the global hints by knowing that the binder name is a
nested function name. This is a bit of hack, and it'd probably be better
to record that information in the binder instead, but that's a more
substantial change than I want to do right now.
This allows, for exmaple, to have apostrophes in module names.
Test was added only for chez, however this should be viable for all
targets with `:exec` implemented.
broaden what Names can be reflected and refied
I did not add the Names I wasn't sure how to test but have put placeholders
that produce clearer error messages.
There's some missing flexibility in how foreign specifiers can be used with
scheme that is addressed here with minimal changes to how scheme specifiers
are read. This opens up uses for users that they otherwise would have had
to modify the compiler's support files to accomplish.
Auxiliary functions introduced in elaboration (e.g., through case splits and with clauses) now
have the same totality annotation as the function they're defined in.
Moved auxiliary function `findSetTotal` into `Context.idr` since it's
now used by `ProcessDef.idr` too.
Added a totality requirement argument to `checkClause` so that the
with-clause case could propagate it to the functions it generates in
elaboration.
Sandwhich the rhs elaboration in pattern matches with code that sets
the global, default, totality requirement to the current one, and
restores the previous default afterwards. It's a bit of a hacky way to
do it, but I don't think we have a better alternative with the current
design.
Until now namespaces were stored as (reversed) lists of strings.
It led to:
* confusing code where we work on the underlying representation of
namespaces rather than say what we mean (using `isSuffixOf` to mean
`isParentOf`)
* potentially introducing errors by not respecting the invariant cf.
bug report #616 (but also name generation in the scheme backend
although that did not lead to bugs as it was self-consistent AFAICT)
* ad-hoc code to circumvent overlapping interface implementation when
showing / pretty-printing namespaces
This PR introduces a `Namespace` newtype containing a list of strings.
Nested namespaces are still stored in reverse order but the exposed
interface aims to support programming by saying what we mean
(`isParentOf`, `isApproximationOf`, `X <.> Y` computes to `X.Y`, etc.)
irrespective of the underlying representation.
As it was, it could break if the argument was repeated more than twice.
When checking dot patterns, we need to check that no further holes are
solved, and that the pattern variable doesn't unify with some other
pattern variable, but if it had already made progress (either for a good
or bad reason) we missed this. Fixes#536
As it was, there was significant backtracking for big expressions,
getting to the end, not finding a **, so having to try again for
application expressions. Fixes#532
This has involved quite a bit of reorganisation and some improvements in
resugaring so that the results look nice. In summary:
* Expression search now gives back a RawImp rather than a checked term,
which allows it to include case expressions
* Case with one pattern is resugared to a destructuring let
* Some name generation issues address in function generation
We look at intermediate results for local variables which are functions
that return a concrete type, or recursive calls that return a single
constructor type. In these cases, we:
* let bind the local variable/recursive call
* generate a new definition for the scope, as a 'case' function
When we recursively generate the definition, it's a bit more restricted
so as not to explode the search space. We only take the first result, we
only look one constructor deep, and we go right to left on variable
splitting so only deconstruct the name we've just added.
These continue the search from :ps and :gd next respectively, giving the
next search result until there are no more results.
Correspondingly, added ':proof-search-next' and ':generate-def-next' in
IDE mode, which continue the search from the previous ':proof-search'
and ':generate-def' respectively.
...until the definition is complete. This is necessary since sometimes
information outside the case block can help resolve interfaces, and in
the simplest case, we might just have delayed resolving a default
Integer. It turns out this was also an obscure bug waiting to happen
with coverage checking of nested case blocks (so there's a test update
there too).
Fixes#443
In a 'Bind', normalise the result of the first action, rather than
quoting the HNF. This improves performance since the HNF could be quite
big when quoted back.
Ideally, we wouldn't have to quote and unquote here, and we can probably
achieve this by tinkering with the evaluator.
This has an unfortunate effect on the reflection002 test, in that the
"typed template Idris" example now evaluates too much. But, I think the
overall performance is too important for the primary motivation
behind elaborator reflection. I will return to this!
Instead of just the cursory name update that we used to do (which didn't
work properly anyway for a lot of reasons), now we add aliases for all
the names in the imported module.
So, like Idris 1, every global has a canonical name by which we can
refer to it, but it can also have aliases via "import ... as".
If we have a delayed thing, but we don't yet know the expected type,
don't commit to forcing because the expected type might turn out to be a
delay.
Fixes#395
'convert' doesn't solve holes, so might reject things that are solvable.
This can be an issue when resolving interfaces, because we were using
convert for arguments of the invertible holes that arise when trying to
resolve them. Fixes#66.
We need to make sure they are inferred again when elaborating methods,
so substitute in a _ in method types before substituting in the explicit
parameters.
In future, it might (probably will) also be useful to allow giving the
implicit parameters explicitly when defining implementations.
Fixes#374
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.
The namespace parser was not requiring a minimum indentation and instead
based its indentation on the following line, which meant that a line like:
namespace Foo
foodef : Int
placed foodef into namespace Foo instead of the module's top level.
And so made it unclear when a namespace ends.
