Changeset 1647 for src/Clight/Cexec.ma


Ignore:
Timestamp:
Jan 17, 2012, 1:13:08 PM (9 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/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〉
Note: See TracChangeset for help on using the changeset viewer.