Changeset 2466


Ignore:
Timestamp:
Nov 14, 2012, 7:17:16 PM (7 years ago)
Author:
campbell
Message:

Show how global environments in clight to cminor pass match up.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2460 r2466  
    178178| whd >(opt_eq_from_res ???? L) % #E destruct
    179179] qed.
     180
     181
     182(* Show how the global environments match up. *)
     183
     184lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
     185  map_partial_All A B P f l H = OK ? l' →
     186  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
     187#A #B #P #f #l
     188elim l
     189[ #H #l' #MAP normalize in MAP; destruct //
     190| #h #t #IH * #p #H #l'
     191  whd in ⊢ (??%? → ?);
     192  lapply (refl ? (f h p)) whd in match (proj1 ???);
     193  cases (f h p) in ⊢ (???% → %);
     194  [ #b #E #MAP cases (bind_inversion ????? MAP)
     195    #tl' * #MAP' #E' normalize in E'; destruct
     196    % [ %{p} @E | @IH [ @H | @MAP' ] ]
     197  | #m #_ #X normalize in X; destruct
     198  ]
     199] qed.
     200 
     201
     202definition clight_cminor_matching : clight_program → matching ≝
     203λp.
     204  let tmpuniverse ≝ universe_for_program p in
     205  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
     206  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
     207  let globals ≝ fun_globals @ var_globals in
     208  mk_matching
     209    ?? (list init_data × type) (list init_data)
     210    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
     211    (λv,w. \fst v = w).
     212
     213lemma clight_to_cminor_varnames : ∀p,p'.
     214  clight_to_cminor p = OK ? p' →
     215  prog_var_names … p = prog_var_names … p'.
     216* #vars #fns #main * #vars' #fns' #main'
     217#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
     218whd in E:(??%%); destruct
     219-MAP normalize
     220elim vars
     221[ //
     222| * * #id #r * #d #t #tl #IH normalize >IH //
     223] qed.
     224
     225
     226lemma clight_to_cminor_matches : ∀p,p'.
     227  clight_to_cminor p = OK ? p' →
     228  match_program (clight_cminor_matching p) p p'.
     229* #vars #fns #main * #vars' #fns' #main'
     230#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
     231whd in E:(??%%); destruct
     232%
     233[ -MAP whd in match (m_V ?); whd in match (m_W ?);
     234  elim vars
     235  [ //
     236  | * * #id #r * #init #ty #tl #IH %
     237    [ % //
     238    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
     239    ]
     240  ]
     241| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
     242  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
     243  normalize in E; destruct
     244  <(clight_to_cminor_varnames … TO)
     245  % whd
     246  % [2: % [2: @TRANSF | skip ] | skip ]
     247| %
     248] qed.
Note: See TracChangeset for help on using the changeset viewer.