Changeset 879 for src/common/IO.ma


Ignore:
Timestamp:
Jun 3, 2011, 5:35:30 PM (9 years ago)
Author:
campbell
Message:

Refine "AST" types to include size/signedness information.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IO.ma

    r797 r879  
    66
    77definition eventval_type : ∀ty:typ. Type[0] ≝
    8 λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
     8λty. match ty with [ ASTint _ _ ⇒ int | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
    99
    1010definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    11 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
     11λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint _ _ ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
    1212*; qed.
    1313
    1414definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    15 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
     15λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint _ _ ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
    1616*; qed.
    1717
     
    2525λev,ty.
    2626match ty with
    27 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
    28 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
     27[ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
     28| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
    2929| _ ⇒ Error ? (msg IllTypedEvent)
    3030].
     
    3333λv,ty.
    3434match ty with
    35 [ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
    36 | ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
     35[ ASTint _ _ ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
     36| ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
    3737| _ ⇒ Error ? (msg IllTypedEvent)
    3838].
Note: See TracChangeset for help on using the changeset viewer.