Changeset 961 for src/common/IO.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IO.ma

    r879 r961  
    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 sz _ ⇒ bvint sz | 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 sz sg ⇒ λv.EVint sz 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 sz _ ⇒ λv.Vint sz 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)]
     27[ ASTint sz _ ⇒ match ev with
     28  [ EVint sz' i ⇒ if eq_intsize sz sz' then OK ? (Vint sz' i) else Error ? (msg IllTypedEvent)
     29  | _ ⇒ Error ? (msg IllTypedEvent)]
    2830| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
    2931| _ ⇒ Error ? (msg IllTypedEvent)
     
    3335λv,ty.
    3436match ty with
    35 [ ASTint _ _ ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
     37[ ASTint sz _ ⇒ match v with
     38  [ Vint sz' i ⇒ if eq_intsize sz sz' then OK ? (EVint sz' i) else Error ? (msg IllTypedEvent)
     39  | _ ⇒ Error ? (msg IllTypedEvent) ]
    3640| ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
    3741| _ ⇒ Error ? (msg IllTypedEvent)
Note: See TracChangeset for help on using the changeset viewer.