TODO

------------------------------------------------------------------------------

TODO (REALLY):

Careful:
  avoid reduce, which is not tail recursive
    e.g. in [ba] and [fa]

System F demo:
  remove TyMu, or handle properly.
  add TyExists.
  Test?
System F-type-term:
  deal with both kinds of variables

Implement avoids. (Test for no-shadowing.)

Implement a subst that does not copy the grafted term?
Or parameterize subst over the copy operation that needs to be performed when grafting?

Implement fused copy/subst, fused avoid/subst?
  Implement a kit that composes two kits, so as to easily implement fused operations.
  Composition of classes? Or composition of kit objects? ...

Test avoid.

Suppose I want to annotate every abstraction with its fa.
Or, suppose I want to annotate every abstraction with the
  number of uses of the bound name.
Can I easily do it?
Need a map_reduce visitor?

Check that every module has an .mli file, except where that would be too heavy.

Operations on each kind of environment:
  Entering a binder (and testing for global uniqueness).

Add printers for Atom.Map
and possibly the various kinds of environments that we use.

Document the precondition and postcondition of every function.

Deal with more complex forms of binding.
  How do we deal with forms where a name can have several binding occurrences?
  e.g., or-patterns, join-calculus
  let, let rec, multiple let, multiple let rec, telescopes
  What about the distinction between expression types and pattern types?

Try dealing with binding and hash-consing at the same time.

Try dealing with suspended substitutions.
  (As a distinct construct. Not necessarily at abstractions.)

Look at the visitors in Why3.

------------------------------------------------------------------------------

TODO (POSSIBLY):