Ignore:
Timestamp:
Jan 17, 2012, 1:13:08 PM (8 years ago)
Author:
tranquil
Message:
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1545 r1647  
    106106    cut (type_region ty s);
    107107    [ cases ty in es:(??%?) ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
    108         whd in e:(??%?); destruct; //;
     108        whd in e:(??%%); destruct; //;
    109109    | #Hty
    110110        cut (type_region ty' s');
    111111        [ cases ty' in es' ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
    112             whd in e:(??%?); destruct; //;
     112            whd in e:(??%%); destruct; //;
    113113        | #Hty'
    114114            cut (s = ptype ptr). elim (eq_region_dec (ptype ptr) s) in eu; //; normalize; #_ #e destruct.
    115115            #e >e in Hty; #Hty
    116116            cases (pointer_compat_dec (pblock ptr) s') in e''';
    117             #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/
     117            #Hcompat #e''' whd in e''':(??%%); destruct /2 by cast_pp/
    118118        ]
    119119    ]
     
    207207    ]
    208208| #ty #e #He whd in ⊢ (???%);
    209     @bind2_OK #v cases v // * #r #l #pc #ofs #tr #Hv whd
     209    @bind2_OK #v cases v / by / * #r #l #pc #ofs #tr #Hv whd
    210210    >Hv in He; #He
    211211    @eval_Ederef [ 3: @He | *: skip ]
     
    505505    whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))
    506506    @(P_res_to_P … (exec_bind_parameters_sound …) BIND)
    507   | #id #argtys #rty @res_bindIO_OK #evs #Hevs
    508     @bindIO_OK #eres whd;
     507  | #id #argtys #rty @res_bindIO_OK #evs #Hevs #v'
     508    @bindIO_OK #eres whd
    509509    @step_external_function % [ @(P_res_to_P … (check_eventval_list_sound …) Hevs)
    510510                              | @mk_val_correct ]
     
    536536  [ whd; %
    537537  | @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s';
    538       [ #f #s #k #e #m | #fd #args #k #m | #r #k #m ]
    539       whd in ⊢ (? → ?????(??????%?));
    540       cases m; #mc #mn #mp #Hstep
    541       whd in ⊢ (?????(??????%?));
     538      [ #f #s #k #e #m | #fd #args #k #m | #r #k #m ] normalize
     539(*      whd in ⊢ (? → ?????(??????%?)); *)
     540      cases m; #mc #mn #mp #Hstep normalize
     541(*      whd in ⊢ (?????(??????%?));*)
    542542      @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps
    543543      whd; @(star_step ????????? Hsteps) [ 2,5,8: @Hstep | 3,6,9: // ]
Note: See TracChangeset for help on using the changeset viewer.