Changeset 718 for src/RTLabs


Ignore:
Timestamp:
Mar 29, 2011, 5:54:37 PM (9 years ago)
Author:
campbell
Message:

Add an AST type (i.e., intermediate language type) for pointers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs-sem.ma

    r702 r718  
    106106
    107107definition eventval_type : ∀ty:typ. Type[0] ≝
    108 λty. match ty with [ ASTint ⇒ int | ASTfloat ⇒ float ].
     108λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
    109109
    110110definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    111 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTfloat ⇒ λv.EVfloat v ].
     111λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
     112*; qed.
    112113
    113114definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    114 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTfloat ⇒ λv.Vfloat v ].
     115λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
     116*; qed.
    115117
    116118lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
    117119  eventval_match (mk_eventval ty v) ty (mk_val ty v).
    118 #ty cases ty; normalize; //; qed.
     120#ty cases ty; normalize; //; * *; qed.
    119121
    120122definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
     
    131133[ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
    132134| ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    133 | _ ⇒ Some ? (Error ?)
     135| _ ⇒ Error ?
    134136].
    135137
Note: See TracChangeset for help on using the changeset viewer.