Add extended environment, support for typechecking and evaluating decls

This is a checkpoint; it builds but doesn't yet work correctly!
initial :let implementation

This works by adding an extended environment to some of the
ModuleSystem functions. This extended environment contains
declarations entered interactively, a naming environment that maps
parsed names to the unique names we use to ensure lexical scope, and
an evaluation environment containing the values of the let-bound
expressions.
additional support for let-bound variables at the repl

Let-bound identifiers now show up in `:browse`, get unloaded whenever
we load a new module context, and can be sent to `:sat` and `:prove`.
getVars processes interactively-bound names better

This change fixes the issue where `getVars` in the REPL would return
names with the `#Uniq_...` prefix. This was confusing, and also
messing up tab-completion.
refactor dynamic environment into ModuleEnv

This just makes for a more consistent API; the "dynamic" environment
as extended by REPL commands is now part of the ModuleEnv. It's
actually more general than just for the REPL. We can use it in general
to add bindings on top of a loaded module context.
added `it` to the REPL
restricted grammar of :let commands

For now, you can only enter one binding at a time at the REPL, and can
only enter expression bindings rather than type signatures or type
synonyms. It wouldn't be too hard to add type synonyms, but the value
is questionable.
change repl syntax to be more like ghci

Since :let was clashing with :load for :l, and for consistency with
ghci, you can now enter bare let expressions at the repl:

> let x = 5

Also, the grammar for the repl parser disallows type bindings, which
were possible in the previous :let.

Semicolons no longer needed, though we can only bind one thing at a
time.
bind counterexamples and satisfying assignments to `it`

If the solver returns values for :sat or :prove, we now bind them at
the repl to `it`. If more than one argument is part of the cex/sat
answer, we tuple up/uncurry the arguments.
Merge branch 'master' into feature/repl-bindings

Conflicts:
	cryptol/REPL/Command.hs
	src/Cryptol/Symbolic.hs

Fixed up Value -> Expr conversion to account for a change in those
types. Reworked sat and prove results to account for changes in that
API.
bind `it` even when no counterexample/sat is available; add tests

Similar to what @weaversa requested in #66, we bind `it` to `False`
when we can't find a sat assignment, and `it` to `True` when we've
proved a theorem.

Also adds some simple tests for the sat/prove result binding, and let
binding at the repl.
Merge branch 'feature/repl-bindings'