Basic completion now works at REPL and in prover

I've implemented a straightforward completion for the main REPL and the prover. It's not the most sophisticated in the world, but it does do things like completing :l with filenames and :t with expressions. Also, in the prover, the local proof context is a source for identifiers for completions.

A part of this work was to completely remove InputT from the Idris stack. Now, it's confined to the areas that actually read input from the user.

Running make relib still works fine.