Changeset 879 for src/common/AST.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/common/AST.ma

    r849 r879  
    7878λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    7979
    80 (* * The intermediate languages are weakly typed, using only three types:
    81   [ASTint] for integers, [ASTptr] for pointers, and [ASTfloat] for floating-point
    82   numbers. *)
     80(* We maintain some reasonable type information through the front end of the
     81   compiler. *)
     82
     83inductive signedness : Type[0] ≝
     84  | Signed: signedness
     85  | Unsigned: signedness.
     86
     87inductive intsize : Type[0] ≝
     88  | I8: intsize
     89  | I16: intsize
     90  | I32: intsize.
     91
     92(* * Float types come in two sizes: 32 bits (single precision)
     93  and 64-bit (double precision). *)
     94
     95inductive floatsize : Type[0] ≝
     96  | F32: floatsize
     97  | F64: floatsize.
    8398
    8499inductive typ : Type[0] ≝
    85   | ASTint : typ
     100  | ASTint : intsize → signedness → typ
    86101  | ASTptr : region → typ
    87   | ASTfloat : typ.
     102  | ASTfloat : floatsize → typ.
    88103
    89104(* XXX aliases *)
    90105definition SigType ≝ typ.
    91 definition SigType_Int ≝ ASTint.
     106definition SigType_Int ≝ ASTint I32 Unsigned.
    92107(*
    93108| SigType_Float: SigType
     
    95110definition SigType_Ptr ≝ ASTptr Any.
    96111
    97 
    98 (* FIXME: ASTint size is not 1 for Clight32 *)
     112definition size_intsize : intsize → nat ≝
     113λsz. match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4].
     114
     115definition size_floatsize : floatsize → nat ≝
     116λsz. match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ].
     117
    99118definition typesize : typ → nat ≝ λty.
    100   match ty with [ ASTint ⇒ 1 | ASTptr r ⇒ size_pointer r | ASTfloat ⇒ 8 ].
     119  match ty with
     120  [ ASTint sz _ ⇒ size_intsize sz
     121  | ASTptr r ⇒ size_pointer r
     122  | ASTfloat sz ⇒ size_floatsize sz ].
    101123
    102124lemma typesize_pos: ∀ty. typesize ty > 0.
    103 #ty cases ty [ 2: * ] /2/ qed.
     125* *; try * /2/ qed.
    104126
    105127lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    106 #t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed.
     128* * * *; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed.
    107129
    108130lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
     
    132154definition proj_sig_res : signature → typ ≝ λs.
    133155  match sig_res s with
    134   [ None ⇒ ASTint
     156  [ None ⇒ ASTint I32 Unsigned
    135157  | Some t ⇒ t
    136158  ].
Note: See TracChangeset for help on using the changeset viewer.