TODO 1.94 KB
Newer Older
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
1 2 3 4 5 6 7
Implement avoid, which renames the bound names of a term so as to
avoid a certain set of names.

Implement fused copy/subst, fused avoid/subst?
  Implement a kit that composes two kits, so as to easily
  implement fused operations.

POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
8 9 10 11 12 13
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?

POTTIER Francois's avatar
POTTIER Francois committed
14
If TVar is a constructor of some type other than term
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
15
  (e.g. value: one substitutes values for variables in terms)
POTTIER Francois's avatar
POTTIER Francois committed
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 47 48 49 50 51 52 53 54 55 56 57 58 59
  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.

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

TODO (POSSIBLY):

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.