This has involved quite a bit of reorganisation and some improvements in
resugaring so that the results look nice. In summary:
* Expression search now gives back a RawImp rather than a checked term,
which allows it to include case expressions
* Case with one pattern is resugared to a destructuring let
* Some name generation issues address in function generation
We look at intermediate results for local variables which are functions
that return a concrete type, or recursive calls that return a single
constructor type. In these cases, we:
* let bind the local variable/recursive call
* generate a new definition for the scope, as a 'case' function
When we recursively generate the definition, it's a bit more restricted
so as not to explode the search space. We only take the first result, we
only look one constructor deep, and we go right to left on variable
splitting so only deconstruct the name we've just added.
Sort by proportion of bound variables used, which is likely to get us
the right answer quicker. The results are generated in batches of 16 (a
completely arbitrary choice) then sorted.
When an erased pattern argument in a non-erased context is of a
datatype that has 0 or 1 constructors, there is no need to dot it
(i.e., require that the canonical term is inferred by other
dependencies): it has to be the unique constructor that appears in the
source.
This gives the number of implementations to reject before accepting one.
It's intended as a reasonably cheap way of giving multiple results from
interactive editing (e.g. the vim mode, which goes via the REPL and
--client rather than the IDE mode)
These continue the search from :ps and :gd next respectively, giving the
next search result until there are no more results.
Correspondingly, added ':proof-search-next' and ':generate-def-next' in
IDE mode, which continue the search from the previous ':proof-search'
and ':generate-def' respectively.
Return a 'Search' rather than a single definition. Also, change the
order of search in expressions so that we look at recursive calls
earlier when under a constructor - the assumption being that this is
more likely than nested constructors.
Rather than returning a complete list of results, return a pair of the
first result, and a continuation. The continuation explains how to
continue the search if the given result is deemed unacceptable (either
on encountering an error somewhere, or just if the caller wants the next
result).
This means we don't search needlessly if we're only looking for the
first result. Fixes#228
For Void and Either
This is because I ended up using them elsewhere, so why not include them in the stdlib.
Also expose left/rightInjective functions, as are used in the DecEq proofs.
