Changeset 2471 for src/common/Globalenvs.ma
 Timestamp:
 Nov 16, 2012, 6:41:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Globalenvs.ma
r2468 r2471 444 444 ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block. 445 445 find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b; 446 447 find_symbol_exists: 448 ∀F,V: Type[0]. ∀p: program F V. 449 ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V. 450 in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) → 451 ∃b. find_symbol ? (globalenv ?? p) id = Some ? b; 446 *) 447 lemma find_symbol_exists: 448 ∀F,V. ∀init. ∀p: program F V. ∀id. 449 Exists ? (λx. x = id) (map … (λx. \fst x) (prog_funct ?? p) @ map … (λx. \fst (\fst x)) (prog_vars ?? p)) → 450 ∃b. find_symbol ? (globalenv … init p) id = Some ? b. 451 #F #V #init * #vars #fns #main #id 452 whd in match (globalenv ????); 453 whd in match (globalenv_allocmem ????); 454 whd in match (prog_var_names ???); 455 generalize in match (F ?) in fns ⊢ %; F #F #fns 456 #EX 457 cut (Exists ident (λx.x = id) (map … (λx.\fst (\fst x)) vars) ∨ 458 ∃b. find_symbol ? (add_functs F (empty F) fns) id = Some ? b) 459 [ cases (Exists_append … EX) 460 [ EX #EX %2 461 elim fns in EX ⊢ %; 462 [ * 463  * #id' #f #tl #IH * 464 [ #E destruct 465 change with (foldr ?????) in match (add_functs F (empty F) ?); 466 change with (lookup ????) in match (find_symbol ???); 467 whd in match (foldr ?????); 468 % [2: @lookup_add_hit  skip ] 469  #TL 470 change with (foldr ?????) in match (add_functs F (empty F) ?); 471 change with (lookup ????) in match (find_symbol ???); 472 whd in match (foldr ?????); 473 cases (identifier_eq ? id id') 474 [ #E destruct 475 % [2: @lookup_add_hit  skip ] 476  #NE >lookup_add_miss // 477 whd in match (drop_fn ???); 478 >lookup_remove_miss // @IH @TL 479 ] 480 ] 481 ] 482  #EX %1 @EX 483 ] 484 ] 485 EX 486 generalize in match (add_functs F (empty F) fns); 487 generalize in match empty_mem; 488 elim vars 489 [ #m #ge * [ *  // ] 490  * * #id' #r' #v' #tl #IH #m #ge * 491 [ * 492 [ #E destruct 493 (* Found one, but it might be shadowed later *) 494 whd in match (foldl ?????); normalize nodelta 495 cases (alloc ????) #m' #b normalize nodelta 496 cut (find_symbol F (add_symbol F id b ge) id = Some ? b) 497 [ change with (lookup ????) in ⊢ (??%?); 498 whd in match add_symbol; normalize nodelta 499 @lookup_add_hit ] 500 #F @IH %2 %{b} @F 501  #TL whd in match (foldl ?????); normalize nodelta 502 cases (alloc ????) #m' #b' 503 @IH %1 @TL 504 ] 505  #H whd in match (foldl ?????); normalize nodelta 506 cases (alloc ????) #m' #b' normalize nodelta 507 @IH %2 508 cases (identifier_eq ? id id') 509 [ #E destruct %{b'} 510 whd in match add_symbol; normalize nodelta 511 @lookup_add_hit 512  #NE cases H #b #H' %{b} 513 whd in match add_symbol; normalize nodelta 514 change with (lookup ???? = ?) >lookup_add_miss // 515 whd in match (drop_fn ???); >lookup_remove_miss // @H' 516 ] 517 ] 518 ] qed. 519 520 (* 452 521 find_funct_ptr_exists: 453 522 ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F.
Note: See TracChangeset
for help on using the changeset viewer.