This improves coverage checking, because it can now see that things like
(Z = S x) and (x = S x) are empty. Previously, it only checked that all
possible constructors had a disjoint index. Now, it looks for matches
and checks for disjointness in the matches, which catches a lot more
things especially with equality.
This is added to functions which are guaranteed to be productive. The
check is currently very conservative - just added when every clause is
constructor headed (or headed by an AllGuarded function), and there are
no other function applications.
This allows a function to be inlined for totality checking purposes
only. So, for example, (>>=) might be a function, but if it evaluates to
something constructor guarded in some context, then it might still be
productive.
It needs to take into account that solving other names might cause
unification errors to succeed, so only give up if there's conflicting
concrete constructors
If we never evaluate under Delay at all, we won't inline interface
methods, which means productive things defined in an interface can never
be today. So, make sure to set the tcinline flag before quoting the
Delayed closure.
If we're delaying because of a unification failure, there's no point in
trying again. This can massively speed up (or maybe I should say "unslow
down") error reporting if there's ambiguity because the elaborator won't
be exploring some paths which can never succeed.
Run once ignoring errors to make progress on interfaces/determining
arguments, then again in full. Second step isn't needed since it was
just covering up an earlier bug.
This means that some errors under lots of delays are reported quicker,
though I still haven't completely got to the bottom of that one.
To make sure the protocol doesn't jam, supply stub implementation to
all protocol commands.
Report to REPL when an unimplemented command is used.
Notes
-----
1. We don't support add-proof-clause. I guess all proof-related stuff
should be removed from the protocol
2. Some types are stub types too. That's because we need to `SExpable`
more structured types like `PTerm`. I'll leave that to the future.
3. I've lifted `REPLResult` into `IDEResult` inside `IDEMode/REPL.idr`.
That's because some results, like `who-calls` only make sense in
the context of an IDE, not in the context of a user-facing REPL.
The Editing commands should be moved from the REPL into the IDE and
called from the REPL.
I leave that to the future, once more of the protocol is
implemented.
4. Export a few functions from the REPL so that the IDE can call them.
5. There's one outstanding issue with the emacs idris-mode: it
currently calls the unsupported `:consolewidth` REPL command. This
is harmless, and can wait until @edwinb decides whether we should
support it in the future or not.
6. There was a bug as to how holes are returned to the user. The
format isn't documented in the protocol, so we'll need to reproduce
it, perhaps from the idris-mode elisp sources.
In which delayed elaborators which arise during other delayed
elaborators might not get run, leading to a hole, so if there's an error
in the delayed elaborator you might just see that there's a hole still
to resolve.
The down side of this, at least in the example that prompted it, is that
it can take a while for an unresolvable ambiguity error to be reported
while it explores everything. even if there's only a few possibilities.
I will try to think of something...
