* deprecate Data.Nat.Order.decideLTE
* Add properties for LTE/GTE that produce the difference.
* remove deprecated function now that it is available in the base library.
* remove two deprecated lines.
* remove module deprecated since v0.4.0
* fix prelude reference to renamed primitive.
* finish removing Data.Num.Implementations
* remove deprecated dirEntry function.
* remove deprecated fastAppend. Update CHANGELOG.
* replace fastAppend in test case
* replace fastAppend uses in compiler.
* remove new properties that weren't actually very new.
* [ 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
* 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.
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`.
* 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.
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).
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>
