Changeset 1647 for src/Clight


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
Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1603 r1647  
    350350  match s with
    351351  [ Sassign a1 a2 ⇒
    352     ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
    353     ! 〈v2,tr2〉 ← exec_expr ge e m a2;
     352    ! 〈l,tr1〉 ← exec_lvalue ge e m a1 : IO ???;
     353    ! 〈v2,tr2〉 ← exec_expr ge e m a2 : IO ???;
    354354    ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2);
    355355    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
    356356  | Scall lhs a al ⇒
    357     ! 〈vf,tr2〉 ← exec_expr ge e m a;
    358     ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
     357    ! 〈vf,tr2〉 ← exec_expr ge e m a : IO ???;
     358    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
    359359    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf);
    360360    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
     
    371371         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
    372372         | Some lhs' ⇒
    373            ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
     373           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs' : IO ???;
    374374           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
    375375         ]
     
    390390      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
    391391      | Kdowhile a s' k' ⇒
    392           ! 〈v,tr〉 ← exec_expr ge e m a;
     392          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    393393          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    394394          match b with
     
    406406      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
    407407      | Kdowhile a s' k' ⇒
    408           ! 〈v,tr〉 ← exec_expr ge e m a;
     408          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    409409          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    410410          match b with
     
    426426      ]
    427427  | Sifthenelse a s1 s2 ⇒
    428       ! 〈v,tr〉 ← exec_expr ge e m a;
     428      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    429429      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    430430      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
    431431  | Swhile a s' ⇒
    432       ! 〈v,tr〉 ← exec_expr ge e m a;
     432      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    433433      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    434434      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
     
    438438      match is_Sskip a1 with
    439439      [ inl _ ⇒
    440           ! 〈v,tr〉 ← exec_expr ge e m a2;
     440          ! 〈v,tr〉 ← exec_expr ge e m a2 : IO ???;
    441441          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
    442442          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
     
    453453        [ inl _ ⇒ Wrong ??? (msg ReturnMismatch)
    454454        | inr _ ⇒
    455           ! 〈v,tr〉 ← exec_expr ge e m a;
     455          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    456456          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
    457457        ]
    458458    ]
    459459  | Sswitch a sl ⇒
    460       ! 〈v,tr〉 ← exec_expr ge e m a;
     460      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    461461      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
    462462                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
     
    473473  [ CL_Internal f ⇒
    474474    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
    475       ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
     475      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs : IO ???;
    476476      ret ? 〈E0, State f (fn_body f) k e m2〉
    477477  | CL_External f argtys retty ⇒
    478       ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
     478      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys) : IO ???;
    479479      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
    480480      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
  • 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.