@@ -124,9 +124,9 @@ Idris has two heaps where objects can be allocated:
124124| collecting garbage, modifying data, | |
125125| registering managed pointers, etc.) | |
126126+--------------------------------------+---------------------------------------+
127−| Contains objects of various types. | Contains items: ``(void *)`` pointers |
128−| | coupled with a finalizer -- a pointer |
129−| | to a routine that deallocates the |
127+| Contains objects of various types. | Contains C heap items: ``(void *)`` |
128+| | pointers with finalizers. A finalizer |
129+| | is a routine that deallocates the |
130130| | resources associated with the item. |
131131+--------------------------------------+---------------------------------------+
132132| Fixed set of object types. | The data pointer may point |
@@ -138,8 +138,8 @@ Idris has two heaps where objects can be allocated:
138138+--------------------------------------+---------------------------------------+
139139| Values form a compact memory block. | Items are kept in a linked list. |
140140+--------------------------------------+---------------------------------------+
141−| Any Idris value, most notably | In Idris, items represented by the |
142−| ``ManagedPtr``. | type ``CData``. |
141+| Any Idris value, most notably | Items represented by the |
142+| ``ManagedPtr``. | Idris type ``CData``. |
143143+--------------------------------------+---------------------------------------+
144144| Data of ``ManagedPtr`` allocated | Data allocated in C, pointer copied |
145145| in C, buffer then copied into the FP | into the C heap. |
@@ -152,10 +152,10 @@ Idris has two heaps where objects can be allocated:
152152+--------------------------------------+---------------------------------------+
153153
154154The FP heap is the primary heap. It may contain values of type ``CData``,
155−which are references to items in the C heap. A C heap item *contains*
155+which are references to items in the C heap. A C heap item contains
156156a ``(void *)`` pointer and the corresponding finalizer. Once a C heap item
157157is no longer referenced from the FP heap, it is marked as unused and
158−the next GC sweep will finalize and deallocate it.
158+the next GC sweep will call its finalizer and deallocate it.
159159
160160There is no Idris interface for ``CData`` other than its type and FFI.
161161
@@ -164,13 +164,13 @@ Usage from C code
164164
165165* Although not enforced in code, ``CData`` is meant to be opaque
166166 and non-RTS code (such as libraries or C bindings) should
167− access only its ``(void *)`` field called "data".
167+ access only its ``(void *)`` field called ``data``.
168168
169−* Feel free to mutate ``cd->data``; the heap does not care
170− about its particular value. However, keep in mind
171− that it must not break Idris's referential transparency.
169+* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)
170+ and the memory it points to. However, keep in mind
171+ that this must not break Idris's referential transparency.
172172
173−* **WARNING!** If you call cdata_allocate or cdata_manage,
173+* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,
174174 the resulting ``CData`` object *must* be returned from your
175175 FFI function so that it is inserted in the C heap by the RTS.
176176 Otherwise the memory will be leaked.
@@ -183,20 +183,20 @@ Usage from C code
183183 other_fun : CData -> Int -> IO Int
184184 other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i
185185
186−.. code:: c
186+.. code:: cpp
187187
188188 #include "idris_rts.h"
189189
190190 static void finalizer(void * data)
191191 {
192− MyStruct * ptr = (MyStruct*) data;
192+ MyStruct * ptr = (MyStruct *) data;
193193 free_something(ptr->something);
194194 free(ptr);
195195 }
196196
197197 CData some_allocating_fun(int arg)
198198 {
199− void * data = (void*) malloc(...);
199+ void * data = (void *) malloc(...);
200200 // ...
201201 return cdata_manage(data, finalizer);
202202 }