Behaviour of :t on names remains the same (showing the non-normalised
type).
Added evaltypes option (on by default) so the old behaviour can be
regained with :unset evaltypes.
This means partially applied things with interesting types will be
displayed more helpfully, e.g.:
*printf> :t printf "%s %d"
printf "%s %d" : String -> Int -> String
Using a nightly stackage config to build on GHC 7.10, and there are some
dependencies that are more advanced than the most recent LTS stackage
config. This should just build using `stack build` in the Idris-dev root.
It's a bit ugly for non-constant operators, but non-constant operators
are ugly anyway, and unusual, so I'm not going to worry too much about
that...
This should now be good enough to use in place of the old evaluator for
things which only need the constructor at the head (which includes
conversion, unification and partial evaluation.)
Some simplifying assumptions on operators, for the moment, in particular
that they are always implemented on constants (which isn't necessarily
true but is fine for most cases at the moment).
Reduction to weak head normal form. Currently includes structure of the
algorithm, but does not yet reduce function names.
Also removed ':hnf' from REPL commands and replaced with ':whnf'.
Now, editors do not need to implement their own regexp-based
highlighting, as all keywords are highlighted by Idris's parser. This
also means that the data exported by --highlight can be used to fully
annotate a source file, either for HTML data or for LaTeX.
Now, editors get highlighting information for integer literals according
to the following rules:
1. If the constant elaborates to a constant (such as the fromInteger
implementations for Integer, Int, Bits8, etc), then the constant
itself is used for highlighting informating, as it would be in the
pretty printer.
2. If the constant elaborates to an inductive datatype, the outermost
constructor is used for highlighting (e.g., the Nat 4 highlights as
S, and the Nat 0 highlights as Z)
3. Otherwise, no highlighting is performed.
In a try or handleError, just take the message from the second thing
that failed. (This may turn out to need more control depending on the
use of the try/handleError. We'll see.)
Instead of guessing the error for the thing that's closest to working,
better to say that no alternative works.
(This makes the bizarre 'score' heuristic for error messages obsolete,
so that'll be removed soon too.)
Mostly by delaying the expensive checking for uniqueness of names until
the point where we actually need the branch, thus removing a significant
amount of unnecesary work.
Now, the elaborator supports highlighting of pairs, lists, and sigmas in
their sugared for, revealing the underlying names in the highlight. This
means that tooltips in Emacs and any other editor supporting
highlighting can now show how a particular notation was disambiguated -
Vects and Lists give different tooltips, and pair types have blue
parentheses and commas while pair values have red ones. Likewise for
dependent pairs.
'implicit' will now only work if there is a concrete argument type and a
concrete return type. This means we can rule out impossible coercions
much quicker, and has the effect of speeding up error reporting by not
trying to fix up the error with coercions which are never going to work.
There's a special case for "lend" but UniqueType is experimental and
probably needs a rethink, so I'm okay with this at least for now.
