Changeset 879 for src/Clight/Csyntax.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/Clight/Csyntax.ma

    r816 r879  
    2525
    2626(* * ** Types *)
    27 
    28 (* * Clight types are similar to those of C.  They include numeric types,
    29   pointers, arrays, function types, and composite types (struct and
    30   union).  Numeric types (integers and floats) fully specify the
    31   bit size of the type.  An integer type is a pair of a signed/unsigned
    32   flag and a bit size: 8, 16 or 32 bits. *)
    33 
    34 inductive signedness : Type[0] ≝
    35   | Signed: signedness
    36   | Unsigned: signedness.
    37 
    38 inductive intsize : Type[0] ≝
    39   | I8: intsize
    40   | I16: intsize
    41   | I32: intsize.
    42 
    43 (* * Float types come in two sizes: 32 bits (single precision)
    44   and 64-bit (double precision). *)
    45 
    46 inductive floatsize : Type[0] ≝
    47   | F32: floatsize
    48   | F64: floatsize.
    4927
    5028(* * The syntax of type expressions.  Some points to note:
     
    891869definition typ_of_type : type → typ ≝ λt.
    892870  match t with
    893   [ Tfloat _ ⇒ ASTfloat
    894   | _ ⇒ ASTint
     871  [ Tvoid ⇒ ASTint I32 Unsigned
     872  | Tint sz sg ⇒ ASTint sz sg
     873  | Tfloat sz ⇒ ASTfloat sz
     874  | Tpointer r _ ⇒ ASTptr r
     875  | Tarray r _ _ ⇒ ASTptr r
     876  | Tfunction _ _ ⇒ ASTptr Code
     877  | _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *)
    895878  ].
    896879
     
    898881  match t with
    899882  [ Tvoid ⇒ None ?
    900   | Tfloat _ ⇒ Some ? ASTfloat
    901   | _ ⇒ Some ? ASTint
     883  | Tint sz sg ⇒ Some ? (ASTint sz sg)
     884  | Tfloat sz ⇒ Some ? (ASTfloat sz)
     885  | Tpointer r _ ⇒ Some ? (ASTptr r)
     886  | Tarray r _ _ ⇒ Some ? (ASTptr r)
     887  | Tfunction _ _ ⇒ Some ? (ASTptr Code)
     888  | _ ⇒ None ? (* structs and unions shouldn't be converted? *)
    902889  ].
    903890
Note: See TracChangeset for help on using the changeset viewer.