Changeset 2608 for src/common/Globalenvs.ma
 Timestamp:
 Feb 6, 2013, 1:01:34 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Globalenvs.ma
r2601 r2608 47 47 symbols: identifier_map SymbolTag block; 48 48 functions_inv: ∀b. lookup_opt ? b functions ≠ None ? → 49 ∃id. lookup … symbols id = Some ? (mk_block Code(neg b))49 ∃id. lookup … symbols id = Some ? (mk_block (*Code*) (neg b)) 50 50 }. 51 51 … … 62 62 [ None ⇒ functions … g 63 63  Some b' ⇒ 64 match b' with 64 match block_id b' with 65 [ neg p ⇒ 66 pm_set … p (None ?) (functions … g) 67  _ ⇒ functions … g 68 ] 69 (* match b' with 65 70 [ mk_block r x ⇒ 66 71 match r with … … 73 78 ] 74 79  _ ⇒ functions … g 75 ] 80 ] *) 76 81 ] 77 82 in mk_genv_t F fns (nextfunction … g) (remove … (symbols … g) id) ?. 83 whd in match fns; fns 84 #b #L 85 cases (functions_inv ? g b ?) 86 [ #id' #L' 87 cases (identifier_eq … id id') 88 [ #E destruct >L' in L; normalize >lookup_opt_pm_set_hit * #H cases (H (refl ??)) 89  #NE %{id'} >lookup_remove_miss /2/ 90 ] 91  cases (lookup ?? (symbols F g) id) in L; 92 [ normalize // 93  normalize nodelta * * normalize nodelta try // 94 #p 95 @(eqb_elim … b p) 96 [ #Heq destruct #NE 97 >lookup_opt_pm_set_hit in NE; #Hneq 98 @False_ind 99 @(absurd … (refl ??) Hneq) 100  #id >lookup_opt_pm_set_miss // ] 101 ] 102 ] qed. 103 (* 78 104 whd in match fns; fns 79 105 #b #L … … 93 119 ] qed. 94 120 121 *) 95 122 lemma drop_fn_id : ∀F,id,ge. 96 123 lookup ?? (symbols … (drop_fn F id ge)) id = None ?. … … 107 134 cases (lookup ??? id) 108 135 [ normalize // 109  * * * [2,3,5,6: #b' ] normalize //136  * * [2,3: #b' ] normalize // 110 137 cases (decidable_eq_pos b b') 111 138 [ #E destruct >lookup_opt_pm_set_hit #E destruct … … 117 144 λF,name_fun,g. 118 145 let blk_id ≝ nextfunction ? g in 119 let b ≝ mk_block Code(neg blk_id) in146 let b ≝ mk_block (* Code *) (neg blk_id) in 120 147 let g' ≝ drop_fn F (\fst name_fun) g in 121 148 mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g')) … … 260 287 let init ≝ extract_init init_info in 261 288 let 〈g,st〉 ≝ g_st in 262 let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) rin289 let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) (* r *) in 263 290 let g' ≝ add_symbol ? id b g in 264 291 〈g', st'〉 … … 360 387 change with (add_globals B ????) in match (foldl (genv_t B × mem) ????); 361 388 cases (varsOK … p) #E1 #E2 362 destruct >E2 cases (alloc ??? ?) #m' #b389 destruct >E2 cases (alloc ???) (* cases (alloc ????)*) #m' #b 363 390 @IH /2/ 364 391 whd in match (add_symbol ????); whd in match (drop_fn ???); … … 425 452 ] (refl ? (symbol_for_block F ge b)). 426 453 whd in H:(??%?); 427 cases b in FFP H ⊢ %; * * b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP  *: * #H cases (H (refl ??)) ] 454 cases b in FFP H ⊢ %; * b [2,3(*,5,6*): #b ] normalize in ⊢ (% → ?); [ 1,3: * #H cases (H (refl ??)) ] 455 #FFP 428 456 cases (functions_inv … ge b FFP) 429 #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code(neg b)))430 lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code(neg b)))457 #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block (*Code*) (neg b)) b') id (mk_block (*Code*) (neg b))) 458 lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block (* Code *) (neg b)) b') id (mk_block (* Code *) (neg b))) 431 459 cases (find ????) 432 460 [ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ *  * #H' cases (H' (refl ??)) ] 433 461  * #id' #b' #_ normalize #_ #E destruct 434 462 ] qed. 435 436 463 437 464 (* … … 492 519 [ #E destruct 493 520 (* Found one, but it might be shadowed later *) 494 whd in match (foldl ?????); normalize nodelta 495 cases (alloc ??? ?) #m' #b normalize nodelta521 whd in match (foldl ?????); normalize nodelta 522 cases (alloc ???) (* cases (alloc ????) *) #m' #b normalize nodelta 496 523 cut (find_symbol F (add_symbol F id b ge) id = Some ? b) 497 524 [ change with (lookup ????) in ⊢ (??%?); … … 499 526 @lookup_add_hit ] 500 527 #F @IH %2 %{b} @F 501  #TL whd in match (foldl ?????); normalize nodelta 502 cases (alloc ??? ?) #m' #b'528  #TL whd in match (foldl ?????); normalize nodelta 529 cases (alloc ???) (*cases (alloc ????)*) #m' #b' 503 530 @IH %1 @TL 504 531 ] 505 532  #H whd in match (foldl ?????); normalize nodelta 506 cases (alloc ??? ?) #m' #b' normalize nodelta533 cases (alloc ???) (* cases (alloc ????) *) #m' #b' normalize nodelta 507 534 @IH %2 508 535 cases (identifier_eq ? id id') … … 693 720 qed. 694 721 695 lemma alloc_pair : ∀m,m',l,h,l',h' ,r. ∀P:mem×(Σb:block. block_region b = r) → mem×(Σb:block. block_region b = r) → Type[0].722 lemma alloc_pair : ∀m,m',l,h,l',h'(*,r*). ∀P:mem×block (*(Σb:block. block_region b = r)*) → mem×block(*(Σb:block. block_region b = r)*) → Type[0]. 696 723 nextblock m = nextblock m' → 697 724 (∀m1,m2,b. nextblock m1 = nextblock m2 → P 〈m1,b〉 〈m2,b〉) → 698 P (alloc m l h r) (alloc m' l' h' r).699 * #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' #r#P #N destruct #H @H %725 P (alloc m l h (*r*)) (alloc m' l' h' (*r*)). 726 * #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' (* #r *) #P #N destruct #H @H % 700 727 qed. 701 728 … … 711 738 ∃f'.find_funct_ptr G (\fst (add_globals G W init' 〈ge',m'〉 vars')) b = Some ? f' ∧ P f f'. 712 739 #F #G #V #W #P #init #init' 713 * * * [ 2,3,5,6: #blk ] [ 4:  *: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 normalize in H5; destruct ]740 * * [ 2,3(*,5,6*): #blk ] [ 2:  1,3: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 whd in H5:(??%?); destruct ] 714 741 #vars elim vars 715 742 [ * [ #ge #ge' #m #m' #f #H #_ #_ #_ @H … … 731 758 cases (lookup … id') 732 759 [ @FFP1 733  * * *try @FFP1 #p try @FFP1760  * * (* * *) try @FFP1 #p try @FFP1 734 761 normalize 735 762 cases (decidable_eq_pos blk p) … … 776 803 lemma lookup_drop_fn_different : ∀F,ge,id,b,f. 777 804 lookup_opt ? b (functions ? (drop_fn F id ge)) = Some ? f → 778 lookup … (symbols ? ge) id ≠ Some ? (mk_block Code(neg b)).805 lookup … (symbols ? ge) id ≠ Some ? (mk_block (*Code*) (neg b)). 779 806 #F #ge #id #b #f 780 807 whd in match (drop_fn F id ge); 781 808 cases (lookup … id) 782 809 [ #_ % #E destruct 783  * * * [2,3,5,6: #b'] normalize784 [ 4: cases (decidable_eq_pos b b')810  * * (* * *) [2,3(*,5,6*): #b'] normalize 811 [ 2: cases (decidable_eq_pos b b') 785 812 [ #E destruct >lookup_opt_pm_set_hit #E destruct 786 813  #NE #_ @(not_to_not … NE) #E destruct // … … 788 815  *: #_ % #E destruct 789 816 ] 790 ] qed. 817 ] qed. 791 818 792 819 lemma lookup_drop_fn_irrelevant : ∀F,ge,id,b. 793 lookup … (symbols ? ge) id ≠ Some ? (mk_block Code(neg b)) →820 lookup … (symbols ? ge) id ≠ Some ? (mk_block (* Code *) (neg b)) → 794 821 lookup_opt ? b (functions ? (drop_fn F id ge)) = lookup_opt ? b (functions ? ge). 795 822 #F #ge #id #b … … 797 824 cases (lookup … id) 798 825 [ // 799  * * *//826  * * (* * *) // 800 827 #b' normalize #NE 801 828 @lookup_opt_pm_set_miss … … 811 838 #A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P 812 839 #Mfns 813 cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ]814 [ 4: (*12:*)  *: #_ #F whd in F:(??%?); destruct ]840 cases b * (* * *) [ 2,3 (*,5,6*) (*,8,9,11,12,14,15,17,18*): #bp ] 841 [ 2: (*12:*)  *: #_ #F whd in F:(??%?); destruct ] 815 842 whd in match (globalenv ????); whd in match (globalenv_allocmem ????); 816 843 whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
Note: See TracChangeset
for help on using the changeset viewer.