TODO 3.2 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1

charguer's avatar
charguer committed
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
MAJOR TODAY


let f () =
  let r : '_a ref = ref [] in
  !r

let f () =
  let r : int ref = ref [] in
  !r

let f () : 'a list =
  let r : 'a ref = ref [] in
  !r

charguer's avatar
docgen  
charguer committed
17

charguer's avatar
tuto  
charguer committed
18

charguer's avatar
charguer committed
19
xwhile: error reporting when arguments don't have the right types.
charguer's avatar
xwhile  
charguer committed
20 21 22

rename xextract to xpull;  and xgen to xpush.

charguer's avatar
charguer committed
23
infix_eq_
charguer's avatar
xwhile  
charguer committed
24 25 26
   comparable_type A || comparable_value x || comparable_value y
   x = y : A
  
charguer's avatar
charguer committed
27
   comparable_value x || comparable_value y
charguer's avatar
xwhile  
charguer committed
28 29 30 31 32
   x = y : A

  forall x : int, comparable_value x


charguer's avatar
charguer committed
33
- record with
charguer's avatar
xwhile  
charguer committed
34

charguer's avatar
charguer committed
35
- when clauses
36

charguer's avatar
charguer committed
37
- open no scope in CF.
charguer's avatar
PRE  
charguer committed
38

charguer's avatar
charguer committed
39
- add support for pure records
charguer's avatar
xwhile  
charguer committed
40

charguer's avatar
xfor  
charguer committed
41 42 43 44
- inline CFHeader.pred  as -1

- xchanges

charguer's avatar
charguer committed
45

charguer's avatar
records  
charguer committed
46

charguer's avatar
PRE  
charguer committed
47

charguer's avatar
records  
charguer committed
48

charguer's avatar
charguer committed
49
MAJOR NEXT
charguer's avatar
charguer committed
50

charguer's avatar
xfor  
charguer committed
51

charguer's avatar
charguer committed
52 53 54 55 56
- partial/over application

- xabstract => reimplement and rename as xgen

- eliminate notations for tags
charguer's avatar
PRE  
charguer committed
57

charguer's avatar
xgc  
charguer committed
58
MAJOR NEXT NEXT
charguer's avatar
PRE  
charguer committed
59

charguer's avatar
xgc  
charguer committed
60
- record single field and array single cell notation
charguer's avatar
charguer committed
61 62
   Notation "x `. f '~>' S" := 
   Notation "x `[ i ] '~>' S" := 
charguer's avatar
charguer committed
63

charguer's avatar
xgc  
charguer committed
64
- realize array specification using single-cell array specifications
charguer's avatar
PRE  
charguer committed
65

charguer's avatar
charguer committed
66 67
- see if we can get rid of make_cmj

charguer's avatar
PRE  
charguer committed
68 69

MAJOR POSTPONED
charguer's avatar
cp  
charguer committed
70

charguer's avatar
xgc  
charguer committed
71 72 73
- support float

- implement the work around for type abbreviations:
charguer's avatar
charguer committed
74 75
   type typerecb1 = | Typerecb_1 of typerecb2
    and typerecb2 = typerecb1 list
charguer's avatar
PRE  
charguer committed
76

charguer's avatar
charguer committed
77
- would it be better to perform all renaming during normalization phase?
charguer's avatar
PRE  
charguer committed
78

charguer's avatar
charguer committed
79 80
- have a flag to control whether functions such as "min", "max", "abs", etc.. 
  should be systematically let-bound; this would allow binding these names.
charguer's avatar
charguer committed
81

charguer's avatar
charguer committed
82

charguer's avatar
charguer committed
83 84
##################################################################
# FUTURE WORK
charguer's avatar
charguer committed
85

86

charguer's avatar
charguer committed
87
OTHER LANGUAGES
88

charguer's avatar
charguer committed
89
- semantics for records|arrays  passed by value / passed by reference
charguer's avatar
fixes  
charguer committed
90

charguer's avatar
charguer committed
91
- support null pointers
charguer's avatar
fixes  
charguer committed
92

charguer's avatar
charguer committed
93

charguer's avatar
charguer committed
94
CODE BEAUTIFY
charguer's avatar
cp  
charguer committed
95

charguer's avatar
xfocus  
charguer committed
96 97 98
- better error message when calling [xapp] on a record application 
  in which the record is not unfocused.

charguer's avatar
charguer committed
99
- make sure that check_var is called where needed 
charguer's avatar
cp  
charguer committed
100

charguer's avatar
charguer committed
101
- unify the source code in main.ml and makecmj.ml
charguer's avatar
cp  
charguer committed
102

charguer's avatar
charguer committed
103
- check that there are no uses of labels in input source files
charguer's avatar
charguer committed
104

charguer's avatar
charguer committed
105 106
- Ltac xcf_core tt  
  should be able to test whether Spec is a top val, and then do rewrite.
charguer's avatar
charguer committed
107 108


charguer's avatar
charguer committed
109
MAKEFILE BEAUTIFY
charguer's avatar
charguer committed
110

charguer's avatar
charguer committed
111 112 113
- no longer rely on myocamldep

- make systematic use of    || (rm -f $@; exit 1)   in cfml calls
charguer's avatar
charguer committed
114

charguer's avatar
charguer committed
115
- In the makefile.Coq, when building the .vq and obtaining
charguer's avatar
charguer committed
116
    "Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
charguer's avatar
charguer committed
117 118 119
  => then delete the .vio file
    (useful for compilations interrupted using CTRL+C)
  => even better, wrap "coqc -quick" with an atomic commit of its result.
charguer's avatar
charguer committed
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143


##################################################################
# PROPOSAL FOR DEFENSIVE CODE

  - VStack.ml  contains a verified stack implemementation using CFML.
    (not polluted by any runtime checks).

  - SStack.ml  is a wrapper for VStack which adds asserts; 
    e.g.    let pop s = assert (!s <> nil); VStack.pop s

  - The file SStack.ml is processed using a special mode of CFML,
    in which "assert t" is interpreted as "t needs to run safely
    and produce some boolean; and the rest of the code may
    assume this boolean to be true". Formally:

        (Assert F) H Q := 
          exists (P:Prop),
            (F H (fun (b:bool) => [b = true <-> P] \* H)) 
          /\ (H \* [P] ==> Q tt)

    During the proof, the user needs to provide the proposition
	 [P] that is tested by the assertion. This proposition can
	 be assumed to be true after the assert is executed.