@@ -100,6 +100,113 @@ follows:
100 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))
100 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))
106+Idris has two heaps where objects can be allocated:
108++--------------------------------------+---------------------------------------+
110++======================================+=======================================+
111+| Cheney-collected | Mark-and-sweep-collected |
112++--------------------------------------+---------------------------------------+
113+| Garbage collections touches only | Garbage collection has to traverse |
114+| live objects. | all registered items. |
115++--------------------------------------+---------------------------------------+
116+| Ideal for FP-style rapid allocation | Ideal for C-style allocation of a few |
117+| of lots of small short-lived pieces | big buffers. |
118+| of memory, such as data constructors.| |
119++--------------------------------------+---------------------------------------+
120+| Finalizers are impossible to support | Items have finalizers that are called |
121+| reasonably. | on deallocation. |
122++--------------------------------------+---------------------------------------+
123+| Data is copied all the time (when | Copying does not happen. |
124+| collecting garbage, modifying data, | |
125+| registering managed pointers, etc.) | |
126++--------------------------------------+---------------------------------------+
127+| Contains objects of various types. | Contains items: ``(void *)`` pointers |
128+| | coupled with a finalizer -- a pointer |
129+| | to a routine that deallocates the |
130+| | resources associated with the item. |
131++--------------------------------------+---------------------------------------+
132+| Fixed set of object types. | The data pointer may point |
133+| | to anything, as long as the finalizer |
134+| | cleans up correctly. |
135++--------------------------------------+---------------------------------------+
136+| Not suitable for C resources and | Suitable for C resources and arbitrary|
137+| arbitrary pointers. | pointers. |
138++--------------------------------------+---------------------------------------+
139+| Values form a compact memory block. | Items are kept in a linked list. |
140++--------------------------------------+---------------------------------------+
141+| Any Idris value, most notably | In Idris, items represented by the |
142+| ``ManagedPtr``. | type ``CData``. |
143++--------------------------------------+---------------------------------------+
144+| Data of ``ManagedPtr`` allocated | Data allocated in C, pointer copied |
145+| in C, buffer then copied into the FP | into the C heap. |
147++--------------------------------------+---------------------------------------+
148+| Allocation and reallocation not | Allocated and reallocate freely in C, |
149+| possible from C code (without having | registering the allocated items |
150+| a reference to the VM). Everything | in the FFI. |
151+| is copied instead. | |
152++--------------------------------------+---------------------------------------+
154+The 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*
156+a ``(void *)`` pointer and the corresponding finalizer. Once a C heap item
157+is no longer referenced from the FP heap, it is marked as unused and
158+the next GC sweep will finalize and deallocate it.
160+There is no Idris interface for ``CData`` other than its type and FFI.
165+* Although not enforced in code, ``CData`` is meant to be opaque
166+ and non-RTS code (such as libraries or C bindings) should
167+ access only its ``(void *)`` field called "data".
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.
173+* If you call cdata_allocate or cdata_manage, the resulting
174+ ``CData`` object *must* be returned from your FFI function so
175+ that it is inserted in the C heap. Otherwise the memory
180+ some_allocating_fun : Int -> IO CData
181+ some_allocating_fun i = foreign FFI_C "some_allocating_fun" (Int -> IO CData) i
183+ other_fun : CData -> Int -> IO Int
184+ other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i
188+ #include "idris_rts.h"
190+ static void finalizer(void * data)
192+ MyStruct * ptr = (MyStruct*) data;
193+ free_something(ptr->something);
197+ CData some_allocating_fun(int arg)
199+ void * data = (void*) malloc(...);
201+ return cdata_manage(data, finalizer);
204+ int other_fun(CData cd, int arg)
206+ int result = foo(cd->data);
103Preorder reasoning
210Preorder reasoning
104==================
211==================
@@ -118,7 +225,7 @@ Here is an example:
118 (a * b * c) ={ sym (multAssociative a b c) }=
225 (a * b * c) ={ sym (multAssociative a b c) }=
119 (a * (b * c)) ={ cong (multCommutative b c) }=
226 (a * (b * c)) ={ cong (multCommutative b c) }=
120 (a * (c * b)) ={ multAssociative a c b }=
227 (a * (c * b)) ={ multAssociative a c b }=
121− (a * c * b) ={ cong {f = (*b)} (multCommutative a c) }=
228+ (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=
122 (c * a * b) QED
229 (c * a * b) QED
124Note that the parentheses are required -- only a simple expression can
231Note that the parentheses are required -- only a simple expression can