TODO 3.3 KB
Newer Older
charguer's avatar
charguer committed
1
2
3
4
5
6
7
8
9
10
11
- xif sans argument pour pouvoir le forcer

- xlet_keep 
		let H := cfml_get_precondition tt in
		xlet (... \*+ H)

- "xapp as x"  pratique sur xlet
- "xapps as x"  pratique sur xlet

- xlet Q => xif Q mais avec branche

POTTIER Francois's avatar
POTTIER Francois committed
12

charguer's avatar
charguer committed
13
14
MAJOR TODAY

charguer's avatar
xwhile    
charguer committed
15

charguer's avatar
cp    
charguer committed
16
- rename xextract to xpull;  and xgen to xpush.
charguer's avatar
xwhile    
charguer committed
17

charguer's avatar
charguer committed
18
19
- Sys.max_array_length 

20

charguer's avatar
charguer committed
21
MAJOR NEXT
charguer's avatar
xwhile    
charguer committed
22

charguer's avatar
xfor    
charguer committed
23
24
- xchanges

charguer's avatar
charguer committed
25
- patterns and when clauses
charguer's avatar
charguer committed
26

charguer's avatar
charguer committed
27
- add support for pure records
charguer's avatar
records    
charguer committed
28

charguer's avatar
charguer committed
29
- record with
charguer's avatar
xfor    
charguer committed
30

charguer's avatar
charguer committed
31
32
33
34
- partial/over application

- xabstract => reimplement and rename as xgen

charguer's avatar
cp    
charguer committed
35

charguer's avatar
xgc    
charguer committed
36
MAJOR NEXT NEXT
charguer's avatar
PRE    
charguer committed
37

charguer's avatar
cp    
charguer committed
38
39
40
41
- xwhile: error reporting when arguments don't have the right types.

- eliminate notations for tags

charguer's avatar
xgc    
charguer committed
42
- record single field and array single cell notation
charguer's avatar
charguer committed
43
44
   Notation "x `. f '~>' S" := 
   Notation "x `[ i ] '~>' S" := 
charguer's avatar
charguer committed
45

charguer's avatar
xgc    
charguer committed
46
- realize array specification using single-cell array specifications
charguer's avatar
PRE    
charguer committed
47

charguer's avatar
charguer committed
48
49
- see if we can get rid of make_cmj

charguer's avatar
cp    
charguer committed
50
51
- mutually recursive polymorhpic functions have too many type variables
  quantified: we need one set of fvs for each def in the recursion.
charguer's avatar
PRE    
charguer committed
52
53

MAJOR POSTPONED
charguer's avatar
cp    
charguer committed
54

charguer's avatar
cp    
charguer committed
55
- support char
charguer's avatar
xgc    
charguer committed
56
57
58
- support float

- implement the work around for type abbreviations:
charguer's avatar
charguer committed
59
60
   type typerecb1 = | Typerecb_1 of typerecb2
    and typerecb2 = typerecb1 list
charguer's avatar
PRE    
charguer committed
61

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

charguer's avatar
charguer committed
64
65
- 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
66

charguer's avatar
charguer committed
67

charguer's avatar
charguer committed
68
69
70
- mutual recursive definitions, polymophic type variables should be more precise


charguer's avatar
charguer committed
71
72
##################################################################
# FUTURE WORK
charguer's avatar
charguer committed
73

74

charguer's avatar
charguer committed
75
OTHER LANGUAGES
76

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

charguer's avatar
charguer committed
79
- support null pointers
charguer's avatar
fixes    
charguer committed
80

charguer's avatar
charguer committed
81

charguer's avatar
charguer committed
82
CODE BEAUTIFY
charguer's avatar
cp    
charguer committed
83

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

charguer's avatar
charguer committed
87
- make sure that check_var is called where needed 
charguer's avatar
cp    
charguer committed
88

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

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

charguer's avatar
charguer committed
93
94
- Ltac xcf_core tt  
  should be able to test whether Spec is a top val, and then do rewrite.
charguer's avatar
charguer committed
95
96


charguer's avatar
charguer committed
97
MAKEFILE BEAUTIFY
charguer's avatar
charguer committed
98

charguer's avatar
charguer committed
99
100
101
- no longer rely on myocamldep

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

charguer's avatar
charguer committed
103
- In the makefile.Coq, when building the .vq and obtaining
charguer's avatar
charguer committed
104
    "Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
charguer's avatar
charguer committed
105
106
107
  => 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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131


##################################################################
# 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.