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.
The following built-in 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.
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.
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:
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.
The dynamic world of ATS has three kind of terms.
After compilation, all linear and propositional proof terms are erased, and the program is left with expressions to be evaluated at run-time when someone executes the program.
Flat array on stack is a bit different.
(TODO: unfinished)