TODO 1.71 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 7 8 9
System F demo:
  remove TyMu, or handle properly.
  add TyExists.
  Test?

POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
10 11 12
Relax ba so as to not require well-formedness?
  Define wf separately, relying on ba_wf internally.
Global uniqueness, or uniqueness along a branch?
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
13
  Which wf criterion do we want? both?
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
14

POTTIER Francois's avatar
POTTIER Francois committed
15 16
Implement a subst that does not copy the grafted term?
Or parameterize subst over the copy operation that needs to be performed when grafting?
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
17 18

Implement fused copy/subst, fused avoid/subst?
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
19 20
  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
21

POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
22 23
Test avoid.

POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
24 25 26 27 28 29
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
30 31 32 33 34 35 36 37
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
38
Document the precondition and postcondition of every function.
POTTIER Francois's avatar
POTTIER Francois committed
39 40

Deal with more complex forms of binding.
POTTIER Francois's avatar
TODO.  
POTTIER Francois committed
41 42 43
  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
POTTIER Francois's avatar
POTTIER Francois committed
44 45 46 47 48 49 50 51 52 53 54

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