Rather than just raw Strings. They get evaluated immediately at the
point of elaboration, and this can be used to save repetition (e.g. of
shared library names) in declarations.
(In the Racket/Chez back ends)
A bit ugly, but it means that after making an executable, all the
necessary files are in the same directory ready for packaging. The
executable can still only be run when the libraries are in the
racket/chez library search path. In practice at the moment that means
they need to be in the current working directory...
Having a separate directory for generating executables will help deal
with packaging executables for back ends which need extra library
support, since we can copy the relevant libraries into the executable
directory and know where everything is.
To build the top level method and interface record correctly, we need to
know where to put the implicit arguments, so invent names if they don't
have them already then we'll know where to put things accurately.
Earlier solutions may influence later ones. Probably we should be
cleverer still here, and keep trying while any delayed elaborators are
run successfully, because really the order shouldn't matter!
When we check a scope in RigW, need to mark all linear things outside
that scope as irrelevant within the scope (since the scope may be used
multiple times).
This fixes the issue where some Scheme compiler like mit-scheme is
installed and that gets picked up first, leading to an infinite
loop in the tests.
Also see attached image in the PR.
Turns out we need this after all, since the types may be necessary
during linearity checking if imported names are imported and reduced
during elaboration for some reason (e.g. during unification)
In the case where the function type is not yet known, and there's a
postponed unification problem, we were returning the function type not
the result type.
--debug-elab-check ought to be extended to catch this sort of thing.
Fixes#168
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.
This is to help Idris2 codegen the correct scripts on NixOS where
Racket and Chicken aren't installed in the standard locations, and
the /usr/bin/env trampoline is disabled at package build time.
This now matches the existing Chez behavior.
Also, fixed the test runner to restore the correct working directory
after a failed test, and fixed the top-level Makefile to allow the
IDRIS2_VERSION variable to be queried without building the project.
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.
