As it was, there was significant backtracking for big expressions,
getting to the end, not finding a **, so having to try again for
application expressions. Fixes#532
The timings flag (`--timing`) displays various timing information during the entire compilation process.
This is useful when performing adhoc profiling of the compiler.
However, the information is a mixture of timestamps and relative progress.
The information is inherently nested, and such nesting is not immediatly clear in the output.
This can be confusing.
This minor changes nests the timing information on output so that when aligned one can see the timestamps at the highest level, and progress during the elaboration stage.
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.
