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

TODO (REALLY):

POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
5
In BindingFormsUnbound, implement [endo] and [iter2].
POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
6

POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
7
8
copy and avoid should use [endo], not [map].

POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
9
10
demos/basic:
  test ParallelRed. (both variants)
POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
11

POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
12
demos/system-F-type:
POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
13
  add TyExists.
POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
14
15
16
17
  Test. (both variants)

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

POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
19
20
21
22
23
24
25
26
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
TODO.    
POTTIER Francois committed
27
Implement fused copy/subst, fused avoid/subst?
POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
28
29
  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
TODO.    
POTTIER Francois committed
30

POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
31
32
33
34
35
36
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
37
38
39
40
41
42
43
44
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
TODO.    
POTTIER Francois committed
45
Document the precondition and postcondition of every function.
POTTIER Francois's avatar
POTTIER Francois committed
46

POTTIER Francois's avatar
TODO.    
POTTIER Francois committed
47
48
49
50
51
------------------------------------------------------------------------------

TODO (POSSIBLY):

Change all of the macros to build objects on the fly instead of using classes?
POTTIER Francois's avatar
POTTIER Francois committed
52
53
54
55
56
57
58

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.