Ignore:
Timestamp:
Nov 7, 2012, 4:42:02 PM (7 years ago)
Author:
campbell
Message:

Get a proper reverse mapping of function blocks to identifiers by getting
rid of shadowing.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2415 r2439  
    4545  functions: positive_map F;
    4646  nextfunction: Pos;
    47   symbols: identifier_map SymbolTag block
     47  symbols: identifier_map SymbolTag block;
     48  functions_inv: ∀b. lookup_opt ? b functions ≠ None ? →
     49                 ∃id. lookup … symbols id = Some ? (mk_block Code (neg b))
    4850}.
     51
     52(* We deal with shadowed names by overwriting their global environment entry
     53   and getting rid of any function mapping (the latter is necessary so that we
     54   get a reverse mapping).  In fact, the parser will prevent these anyway, but
     55   adding the uniqueness of these names throughout would be more trouble than
     56   it's worth. *)
     57   
     58definition drop_fn : ∀F:Type[0]. ident → genv_t F → genv_t F ≝
     59λF,id,g.
     60let fns ≝
     61  match lookup ?? (symbols … g) id with
     62  [ None ⇒ functions … g
     63  | Some b' ⇒
     64      match b' with
     65      [ mk_block r x ⇒
     66        match r with
     67        [ Code ⇒
     68          match x with
     69          [ neg p ⇒ pm_set … p (None ?) (functions … g)
     70          | _ ⇒ functions … g
     71          ]
     72        | _ ⇒ functions … g
     73        ]
     74      | _ ⇒ functions … g
     75      ]
     76  ]
     77in mk_genv_t F fns (nextfunction … g) (remove … (symbols … g) id) ?.
     78whd in match fns; -fns
     79#b #L
     80cases (functions_inv ? g b ?)
     81[ #id' #L'
     82  cases (identifier_eq … id id')
     83  [ #E destruct >L' in L; normalize >lookup_opt_pm_set_hit * #H cases (H (refl ??))
     84  | #NE %{id'} >lookup_remove_miss /2/
     85  ]
     86| cases (lookup ?? (symbols F g) id) in L;
     87  [ normalize //
     88  | * * * [ 2,3,5,6: #b' ] normalize //
     89    #H cut (b ≠ b')
     90    [ % #E destruct >lookup_opt_pm_set_hit in H; * /2/ ]
     91    #NE >lookup_opt_pm_set_miss in H; //
     92  ]
     93] qed.
     94
     95lemma drop_fn_id : ∀F,id,ge.
     96  lookup ?? (symbols … (drop_fn F id ge)) id = None ?.
     97#F #id * #fns #next #syms #inv
     98whd in match (drop_fn ???);
     99@lookup_remove_hit
     100qed.
     101
     102lemma drop_fn_lfn : ∀F,id,ge,b,f.
     103  lookup_opt ? b (functions … (drop_fn F id ge)) = Some ? f →
     104  lookup_opt ? b (functions … ge) = Some ? f.
     105#F #id #ge #b #f
     106whd in match (drop_fn ???);
     107cases (lookup ??? id)
     108[ normalize //
     109| * * * [2,3,5,6: #b' ] normalize //
     110  cases (decidable_eq_pos b b')
     111  [ #E destruct >lookup_opt_pm_set_hit #E destruct
     112  | #NE >lookup_opt_pm_set_miss //
     113  ]
     114] qed.
    49115
    50116definition add_funct : ∀F:Type[0]. (ident × F) → genv_t F → genv_t F ≝
     
    52118  let blk_id ≝ nextfunction ? g in
    53119  let b ≝ mk_block Code (neg blk_id) in
    54   mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g))
     120  let g' ≝ drop_fn F (\fst name_fun) g in
     121  mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g'))
    55122              (succ blk_id)
    56               (add ?? (symbols … g) (\fst name_fun) b).
     123              (add ?? (symbols … g') (\fst name_fun) b) ?.
     124#b' #L whd in match b;
     125cases (decidable_eq_pos blk_id b')
     126[ #E destruct
     127  %{(\fst name_fun)} @lookup_add_hit
     128| #NE
     129  cases (functions_inv ? g' b' ?)
     130  [ #id #L' %{id} >lookup_add_miss
     131    [ @L'
     132    | % #E destruct
     133      >drop_fn_id in L'; #E destruct
     134    ]
     135  | >lookup_opt_insert_miss in L; /2/
     136  ]
     137] qed.
    57138
    58139definition add_symbol : ∀F:Type[0]. ident → block → genv_t F → genv_t F ≝
    59140λF,name,b,g.
    60   mk_genv_t F (functions … g)
    61               (nextfunction … g)
    62               (add ?? (symbols … g) name b).
     141  let g' ≝ drop_fn F name g in
     142  mk_genv_t F (functions … g')
     143              (nextfunction … g')
     144              (add ?? (symbols … g') name b)
     145              ?.
     146#b' #L
     147cases (functions_inv ? g' b' ?)
     148[ #id #L' %{id} >lookup_add_miss
     149  [ @L'
     150  | % #E destruct
     151    >drop_fn_id in L'; #E destruct
     152  ]
     153| @L
     154] qed.
    63155
    64156(* Construct environment and initial memory store *)
    65157definition empty_mem ≝ empty. (* XXX*)
    66158definition empty : ∀F. genv_t F ≝
    67   λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??).
     159  λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??) ?.
     160#b #L normalize in L; cases L #L cases (L (refl ??))
     161qed.
    68162
    69163definition add_functs : ∀F:Type[0]. genv_t F → list (ident × F) → genv_t F ≝
     
    247341  (*%{pty}*) %{b} (*%{c}*) % // @E
    248342] qed.
    249 
    250 
    251 lemma vars_irrelevant_to_find_funct_ptr : ∀F,V,init,b,vars,ge,m.
    252   find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = find_funct_ptr F ge b.
    253 #F #V #init * * // * // #blk
    254 whd in ⊢ (? → ? → ? → ??%%);
    255 #vars elim vars
    256 [ #ge #m %
    257 | * * #id #r #v #tl #IH #ge #m
    258   whd in match (add_globals ?????);
    259   whd in ⊢ (??(???(??(???(????%?))))?);
    260   cases (alloc ????) #m' #b
    261   whd in ⊢ (??(???(??(???(????%?))))?);
    262   >IH cases ge #fnmap #nextblock #symmap
    263   whd in ⊢ (??(???%)?);
    264   %
    265 ] qed.
    266 
     343 
    267344lemma add_globals_match : ∀A,B,V,W,initV,initW.
    268345  ∀P:(ident × region × V) → (ident × region × W) → Prop.
     
    285362  destruct >E2 cases (alloc ????) #m' #b
    286363  @IH /2/
    287   whd in match (add_symbol ????);
    288   whd in match (add_symbol ????);
     364  whd in match (add_symbol ????); whd in match (drop_fn ???);
     365  whd in match (add_symbol ????); whd in match (drop_fn ???);
    289366  >E %
    290367] qed.
     368
    291369
    292370lemma pre_matching_fns_get_same_blocks : ∀A,B,P.
     
    306384  change with (add_functs ???) in match (foldr (ident × B) ????);
    307385  cases (IH tl' H) #E1 #E2
    308   % [ >E1 % | >E1 >E2 % ]
     386  % [ >E1 %
     387    | whd in match (drop_fn ???);
     388      whd in match (drop_fn ???);
     389      >E1 >E2 % ]
    309390] qed.
    310391
     
    334415  ]
    335416] qed.
     417
     418(* The mapping of blocks to symbols is total for functions. *)
     419
     420definition symbol_of_function_block : ∀F,ge,b. find_funct_ptr F ge b ≠ None ? → ident ≝
     421λF,ge,b,FFP.
     422match symbol_for_block F ge b return λx. symbol_for_block ??? = x → ? with
     423[ None ⇒ λH. ⊥
     424| Some id ⇒ λ_. id
     425] (refl ? (symbol_for_block F ge b)).
     426whd in H:(??%?);
     427cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
     428cases (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)))
     430lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
     431cases (find ????)
     432[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
     433| * #id' #b' #_ normalize #_ #E destruct
     434] qed.
     435
    336436
    337437(*
     
    524624qed.
    525625
     626lemma 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].
     627  nextblock m = nextblock m' →
     628  (∀m1,m2,b. nextblock m1 = nextblock m2 → P 〈m1,b〉 〈m2,b〉) →
     629  P (alloc m l h r) (alloc m' l' h' r).
     630* #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' #r #P #N destruct #H @H %
     631qed.
     632
     633lemma vars_irrelevant_to_find_funct_ptr :
     634  ∀F,G,V,W.
     635  ∀P:F → G → Prop.
     636  ∀init,init',b,vars,vars',ge,ge',m,m',f.
     637  (find_funct_ptr F ge b = Some ? f → ∃f'. find_funct_ptr G ge' b = Some ? f' ∧ P f f') →
     638  symbols F ge = symbols G ge' →
     639  nextblock m = nextblock m' →
     640  All2 … (λx,y. \fst x = \fst y) vars vars' →
     641  find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = Some ? f →
     642  ∃f'.find_funct_ptr G (\fst (add_globals G W init' 〈ge',m'〉 vars')) b = Some ? f' ∧ P f f'.
     643#F #G #V #W #P #init #init'
     644* * * [ 2,3,5,6: #blk ] [ 4: | *: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 normalize in H5; destruct ]
     645#vars elim vars
     646[ * [ #ge #ge' #m #m' #f #H #_ #_ #_ @H
     647    | #x #tl #ge #ge' #m #m' #f #_ #_ #_ *
     648    ]
     649| * * #id #r #v #tl #IH *
     650  [ #ge #ge' #m #m' #f #_ #_ #_ *
     651  | * * #id' #r' #v' #tl'
     652    #ge #ge' #m #m' #f #FFP1 #Esym #Enext * #E destruct #MATCH
     653    whd in match (add_globals ?????); whd in match (add_globals G ????);
     654    whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?));
     655    @(alloc_pair … Enext) #m1 #m2 #b #Enext'
     656    whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?));
     657    #FFP
     658    @(IH … MATCH FFP)
     659    [ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
     660      whd in ⊢ (??(???%)? → ??(λ_.?(??(???%)?)?));
     661      >Esym
     662      cases (lookup … id')
     663      [ @FFP1
     664      | * * * try @FFP1 #p try @FFP1
     665        normalize
     666        cases (decidable_eq_pos blk p)
     667        [ #E destruct >lookup_opt_pm_set_hit #E destruct
     668        | #NE >(lookup_opt_pm_set_miss … NE) >(lookup_opt_pm_set_miss … NE)
     669          @FFP1
     670        ]
     671      ]
     672    | whd in match (add_symbol ????); whd in match (drop_fn ???);
     673      whd in match (add_symbol ????); whd in match (drop_fn ???);
     674      >Esym %
     675    | assumption
     676    ]
     677  ]
     678] qed.
     679
    526680(* Now link functions in related programs, but without dealing with the type
    527681   casts yet. *)
    528682
     683lemma symbols_drop_fn_eq : ∀A,B,ge,ge',id.
     684  symbols A ge = symbols B ge' →
     685  symbols A (drop_fn A id ge) = symbols B (drop_fn B id ge').
     686#A #B #ge #ge' #id #E
     687whd in ⊢ (??(??%)(??%));
     688>E %
     689qed.
     690
     691lemma ge_add_functs : ∀A,B,fns,fns'.
     692  All2 ?? (λx,y. \fst x = \fst y) fns fns' →
     693  symbols A (add_functs A (empty ?) fns) = symbols B (add_functs B (empty ?) fns') ∧
     694  nextfunction A (add_functs A (empty ?) fns) = nextfunction B (add_functs B (empty ?) fns').
     695#A #B
     696#fns elim fns
     697[ * [ #_ % % | #h #t * ]
     698| * #id #a #tl #IH * * #id' #b #tl' * #E destruct #TL
     699  whd in match (add_functs ???); whd in match (add_functs B ??);
     700  cases (IH ? TL) #S #N >N % [2: % ]
     701  >(symbols_drop_fn_eq A B (foldr ??? (empty A) tl) (foldr ?? (add_funct B) (empty B) tl'))
     702  [ %
     703  | @S
     704  ]
     705] qed.
     706
     707lemma lookup_drop_fn_different : ∀F,ge,id,b,f.
     708  lookup_opt ? b (functions ? (drop_fn F id ge)) = Some ? f →
     709  lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)).
     710#F #ge #id #b #f
     711whd in match (drop_fn F id ge);
     712cases (lookup … id)
     713[ #_ % #E destruct
     714| * * * [2,3,5,6: #b'] normalize
     715  [4: cases (decidable_eq_pos b b')
     716    [ #E destruct >lookup_opt_pm_set_hit #E destruct
     717    | #NE #_ @(not_to_not … NE) #E destruct //
     718    ]
     719  | *: #_ % #E destruct
     720  ]
     721] qed.
     722
     723lemma lookup_drop_fn_irrelevant : ∀F,ge,id,b.
     724  lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)) →
     725  lookup_opt ? b (functions ? (drop_fn F id ge)) = lookup_opt ? b (functions ? ge).
     726#F #ge #id #b
     727whd in match (drop_fn F id ge);
     728cases (lookup … id)
     729[ //
     730| * * * //
     731  #b' normalize #NE
     732  @lookup_opt_pm_set_miss
     733  @(not_to_not … NE)
     734  #E destruct %
     735] qed.
     736
    529737lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P.
     738  All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') →
     739  All2 … (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p') →
    530740  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
    531   All2 ?? (λx,y. P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') →
    532741  ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'.
    533742#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
     743#Mfns
    534744cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ]
    535 [ 4: (*12:*) | *: #F whd in F:(??%?); destruct ]
    536 >vars_irrelevant_to_find_funct_ptr
    537 >vars_irrelevant_to_find_funct_ptr
    538 letin varnames ≝ (map ??? vars)
    539 cut (lookup_opt (A varnames) bp (functions ? (add_functs ? (empty ?) [ ])) = None ?)
    540 //
    541 cut (nextfunction (A varnames) (empty ?) = nextfunction (B (map … (λx.\fst (\fst x)) vars')) (empty ?))
    542 //
    543 generalize in match (empty ?);
    544 generalize in match (empty ?);
    545 generalize in match fns';
    546 elim fns
    547 [ #fns' #ge' #ge #_ #F1 #FFP @⊥ normalize in FFP; >F1 in FFP; #E destruct
    548 | * #id #fn #tl #IH #fns' #ge' #ge #NF #F1 whd in ⊢ (??%? → ?);
    549   whd in match (functions ??);
    550   change with (add_functs ???) in match (foldr ?????);
    551   cases (decidable_eq_pos bp (nextfunction … (add_functs ? ge tl)))
    552   [ #E destruct  >lookup_opt_insert_hit #E destruct
    553     cases fns' [ * ]
    554     * #id' #fn' #tl' * #M #Mtl
    555     %{fn'} % // whd in ⊢ (??%?);
     745[ 4: (*12:*) | *: #_ #F whd in F:(??%?); destruct ]
     746whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     747whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     748@vars_irrelevant_to_find_funct_ptr
     749[ letin varnames ≝ (map ??? vars)
     750  generalize in match fns' in Mfns ⊢ %;
     751  elim fns
     752  [ #fns' #Mfns whd in ⊢ (??%? → ?); #E destruct
     753  | * #id #fn #tl #IH * * #id' #fn' #tl' * * #E #Phd destruct #Mtl
     754    whd in ⊢ (??%? → ?);
    556755    whd in match (functions ??);
    557     change with (add_functs ???) in match (foldr ???? tl');
    558     >nextfunction_length >nextfunction_length <NF >(All2_length  … Mtl)
    559     >lookup_opt_insert_hit @refl
    560   | #NE >lookup_opt_insert_miss //
    561     #FFP cases fns' [ * ] * #id' #fn' #tl' * #M #Mtl
    562     cases (IH ?????? Mtl)
    563     [ #fn'' * #FFP' #P' %{fn''} % [ whd in ⊢ (??%?); >lookup_opt_insert_miss [2: >nextfunction_length <NF <(All2_length … Mtl) <nextfunction_length @NE ] @FFP' | @P' ]
    564     | skip
    565     | 4: @NF
    566     | skip
    567     | //
    568     | @FFP
     756    change with (add_functs ???) in match (foldr ?????);
     757    cases (ge_add_functs ?? tl tl' ?) [2: @(All2_mp … Mtl) * #idA #a * #idB #b * // ]
     758    #SYMS #NEXT
     759    cases (decidable_eq_pos bp (nextfunction … (add_functs ? (empty ?) tl)))
     760    [ #E destruct >lookup_opt_insert_hit #E destruct
     761      %{fn'} % // whd in ⊢ (??%?);
     762      whd in match (functions ??);
     763      change with (add_functs ???) in match (foldr ???? tl');
     764      >NEXT >lookup_opt_insert_hit @refl
     765    | #NE >lookup_opt_insert_miss //
     766      #FFP cases (IH tl' Mtl ?)
     767      [ #fn'' * #FFP' #P' %{fn''} %
     768        [ whd in ⊢ (??%?);
     769          >lookup_opt_insert_miss [2: <NEXT // ]
     770          lapply (lookup_drop_fn_different ????? FFP)
     771          >SYMS
     772          #L >lookup_drop_fn_irrelevant // @FFP'
     773        | @P'
     774        ]
     775      | @(drop_fn_lfn … FFP)
     776      ]
    569777    ]
    570778  ]
     779| cases (ge_add_functs ?? fns fns' ?) [2: @(All2_mp … Mfns) * #idA #a * #idB #b * // ]
     780  #S #_ @S
     781| @refl
    571782] qed.
    572783
     
    577788  P f.
    578789#A #V #b #p #f #initV #P #FFP #ALL
    579 cut (All2 ?? (λx,y. P (\snd x)) (prog_funct ?? p) (prog_funct ?? p))
     790cut (All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x)) (prog_funct ?? p) (prog_funct ?? p))
    580791[ elim (prog_funct … p) in ALL ⊢ %;
    581792  [ // | #h #t #IH * #Hh #Ht % /2/ ] ]
    582 #ALL2
    583 cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FFP ALL2)
     793cut (All2 ?? (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p))
     794[ elim (prog_vars … p) [ // | * #x #x' #tl #TL /2/ ] ]
     795#VARS2 #FNS2
     796cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FNS2 VARS2 FFP)
    584797#x * //
    585798qed.
     
    602815#p #p' * #Mvars #Mfn #Mmain
    603816#b #f #FFP
    604 @(find_funct_ptr_All2 A B V W ??????? FFP)
    605 lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
    606 #E
    607 @(All2_mp … Mfn)
    608 * #id #f * #id' #f'
    609 <E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
    610 normalize #H @(match_funct_entry_inv … H) //
     817@(find_funct_ptr_All2 A B V W ????????? FFP)
     818[ lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
     819  #E
     820  @(All2_mp … Mfn)
     821  * #id #f * #id' #f'
     822  <E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
     823  normalize #H @(match_funct_entry_inv … H)
     824  #vs #id1 #f1 #f2 #M % //
     825| @(All2_mp … Mvars)
     826  * #x #x' * #y #y' #M inversion M #id #r #v1 #v2 #M' #E1 #E2 #_ destruct //
    611827qed.
    612828
Note: See TracChangeset for help on using the changeset viewer.