Changeset 1878 for src/RTLabs/syntax.ma


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/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.