Ignore:
Timestamp:
Feb 11, 2011, 4:45:36 PM (9 years ago)
Author:
campbell
Message:

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r496 r498  
    118118
    119119(* Use to narrow down the choice of expression to just the lvalues. *)
    120 lemma lvalue_expr: ∀ge,env,m,e,ty,sp,l,ofs,tr. ∀P:expr_descr → Prop.
    121   eval_lvalue ge env m (Expr e ty) sp l ofs tr →
     120lemma lvalue_expr: ∀ge,env,m,e,ty,l,ofs,tr. ∀P:expr_descr → Prop.
     121  eval_lvalue ge env m (Expr e ty) l ofs tr →
    122122  (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) →
    123123  P e.
    124 #ge #env #m #e #ty #sp #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
     124#ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
    125125[ #id #l #ty #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
    126126| #id #sp #l #ty #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
    127127| #e #ty #sp #l #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
    128 | #e #id #ty #sp #l #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
    129 | #e #id #ty #sp #l #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
     128| #e #id #ty #l #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
     129| #e #id #ty #l #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
    130130] qed.
    131131
     
    159159lemma expr_lvalue_complete: ∀ge,env,m.
    160160(∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉)) ∧
    161 (∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)).
     161(∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)).
    162162#ge #env #m
    163163@(combined_expr_lvalue_ind ge env m
    164164  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
    165   (λe,sp,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)));
     165  (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
    166166[ #i #ty @refl
    167167| #f #ty @refl
    168 | #e #ty #sp #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
     168| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
    169169    [ #id | #e' | #e' #id ] #H3
    170170    whd in ⊢ (??%?);
     
    224224  (* lvalues *)
    225225| #id #l #ty #e1 whd in ⊢ (??%?); >e1 @refl
    226 | #id #sp #l #ty #e1 #e2 whd in ⊢ (??%?); >e1
     226| #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1
    227227    >e2 @refl
    228 | #e #ty #sp #l #ofs #tr #H1 #H2 whd in ⊢ (??%?);
     228| #e #ty #r #l #ofs #tr #H1 #H2 whd in ⊢ (??%?);
    229229    >(yields_eq ??? H2)
    230230    @refl
    231 | #e #i #ty #sp #l #ofs #id #fList #delta #tr #H1 #H2 #H3 #H4 cases e in H2 H4 ⊢ %;
     231| #e #i #ty #l #ofs #id #fList #delta #tr #H1 #H2 #H3 #H4 cases e in H2 H4 ⊢ %;
    232232    #e' #ty' #H2 whd in H2:(??%?); >H2 #H4 whd in ⊢ (??%?);
    233233    >(yields_eq ??? H4) whd in ⊢ (??%?);
    234234    >H3 @refl
    235 | #e #i #ty #sp #l #ofs #id #fList #tr cases e; #e' #ty' #H1 #H2
     235| #e #i #ty #l #ofs #id #fList #tr cases e; #e' #ty' #H1 #H2
    236236    whd in H2:(??%?); >H2 #H3 whd in ⊢ (??%?);
    237237    >(yields_eq ??? H3) @refl
     
    253253
    254254theorem lvalue_complete: ∀ge,env,m.
    255  ∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉).
     255 ∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉).
    256256#ge #env #m elim (expr_lvalue_complete ge env m); /2/; qed.
    257257
     
    363363  step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉.
    364364#ge #s #tr #s' #H elim H;
    365 [ #f #e #e1 #k #e2 #m #sp #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
     365[ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
    366366    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
    367367    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
     
    373373    >H4 elim (assert_type_eq_true (fun_typeof e)); #pty #ety >ety
    374374    @refl
    375 | #f #el #ef #eargs #k #env #m #sp #loc #ofs #vf #vargs #f' #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
     375| #f #el #ef #eargs #k #env #m #loc #ofs #vf #vargs #f' #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
    376376    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
    377377    >(yields_eq ??? (exprlist_complete … H3)) whd in ⊢ (??%?);
     
    455455    @refl
    456456| #v #f #env #k #m @refl
    457 | #v #f #env #k #m1 #m2 #sp #loc #ofs #ty #H whd in ⊢ (??%?);
     457| #v #f #env #k #m1 #m2 #loc #ofs #ty #H whd in ⊢ (??%?);
    458458    >H @refl
    459459| #f #l #s #k #env #m @refl
Note: See TracChangeset for help on using the changeset viewer.