Skip to content

Commit

Permalink
Merge pull request #4630 from unalos/4629
Browse files Browse the repository at this point in the history
Documenting usage of MKSTR and the Raw type constructor when interacting with C code.
  • Loading branch information
melted committed Dec 26, 2018
2 parents 33d8d91 + ecfb081 commit 32940be
Showing 1 changed file with 21 additions and 0 deletions.
21 changes: 21 additions & 0 deletions docs/reference/ffi.rst
Original file line number Diff line number Diff line change
Expand Up @@ -348,6 +348,27 @@ Usage from C code
return result;
}
The ``Raw`` type constructor allows you to access or return a runtime
representation of the value. For instance, if you want to copy a string
generated from C code into an Idris value, you may want to return a
``Raw String``instead of a ``String`` and use ``MKSTR`` or ``MKSTRlen`` to
copy it over.

.. code-block:: idris
getString : () -> IO (Raw String)
getString () = foreign FFI_C "get_string" (IO (Raw String))
.. code-block:: cpp
const VAL get_string ()
{
char * c_string = get_string_allocated_with_malloc()
const VAL idris_string = MKSTR(c_string);
free(c_string);
return idris_string
}
FFI implementation
------------------

Expand Down

0 comments on commit 32940be

Please sign in to comment.