Changeset 2251 for src/Cminor
- Timestamp:
- Jul 24, 2012, 7:40:21 PM (7 years ago)
- Location:
- src/Cminor
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/initialisation.ma
r2249 r2251 19 19 ]. 20 20 21 (* None of the additional code introduces locals or labels. *)21 (* None of the additional code introduces locals, labels or returns. *) 22 22 definition stmt_inv : stmt → Prop ≝ 23 stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s ).23 stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s ∧ match s with [ St_return _ ⇒ False | _ ⇒ True ]). 24 24 25 25 discriminator option. … … 38 38 ] 39 39 ]. 40 % / /40 % /2/ 41 41 cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p; 42 destruct;/ 2/42 destruct;/3/ 43 43 qed. 44 44 … … 50 50 〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉) 51 51 〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init). 52 [ % / /52 [ % /2/ 53 53 | elim init 54 [ % // 55 | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(pi2 … (init_datum …)) ] | @IH ] 54 [ % /2/ 55 | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); 56 % [ % [ % /2/ | @(pi2 … (init_datum …)) ] | @IH ] 56 57 ] qed. 57 58 58 59 definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝ 59 60 λvars. foldr ? (Σs:stmt. stmt_inv s) 60 (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? II)) vars.61 % [ % [ % / / | @(pi2 … s) ] | @(pi2 … (init_var …)) ]61 (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? (conj ?? I I) I)) vars. 62 % [ % [ % /2/ | @(pi2 … s) ] | @(pi2 … (init_var …)) ] 62 63 qed. 63 64 64 65 lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ]. 65 66 #s elim s // 66 [ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);67 [ #s1 #s2 #IH1 #IH2 * * * * #_ #_ #_ #H1 #H2 whd in ⊢ (??%?); 67 68 >(IH1 H1) >(IH2 H2) @refl 68 69 | #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?); 69 70 >(IH1 H1) >(IH2 H2) @refl 70 | #l #s #IH * * #_ *71 | #l #s #IH * * * #_ * 71 72 | #l #s #IH * * #_ #_ #H @(IH H) 72 73 ] qed. … … 95 96 % 96 97 [ % [ % // | 97 @(stmt_P_mp … H) #s * #V #L%98 @(stmt_P_mp … H) #s * * #V #L #R % 98 99 [ @(stmt_vars_mp … V) #i #t * 99 100 | @(stmt_labels_mp … L) #l * 101 | cases s in R ⊢ %; // #x * 100 102 ] 101 103 ] -
src/Cminor/semantics.ma
r2232 r2251 395 395 | 7,8: 396 396 @(stmt_P_mp … (f_inv f)) 397 #s * #V #L %397 #s * #V #L #R % 398 398 [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX) 399 399 [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en)) -
src/Cminor/syntax.ma
r2249 r2251 128 128 ]. 129 129 130 record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (s:stmt) : Prop ≝ { 130 inductive rettyp_match : option typ → option (𝚺t.expr t) → Prop ≝ 131 | rettyp_none : rettyp_match (None ?) (None ?) 132 | rettyp_some : ∀t,e. rettyp_match (Some ? t) (Some ? ❬t,e❭). 133 134 record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (rettyp:option typ) (s:stmt) : Prop ≝ { 131 135 cm_inv_var : stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) env) s; 132 cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s 136 cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s; 137 cm_inv_return : match s with [ St_return oe ⇒ rettyp_match rettyp oe 138 | _ ⇒ True ] 133 139 }. 134 140 … … 142 148 (* Ensure that variables appear in the params and vars list with the 143 149 correct typ; and that all goto labels used are declared. *) 144 ; f_inv : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body) ) f_body150 ; f_inv : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body) f_return) f_body 145 151 }. 146 152 -
src/Cminor/toRTLabs.ma
r2232 r2251 837 837 ). 838 838 [ -emptyfn @(stmt_P_mp … (f_inv f)) 839 #s * #V #L %839 #s * #V #L #R % 840 840 [ @(stmt_vars_mp … V) 841 841 #i #t #H cases (Exists_append … H)
Note: See TracChangeset
for help on using the changeset viewer.