Changeset 879 for src/common


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/common
Files:
4 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  ].
  • src/common/Animation.ma

    r797 r879  
    1010λo,ev.
    1111match io_in_typ o return λt. res (eventval_type t) with
    12 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ]
    13 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
     12[ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ]
     13| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
    1414| ASTptr _ ⇒ Error ? (msg IllTypedEvent)
    1515].
  • src/common/Events.ma

    r781 r879  
    193193inductive eventval_match: eventval -> typ -> val -> Prop :=
    194194  | ev_match_int:
    195       ∀i. eventval_match (EVint i) ASTint (Vint i)
     195      ∀i,sz,sg. eventval_match (EVint i) (ASTint sz sg) (Vint i)
    196196  | ev_match_float:
    197       ∀f. eventval_match (EVfloat f) ASTfloat (Vfloat f).
     197      ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f).
    198198
    199199inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
  • src/common/IO.ma

    r797 r879  
    66
    77definition eventval_type : ∀ty:typ. Type[0] ≝
    8 λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
     8λty. match ty with [ ASTint _ _ ⇒ int | 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 ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
     11λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint _ _ ⇒ λv.EVint v | ASTptr r ⇒ ? | 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 ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
     15λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint _ _ ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
    1616*; qed.
    1717
     
    2525λev,ty.
    2626match ty with
    27 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
    28 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
     27[ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
     28| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
    2929| _ ⇒ Error ? (msg IllTypedEvent)
    3030].
     
    3333λv,ty.
    3434match ty with
    35 [ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
    36 | ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
     35[ ASTint _ _ ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
     36| ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
    3737| _ ⇒ Error ? (msg IllTypedEvent)
    3838].
Note: See TracChangeset for help on using the changeset viewer.