TODO 1.13 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


sémantique
----------
10

Andrei Paskevich's avatar
Andrei Paskevich committed
11 12 13
  - 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
14 15
  - should split_goal provide a "right-hand side only split"?

16 17 18 19 20
  - 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
21 22
    since the key is the value. Should we use generation numbers in arguments
    and results of transformations?
23

Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
24 25
  - 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
26 27 28 29

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

30 31 32 33 34 35
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)