Tweak reduction rules for private/abstract names

It is better if private names reduce during typechecking (since such
things arise in public functions which should reduce completely) and
only abstract names are prevented from reducing.

Fixes #348
Remove some of the more easily avoided %assert_totals
Use toNat to avoid %assert_total when negative Int is treated the same as 0.
Replace some Heap proofs with impossible.
Turn off optimisations when compiling parser

Disabling optimisations in Parser and ParserExpr allows to compile
these modules in a matter of seconds. It also doesn't seem to
affect compilation times of Idris programs.
Merge pull request #664 from sjdrodge/assert_total_cleanup

Some %assert_total cleanup
Merge pull request #666 from jstolarek/fast-parser-compilation

Turn off optimisations when compiling parser
Merge branch 'master' of github.com:idris-lang/Idris-dev
Add String offsets to VM

Now strTail just stores an offset into a string, meaning that it doesn't
need to reallocate or copy an entire string. Therefore traversing a
large string is now much quicker.

Note - this means the entire string gets GCed at once, so if there is a
large string but only a pointer to the end of it, the whole string still
needs to be stored. For traversal, this isn't really a problem, but we
may want to reallocate if the GC discovers there is only one reference
to an offset string.
Change Show instances for Char and String to match their literals
Adjust tests to the changed String show instance
Fix Char literal matching in C codegen
Update language-java dependency to 0.2.6

This version is required for the Java backend to emit correct char and string
literals in nonprinting and/or nonascii cases.
Fix rendering of LChInt in Java backend
Make GMP optional (default off)

This removes the last common obstacle to getting Idris built, at the
expense of using mini-gmp which is supposedly slower (but I haven't yet
measured how much this is likely to affect us).
Don't need NFData instances for constants

Because 'seq' alone already does the right thing
Merge pull request #669 from Melvar/showstring

Change Show instances for Char and String to match their literals
Merge pull request #670 from walkie/master

Minor bug fix in Prelude.Fin.integerToFin.
Documented the Chars module and added new functions.

+ ord and chr
+ isOctDigit
Switch on 'elabPE'

Generates a new specialised definition for [static] argument positions
which are then elaborated recursively.

Not yet transforming from the original call to the specialised
definition. Also still need to take more care in how we specialise
definitions - however, the mechanics of generating the new definitions
is now done.

Generating new definitions may fail for various reasons (scoping errors,
for example). This is considered safe, and just fails silently, because
it just means it's not a specialisable call.

Also removed the {static} syntax because it's inconsistent. [static]
only works on named pi bindings due to awkwardness in the parser.