src/Idris/ParseHelpers.hs: workaround build failure against ghc-7.8

> [50 of 75] Compiling Idris.ParseHelpers ( src/Idris/ParseHelpers.hs, dist/build/Idris/ParseHelpers.o )
>
> src/Idris/ParseHelpers.hs:40:97:
>     Could not coerce from ‘Monad Parser’ to ‘Monad IdrisInnerParser’
>       because the first type argument of ‘Monad’ has role Nominal,
>       but the arguments ‘Parser’ and ‘IdrisInnerParser’ differ
>       arising from the coercion of the method ‘notFollowedBy’ from type
>                    ‘forall a. (Monad Parser, Show a) => Parser a -> Parser ()’ to type
>                    ‘forall a.
>                     (Monad IdrisInnerParser, Show a) =>
>                     IdrisInnerParser a -> IdrisInnerParser ()’
>     Possible fix:
>       use a standalone 'deriving instance' declaration,
>         so you can specify the instance context yourself
>     When deriving the instance for (Parsing IdrisInnerParser)

I'm not sure if it's a ghc-7.8.1-rc2 bug or feature.
Looks like standalone deriving does not try to infer (too tight) context.

Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org>
Add support for reflecting ByReflection
Allow users to disable the auto-solve in the prover

Use :set autosolve and :unset autosolve to do this.
Rename 'new' to 'newInit' in neweffects

Also, updated version of 'new' which takes a default resource, now
corresponding to run/runInit and runPure/runPureInit.
Skip unnecessary coverage checking

If the last clause in a definition contains only _, we don't need to
coverage check it. This vastly, vastly improves the speed of this defn:

fourTupleElems : TT -> Maybe (TT, (TT, (TT, TT)))
fourTupleElems (App (App (App (App p ty1) ty2) tm1)
                (App (App (App (App p ty3) ty4) tm2)
                 (App (App (App (App p ty1) ty2) tm3) tm4))) = Just (tm1, tm2, tm3, tm4)
fourTupleElems _ = Nothing
Skip unnecessary coverage checking

If the last clause in a definition contains only _, we don't need to
coverage check it. This vastly, vastly improves the speed of this defn:

fourTupleElems : TT -> Maybe (TT, (TT, (TT, TT)))
fourTupleElems (App (App (App (App p ty1) ty2) tm1)
                (App (App (App (App p ty3) ty4) tm2)
                 (App (App (App (App p ty1) ty2) tm3) tm4))) = Just (tm1, tm2, tm3, tm4)
fourTupleElems _ = Nothing
Syntax for failures  in pattern matching let/<-

  let pat = val | <alternatives> in x'

...becomes...

  case val of
       pat => x'
       <alternatives>

  do pat <- val | <alternatives>
     p

...becomes...

  do x <- val
     case x of
          pat => p
          <alternatives>

So in particular, large effectful functions can deal with failure inline
rather than having lots of nested case blocks, e.g.

main : IO ()
main = do [p, a] <- getArgs
                      | [p] => putStrLn "No arguments!"
                      | (x :: y :: _) => putStrLn "Too many arguments!"
          print (foo (Just (cast a)))
javascript: add time function
javascript: quick & dirty compile time error on invalid FFI
Use Markdown to represent docstrings

We now use the Cheapskate library to process Markdown, but the
dependency is as encapsulated as possible in case we need a different
library in the future.

Remaining:
 1. Rendering of code blocks with syntax highlighting
 2. IDESlave annotation and console font support for things like *bold*
 3. Support for considering the first block-level element to be a
    summary of the docs
Merge pull request #946 from trofi/master

src/Idris/ParseHelpers.hs: workaround build failure against ghc-7.8
Merge pull request #958 from david-christiansen/reflection-reflection

Proof automation improvements
Merge pull request #960 from david-christiansen/skip-coverage-on-default-pattern

Skip obviously  unnecessary coverage checking
Merge pull request #961 from raichoo/javascript

Javascript
Merge pull request #962 from david-christiansen/markdown-docs

Markdown syntax for documenation strings
Merge remote-tracking branch 'upstream/master'