Changeset 24 for Csemantics/Globalenvs.ma
 Timestamp:
 Aug 27, 2010, 1:21:50 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Globalenvs.ma
r3 r24 40 40 41 41 (* FIXME: unimplemented stuff in AST.ma 42 naxiom transform_program: ∀A,B,V:Type. (A → B) → program A V → program B V.43 42 naxiom transform_partial_program: ∀A,B,V:Type. (A → res B) → program A V → res (program B V). 44 43 naxiom transform_partial_program2: ∀A,B,V,W:Type. (A → res B) → (V → res W) → program A V → res (program B W). … … 46 45 *) 47 46 48 nrecord GENV : Type[ 1] ≝ {47 nrecord GENV : Type[2] ≝ { 49 48 (* * ** Types and operations *) 50 49 … … 67 66 a value, which must be a pointer with offset 0. *) 68 67 69 find_symbol: ∀F: Type. genv_t F → ident → option block 68 find_symbol: ∀F: Type. genv_t F → ident → option block; 70 69 (* * Return the address of the given global symbol, if any. *) 71 }. 70 72 71 (* * ** Properties of the operations. *) 73 72 (* … … 143 142 (* * Commutation properties between program transformations 144 143 and operations over global environments. *) 145 144 *)*) 146 145 find_funct_ptr_transf: 147 146 ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V. … … 171 170 ∀v : val. ∀tf : B. 172 171 find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf → 173 ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf ;174 172 ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf 173 (* 175 174 (* * Commutation properties between partial program transformations 176 175 and operations over global environments. *) … … 303 302 init_mem ?? p' = init_mem ?? p*) 304 303 }. 305 *) 304 305 306 nlet rec foldl (A,B:Type) (f:A → B → A) (a:A) (l:list B) on l : A ≝ 307 match l with 308 [ nil ⇒ a 309  cons h t ⇒ foldl A B f (f a h) t 310 ]. 306 311 307 312 (* XXX: temporary definition … … 327 332 (λF,ge,v. match v with [ Vptr b o ⇒ if eq o zero then functions ? ge b else None ?  _ ⇒ None ? ]) (* find_funct *) 328 333 (λF,ge. symbols ? ge) (* find_symbol *) 334 ? 335 ? 336 ? 337 ? 338 ? 339 ? 329 340 . 330 341 ##[ #A B C transf p b f; nelim p; #fns main vars; 342 nelim fns; 343 ##[ nnormalize; #H; ndestruct; 344 ## #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??(??%?)? → ??(??%?)?); 345 nrewrite > (?:nextfunction ?? = length ? t); 346 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; 347 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] 348 ## nrewrite > (?:nextfunction ?? = length ? t); 349 ##[ ##2: nelim t; ##[ //; ## #h t IH; nwhd in ⊢ (??%?); nrewrite > IH; 350 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] 351 ## napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??%?); 352 ##[ #H; ndestruct (H); //; 353 ## #H; napply IH; napply H; 354 ##] 355 ##] 356 ##] 357 ##] 358 ## #A B C transf p v f; nelim v; 359 ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct; 360 ## ##2,3: #x; nwhd in ⊢ (??%? → ??%?); #H; ndestruct; 361 ## #b off; nwhd in ⊢ (??%? → ??%?); nelim (eq off zero); 362 nwhd in ⊢ (??%? → ??%?); 363 ##[ nelim p; #fns main vars; nelim fns; 364 ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct; 365 ## #h t; nelim h; #f fn IH; 366 nwhd in ⊢ (??%? → ??%?); 367 nrewrite > (?:nextfunction ?? = length ? t); 368 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; 369 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] 370 ## nrewrite > (?:nextfunction ?? = length ? t); 371 ##[ ##2: nelim t; ##[ //; ## #h t IH; nwhd in ⊢ (??%?); nrewrite > IH; 372 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] 373 ## napply eqZb_elim; #e; nwhd in ⊢ (??%? → ??%?); #H; 374 ##[ ndestruct (H); //; 375 ## napply IH; napply H; 376 ##] 377 ##] 378 ##] 379 ##] 380 ## #H; ndestruct; 381 ##] 382 ##] 383 ## #A B C transf p id; nelim p; #fns main vars; 384 nelim fns; 385 ##[ nnormalize; // 386 ## #h t; nelim h; #fid fd; nwhd in ⊢ (??%% → ??%%); #IH; 387 nelim (ident_eq fid id); #e; 388 ##[ nwhd in ⊢ (??%%); 389 nrewrite > (?:nextfunction ?? = length ? t); 390 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; 391 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] 392 ## nrewrite > (?:nextfunction ?? = length ? t); 393 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; 394 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] 395 ## // 396 ##] 397 ##] 398 ## nwhd in ⊢ (??%%); nrewrite > IH; napply refl; 399 ##] 400 ##] 401 ## //; 402 ## #A B C transf p b tf; nelim p; #fns main vars; 403 nelim fns; 404 ##[ nnormalize; #H; ndestruct; 405 ## #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); 406 nrewrite > (?:nextfunction ?? = length ? t); 407 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; 408 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] 409 ## nrewrite > (?:nextfunction ?? = length ? t); 410 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; 411 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] 412 ## napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); 413 ##[ #H; @fd; @; //; nelim (grumpydestruct1 ??? H); //; 414 ## #H; napply IH; napply H; 415 ##] 416 ##] 417 ##] 418 ##] 419 ## #A B C transf p v tf; nelim p; #fns main vars; nelim v; 420 ##[ nnormalize; #H; ndestruct; 421 ## ##2,3: #x; nnormalize; #H; ndestruct; 422 ## #b off; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); nelim (eq off zero); 423 ##[ nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); 424 nelim fns; 425 ##[ nnormalize; #H; ndestruct; 426 ## #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); 427 nrewrite > (?:nextfunction ?? = length ? t); 428 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; 429 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] 430 ## nrewrite > (?:nextfunction ?? = length ? t); 431 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; 432 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] 433 ## napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); 434 ##[ #H; @fd; @; //; nelim (grumpydestruct1 ??? H); //; 435 ## #H; napply IH; napply H; 436 ##] 437 ##] 438 ##] 439 ##] 440 ## nnormalize; #H; ndestruct; 441 ##] 442 ##] 443 ##] nqed. 444 331 445 (* 332 446 (** The rest of this library is a straightforward implementation of
Note: See TracChangeset
for help on using the changeset viewer.