Changeset 1316 for src/Cminor/initialisation.ma
 Timestamp:
 Oct 7, 2011, 12:26:39 PM (9 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src

Property
svn:mergeinfo
set to
/Deliverables/D3.3/idlookupbranch merged eligible

Property
svn:mergeinfo
set to

src/Cminor/initialisation.ma
r1224 r1316 4 4 include "Cminor/syntax.ma". 5 5 include "common/Globalenvs.ma". 6 include "utilities/pair.ma". 7 include "utilities/deppair.ma". 6 8 7 9 (* XXX having to specify the return type in the match is annoying. *) … … 19 21 ]. 20 22 23 (* None of the additional code introduces locals or labels. *) 24 definition stmt_inv : stmt → Prop ≝ 25 stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s). 26 21 27 (* Produces a few extra skips  hopefully the compiler will optimise these 22 28 away. *) 23 29 24 definition init_datum : ident → region → init_data → nat (*offset*) → stmt≝30 definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s ≝ 25 31 λid,r,init,off. 26 32 match init_expr init with … … 31 37 ] 32 38 ]. 39 % // 40 cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/ 41 qed. 33 42 34 definition init_var : ident → region → list init_data → stmt≝43 definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝ 35 44 λid,r,init. 36 45 \snd (foldr ?? … … 38 47 let 〈off,s〉 ≝ os in 39 48 〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉) 40 〈0, St_skip〉 init). 49 〈0, dp ? (λx.stmt_inv x) St_skip ?〉 init). 50 [ % // 51  elim init 52 [ % // 53  #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % //  @(use_sig ? stmt_inv) ]  @IH ] 54 ] qed. 41 55 42 definition init_vars : list (ident × region × (list init_data)) → stmt ≝ 43 λvars. foldr ?? 44 (λvar,s. St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) St_skip vars. 56 definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝ 57 λvars. foldr ? (Σs:stmt. stmt_inv s) 58 (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars. 59 % [ % [ % //  @(use_sig ? stmt_inv) ]  @(use_sig ? stmt_inv) ] 60 qed. 45 61 46 definition add_statement : ident → stmt → 62 lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ]. 63 #s elim s // 64 [ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?) 65 >(IH1 H1) >(IH2 H2) @refl 66  #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?) 67 >(IH1 H1) >(IH2 H2) @refl 68  #s #IH * * #_ #_ #H @(IH H) 69  #s #IH * * #_ #_ #H @(IH H) 70  #l #s #IH * * #_ * 71  #l #s #IH * * #_ #_ #H @(IH H) 72 ] qed. 73 74 definition add_statement : ident → (Σs:stmt. stmt_inv s) → 47 75 list (ident × (fundef internal_function)) → 48 76 list (ident × (fundef internal_function)) ≝ 49 λid,s. 77 λid,s. match s with [ dp s H ⇒ 50 78 map ?? 51 79 (λidf. … … 59 87 (f_vars f) 60 88 (f_stacksize f) 61 (St_seq s (f_body f)))〉 89 (St_seq s (f_body f)) 90 ?)〉 62 91  External f ⇒ 〈id, External ? f〉 (* Error ? *) 63 92 ] 64  inr _ ⇒ 〈id',f'〉 ]). 93  inr _ ⇒ 〈id',f'〉 ]) ]. 94 % 95 [ % [ % //  96 @(stmt_P_mp … H) #s * #V #L % 97 [ @(stmt_vars_mp … V) #i * 98  @(stmt_labels_mp … L) #l * 99 ] 100 ] 101  whd in ⊢ (?(λ_.??(?(λ_.???%)?))?) >(no_labels … H) @(f_inv f) 102 ] qed. 65 103 66 104 definition empty_vars : list (ident × region × (list init_data)) →
Note: See TracChangeset
for help on using the changeset viewer.