TODO 2.37 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
WhyML
-----

  - should the API ensure that every psymbol resets the new regions?
    Should they be always reset at the last arrow? What if they are
    already reset at some earlier arrows, should we reset them again?

  - in "val" and "any", when a region rho is written into, but some
    subregion rho' of rho is not, should we reset rho' under rho?
    In Mlw_typing or in Mlw_expr?

12 13 14 15

syntaxe
-------

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

18 19 20 21 22 23 24 25
  - 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
26

27
sémantique
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
28
----------
29

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

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

35 36 37 38 39
  - 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
40 41
    since the key is the value. Should we use generation numbers in arguments
    and results of transformations?
42
     François -- I don't get that point the weak Hashtbl that we use
43 44 45
   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.
46

47 48
  - 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
49

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

53 54 55 56 57 58
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)
59 60 61 62 63

session
-------
  - save the output of the prover
  - escape the string in the xml
François Bobot's avatar
François Bobot committed
64 65
  - the filenames in the location inside a session should be relative
   to the session_dir.
66 67 68 69 70 71 72 73

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
74
   are taken into account in session.