Re: [ats-lang-users] Dissecting compound views

[Hongwei Xi <hw...@cs...>]

On Thu, 28 Oct 2010, Matthias Berndt wrote:

>>Hi, 
>>
>>> Say I have the view [(int, float) @ l]. Is it possible to break it
>>> down into [int @ l] and [float @ (l+sizeof int)]?
>>
>>If you consider the case of [(byte, int) @ l], then the int can't be at 
>>l+sizeof byte, because it has to be aligned on a four byte boundary. 
>>
>>It may still be possible to split this up in some other way though, perhaps 
>>there is an ATS variant of C's offsetof macro. 

If you have pf: (int, float) @ l, you can assume that pf contains proofs
pf1: int @ l1 and pf2: int @ l2. The relation between l, l1 and l2 is
not explicitly stated in ATS. More precisely, you have the following
proof function (lemma):

{a,b:t@ype}
(a, b) @ l -> [l1,l2:addr] (a @ l1, b @ l2, (a @ l1, b @ l2) -> (a, b) @ l)

The part (a@l1, b@l2) -> (a, b) @ l essentially refers to some possible padding
done by a C compiler.

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hw...@cs...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)