Now only abstracts over the environment once and deals with 'where'
clauses by rewriting the nested name with the rearranged environment. As
a result, it interacts far better with local definitions (i.e. where
blocks).
They're global, and so we don't reset per file, so we might get
duplicates, so it's much quicker to store as a map even though we'd
expect few of them overall.
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
