TODO 1.89 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 32 33 34
     François -- I don't get that point the weak Hashtbl that we use
   are designed to work on this case, even with the identity function.
   What we should do is a way to remove the task from a session when
   they are not needed anymore.
35

Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
36 37
  - 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
38 39 40 41

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

42 43 44 45 46 47
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)
48 49 50 51 52 53 54 55 56 57 58 59 60 61

session
-------
  - save the output of the prover
  - escape the string in the xml

tools
-----

  - the tools should verify that the provers have the same version
   than reported in the configuration
  - Maybe : make something generic for the dialog box with memory.
  - autodetection can be modified now that only name/version/altern
   are taken into account in session.