Changeset 127 for C-semantics/Csyntax.ma


Ignore:
Timestamp:
Sep 24, 2010, 10:31:34 AM (10 years ago)
Author:
campbell
Message:

Allow the storage of pointers in suitably large integers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csyntax.ma

    r126 r127  
    437437(* * Size of a type, in bytes. *)
    438438
     439ndefinition sizeof_pointer : memory_space → Z ≝
     440λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     441
    439442nlet rec sizeof (t: type) : Z ≝
    440443  match t return λ_.Z with
     
    442445  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    443446  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    444   | Tpointer sp _ ⇒ match sp with [ Data ⇒ 1 | IData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 4 ]
     447  | Tpointer sp _ ⇒ sizeof_pointer sp
    445448  | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
    446449  | Tfunction _ _ ⇒ 1
Note: See TracChangeset for help on using the changeset viewer.