TODO 1.95 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4
------------------------------------------------------------------------------

TODO (REALLY):

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

POTTIER Francois's avatar
POTTIER Francois committed
12 13
copy and avoid should use [endo], not [map].

POTTIER Francois's avatar
POTTIER Francois committed
14 15
demos/basic:
  test ParallelRed. (both variants)
POTTIER Francois's avatar
POTTIER Francois committed
16

POTTIER Francois's avatar
POTTIER Francois committed
17
demos/system-F-type:
POTTIER Francois's avatar
POTTIER Francois committed
18
  add TyExists.
POTTIER Francois's avatar
POTTIER Francois committed
19 20 21 22
  Test. (both variants)

demos/system F-type-term:
  deal with both kinds of variables. (One or two namespaces?)
POTTIER Francois's avatar
POTTIER Francois committed
23

POTTIER Francois's avatar
POTTIER Francois committed
24 25 26 27 28 29 30 31
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's avatar
POTTIER Francois committed
32
Implement fused copy/subst, fused avoid/subst?
POTTIER Francois's avatar
POTTIER Francois committed
33 34
  Implement a kit that composes two kits, so as to easily implement fused operations.
  Composition of classes? Or composition of kit objects? ...
POTTIER Francois's avatar
POTTIER Francois committed
35

POTTIER Francois's avatar
POTTIER Francois committed
36 37 38 39 40 41
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
42 43 44 45 46 47 48 49
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's avatar
POTTIER Francois committed
50
Document the precondition and postcondition of every function.
POTTIER Francois's avatar
POTTIER Francois committed
51

POTTIER Francois's avatar
POTTIER Francois committed
52 53 54 55 56
------------------------------------------------------------------------------

TODO (POSSIBLY):

Change all of the macros to build objects on the fly instead of using classes?
POTTIER Francois's avatar
POTTIER Francois committed
57 58 59 60 61 62 63

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.