TODO 1.29 KB
Newer Older
1 2 3 4

syntaxe
-------

5
  - open
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
6

7 8 9 10 11 12 13 14
  - infix symbols as constructors, e.g.

       type list 'a = Nil | (::) 'a (list 'a)

  - constants in patterns, e.g.

       match ... with 0 :: r -> ... | ...

Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
15 16 17

sémantique
----------
18

Andrei Paskevich's avatar
Andrei Paskevich committed
19 20 21
  - env should not contain theories under the null path. 
    The current implementation of Typing.find_theory is potentially broken.

Andrei Paskevich's avatar
Andrei Paskevich committed
22 23
  - should split_goal provide a "right-hand side only split"?

24 25 26 27 28
  - produce reparsable tasks in Why3 format: how to preserve information about
    the origins of symbols to be able to use drivers after reparsing?

  - weak memoization in transformations has a disadvantage: if a task or a decl
    is not changed by a transformation, it will stay in the hash table forever,
Andrei Paskevich's avatar
Andrei Paskevich committed
29 30
    since the key is the value. Should we use generation numbers in arguments
    and results of transformations?
31

Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
32 33
  - uses : pour l'instant, l'ordre des théories dans le fichier est important 
    i.e. les théories mentionnées par uses doivent être définies précédemment
34 35 36 37

  - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole 
    de même nom)

38 39 40 41 42 43
error reporting
---------------

  - should we create a common [exception Why.Error of exn] to facilitate
    integration of the library? This would require a special [raise] call:
        why_raise e = raise (Why.Error e)