Ignore:
Timestamp:
Oct 23, 2012, 3:57:02 PM (7 years ago)
Author:
campbell
Message:

Add the ability to map blocks to symbols in preparation for stack space.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2319 r2415  
    228228
    229229
     230(* Turn a memory block into the original symbol. *)
     231definition symbol_for_block: ∀F:Type[0]. genv_t F → block → option ident ≝
     232λF,genv,b.
     233  option_map ?? (fst ??) (find … (symbols … genv) (λid,b'. eq_block b b')).
     234
     235
    230236lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
    231237  find_funct F ge v = Some F f →
     
    312318#A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK
    313319qed.
     320
     321lemma symbol_of_block_rev : ∀F,genv,b,id.
     322  symbol_for_block F genv b = Some ? id →
     323  find_symbol F genv id = Some ? b.
     324#F #genv #b #id #H whd in H:(??%?);
     325@(find_lookup … (λid,b'. eq_block b b'))
     326lapply (find_predicate … (symbols … genv) (λid,b'. eq_block b b'))
     327cases (find ????) in H ⊢ %;
     328[ normalize #E destruct
     329| * #id' #b' normalize in ⊢ (% → ?); #E destruct
     330  #H lapply (H … (refl ??))
     331  @eq_block_elim
     332  [ #E destruct //
     333  | #_ *
     334  ]
     335] qed.
    314336
    315337(*
Note: See TracChangeset for help on using the changeset viewer.