TODO 2.12 KB
Newer Older
POTTIER Francois committed
1 2 3 4
------------------------------------------------------------------------------

TODO (REALLY):

POTTIER Francois committed
5
Continue work on BindingFormsUnbound or BindingCombinators.
POTTIER Francois committed
6 7
Think about other approaches to Rec:
- using laziness combined with mutability? might allow a single traversal.
POTTIER Francois committed
8
- offering DefRec(p, t) as a primitive combinator?
POTTIER Francois committed
9
Think about other approaches to repeated names.
POTTIER Francois committed
10 11

If the [lookup] method is no longer used, remove it from all kits.
POTTIER Francois committed
12

POTTIER Francois committed
13 14
copy and avoid should use [endo], not [map].

POTTIER Francois committed
15 16
demos/basic:
  test ParallelRed. (both variants)
POTTIER Francois committed
17 18
  implement conversion from de bruijn to nominal,
  test the round-trip properties.
POTTIER Francois committed
19

POTTIER Francois committed
20
demos/system-F-type:
POTTIER Francois committed
21
  add TyExists.
POTTIER Francois committed
22 23
  Test. (both variants)

POTTIER Francois committed
24 25 26
demos/advanced:
  make sure that the operations seem to work.

POTTIER Francois committed
27 28
demos/system F-type-term:
  deal with both kinds of variables. (One or two namespaces?)
POTTIER Francois committed
29

POTTIER Francois committed
30 31 32 33 34 35 36 37
Implement an alpha-respecting comparison, following Unbound.
  Just convert to locally nameless on the fly, followed with
  a lexicographic comparison.

Simultaneous unbinding.

LFresh monad. (Locally fresh names, for better printing.)

POTTIER Francois committed
38
Implement fused copy/subst, fused avoid/subst?
POTTIER Francois committed
39 40
  Implement a kit that composes two kits, so as to easily implement fused operations.
  Composition of classes? Or composition of kit objects? ...
POTTIER Francois committed
41

POTTIER Francois committed
42 43 44 45 46 47
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 committed
48 49 50 51 52 53 54 55
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.

POTTIER Francois committed
56
Document the precondition and postcondition of every function.
POTTIER Francois committed
57

POTTIER Francois committed
58 59 60 61 62
------------------------------------------------------------------------------

TODO (POSSIBLY):

Change all of the macros to build objects on the fly instead of using classes?
POTTIER Francois committed
63 64 65 66 67 68 69

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.