TODO 6.5 KB
Newer Older
charguer's avatar
charguer committed
1 2 3 4 5 6 7 8

clean up CFAsymptoticsDemos.v



=============


9 10 11 12
opam switch 4.03.0
eval `opam config env`


charguer's avatar
charguer committed
13

charguer's avatar
charguer committed
14 15 16
 (* TODO: why jauto does clearbody? *) 

=============
charguer's avatar
charguer committed
17

charguer's avatar
charguer committed
18
-- lib/stdlib should have make quick target
charguer's avatar
charguer committed
19 20


charguer's avatar
charguer committed
21 22 23 24 25 26 27 28 29 30 31
-- while loop invariant : when b is false, should not prove decrease 
   Lemma xwhile_inv_basic_lemma :
   forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop), 
   forall (F1:~~bool) (F2:~~unit) H,
   wf R ->
   (H ==> (Hexists b X0, I b X0) \* \GC) ->
   (forall b X, F1 (I b X) (fun b' => I b' X)) ->
   (forall X, F2 (I true X) (# Hexists b X', \[b -> R X' X] \* I b X')) -> 
   (While F1 Do F2 Done_) H (# Hexists X, I false X).


charguer's avatar
charguer committed
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
-- xapp as b'

-- xapp on a leaf does not do xpull

-- case_if checking single goal

-- xmatch_no_intros  should do the inversion.

-- improve xauto spec

-- xcf_show without argument should put at head of goal

-- xunfold at fait pas le unfold

-- Ouvrir liblistZ à la fin de cflib

-- Demo de la notation pour les records

-- Array : compléter.

-- LibListZ.sub

-- Array.iter    forall l, Array xs \c I l 

-- renommer Array.of_list

charguer's avatar
charguer committed
58
-- utiliser "of_list []" à la place de make_empty
charguer's avatar
charguer committed
59 60 61 62

-- avoir un flag pour _output

-- external sur une constante, passe pas le typeur
63

charguer's avatar
charguer committed
64
-- documenter la faiblesse de Array.make
charguer's avatar
charguer committed
65

charguer's avatar
charguer committed
66
-- remettre les vrais noms des external
charguer's avatar
charguer committed
67

charguer's avatar
charguer committed
68
-- todo: test xif new variants
charguer's avatar
charguer committed
69

charguer's avatar
charguer committed
70
-- todo: test xand
charguer's avatar
charguer committed
71

charguer's avatar
charguer committed
72
-- xclose with args for the change.
charguer's avatar
charguer committed
73

charguer's avatar
charguer committed
74
-- xsimpl on   I X ==> I Y    produces X = Y.
charguer's avatar
charguer committed
75

charguer's avatar
charguer committed
76
-- xapp_rm
77

charguer's avatar
charguer committed
78
-- generate inhab instance for algebraic
79

charguer's avatar
charguer committed
80
-- hint spec based on type args
81

charguer's avatar
charguer committed
82
-- xchanges
83

charguer's avatar
charguer committed
84
-- implement xpush.
charguer's avatar
charguer committed
85

86 87


charguer's avatar
charguer committed
88 89 90 91 92
(* TODO / FIX
Open Scope set_scope.
Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
 (at level 0, x ident, A at level 0, P at level 200) : set_scope.
*)
POTTIER Francois's avatar
POTTIER Francois committed
93

charguer's avatar
charguer committed
94

charguer's avatar
charguer committed
95
----
charguer's avatar
charguer committed
96 97
MAJOR TODAY

charguer's avatar
charguer committed
98
----
charguer's avatar
charguer committed
99
MAJOR NEXT
charguer's avatar
charguer committed
100

charguer's avatar
charguer committed
101
- record with imperative
charguer's avatar
charguer committed
102

charguer's avatar
charguer committed
103
- partial/over application
104

charguer's avatar
charguer committed
105 106
- "xapp as x"  pratique sur xlet
  "xapps as x"  pratique sur xlet
charguer's avatar
charguer committed
107

charguer's avatar
charguer committed
108
- Sys.max_array_length  discuss with francois
charguer's avatar
charguer committed
109

charguer's avatar
charguer committed
110
- patterns and when clauses
charguer's avatar
charguer committed
111

charguer's avatar
charguer committed
112
- add support for pure records
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
     Record 'A T := T_intro { f' : T1; .. }

	  if mutually recursive, encode record def using 
		
		Ind 'A T := T_intro : T1 -> ... -> 'A T
		
		Implicit Types T ['A]

		Def f' 'A (p:'A T) :=
		  match p with T_intro x1 .. xN => xi end

	alloc: (T_intro v1 .. vN : typ)
	set : impossible
	with : match r with T_intro x1 .. xN => T_intro x1 .. yI .. xN
	  => requires the order of labels to be fixed as in the definition.
charguer's avatar
charguer committed
128

charguer's avatar
charguer committed
129
----
charguer's avatar
charguer committed
130
MAJOR NEXT NEXT
charguer's avatar
charguer committed
131

charguer's avatar
charguer committed
132 133 134
- xlet_keep 
		let H := cfml_get_precondition tt in
		xlet (... \*+ H)
charguer's avatar
charguer committed
135

charguer's avatar
charguer committed
136
- record single field and array single cell notation
charguer's avatar
charguer committed
137
   Notation "x `. f '~>' S" := 
138 139 140 141
   Notation "x `[ i ] '~>' S" :=
	
	t ~> Array L= t ~> Arraylen n * exists G, Groupof Cell G
	    dom G = [0,n] * lenght L = n * forall i indom G, L[i] = G[i]
charguer's avatar
charguer committed
142

charguer's avatar
charguer committed
143
- realize array specification using single-cell array specifications
charguer's avatar
charguer committed
144

charguer's avatar
charguer committed
145 146
- see if we can get rid of make_cmj, using -only-cmj 
  => make_cmj seems to already be never used.
147

charguer's avatar
charguer committed
148 149
-- xwhile: error reporting when arguments don't have the right types.

150

charguer's avatar
charguer committed
151
----
charguer's avatar
charguer committed
152
MAJOR POSTPONED
charguer's avatar
charguer committed
153

charguer's avatar
charguer committed
154
- support char, string, float
charguer's avatar
charguer committed
155 156

- implement the work around for type abbreviations:
charguer's avatar
charguer committed
157 158
   type typerecb1 = | Typerecb_1 of typerecb2
    and typerecb2 = typerecb1 list
charguer's avatar
charguer committed
159

charguer's avatar
charguer committed
160
- would it be better to perform all renaming during normalization phase?
charguer's avatar
charguer committed
161

charguer's avatar
charguer committed
162 163
- 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
164

charguer's avatar
charguer committed
165 166 167
- mutual recursive definitions, polymophic type variables should be more precise


charguer's avatar
charguer committed
168 169
##################################################################
# FUTURE WORK
charguer's avatar
charguer committed
170

171

charguer's avatar
charguer committed
172
OTHER LANGUAGES
173

charguer's avatar
charguer committed
174
- semantics for records|arrays  passed by value / passed by reference
charguer's avatar
charguer committed
175

charguer's avatar
charguer committed
176
- support null pointers
charguer's avatar
charguer committed
177

charguer's avatar
charguer committed
178

charguer's avatar
charguer committed
179
CODE BEAUTIFY
charguer's avatar
charguer committed
180

charguer's avatar
charguer committed
181 182 183
- better error message when calling [xapp] on a record application 
  in which the record is not unfocused.

charguer's avatar
charguer committed
184
- make sure that check_var is called where needed 
charguer's avatar
charguer committed
185

charguer's avatar
charguer committed
186
- unify the source code in main.ml and makecmj.ml
charguer's avatar
charguer committed
187

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

charguer's avatar
charguer committed
190 191
- Ltac xcf_core tt  
  should be able to test whether Spec is a top val, and then do rewrite.
charguer's avatar
charguer committed
192 193


charguer's avatar
charguer committed
194
MAKEFILE BEAUTIFY
charguer's avatar
charguer committed
195

charguer's avatar
charguer committed
196 197 198
- no longer rely on myocamldep

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

charguer's avatar
charguer committed
200
- In the makefile.Coq, when building the .vq and obtaining
charguer's avatar
charguer committed
201
    "Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
charguer's avatar
charguer committed
202 203 204
  => 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
205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228


##################################################################
# 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.
229 230 231



charguer's avatar
charguer committed
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315
##############################################


Regarding compilation speeed, I confirm that v8.6 is a little bit
faster than v8.5, typically around 10% faster for my scripts,
and sometimes up to 25%, depending on the file. Details follow.


=======================================================

sequential = make -j 1, to create vo in order
interfaces = make -j 4, to create vio only
parallel   = make -j 4, to create vio, and compile them independently

---------------
TLC, sequential
v8.5:
	real	1m23.587s
	user	1m18.128s
	sys	0m5.120s
v8.6:
	real	1m19.624s
	user	1m14.688s
	sys	0m4.611s

---------------
TLC, interfaces 
v8.5:
	real	0m24.113s
	user	0m47.835s
	sys	0m8.872s
v8.6:
	real	0m22.603s
	user	0m46.138s
	sys	0m8.494s

---------------
TLC, parallel 
v8.5:
	real	1m15.226s
	user	4m5.916s
	sys	0m24.104s
v8.6:
	real	1m22.035s
	user	4m12.348s
	sys	0m24.212s

---------------
LN, parallel
v8.5:
	real	0m53.184s
	user	2m38.325s
	sys	0m19.126s
v8.6:
	real	0m48.436s
	user	2m21.484s
	sys	0m18.841s

---------------
CFML(lib), sequential
v8.5:
	real	0m26.864s
	user	0m25.191s
	sys	0m1.620s
v8.6:
	real	0m21.157s
	user	0m19.611s
	sys	0m1.482s

=======================================================




##############################################