Removal of minor TODOs

Some were completed before and we forgot to remove the TODO, while
others I just took care of.
Optimisation options

--partial-eval and --no-partial eval (former is the default)
-O[0-3] now set packages of optimisation options (although the only one
currently existing is partial-eval, which is set at levels >=2)
Default -O2
Make do blocks require an expression

This makes for better error messages and fixes #1656.

Old message:

    > :t do
    When elaborating an application of constructor __infer:
            INTERNAL ERROR: Invalid statement in do block
            This is probably a bug, or a missing error message.
            Please consider reporting at
            https://github.com/idris-lang/Idris-dev/issues

New message:

    > :t do
    (input):1:6: error: unexpected
        EOF, expected: ")",
        do block expression,
        end of "do", start of block
    :t do<EOF>
No longer show __infer in pretty-printed errors

__infer is an implementation detail and shouldn't leak. Fixes #1626.

Old error:

    > a
    (input):1:1:When elaborating an application of constructor __infer:
            No such variable a

New error:

    > a
    (input):1:1:No such variable a
Merge pull request #1659 from edwinb/partial-eval

More partial evaluation goodness
Merge pull request #1658 from david-christiansen/todo-removal

Removal of minor TODOs
Merge pull request #1660 from david-christiansen/issue/1656

Make do blocks require an expression
Merge pull request #1661 from david-christiansen/issue/1626

No longer show __infer in pretty-printed errors
Propagate static flags into with blocks

Need this to properly specialise functions generated using 'with',
otherwise the with blocks get left alone.
Merge branch 'master' of github.com:edwinb/Idris-dev
Merge branch 'partial-eval'