This guide gives an overview about manipulating flat memory data structure in ATS. The types of flat memory supported by ATS have the t@ype sort.
Flat type and size
The following builtin primitive types have the sort t@ype and are all flat: bool, char, double, int, uint, size_t and void. In addition, ATS supports flat data structure types for tuple, record, and array.
t@ype 
Type 
Tuple 
@(t_{1}, t_{2}, ... t_{n}) 
Record 
@{lab_{1} = t_{1}, lab_{2}= t_{2}, ... lab_{n}= t_{n}} 
Array

@[t][n]

Every t@ype has an associated size information, but the size information is unknown to the ATS compiler. The static sizeof(t) function (where t is a t@ype or a viewt@ype) gives you the unique static variable of the int sort, assigned to represent the size of t. The dynamic "{t:viewt@ype} sizeof()" function (which is a template function parameterized by t@ype or viewt@ype t) gives you an integer indexed by the static variable associated with static sizeof(t). It is possible to write "sif sizeof(t) == 4 then ... else ..." or "assert {t} sizeof() == 4" to make assumption about the size of t, but in general the size of any t@ype is unknown to us.
View of memory region
Flat t@ype on its own isn't very useful. If anything, it describes just the layout of memory but doesn't tell you anything else. In particular, it doesn't tell you:
 If we do own a piece of memory with that layout.
 The address of the memory.
 Whether the memory is wellaligned.
 How the memory is allocated: from the garbage collector, malloc(), shmget()/shmat(), mmap(), or even on the stack.
Terminology
The dynamic world of ATS has three kind of terms.
 A type (also t@ype, viewt@ype) characterizes an expression.
 A view characterizes a linear proof term.
 A prop characterizes a propositional proof term.
After compilation, all linear and propositional proof terms are erased, and the program is left with expressions to be evaluated at runtime when someone executes the program.
Terminology
The dynamic world of ATS has three kind of terms.
 A type (also t@ype, viewt@ype) characterizes an expression.
 A view characterizes a linear proof term.
 A prop characterizes a propositional proof term.
After compilation, all linear and propositional proof terms are erased, and the program is left with expressions to be evaluated at runtime when someone executes the program.
In order to access flat memory, we need two pieces of information: a proof of the view "t @ l", which states that we have type t at memory location l, and a value of type "ptr l", which is a pointer pointing to memory location l.
Typically, each heap allocator will also give you a linear proof of an abstract view of the sort "addr > view" which testifies that location l:addr is allocated by that allocator. This way, the memory allocated from one heap cannot be freed to another heap.
To allocate flat data structure on stack, ATS introduces a new form of "var" binding.
t@ype 
Expression 
Type 
Tuple 
@(e_{1}, e_{2}, ... e_{n}) 
@(t_{1}, t_{2}, ... t_{n}) 
Record 
@{lab_{1} = e_{1}, lab_{2} = e_{2}, ... lab_{n}= e_{n}} 
@{lab_{1} = t_{1}, lab_{2}= t_{2}, ... lab_{n}= t_{n}} 
Flat array on stack is a bit different.
t@ype 
Syntax 
Binding 
Array
(single initializer)

var !p with pf = @[t][n](e)

p:ptr l pf:@[t][n] @ l

Array
(uninitialized) 
var !p with pf = @[vt][n]() 
p:ptr l pf:@[vt?][n] @ l

(TODO: unfinished)