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`).
This also changes the return type of `char` and `string`. They
previously returned `()`, they now return `Char` and `String`
repectively.
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Rather than translating the constraints to a Dybjer-Setzer IR code
we can produce an ad-hoc definition of a `Domain` that we will be
able to make runtime irrelevant.
This means that compiled code will never need to construct a proof
that a value is in the domain of the function: it will simply run
the function!
Refactor the DIY equational reasoning library to be a bit more like
the generic pre-order reasoning library:
Change the `...` notation into a constructor for a new `Step` datatype.
This seems to help idris disambiguate between the two kinds of
reasoning when they're used in the same file (e.g., frex).
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
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>
This mirrors the (>>) found in Haskell, which is the same as (>>=), except the
second computation (on the right hand side) takes no arguments, and the result
of the first computation is discarded. This is a trivial implementation written
in terms of (>>=).
The Network.Socket.Data code previously used hardcoded constants manually read
from auto-generated C source code, however these constants are specific to
Linux. The original code looked like this:
export
ToCode SocketFamily where
-- Don't know how to read a constant value from C code in idris2...
-- gotta to hardcode those for now
toCode AF_UNSPEC = 0 -- unsafePerformIO (cMacro "#AF_UNSPEC" Int)
toCode AF_UNIX = 1
toCode AF_INET = 2
toCode AF_INET6 = 10
The AF_INET6 constant is correct on my Debian 10 laptop:
molly on flywheel ~> grep -rE '^#define AF_INET6' /usr/include
/usr/include/x86_64-linux-gnu/bits/socket.h:#define AF_INET6 PF_INET6
molly on flywheel ~> grep -rE '^#define PF_INET6' /usr/include
/usr/include/x86_64-linux-gnu/bits/socket.h:#define PF_INET6 10 /* IP version 6. */
However, this is not the case on an OpenBSD machine:
spanner# grep -rE '^#define[[:space:]]+AF_INET6' /usr/include
/usr/include/sys/socket.h:#define AF_INET6 24 /* IPv6 */
This commit adds accessor functions to the C runtime support library for
retrieving the values of these macros as they appear in the system libc header
files, which can then be invoked using the normal C FFI machinery.
useful items for applying multiple predicates, e.g.
sortBy (comparing length <+> compare)
To sort some lists elements by length and then lexographically
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 lack of a better place, I've put it in `Syntax.PreorderReasoning`
These equations are natural in equational reasoning, but less so when
rewriting, so that's why it's there
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!
This is partly to tidy things up, but also a good test for 'import as'.
Requires some internal changes since there are parts of reflection,
unelaboration and a compiler hack that rely on where things are in the
Prelude.
This is helpful when defining auto-implicits of the form:
pairEqF : DecEq a
=> (thisX, x, y : a)
-> {prfRefl : Equal x thisX}
-> (prfEq : decEq x thisX = Yes prfRefl)
=> Pair a a
pairEqF thisX x y {prfRefl} {prfEq} = MkPair x y
before auto-implicit search would fail to find `Refl` for `prfRefl`.
With this fix the solution is found.
This fix means we can avoid having to write the following.
pairEqF' : DecEq a
=> (thisX, x, y : a)
-> (prfEq : decEq x thisX = Yes (the (Equal x x) Refl))
=> Pair a a
pairEqF' thisX x y {prfEq} = MkPair x y
This didn't cause a problem before as it was likely just ignored by the C
function. According to Edwin the extra argument is a leftover from when this
was a pure scheme call.
There is an argument that, for import public, this should be automatic
(that is, the publicly imported things should be reexported with the
parent namespace). I decided not to do this, because another use of
import public which we do a lot in the Idris 2 code base is purely as a
convenience, where we still expect things to be in their original
namespace.
Also, where there's a choice between things being explicit and implicit,
I prefer to err on the side of explicit now.
So, if what you really want in an API is to reexport, you can do that,
but explicitly.
The ports are rather straight forward and I have purposefully written
the documentation to be beginner friendly.
Note, I have diverged from Idris1 over the naming of the projection
functions to make them consistent with `Pair` and `DPair`.
Apparently the concrete syntax is controversial ("{apples}"
vs. "$oranges"), so I'm just adding a simple DYI version until we
agree on a concrete syntax
This involves updating the bootstrap code since it needs a fix in
interface resolution. It shouldn't affect the Idris2-boot build though,
since it's in the libraries not the Idris2 source.
It's worth delaying in case doing some more work (and some more
interface resolution) can make the type more concrete. This makes
test linear011 work more smoothly, and will help with this sort of
program in general.
A better way, later, would be to try elaborating and delay only if the
type is not yet known. We have the facilities, but it's too fiddly for
me to want to implement it right now...
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.
Doing this is awkward, for a number of reasons, including 'pure' not
being linear in its argument - there's no guarantee it'll be used
linearly after all - and lack of multiplicity polymorphism. Fortunately
the user doesn't have to know about the ugliness underneath!
We can look at ways to make it less horrible later :). For now, this is
starting to look like something that allows us to write linear protocols
without too much extra machinery on top of IO.
Conditional variables with timeout in Chez didn't work, so changed to a
consistent meaning of the timeout (microseconds). Also fix linearity of
unsafePerformIO.
Following a fairly detailed discussion on slack, the feeling is
generally that it's better to have a single interface. While precision
is nice, it doesn't appear to buy us anything here. If that turns out to
be wrong, or limiting somehow, we can revisit it later. Also:
- it's easier for backend authors if the type of IO operations is
slightly less restrictive. For example, if it's in HasIO, that limits
alternative implementations, which might be awkward for some
alternative back ends.
- it's one less extra detail to learn. This is minor, but there needs to
be a clear advantage if there's more detail to learn.
- It is difficult to think of an underlying type that can't have a Monad
instance (I have personally never encountered one - if they turns out
to exist, again, we can revisit!)
