Gets the OS info from the host compiler, which we'll need to be careful
with when bootstrapping (since maybe we'll distribute generated chez or
racket as a starting point for bootstrapping...)
Not in generating install directories, otherwise we end up with loads of
new directories for every patch and the purpose is to make it easy to
see which version you're working with.
The Chicken backend and reflection code are currently unused, and add to
memory usage and build time, so best leave them out for the moment.
They will be back! But probably best to wait until we can self host -
which hopefully won't be long - and we can take advantage of some of
the things Idris 2 does to compile quicker and using less space!
Always infer a multiplicity of W. Since we can pass a linear function to
one which expects an unrestricted argument, this gives the more general
result if the multiplicity is otherwise unknown.
This makes things like 'maybe id (+) x y' type check again even in the
presence of an 'id' which is declared linear!
This is the same as %auto_implicits in Idris 1, but with a more
appropriate name, because auto implicits are something else.
'%unbound_implicits off' turns off implicit forall bindings. See test
basic033 for an example.
In a small change from Idris 1, this lifts to the nearest binder or
block, so doesn't lift past an explicit "do" in particular. Blocks are:
- case branches
- if branches
- scope of local function definitions, or any binder
- do blocks
Need to use 'check' which expands ambiguous names, rather than
'checkImp' which does nothing. It won't insert any new dots since it
checks in expression context.
It's a big patch, but the summary is that it's okay to use a pattern in
an erased position if either:
- the pattern can also be solved by unification (this is the same as
'dot patterns' for matching on non-constructor forms)
- the argument position is detaggable w.r.t. non-erased arguments, which
means we can tell which pattern it is without pattern matching
The second case, in particular, means we can still pattern match on
proof terms which turn out to be irrelevant, especially Refl.
Fixes#178
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.
