TreeMaker approximation refactorings and bug fixes

- TypeTestTreeMaker subsumes the old TypeTestTM and TypeAndEqualityTM
  its type- and equality-testing logic is configurable so that it can:
    - generate trees (main purpose)
    - check whether this tree maker is a pure type test
    - generate the proposition that models this tree maker
      (for exhaustivity and other analyses)

- [CSE] subst binders of dropped tm's to stored ones
  somehow the refactoring broke the replacement of the binder of dropped
  treemakers by the binder of the reused treemaker

  when replacing

  TM1(x1 => ...) >> TM2(x2 => ...) >> TM3(x3 => ...) >>  ...
  TM1'(x1' => ...) >> TM2'(x2' => ...) >> TM3(x3' => ...) >> ...

  by

  Memo1(x1 => ...) >> TM2(x2 => ...) >> Memo2(x3 => ...) >>  ...
  Reuse(Memo2)...

  you need to replace x1' and x2' by x1

  since TM2 tested a shared condition but was not memo-ised,
  that implies it simply passed x1 through to x3 unmodified,
  and x2' can simply use the stored x1

- type of first uniqued binder sets type of tree
  when approximating a tree of treemakers as a DAG,
  where sharing indicates the same value is tested,
  use the type of the binder that was first used to
  create a unique tree as the type of that tree,
  and thus all trees used for the same binder in the future

- track substitution of alternatives when approximating

- error on unswitchable @switch annotated matches
  if we can't turn a match (with more than two cases) into a switch,
  but the user insists, emit an error

misc notes:
- when all you need is nextBinder, FunTreeMaker is your guy
- must pass flag to TypeTestTM for extractorarg test
  case TypeTestTreeMaker(prevBinder, testedBinder, expectedTp, nextBinderTp)
  (prevBinder eq testedBinder) does not imply it's a pure type test for an extractor call
  note that the expected type for an extractor argument is not a type pattern,
  thus we only do a classic type test -- the idea was to detect that case by noticing we're
  being called with the same previous and tested binder, but that case also arises
  for Typed patterns

Author: Adriaan Moors