c6d8703 · Idris-dev · git.iko.soy

124| collecting garbage, modifying data, | |

125| registering managed pointers, etc.) | |

126+--------------------------------------+---------------------------------------+

127−| Contains objects of various types. | Contains items: ``(void *)`` pointers |

127+| Contains objects of various types. | Contains C heap items: ``(void *)`` |

128−| | coupled with a finalizer -- a pointer |

128+| | pointers with finalizers. A finalizer |

129−| | to a routine that deallocates the |

129+| | is a routine that deallocates the |

130| | resources associated with the item. |

131+--------------------------------------+---------------------------------------+

132| Fixed set of object types. | The data pointer may point |

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 |

141+| Any Idris value, most notably | Items represented by the |

142−| ``ManagedPtr``. | type ``CData``. |

142+| ``ManagedPtr``. | Idris 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. |

152+--------------------------------------+---------------------------------------+

153

154The 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

156a ``(void *)`` pointer and the corresponding finalizer. Once a C heap item

157is 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.

159

160There is no Idris interface for ``CData`` other than its type and FFI.

161

164

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".

167+ access only its ``(void *)`` field called ``data``.

168

169−* Feel free to mutate ``cd->data``; the heap does not care

169+* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)

170− about its particular value. However, keep in mind

170+ and the memory it points to. However, keep in mind

171− that it must not break Idris's referential transparency.

171+ that this must not break Idris's referential transparency.

172

173−* **WARNING!** If you call cdata_allocate or cdata_manage,

173+* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,

174 the resulting ``CData`` object *must* be returned from your

175 FFI function so that it is inserted in the C heap by the RTS.

176 Otherwise the memory will be leaked.

183 other_fun : CData -> Int -> IO Int

184 other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i

185

186−.. code:: c

186+.. code:: cpp

187

188 #include "idris_rts.h"

189

190 static void finalizer(void * data)

191 {

192− MyStruct * ptr = (MyStruct*) data;

192+ MyStruct * ptr = (MyStruct *) data;

193 free_something(ptr->something);

194 free(ptr);

195 }

196

197 CData some_allocating_fun(int arg)

198 {

199− void * data = (void*) malloc(...);

199+ void * data = (void *) malloc(...);

200 // ...

201 return cdata_manage(data, finalizer);

202 }