This changes the behaviour of 'auto' implicits so that by default they
return the first result, rather than checking for unique results. This
is consistent with Idris 1. However, we still want to check for
uniqueness somtimes (for example, with interface search, which should
reject overlapping results) so the 'uniqueSearch' option means that any
auto implicit search for the type should check uniqueness of results.
Fixes#169
This is further progress towards a metaprogramming system in a form
similar to Elaborator Reflection or Template Haskell, but trying to
avoid leaking too many implementation details of the elaborator itself.
Also include proof the tail-recursive versions are extensionally equivalent to the non-tail-recursive one
I'm a bit worried that some of those proofs came through, as
visibility modifiers should get in the way. If they cause problems at
some future point, just delete/comment them out.
This is the result of running the command:
$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +
I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
These functions use the NonEmpty predicate type in order to prove
that the operation will be valid.
Implementations copied from Idris1's Prelude.List module, except without
expanding the auto implicit argument.
See e.g. Applicative instance in Data.Vect. This allows implementations
to use implicits at run time (by default, they'd be 0 multiplicity so
erased, but it might be useful to have an index available at run time).
At the moment, the parser requires implicits to be given before
constraints. Ideally it should be possible to give them in any order.
I'll come back to this.
This makes it easier for more complicated packages (e.g. network, which
needs to install a C shared library) to know where to put things without
having to work out the prefix themselves.
Since they'll be incompatible between different Idris2 versions, this
helps protect against importing the wrong thing by mistake. Also, it
means the canonical place for the version number is now the top level
Makefile.
You'll need to delete src/YafflePaths.idr before rebuilding, since it's
now generated slightly differently.
This is so that we can put other build artefacts (e.g. executables) in
properly organised subdirectories of build, e.g. build/bin/chez,
build/bin/js, etc.
Functions can be declared as %foreign with a list of calling
conventions, which a backend will work through until it finds one it can
understand. Currently implemented only in Chez backend. If this works
out, I'll implement it for Racket too, and remove the old primitive
functions.
There's a bit more boiler plate here than before, but it has the benefit
of being more extensible and portable between different back ends.
Some examples, pending proper documentation:
%foreign "C:puts,libc" "scheme:display"
putline : String -> PrimIO ()
%foreign "C:exp, libm.so.6, math.h"
fexp : Double -> Double
%foreign "C:initscr, ncurses_glue.so, ncurses.h"
prim_initscr : PrimIO ()
Since it's just to check that it's built successful and we can send a
message back and forth, remove the diagnostic message that might come
out in a different order depending on scheduling.
