Changeset 1369 for src/common/Values.ma


Ignore:
Timestamp:
Oct 14, 2011, 10:56:45 AM (9 years ago)
Author:
campbell
Message:

Put type information into front-end unary ops.
Slight change to semantics: booleans produced by Onotbool can be any given
integer size.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Values.ma

    r1347 r1369  
    4949definition Vtrue: val ≝ Vone I32.
    5050definition Vfalse: val ≝ Vzero I32.
     51
     52inductive val_typ : val → typ → Prop ≝
     53  | VTint: ∀sz,sg,i. val_typ (Vint sz i) (ASTint sz sg)
     54  | VTfloat: ∀sz,f. val_typ (Vfloat f) (ASTfloat sz)
     55  | VTnull: ∀r. val_typ (Vnull r) (ASTptr r)
     56  | VTptr: ∀r,b,c,o. val_typ (Vptr r b c o) (ASTptr r).
    5157
    5258(*
Note: See TracChangeset for help on using the changeset viewer.