Changeset 2466

Timestamp:

Nov 14, 2012, 7:17:16 PM (8 years ago)

Author:

campbell

Message:

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

File:

• src/Clight/toCminorCorrectness.ma (modified) (1 diff)

src/Clight/toCminorCorrectness.ma

@@ -178 +178 @@
 | whd >(opt_eq_from_res ???? L) % #E destruct
 ] qed.
+
+
+(* Show how the global environments match up. *)
+
+lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
+  map_partial_All A B P f l H = OK ? l' →
+  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
+#A #B #P #f #l
+elim l
+[ #H #l' #MAP normalize in MAP; destruct //
+| #h #t #IH * #p #H #l'
+  whd in ⊢ (??%? → ?);
+  lapply (refl ? (f h p)) whd in match (proj1 ???);
+  cases (f h p) in ⊢ (???% → %);
+  [ #b #E #MAP cases (bind_inversion ????? MAP)
+    #tl' * #MAP' #E' normalize in E'; destruct
+    % [ %{p} @E | @IH [ @H | @MAP' ] ]
+  | #m #_ #X normalize in X; destruct
+  ]
+] qed.
+  
+
+definition clight_cminor_matching : clight_program → matching ≝
+λp.
+  let tmpuniverse ≝ universe_for_program p in
+  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
+  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
+  let globals ≝ fun_globals @ var_globals in
+  mk_matching
+    ?? (list init_data × type) (list init_data)
+    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
+    (λv,w. \fst v = w).
+
+lemma clight_to_cminor_varnames : ∀p,p'.
+  clight_to_cminor p = OK ? p' →
+  prog_var_names … p = prog_var_names … p'.
+* #vars #fns #main * #vars' #fns' #main'
+#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
+whd in E:(??%%); destruct
+-MAP normalize
+elim vars
+[ //
+| * * #id #r * #d #t #tl #IH normalize >IH //
+] qed.
+
+
+lemma clight_to_cminor_matches : ∀p,p'.
+  clight_to_cminor p = OK ? p' →
+  match_program (clight_cminor_matching p) p p'.
+* #vars #fns #main * #vars' #fns' #main'
+#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
+whd in E:(??%%); destruct
+%
+[ -MAP whd in match (m_V ?); whd in match (m_W ?);
+  elim vars
+  [ //
+  | * * #id #r * #init #ty #tl #IH %
+    [ % //
+    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
+    ]
+  ]
+| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
+  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
+  normalize in E; destruct
+  <(clight_to_cminor_varnames … TO)
+  % whd
+  % [2: % [2: @TRANSF | skip ] | skip ]
+| %
+] qed.