Ignore:
Timestamp:
Sep 3, 2012, 1:16:29 PM (8 years ago)
Author:
campbell
Message:

Generate per-program cost labels rather than per-function ones, and
produce an extra cost label for the global variable initialisation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2226 r2319  
    770770//
    771771qed.
     772
     773lemma
     774  init_mem_transf_gen:
     775    ∀tag,A,B,V,iV,g. ∀transf: (∀vs. universe tag → A vs → B vs × (universe tag)). ∀p: program A V.
     776    init_mem … iV (\fst (transform_program_gen … g p transf)) = init_mem … iV p.
     777#tag #A #B #C #iV #g #transf #p
     778@(init_mem_match … (transform_program_gen_match … transf ?))
     779//
     780qed.
    772781   
    773782
     
    791800| @(find_funct_transf A B V iV tf p)
    792801| @(find_funct_ptr_transf A B V iV p tf)
     802] qed.
     803
     804record related_globals_gen (tag:String) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
     805  rgg_find_symbol: ∀s.
     806    find_symbol … ge s = find_symbol … ge' s;
     807  rgg_find_funct_ptr: ∀b,f.
     808    find_funct_ptr … ge b = Some ? f →
     809    ∃g. find_funct_ptr … ge' b = Some ? (\fst (t g f));
     810  rgg_find_funct: ∀v,f.
     811    find_funct … ge v = Some ? f →
     812    ∃g. find_funct … ge' v = Some ? (\fst (t g f))
     813}.
     814
     815include "utilities/bool.ma".
     816
     817theorem transform_program_gen_related : ∀tag,A,B,V,init,g,p. ∀tf:∀vs. universe tag → A vs → B vs × (universe tag).
     818  related_globals_gen tag (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (\fst (transform_program_gen tag A B V g p tf))).
     819#tag #A #B #V #iV #g #p #tf %
     820[ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p))
     821  #v #w * //
     822| #b #f #FFP
     823  cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
     824  [ 2: @iV
     825  | #fn' * #FFP'
     826    generalize in match (matching_vars ????);
     827    whd in match (prog_var_names ???); whd in match (prog_vars ???);
     828    #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E' >FFP' %{g1} >E' %
     829  | skip
     830  ]
     831| * [5: #ptr #fn whd in match (find_funct ???);
     832     @if_elim #Eoff #FFP
     833     [ cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
     834       [ 2: @iV
     835       | #fn' * #FFP'
     836         generalize in match (matching_vars ????);
     837         whd in match (prog_var_names ???); whd in match (prog_vars ???);
     838         #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E'
     839         %{g1} whd in ⊢ (??%?); >Eoff >FFP' >E' %
     840       ]
     841     | destruct
     842     ]
     843    | *: normalize #A #B try #C try #D destruct
     844    ]
    793845] qed.
    794846
Note: See TracChangeset for help on using the changeset viewer.