* [ 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).
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.
* 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
We should really get these automatically, but until we do, add the
flags. Chez seems to spot these anyway, but again it makes the generated
code easier to look at, and it removes some needless abstraction over
interfaces at runtime.
We've had these for a while, used for interface specialisation, but
they're not yet used anywhere else or properly documented. We should
document them soon, but for now, it's a useful performance boost to
always use the fast versions of pack/unpack/concat at runtime.
Also moves a couple to the prelude, to ensure that the fast versions are
defined in the same place as the 'normal' version so that the
transformation will always fire (that is, no need to import Data.String
for the transformation to work).
This has a much better behaviour with respect to proof search and
the coverage checker realising we don't need to consider the Z case
than the `Not (x = Z)` we used earlier.
When bootstrapping, we're building things without packages being
available, so we can't expect to find them when looking for
dependencies. So, we find them another way, with an environment
variable. This flag is to tell Idris not to worry about missing
dependencies in this situation.
We also need to update the bootstrapping code, to deal with the new
version number format and new flag in the ipkg files for the libraries.
I think it's still safe to build from the previous version though - lets
see if CI agrees!
Packages are now installed in a directory with their version number.
On adding a package directory, we now look in a local 'depends'
directory first (to allow packages to be installed locally to another
project) before the global install directory.
Dependencies can have version bounds (details yet to be implemented) and
we pick the package with the highest version number that matches.
Added several functions for `Dec`. The set of functions and names
are picked consistently with `Maybe`:
* `isNothing` -> `isNo`
* `isJust` -> `isYes`
* `IsJust` -> `IsYes`
* `isItJust` -> `isItYes`
This is follow-up to #942
Ideally, liftIO would always be linear, but that has lots of knock-on
effects for other monads which we might want to put in HasIO, now that
subtyping is gone. We'll have to revisit this when we have some kind of
multiplicity polymorphism.
Snoc add an element at the end of the vector. The main use case
for such a function is to get the expected type signature
Vect n a -> a -> Vect (S n) a instead of
Vect n a -> a -> Vect (n + 1) a which you get by using `++ [x]`
Snoc gets is name from `cons` by reversin each letter, indicating
tacking on the element at the end rather than the begining.
`append` would also be a suitable name.
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).
This is done to make able for `Data.*` modules of datatypes declared in
prelude to import modules that have their own definitions of `DecEq`
inside them (i.e. modules of datatypes declared in the `base`).
Division Theorem. For every natural number `x` and positive natural
number `n`, there is a unique decomposition:
`x = q*n + r`
with `q`,`r` natural and `r` < `n`.
`q` is the quotient when dividing `x` by `n`
`r` is the remainder when dividing `x` by `n`.
This commit adds a proof for this fact, in case
we want to reason about modular arithmetic (for example, when dealing
with binary representations). A future, more systematic, development could
perhaps follow: @clayrat 's (idris1) port of Coq's binary arithmetics:
https://github.com/sbp/idris-bi/blob/master/src/Data/Bin/DivMod.idrhttps://github.com/sbp/idris-bi/blob/master/src/Data/Biz/DivMod.idrhttps://github.com/sbp/idris-bi/blob/master/src/Data/BizMod2/DivMod.idr
In the process, it bulks up the stdlib with:
+ a generic PreorderReasoning module for arbitrary preorders,
analogous for the equational reasoning module
+ some missing facts about Nat operations.
+ Refactor some Nat order properties using a 'reflect' function
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
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.
Nipping this historical artifact in the bud before it roots. It's often
useful to be able to `map` directly to the result of a StateT computation
and due to how Functor works this is made harder when the tuple is
(a,state) vs (state,a)
* [contrib] Add misc libraries to contrib
Expose some `private` function in libs/base that I needed, and seem like
their visibility was forgotten
I'd appreciate a code review, especially to tell me I'm
re-implementing something that's already elsewhere in the library
Mostly extending existing functionality:
* `Data/Void.idr`: add some utility functions for manipulating absurdity.
* `Decidable/Decidable/Extra.idr`: add support for double negation elimination in decidable relations
* `Data/Fun/Extra.idr`:
+ add `application` (total and partil) for n-ary functions
+ add (slightly) dependent versions of these operations
* `Decidable/Order/Strict.idr`: a strict preorder is what you get when
you remove the diagonal from a pre-order. For example, `<` is the
associated preorder for `<=` over `Nat`.
Analogous to `Decidable.Order`. The proof search mechanism struggled
a bit, so I had to hack it --- sorry.
Eventually we should move `Data.Fun.Extra.Pointwise` to `Data.Vect.Quantifiers` in base
but we don't have any interesting uses for it at the moment so it's not
urgent.
Co-authored by @gallais
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.
Until now namespaces were stored as (reversed) lists of strings.
It led to:
* confusing code where we work on the representation rather than say
what we mean (e.g. 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 implementations when
showing / pretty-printing namespaces
This introduces a Namespace newtype containing non-empty lists 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.
Main change
===========
The main change is to the type of function dealing with an untouched
segment of the local scope. e.g.
```
weak : {outer, vars : _} -> (ns : List Name) ->
tm (outer ++ inner) -> tm (outer ++ ns ++ inner)
```
Instead we now write
```
weak : SizeOf ns -> tm (outer ++ inner) -> tm (outer ++ ns ++ inner)
```
meaning that we do not need the values of `outer`, `inner` and `ns`
at runtime. Instead we only demand a `SizeOf ns` which is a `Nat`
together with an (erased) proof that `ns` is of that length.
Other modifications
===================
Quadratic behaviour
-------------------
A side effect of this refactor is the removal of two sources of
quadratic behaviour. They typically arise in a situation where
work is done on a scope of the form
```
outer ++ done ++ ns ++ inner
```
When `ns` is non-empty, some work is performed and then the variable
is moved to the pile of things we are `done` with. This leads to
recursive calls of the form `f done` -> `f (done ++ [v])` leading
to a cost quadratic in the size of `ns`.
Now that we only care about `SizeOf done`, the recursive call is
(once all the runtime irrelevant content is erased) for the form
`f n` -> `f (S n)`!
More runtime irrelevance
------------------------
In some places we used to rely on a list of names `vars` being
available. However once we only care about the length of `vars`,
the fact it is not available is not a limitation.
For instance a `SizeOf vars` can be reconstructed from an environment
assigning values to `vars` even if `vars` is irrelevant. Indeed the
size of the environment is the same as that of `vars`.
For Void and Either
This is because I ended up using them elsewhere, so why not include them in the stdlib.
Also expose left/rightInjective functions, as are used in the DecEq proofs.
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!
