Implement A-normalization

This also implements a check to see if an expression is atomic. This is in a
separate module to be reused inside BetaReduction.
Clarify comment
Reuse IsAtomic inside BetaReduction
Start adding untyped lets
Add Bacchus.scala for convenient testing

This class contains all Bacchus dependencies, so it's much easier to use for
testing.
Scala Worksheet for testing A-normalization

This is still affected by
https://github.com/scala-ide/scala-worksheet/issues/185
Split UntypedSyntax out of Inference
Type inference: refactor/fix substitution on TVar

The current substitution would duplicate the handling for type variables
and not recurse into other types, which is bad.

In the context of type inference, triggering this bug is
impossible (because variable are typed by collectConstraints(UAbs) with
either type variables or type annotations, which do not contain type
variables since in practice never use them in client programs. But this
seems fragile, so let's fix it anyway.
Change prefix for vars generated by A-normalization
Move dangerous implicit conv. out of Inference

You don't want an implicit conversion in scope inside its own
implementation. In particular, a conversion from UntypedTerm to
TypedTerm is bad while you're writing a (recursive) function with that
type, since you might inadvertently call it on a subterm (which happened
to me).
Inference: cleanup overloads of substitute

* Ensure all "overloads" have the same argument order.
* Avoid actual overloading for coherence. We can't overload these
  methods if we curry them on the second argument, overloading is
  arguably "evil" anyway, so let's just avoid it.
* Inline a trivial overload (on Set[Constraint]) used only once and
  trivial to define with map.
Support Let in untyped language&type inference
ANormalFormTest.sc: misc updates

This does not yet switch yet to using the let-based desugaring of
let(...).
ANormalFormTest.sc: Switch to Let-based desugaring

This way, calls to let produce ULet nodes rather than their desugaring;
let nodes are preserved by type inference (by converting them down to
Let nodes).
Map-based A-normalization/CSE

Tillmann suggested this, and it was easy. It seems a small change might
implement CSE.
Deal a bit with name clashes

This is needed to mix in ANormalForm with BetaReduction.
Add scalaz
BetaReduction: Improve error message
ANormalFormStateful: switch state to fix all cases

Now this seems to work for all combinations of settings (CSE
enabled/disabled, copy propagation enabled/disabled).

* for CSE, we need to be able to replace existing variables with other
  variables. Hence, thread a substitution map from variables to variables.
* this enables doing copy propagation of atomic terms. Hence, generalize
  the map to be from variables to terms.
* To test CSE, I added a duplicate binding to a test case, and this
  revealed a flaw: the existing map would not preserve both bindings
  with CSE disabled, so we need also a list of bindings to output at the
  end. (In fact, we need this list in alternative to the map, but this
  is not yet in the code).
* All these changes required significant refactorings.
* Update the ANormalFormTest.sc significantly.
ANormalForm: Abstract over state difference

The whole difference between CSE and non-CSE can indeed be encapsulated
by changing the state which is propagated, as done here.

Most of this commit just updates code threading the state and accessing
it.

The nontrivial bit was that CSE does an extra lookup - we ensure this
always fails in the non-CSE case.

This avoids giving the state a conditional type (with a Map interface in
one case, and without this interface in the other).

This commits also avoids representing and updating both kinds of
state (as done before).