Changeset 879 for src/Clight


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

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

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r797 r879  
    440440    #H1 #H2
    441441    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
    442     whd; inversion H2; #x #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
     442    whd; inversion H2; #x #sz [ #sg ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
    443443    @refl
    444444| #v #f #env #k #m @refl
  • src/Clight/CexecSound.ma

    r797 r879  
    365365  [ //
    366366  | #ty #tys whd in ⊢ (???%)
    367     cases ty cases v // #v'
     367    cases ty cases v // #v' #sz try #sg
    368368    @bind_OK #evs #CHECK
    369369    @(evl_match_cons ??????? (P_res_to_P … CHECK)) //
  • 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.