Ignore:
Timestamp:
Aug 3, 2011, 5:18:17 PM (10 years ago)
Author:
campbell
Message:

Label preservation in Cminor initialisation and RTLabs translation
on branch.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

    r1087 r1101  
    1919].
    2020
     21(* None of the additional code introduces locals or labels. *)
     22definition stmt_inv : stmt → Prop ≝
     23  stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s).
     24
    2125(* Produces a few extra skips - hopefully the compiler will optimise these
    2226   away. *)
    2327
    24 definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_vars s (λ_.False)
     28definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s
    2529λid,r,init,off.
    2630match init_expr init with
     
    3135    ]
    3236].
    33 //
     37% //
    3438cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
    3539qed.
     
    4448qed.
    4549
    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 ⊢ (?%?) //
     50lemma sig_stmt_inv : ∀s:Σs:stmt.stmt_inv s.
     51  stmt_inv s.
     52* #s #p @p
    4953qed.
    5054
    51 definition init_var : ident → region → list init_data → Σs:stmt. stmt_vars s (λ_.False)
     55definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s
    5256λid,r,init.
    5357\snd (foldr ??
     
    5559   let 〈off,s〉 ≝ os in
    5660     〈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 ]
    6166] qed.
    6267
    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
     68definition 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 ]
    6772qed.
    6873
    69 definition add_statement : ident → (Σs:stmt. stmt_vars s (λ_.False)) →
     74lemma 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
     86definition add_statement : ident → (Σs:stmt. stmt_inv s) →
    7087                              list (ident × (fundef internal_function)) →
    7188                              list (ident × (fundef internal_function)) ≝
     
    87104          ]
    88105      | 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)
    92114] qed.
    93115
Note: See TracChangeset for help on using the changeset viewer.