Ignore:
Timestamp:
Apr 4, 2012, 6:48:27 PM (8 years ago)
Author:
campbell
Message:

Enforce typing of constants in front-end, plus binops for RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1874 r1878  
    9696  [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉
    9797  | St_cost cl l ⇒ λH. return 〈Echarge cl, build_state f fs m l ?〉
    98   | St_const r cst l ⇒ λH.
    99       ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
     98  | St_const _ r cst l ⇒ λH.
     99      ! v ← opt_to_res … (msg FailedConstant) (eval_constant ? (find_symbol … ge) (sp f) cst);
    100100      ! locals ← reg_store r v (locals f);
    101101      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     
    296296  [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
    297297  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
    298   | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
     298  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
    299299  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    300300  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
Note: See TracChangeset for help on using the changeset viewer.