It's not actually used as part of any compilation pipeline yet, and I've
only tested it by eyeballing the output, but it'll be useful soon, and
it's good for it to be available to any new back ends that might need
it. It will need some optimisation.
e.g. in a C file. This means we don't accidentally treat things as
empty, since previously we just defined these as empty types, but that
broke coverage checking. Fixes#240
The names the locals were being applied to weren't being updated
properly, so applications of local functions inside case blocks were
sometimes given the wrong arguments. This is one of the few places where
it's hard to keep track of names in the type system! So naturally that'd
be where things go wrong I suppose...
Make desugaring/elaboration of interfaces, interface implementations,
records, and parameter blocks take into account the pragma
`%unbound_implicits off`.
Main changes:
(a) Execute the pragma also during desugaring
(b) Check whether `isUnboundImplicits` is on at each desugaring step
Alternatives I didn't take:
(1) Changing `findBindableNames` to effectfully check the flag.
Rationale:
Apart from turning a pure function into an effectful one, this
would mean repeatedly calling `findBindableNames`, only to do
nothing once the flag is read.
(2) Adding another function that takes multiple places (list of terms)
that might contain bindable names, and before dispatching
`findBindableNames` on each term, checking the flag.
Rationale: I didn't want to add another abstraction. (weak
rationale)
@edwinb @gallais : if you prefer (2), I can do that.
My first attempt at refolding natural constants led to all names
being printed with their namespace prefixes. This fixes that,
most notably by introducing the massive `mapPTermM` function in
`Idris.Syntax`.
We should be able to comment out any part of a program that parses
and still get a program that parses. This means we need to properly
ignore `{-` and `-}` when hidden behind a `--` comment or inside of
a string literal.
The names weren't fully explicit in the elaborator, so ambiguity
resolution wasn't able to take advantage of type-directed pruning. Now
they're explicit (but hard-coded, which we should fix later...) so they
can be resolved more easily.
- Add support for .lidr files.
- Add new Parse Error for Literate fails.
- Add support for Case Split.
- Add support for Add Clause.
- Add support for Add Lemma.
- Add tests.
We can work out what it should be since each case is supposed to have
the same type, so we can look ahead to the alternatives. This way, we
don't have to rely on the scrutinee alone to calculate the type of the
case block. (Idris 1 does this too but I've only just encountered the
need for it in Idris 2 now!)
Sorry for the less than informative title :). Lots going on here. It
started as an attempt to fix unification to deal with laziness coercions
in trickier places, but unearthed a couple of tricky and interconnected
issues that are hard to unpick into a single patch. So, this fixes a few
things:
- default hints should only be resolved on the current elaboration (e.g.
nested function definitions, not the outer definition which might not
yet be complete)
- delayed elaborators should be allowed to have nested delayed
elaborators, which means disambiguation is a little bit better
- we should delay elaborating arguments where the type isn't known yet,
because later arguments may resolve the type, and we can use this to
help with disambiguation/laziness coercions
- other bits and pieces arising
Record name and constructor are in the outer namespace, fields in the
nested namepsace. Private names in the nested namespace is visible from
the outer namespace. Fixes#183
Also remove the 'nested' flag on INamespace, since it was only there for
records, and not really the right way to do things. The nested namespace
name is now given in the IRecord constructor (a front end might not want
to use a new namespace after all).
They might match on runtime-erased things (which is okay, since they're
erased too!) and if we try building the tree, it'll report an error
incorrectly. Fixes#229
Check that none of the generated missing cases match explicitly given
clauses, which might happen if there's some overlaps in the clauses or
if there's some matching on implicits. Ignore erased argument positions
when checking the match.
If we postpone unification problems, it's not necessarily at the top
level of a term, but then if we retry and find we need to insert a
'Delay' or 'Force' then it had better be at the top level or we'll get
an incorrect term. So, keep track of this in postponed constraints.
For example, delayed elaborators. If it resolves one, and it's not a
complete solution, we might end up with unsolved holes. Or - possibly
worse - we might end up with an error in a program that is silently
fixed rather than reported!
Fixes#223
