TODO 1.52 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
If TVar is a constructor of some type other than term
  (e.g. value: one substitues values for variables in terms)
  then Toolbox must be adapted.

Check that every module has an .mli file, except where that would be too heavy.
The type (_, _) abstraction could be transparent, private, or opaque.

Benchmark fa versus fa' and decide which one to keep.

Possibly cut Toolbox.Make down into several smaller functors.
  At least [subst] should be a separate functor.

Operations on terms:
  simultaneous opening? (nominal)
  conversion from debruijn back to nominal
  a printer for debruijn terms?

-- test for global uniqueness everywhere an environment is extended?

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
  in terms of ownership of atoms.

Deal with more complex forms of binding.

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.



Can we treat 'bn specially so that we do not need to implement visit_'bn?
  Or should we just mark 'bn as [@opaque] so as to get visit_'bn for free? Ugly.

Operations in nominal style, without the GUH.
  Capture-avoiding substitution with freshening of bound names.