 Timestamp:
 Aug 3, 2011, 5:18:17 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/Cminor/initialisation.ma
r1087 r1101 19 19 ]. 20 20 21 (* None of the additional code introduces locals or labels. *) 22 definition stmt_inv : stmt → Prop ≝ 23 stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s). 24 21 25 (* Produces a few extra skips  hopefully the compiler will optimise these 22 26 away. *) 23 27 24 definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_ vars s (λ_.False)≝28 definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s ≝ 25 29 λid,r,init,off. 26 30 match init_expr init with … … 31 35 ] 32 36 ]. 33 //37 % // 34 38 cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/ 35 39 qed. … … 44 48 qed. 45 49 46 lemma sig_stmt_ vars : ∀P:ident → Prop. ∀s:Σs:stmt.stmt_vars s P.47 stmt_ vars s P.48 #P * #s #p whd in ⊢ (?%?) // 50 lemma sig_stmt_inv : ∀s:Σs:stmt.stmt_inv s. 51 stmt_inv s. 52 * #s #p @p 49 53 qed. 50 54 51 definition init_var : ident → region → list init_data → Σs:stmt. stmt_ vars s (λ_.False)≝55 definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝ 52 56 λid,r,init. 53 57 \snd (foldr ?? … … 55 59 let 〈off,s〉 ≝ os in 56 60 〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉) 57 〈0, dp ? (λx.stmt_vars x (λ_.False)) St_skip ?〉 init). 58 [ whd // 59  elim init whd // 60 #h #t #IH whd in ⊢ (?(???%)?) @sndredex whd % [ @sig_stmt_vars  @IH ] 61 〈0, dp ? (λx.stmt_inv x) St_skip ?〉 init). 62 [ % // 63  elim init 64 [ % // 65  #h #t #IH whd in ⊢ (?(???%)) @sndredex % [ % [ % //  @sig_stmt_inv ]  @IH ] 61 66 ] qed. 62 67 63 definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_ vars s (λ_.False)≝64 λvars. foldr ? (Σs:stmt. stmt_ vars s (λ_.False))65 (λvar,s. dp ? (λx.stmt_ vars x (λ_.False)) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_vars x (λ_.False)) St_skip I) vars.66 whd % @sig_stmt_vars 68 definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_inv s ≝ 69 λvars. foldr ? (Σs:stmt. stmt_inv s) 70 (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars. 71 % [ % [ % //  @sig_stmt_inv ]  @sig_stmt_inv ] 67 72 qed. 68 73 69 definition add_statement : ident → (Σs:stmt. stmt_vars s (λ_.False)) → 74 lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ]. 75 #s elim s // 76 [ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?) 77 >(IH1 H1) >(IH2 H2) @refl 78  #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?) 79 >(IH1 H1) >(IH2 H2) @refl 80  #s #IH * * #_ #_ #H @(IH H) 81  #s #IH * * #_ #_ #H @(IH H) 82  #l #s #IH * * #_ * 83  #l #s #IH * * #_ #_ #H @(IH H) 84 ] qed. 85 86 definition add_statement : ident → (Σs:stmt. stmt_inv s) → 70 87 list (ident × (fundef internal_function)) → 71 88 list (ident × (fundef internal_function)) ≝ … … 87 104 ] 88 105  inr _ ⇒ 〈id',f'〉 ]) ]. 89 whd % 90 [ @(stmt_vars_mp … H) #i * 91  // 106 % 107 [ % [ % //  108 @(stmt_P_mp … H) #s * #V #L % 109 [ @(stmt_vars_mp … V) #i * 110  @(stmt_labels_mp … L) #l * 111 ] 112 ] 113  whd in ⊢ (?(λ_.??(?(λ_.???%)?))?) >(no_labels … H) @(f_inv f) 92 114 ] qed. 93 115
Note: See TracChangeset
for help on using the changeset viewer.