I can't make sense of this code, it seems to try to convert the
case function corresponding to `let (a, b) = f n in ...` into a
different case function where `f n` and `(a, b)` have been unified.
But if `f n` is a bona fide stuck computation, there's no chance of
this happening.
Just turning this off solves the #1782 and only breaks one function
in the whole of the idris2 repo (I would have expected our current
termination oracle to be too weak to detect it as valid anyway!)
and one in frex (which, again, should not have been seen as terminating).
Also fixes#1460
In the `MkFix : f (Fix f) -> Fix f` example, using `Erased` for `f`
makes the type reduce to `[__] (Fix [__]) -> Fix [__]` and because
`[__] e1 ... en` computes to `[__]`, we end up with `[__] -> Fix [__]`
which does not reference `Fix` anymore.
In theory argument elaboration order doesn't matter, but in practice we
sometimes make choices for performance reasons, like helping with
disambiguation by knowing the target type.
This was kind of messy, now we can more clearly see what's going on.
Also, more importantly, it gives us a bit more control which we
sometimes need. For example, if we go choose to go right to left for
some performance heuristic it might turn out we don't have enough
information yet, in which case we need to delay and try again later.
Fixes#1743
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
These entries returned by `readdir` are legacy of Unix API, we don't
really need them. Most APIs do not return them (for example Java
`Files.newDirectoryStream` or Python `os.listdir`).
* 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
Operating system counter stores signals as flag set without counter.
So sending two signals to a process may result to one or two signal
handler invocation. Queueing signals inside Idris could give users
false sense of signals being are queue, while they are not.
In particular, test for signal could not work reliably for that
reason.
Also, practically we usually don't need have more than once signal
event.
This is follow-up to #1660. CC @mattpolzin
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.
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
