Changeset 1878 for src/RTLabs


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.

Location:
src/RTLabs
Files:
2 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 % %
  • src/RTLabs/syntax.ma

    r1872 r1878  
    1212| St_skip : label → statement
    1313| St_cost : costlabel → label → statement
    14 | St_const : register → constant → label → statement
    15 | St_op1 : ∀t,t'. unary_operation t' t → register → register → label → statement (* destination source *)
    16 | St_op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → register → register → register → label → statement (* destination source1 source2 *)
     14| St_const : ∀t. register → constant t → label → statement
     15| St_op1 : ∀t',t. unary_operation t t' → register → register → label → statement (* destination source *)
     16| St_op2 : ∀t',t1,t2. binary_operation t1 t2 t' → register → register → register → label → statement (* destination source1 source2 *)
    1717| St_load : typ → register → register → label → statement
    1818| St_store : typ → register → register → label → statement
     
    3333definition statement_typed : list (register × typ) → statement → Prop ≝
    3434λe,s. match s with
    35 [ St_op1 t t' _ r r' _ ⇒ env_has e r t ∧ env_has e r' t'
     35[ St_const t r _ _ ⇒ env_has e r t
     36| St_op1 t' t _ r' r _ ⇒ env_has e r' t' ∧ env_has e r t
     37| St_op2 t' t1 t2 _ r' r1 r2 _ ⇒ env_has e r1 t1 ∧ env_has e r2 t2 ∧ env_has e r' t'
    3638| _ ⇒ True
    3739].
     
    4143[ St_skip l ⇒ P l
    4244| St_cost _ l ⇒ P l
    43 | St_const _ _ l ⇒ P l
     45| St_const _ _ _ l ⇒ P l
    4446| St_op1 _ _ _ _ _ l ⇒ P l
    4547| St_op2 _ _ _ _ _ _ _ l ⇒ P l
Note: See TracChangeset for help on using the changeset viewer.