Ignore:
Timestamp:
Jul 24, 2012, 7:40:21 PM (8 years ago)
Author:
campbell
Message:

Add new invariant to Cminor that return typs should be respected.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r2249 r2251  
    1919].
    2020
    21 (* None of the additional code introduces locals or labels. *)
     21(* None of the additional code introduces locals, labels or returns. *)
    2222definition 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 ]).
    2424 
    2525discriminator option.
     
    3838    ]
    3939].
    40 % //
     40% /2/
    4141cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
    42 destruct;/2/
     42destruct;/3/
    4343qed.
    4444
     
    5050     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
    5151  〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init).
    52 [ % //
     52[ % /2/
    5353| 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 ]
    5657] qed.
    5758
    5859definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
    5960λ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 ?? I I)) 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 …)) ]
    6263qed.
    6364
    6465lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
    6566#s elim s //
    66 [ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
     67[ #s1 #s2 #IH1 #IH2 * * * * #_ #_ #_ #H1 #H2 whd in ⊢ (??%?);
    6768  >(IH1 H1) >(IH2 H2) @refl
    6869| #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
    6970  >(IH1 H1) >(IH2 H2) @refl
    70 | #l #s #IH * * #_ *
     71| #l #s #IH * * * #_ *
    7172| #l #s #IH * * #_ #_ #H @(IH H)
    7273] qed.
     
    9596%
    9697[ % [ % // |
    97   @(stmt_P_mp … H) #s * #V #L %
     98  @(stmt_P_mp … H) #s * * #V #L #R %
    9899  [ @(stmt_vars_mp … V) #i #t *
    99100  | @(stmt_labels_mp … L) #l *
     101  | cases s in R ⊢ %; // #x *
    100102  ]
    101103  ]
Note: See TracChangeset for help on using the changeset viewer.