* [ breaking ] remove parsing of dangling binders
It used to be the case that
```
ID : Type -> Type
ID a = a
test : ID (a : Type) -> a -> a
test = \ a, x => x
```
and
```
head : List $ a -> Maybe a
head [] = Nothing
head (x :: _) = Just x
```
were accepted but these are now rejected because:
* `ID (a : Type) -> a -> a` is parsed as `(ID (a : Type)) -> a -> a`
* `List $ a -> Maybe a` is parsed as `List (a -> Maybe a)`
Similarly if you want to use a lambda / rewrite / let expression as
part of the last argument of an application, the use of `$` or parens
is now mandatory.
This should hopefully allow us to make progress on #1703
* Stub for future 'identity' optimisation
I plan to add this later, but I'm using for now for
NaturalToInteger and IntegerToNatural
* Refactor `%builtin`
fixes#1799
- automatically optimise all Natural shaped things
- NaturalToInteger and IntegerToNatural now use
new `Identity` flag (internal use only for now)
which signals the function is identity at runtime
* Use NaturalToInteger and IntegerToNatural for Nat and Fin
Also define show fin in terms of finToInteger, for speed
* Fix name handling for %builtin
* [ tests ] fixes + #1799
* remove %builtin from libs
Add back after next version
* Use resolved names where convenient
Turns out that `Smaller` and `LT` won't unify because
1. the instance Sized Nat is not publicly exported
2. Smaller, and LT are stuck until fully applied
The given changes make that go away.
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
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
To be able to use `C` functions for both Scheme and RefC: it was
not possible for `Buffer` before this PR.
As an example, `writeBufferData` and `readBufferData` functions are
removed: generic C backend implementations are used instead.
* 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
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)
| ^^^^^^^^^
```
Since `[a..b]` uses `takeUntil`/`takeBefore` indirectly those too had to
be changed to `public export` clashing with `Data.Stream` definitions.
A small readability refactor was made with the `compare` function from
`EqOrd`.
To be able to eventually refactor/extend `system` function: to be
able to specify a directory, environment variables, specify arguments
as array etc. Ideally it should be something like Rust
[`std::process::Command`](https://doc.rust-lang.org/std/process/struct.Command.html).
