Ignore:
Timestamp:
Oct 7, 2011, 12:26:39 PM (9 years ago)
Author:
campbell
Message:

Merge in id-lookup-branch to trunk.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src

  • src/Cminor/initialisation.ma

    r1224 r1316  
    44include "Cminor/syntax.ma".
    55include "common/Globalenvs.ma".
     6include "utilities/pair.ma".
     7include "utilities/deppair.ma".
    68
    79(* XXX having to specify the return type in the match is annoying. *)
     
    1921].
    2022
     23(* None of the additional code introduces locals or labels. *)
     24definition stmt_inv : stmt → Prop ≝
     25  stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s).
     26
    2127(* Produces a few extra skips - hopefully the compiler will optimise these
    2228   away. *)
    2329
    24 definition init_datum : ident → region → init_data → nat (*offset*) → stmt
     30definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s
    2531λid,r,init,off.
    2632match init_expr init with
     
    3137    ]
    3238].
     39% //
     40cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
     41qed.
    3342
    34 definition init_var : ident → region → list init_data → stmt
     43definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s
    3544λid,r,init.
    3645\snd (foldr ??
     
    3847   let 〈off,s〉 ≝ os in
    3948     〈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.
    4155
    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.
     56definition 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) ]
     60qed.
    4561
    46 definition add_statement : ident → stmt →
     62lemma 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
     74definition add_statement : ident → (Σs:stmt. stmt_inv s) →
    4775                              list (ident × (fundef internal_function)) →
    4876                              list (ident × (fundef internal_function)) ≝
    49 λid,s.
     77λid,s. match s with [ dp s H ⇒
    5078  map ??
    5179    (λidf.
     
    5987                                           (f_vars f)
    6088                                           (f_stacksize f)
    61                                            (St_seq s (f_body f)))〉
     89                                           (St_seq s (f_body f))
     90                                           ?)〉
    6291          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
    6392          ]
    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.
    65103
    66104definition empty_vars : list (ident × region × (list init_data)) →
Note: See TracChangeset for help on using the changeset viewer.