Ignore:
Timestamp:
Jun 21, 2012, 5:21:04 PM (8 years ago)
Author:
campbell
Message:

Show some results about globalenvs and program transformations.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2103 r2105  
    33include "Clight/Cexec.ma".
    44include "Clight/CexecInd.ma".
    5 
    6 (* TODO: make something general that can live in common/Globalenvs.ma. *)
    7 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
    8   rg_find_symbol: ∀s.
    9     find_symbol … ge s = find_symbol … ge' s;
    10   rg_find_funct: ∀v,f.
    11     find_funct … ge v = Some ? f →
    12     find_funct … ge' v = Some ? (t f);
    13   rg_find_funct_ptr: ∀b,f.
    14     find_funct_ptr … ge b = Some ? f →
    15     find_funct_ptr … ge' b = Some ? (t f)
    16 }.
    17 
    18 (* FIXME with a more general result *)
    19 axiom transform_program_related : ∀F,V,init,t,p.
    20   related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p (λ_.t))).
    21 (*
    22 #F #V #init #t * #vars #fns #main
    23 whd in match (transform_program ?????);
    24 whd in match (transf_program ????);
    25 elim fns
    26 [ % [ // | * [ | #sz #i | #f | #r | #ptr ] #f #F1 whd in F1:(??%?); destruct
    27              cases (eq_offset ??) in F1; #F1 whd in F1:(??%?);
    28              whd in match (globalenv ?????) in F1;
    29              whd in match (globalenv_allocmem ????) in F1;
    30              elim
    31 %
    32 [ #s
    33 *)
    345
    356(* Useful for breaking up the labeling functions, because we don't care about
     
    8455
    8556theorem label_expr_ok : ∀ge,ge',en,m.
    86   related_globals ? label_fundef ge ge' →
     57  related_globals label_fundef ge ge' →
    8758  (∀e,v,tr.
    8859   exec_expr ge en m e = OK … 〈v,tr〉 →
     
    274245
    275246lemma label_exprs_ok : ∀ge,ge'.
    276    related_globals ? label_fundef ge ge' →
     247   related_globals label_fundef ge ge' →
    277248   ∀en,m,es,vs,tr.
    278249   exec_exprlist ge en m es = OK … 〈vs,tr〉 →
     
    397368
    398369lemma opt_find_funct : ∀ge,ge',m,vf,fd.
    399   related_globals ? label_fundef ge ge' →
     370  related_globals label_fundef ge ge' →
    400371  opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd →
    401372  opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd).
     
    684655   for labeled_statements. *)
    685656lemma step_with_labels_partial : ∀ge,ge'.
    686   related_globals ? label_fundef ge ge' →
     657  related_globals label_fundef ge ge' →
    687658  ∀s1,s1',tr,s2.
    688659  state_with_labels_partial s1 s1' →
     
    10651036
    10661037theorem step_with_labels : ∀ge,ge'.
    1067   related_globals ? label_fundef ge ge' →
     1038  related_globals label_fundef ge ge' →
    10681039  ∀s1,s1',tr,s2.
    10691040  state_with_labels s1 s1' →
     
    11101081whd in match (make_initial_state ?);
    11111082letin ge' ≝ (make_global ?)
    1112 cut (related_globals ? label_fundef ge ge')
     1083cut (related_globals label_fundef ge ge')
    11131084[ // ] #RG
    11141085% [2: %
Note: See TracChangeset for help on using the changeset viewer.