TODO 1.41 KB
Newer Older
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
1 2 3 4 5 6 7 8 9
------------------------------------------------------------------------------

TODO (REALLY):

Relax ba so as to not require well-formedness?
  Define wf separately, relying on ba_wf internally.
Global uniqueness, or uniqueness along a branch?
  Which wf criterion do we want?

POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
10 11 12 13 14 15 16
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
17 18 19 20 21 22
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
23 24 25 26 27 28 29 30 31
Check that every module has an .mli file, except where that would be too heavy.
The type (_, _) abstraction could be transparent, private, or opaque.

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.

POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
32
Document the precondition and postcondition of every function.
POTTIER Francois's avatar
POTTIER Francois committed
33 34 35 36 37 38 39 40 41 42 43 44 45

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):