Changeset 2176 for src/common/IO.ma


Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (8 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IO.ma

    r961 r2176  
    66
    77definition eventval_type : ∀ty:typ. Type[0] ≝
    8 λty. match ty with [ ASTint sz _ ⇒ bvint sz | 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 sz sg ⇒ λv.EVint sz 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 ⇒ ? | 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 sz _ ⇒ λv.Vint sz 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 ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
    1616*; qed.
    1717
Note: See TracChangeset for help on using the changeset viewer.