Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1510 r1516  
    66cases v; [ | #sz #i | #f | #r1 | #r' #b #pc #of ]
    77cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
    8 whd in ⊢ (??%? → ?)
     8whd in ⊢ (??%? → ?);
    99[ 2: @intsize_eq_elim_elim
    1010  [ #NE #H destruct
     
    1515  ]
    1616| 8: #H cases (eq_dec f Fzero)
    17   [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
    18   | #ne >Feq_zero_false in H // #E destruct @bool_of_val_true @is_true_float @ne
     17  [ #e >e in H ⊢ %; >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
     18  | #ne >Feq_zero_false in H; // #E destruct @bool_of_val_true @is_true_float @ne
    1919  ]
    2020| 14: #H destruct @bool_of_val_false @is_false_pointer
     
    3535lemma try_cast_null_sound: ∀m,sz,i,ty,ty',v'. try_cast_null m sz i ty ty' = OK ? v' → cast m (Vint sz i) ty ty' v'.
    3636#m #sz #i #ty #ty' #v'
    37 whd in ⊢ (??%? → ?)
     37whd in ⊢ (??%? → ?);
    3838@eq_bv_elim
    3939[ #e >e
     
    5555  | 7,8,9: #a #b #H whd in H:(??%?); destruct;
    5656  | #sz1 #si1 cases ty';
    57     [ whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     57    [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    5858      [ #NE #H destruct
    5959      | *; whd #H whd in H:(??%?); destruct;
    6060      ]
    61     | 3: #a whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     61    | 3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    6262      [ #E #H whd in H:(??%?); destruct
    6363      | *; whd #H whd in H:(??%?); destruct; @cast_if
    6464      ]
    65     | 2,7,8,9: #a #b whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     65    | 2,7,8,9: #a #b whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    6666      [ 1,3,5,7: #NE #H destruct
    6767      | *: *; whd #H whd in H:(??%?); destruct; //
     
    7070                 | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
    7171                 | #args #rty letin t ≝ (Tfunction args rty) ]
    72         whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     72        whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    7373        [ 1,3,5: #NE #H destruct
    7474        | *: *; whd
     
    100100    cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
    101101    @cast_pp_z //;
    102 | #r #b #pc #of whd in ⊢ (??%? → ?) #e
     102| #r #b #pc #of whd in ⊢ (??%? → ?); #e
    103103    elim (bind_inversion ????? e) #s * #es #e'
    104104    elim (bind_inversion ????? e') #u * #eu #e'' -e';
     
    113113        | #Hty'
    114114            cut (s = r). elim (eq_region_dec r s) in eu; //; normalize; #_ #e destruct.
    115             #e >e in Hty #Hty
    116             cases (pointer_compat_dec b s') in e'''
     115            #e >e in Hty; #Hty
     116            cases (pointer_compat_dec b s') in e''';
    117117            #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/
    118118        ]
     
    190190(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
    191191#ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
    192 [ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%)
     192[ #sz #ty #c whd in ⊢ (???%); cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%);
    193193  @eq_intsize_elim #E try @I <E whd %
    194194| #ty #c whd //
     
    197197    @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
    198198    @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl)
    199     >H in He' #He' @He'
     199    >H in He'; #He' @He'
    200200| #v #ty
    201201    whd in ⊢ (???%);
    202202    lapply (refl ? (lookup SymbolTag block en v))
    203     cases (lookup SymbolTag block en v) in ⊢ (???% → %)
     203    cases (lookup SymbolTag block en v) in ⊢ (???% → %);
    204204    [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
    205205        whd; @(eval_Evar_global … eget efind)
    206206    | #loc #eget @(eval_Evar_local … eget)
    207207    ]
    208 | #ty #e #He whd in ⊢ (???%)
     208| #ty #e #He whd in ⊢ (???%);
    209209    @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd
    210     >Hv in He #He
     210    >Hv in He; #He
    211211    @eval_Ederef [ 3: @He | *: skip ]
    212212| #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
    213213  cases ty // * #pty
    214   cases loc in H ⊢ % * #loc' #H
     214  cases loc in H ⊢ %; * #loc' #H
    215215  whd try @I
    216   @eval_Eaddrof whd in H:(??%?) >H in He'' #He'' @He''
     216  @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He''
    217217| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
    218218    @opt_bind_OK #v #ev
    219219    @(eval_Eunop … ev)
    220     >Hv1 in He1 #He1 @He1
     220    >Hv1 in He1; #He1 @He1
    221221| #ty #op #e1 #e2 #He1 #He2
    222     @bind2_OK #v1 #tr1 #ev1 >ev1 in He1 #He1
    223     @bind2_OK #v2 #tr2 #ev2 >ev2 in He2 #He2
     222    @bind2_OK #v1 #tr1 #ev1 >ev1 in He1; #He1
     223    @bind2_OK #v2 #tr2 #ev2 >ev2 in He2; #He2
    224224    @opt_bind_OK #v #ev whd in He1 He2; whd;
    225225    @(eval_Ebinop … He1 He2 ev)
    226226| #ty #ty' #e' #He'
    227     @bind2_OK #v #tr #Hv >Hv in He' #He'
     227    @bind2_OK #v #tr #Hv >Hv in He'; #He'
    228228    @bind_OK #v' #ev'
    229229    @(eval_Ecast … He' ?)
     
    231231    @(exec_cast_sound … ev')
    232232| #ty #e1 #e2 #e3 #He1 #He2 #He3
    233     @bind2_OK #vb #tr1 #Hvb >Hvb in He1 #He1
     233    @bind2_OK #vb #tr1 #Hvb >Hvb in He1; #He1
    234234    @bind_OK #b
    235235    cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
    236     @bind2_OK #v #tr #Hv whd in Hv:(??%?)
    237     [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%;
     236    @bind2_OK #v #tr #Hv whd in Hv:(??%?);
     237    [ >Hv in He2; #He2 whd in He2 Hv:(??%?) ⊢%;
    238238        @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb)
    239     | >Hv in He3 #He3 whd in He3 Hv:(??%?) ⊢%;
     239    | >Hv in He3; #He3 whd in He3 Hv:(??%?) ⊢%;
    240240        @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb)
    241241    ]
    242242| #ty #e1 #e2 #He1 #He2
    243     @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
     243    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
    244244    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
    245     [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
     245    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
    246246        @bind_OK #b2 #eb2
    247247        @(eval_Eandbool_2 … He1 … He2)
     
    250250    ]
    251251| #ty #e1 #e2 #He1 #He2
    252     @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
     252    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
    253253    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
    254254    [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1)
    255     | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
     255    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
    256256        @bind_OK #b2 #eb2
    257257        @(eval_Eorbool_2 … He1 … He2)
     
    261261| #ty #e' #ty' #i cases ty'; //;
    262262    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
    263         @bind_OK #delta #Hdelta whd in H:(??%?) >H in He' #He'
     263        @bind_OK #delta #Hdelta whd in H:(??%?); >H in He'; #He'
    264264        @(eval_Efield_struct …  He' (refl ??) Hdelta)
    265     | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?)
    266         >H in He' #He'
     265    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?);
     266        >H in He'; #He'
    267267        @(eval_Efield_union … He' (refl ??))
    268268    ]
    269 | #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He' #He'
     269| #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He'; #He'
    270270    @(eval_Ecost … He')
    271271(* exec_lvalue fails on non-lvalues. *)
     
    280280#ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
    281281[ 1,2,5: #a #b #c #H @False_ind destruct (H);
    282 | #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1 #H1 @False_ind
     282| #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind
    283283    @(eval_lvalue_inv_ind … H1)
    284284    [ #a #b #c #d #bad destruct (bad);
     
    304304exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
    305305exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr r (mk_block r loc) (same_compat ??) off, tr〉.
    306 #ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?)
    307 >H whd in ⊢ (??%?) cases r @refl
     306#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
     307>H whd in ⊢ (??%?); cases r @refl
    308308qed.
    309309
     
    312312#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
    313313cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    314 [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ % #locr #loci #H
     314[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H
    315315    @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ]
    316316    lapply (addrof_exec_lvalue … H) #H'
     
    350350| * #id #ty #t #IH #en #m #en' #m'
    351351  lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
    352   whd in EXEC:(??%?) ALLOC:(???%)
     352  whd in EXEC:(??%?) ALLOC:(???%);
    353353 @(alloc_variables_cons … ALLOC)
    354354 @IH @EXEC
     
    365365      @opt_bind_OK #m' #STORE
    366366      lapply (refl ? (exec_bind_parameters en m' ps' vs))
    367       cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #msg #_ %]
     367      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %); [2: #msg #_ %]
    368368      #m'' #BIND
    369369      @(bind_parameters_cons … GET STORE)
    370       lapply (IH vs en m') whd in ⊢ (% → ?) >BIND //
     370      lapply (IH vs en m') whd in ⊢ (% → ?); >BIND //
    371371    ]
    372372] qed.
     
    378378| #v #vs #IH *
    379379  [ //
    380   | #ty #tys whd in ⊢ (???%)
     380  | #ty #tys whd in ⊢ (???%);
    381381    cases ty [ #sz #sg | #sz | #r ] cases v //
    382     [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?)
     382    [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?);
    383383      @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct
    384384    | #v ] @bind_OK #evs #CHECKevs
     
    498498  ]
    499499| #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
    500   [ #fn whd in ⊢ (?????%)
     500  [ #fn whd in ⊢ (?????%);
    501501    lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)))
    502     cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %)
    503     #en' #m' #ALLOC whd in ⊢ (?????%)
     502    cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %);
     503    #en' #m' #ALLOC whd in ⊢ (?????%);
    504504    @res_bindIO_OK #m2 #BIND
    505505    whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))
Note: See TracChangeset for help on using the changeset viewer.