TODO 2.11 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 6
In BindingForms, implement iter2 directly instead of via reduce2.

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

POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
10
demos/system-F-type:
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
11
  add TyExists.
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
12 13 14 15
  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
16

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

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

Deal with more complex forms of binding.
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
46 47 48
  How do we deal with forms where a name can have several binding occurrences?
  e.g., or-patterns, join-calculus
  let, let rec, multiple let, multiple let rec, telescopes
49
  What about the distinction between expression types and pattern types?
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
50
  Term mode versus pattern mode in Unbound.
POTTIER Francois's avatar
POTTIER Francois committed
51 52 53 54 55 56 57 58 59 60 61

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):
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
62

POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
63 64
Change all of the macros to build objects on the fly instead of using classes?

POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
65 66 67
Avoid reduce, which is not tail recursive.
  Use iter in [ba] and [fa].
  That should save a constant factor in stack usage?