Prover commands for evaluation and typechecking expressions

Now, the prover supports two new commands:

 * :t, :type gives the type of an expression
 * :e, :eval normalises the expression and prints the result

These work within the proof environment, so evaluating expressions that
contain references to hypotheses is allowed.
Merge pull request #924 from david-christiansen/prover-new-commands

Prover commands for evaluation and typechecking expressions
Tail recursive verison of treeToList (avoiding ++)
Merge branch 'master' into TailRecursiveTreeToList
shortcut to obtain the target type of a function
Chain higher order Fun types
Replace occaisional segfault with bad data

Previously, Show of Bits32 would cause segfaults once out of every few
thousand times it was called. Now, a ? is emitted for the odd digit.

This is sub-optimal - better would be to fix it. But in the meantime,
it's better not to segfault.
Fix non-termination bug in class resolution

Record the classes we've resolved, and reduce the depth when we
encounter any; not just if it's we're resolving a class that's the same
as the parent.

Fixes #931
Transpose on lists of lists
Merge pull request #925 from JanBessai/TailRecursiveTreeToList

Tail recursive treeToList
Merge pull request #926 from JanBessai/FunctionTarget

Shortcut to obtain the target type of a function
Merge pull request #928 from david-christiansen/bits-show-segfault

Replace occaisional segfault with bad data
Merge pull request #933 from JanBessai/transpose

Transpose on lists of lists
Stop getArgs from crashing executor
Postulate providers

Now, type providers don't need to return a proof - they can postulate
new axioms. The intention is to connect this both to QuickCheck and to
external proof oracles, such as SMT solvers.
Control whether provider decls accept postulates

Extends the provider syntax to accept an optional "what" parameter,
which controls if it can be satisfied with just proof terms, just
postulates, or either.
Rely on generated runMain to test if a main method is present instead of hardcoded Main.main
Split out Windows versions of some rts files

This allows the introduction of Posix functionality, parallel Windows
implementations can then be put in the windows/ directory.
Conversion checking tweak

Slightly more liberal if there are holes in the terms being checked, so
that we don't fail too early.
Merge branch 'master' of github.com:idris-lang/Idris-dev