Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r2120 r2176  
    3939] qed.
    4040
     41(*
    4142lemma is_pointer_compat_true: ∀b,sp.
    4243  pointer_compat b sp →
     
    4647[ //
    4748| #H' @False_ind @(absurd … H H')
    48 ] qed.
     49] qed.*)
    4950
    5051theorem is_det: ∀p,s,s'.
     
    9293| #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
    9394| #m #f #sz #sz' @refl
     95| #m #ty0 #ty0' #ptr #H1 #H2 cases H1 cases H2 //
     96| #m #sz #sg #ty' #H' cases H' [ #ty'' | #ty'' #n | #tys #ty'' ] whd in ⊢ (??%?);
     97  >intsize_eq_elim_true whd in ⊢ (??%?); cases sz //
     98| #m #ty0 #ty0' #H1 #H2 cases H1 cases H2 //
     99(*
    94100| #m #ty #ty' * #r #b #pc #ofs #r' #H1 #H2 #pc'
    95101    elim H1 in pc ⊢ %; [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]
     
    103109| #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
    104110    whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
     111*)
    105112] qed.
    106113
     
    122129  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?); >intsize_eq_elim_true
    123130    >(eq_bv_false … ne) //
    124   | * #r #b #pc #i #i0 #s %{ true} % //
     131  | *  #b #i #i0 %{ true} % //
    125132  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
    126133  | #sz #sg %{ false} % // whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //
    127   | #r #r' #t %{ false} % //;
     134  | #t %{ false} % //;
    128135  | #s %{ false} % //; whd; >(Feq_zero_true …) //;
    129136  ]
     
    133140#v #ty #H elim H;
    134141  [ #i #is #s #ne whd in ⊢ (??%?); >intsize_eq_elim_true >(eq_bv_false … ne) //;
    135   | * #p #b #i #i0 #s //
     142  | #s //
    136143  | #f #s #ne whd; >(Feq_zero_false … ne) //;
    137144  ]
     
    141148#v #ty #H elim H;
    142149  [ #sz #sg whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //;
    143   | #r #r' #t //;
     150  | #t //;
    144151  | #s whd; >(Feq_zero_true …) //;
    145152  ]
     
    165172    whd in ⊢ (??%?); change with (load_value_of_type' ty m 〈l,off〉) in H2:(??%?);
    166173    >H2 @refl
    167 | #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
     174| #e #ty #l #off #tr #H1 #H2 whd in ⊢ (??%?);
    168175    >(yields_eq ??? H2) whd in ⊢ (??%?);
    169     @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
     176(*    @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd*)
    170177    @refl
    171178| #ty' #sz #sg @refl
     
    221228| #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1
    222229    >e2 @refl
    223 | #e #ty #r #l #pc #ofs #tr #H1 #H2 whd in ⊢ (??%?);
     230| #e #ty #l #ofs #tr #H1 #H2 whd in ⊢ (??%?);
    224231    >(yields_eq ??? H2)
    225232    @refl
     
    262269  (it:∀i,s. P (Tint i s))
    263270  (fl:∀f. P (Tfloat f))
    264   (pt:∀s,t. P t → P (Tpointer s t))
    265   (ar:∀s,t,n. P t → P (Tarray s t n))
     271  (pt:∀t. P t → P (Tpointer t))
     272  (ar:∀t,n. P t → P (Tarray t n))
    266273  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
    267274  (st:∀i,fl. P (Tstruct i fl))
    268275  (un:∀i,fl. P (Tunion i fl))
    269   (cp:∀r,i. P (Tcomp_ptr r i))
     276  (cp:∀i. P (Tcomp_ptr i))
    270277  (nl:Q Tnil)
    271278  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
     
    275282  | Tint i s ⇒ it i s
    276283  | Tfloat s ⇒ fl s
    277   | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
    278   | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
     284  | Tpointer t' ⇒ pt t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
     285  | Tarray t' n ⇒ ar t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
    279286  | Tfunction tl t' ⇒ fn tl t' (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
    280287  | Tstruct i fs ⇒ st i fs
    281288  | Tunion i fs ⇒ un i fs
    282   | Tcomp_ptr r i ⇒ cp r i
     289  | Tcomp_ptr i ⇒ cp i
    283290  ]
    284291and typelist_ind2l
     
    287294  (it:∀i,s. P (Tint i s))
    288295  (fl:∀f. P (Tfloat f))
    289   (pt:∀s,t. P t → P (Tpointer s t))
    290   (ar:∀s,t,n. P t → P (Tarray s t n))
     296  (pt:∀t. P t → P (Tpointer t))
     297  (ar:∀t,n. P t → P (Tarray t n))
    291298  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
    292299  (st:∀i,fl. P (Tstruct i fl))
    293300  (un:∀i,fl. P (Tunion i fl))
    294   (cp:∀r,i. P (Tcomp_ptr r i))
     301  (cp:∀i. P (Tcomp_ptr i))
    295302  (nl:Q Tnil)
    296303  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
Note: See TracChangeset for help on using the changeset viewer.