diff --git a/docs/ffi/ffi.rst b/docs/ffi/ffi.rst index 072d22d..94d98a1 100644 --- a/docs/ffi/ffi.rst +++ b/docs/ffi/ffi.rst @@ -138,6 +138,8 @@ use that instead: %foreign (libsmall "addWithMessage") prim_addWithMessage : String -> Int -> Int -> PrimIO Int +.. _sect-ffi-string: + Primitive FFI Types ------------------- @@ -197,6 +199,8 @@ For an example, see the sample :ref:`sect-readline` bindings. Additionally, foreign functions can take *callbacks*, and take and return C ``struct`` pointers. +.. _sect-callbacks: + Callbacks --------- diff --git a/docs/ffi/readline.rst b/docs/ffi/readline.rst index 9bdb8f2..f7f223a 100644 --- a/docs/ffi/readline.rst +++ b/docs/ffi/readline.rst @@ -4,5 +4,293 @@ Example: Minimal Readline Bindings ********************************** -[TODO] +In this section, we'll see how to create bindings for a C library (the `GNU +Readline `_ library) in +Idris, and make them available in a package. We'll only create the most minimal +bindings, but nevertheless they demonstrate some of the trickier problems in +creating bindings to a C library, in that they need to handle memory allocation +of ``String``. +You can find the example in full in the Idris 2 source repository, +in `samples/FFI-readline +`_. As a +minimal example, this can be used as a starting point for other C library +bindings. + +We are going to provide bindings to the following functions in the Readline +API, available via ``#include ``: + +:: + + char* readline (const char *prompt); + void add_history(const char *string); + +Additionally, we are going to support tab completion, which in the Readline +API is achieved by setting a global variable to a callback function +(see Section :ref:`sect-callbacks`) which explains how to handle the +completion: + +:: + + typedef char *rl_compentry_func_t (const char *, int); + + rl_compentry_func_t * rl_completion_entry_function; + +A completion function takes a ``String``, which is the text to complete, and +an ``Int``, which is the number of times it has asked for a completion so far. +In Idris, this could be a function ``complete : String -> Int -> IO String``. +So, for example, if the text so far is ``"id"``, and the possible completions +are ``idiomatic`` and ``idris``, then ``complete "id" 0`` would produce the +string ``"idiomatic"`` and ``complete "id" 1`` would produce ``"idris"``. + +We will define *glue* functions in a C file ``idris_readline.c``, which compiles +to a shared object ``libidrisreadline``, so we write a function for locating +the C functions: + +.. code-block:: idris + + rlib : String -> String + rlib fn = "C:" ++ fn ++ ",libidrisreadline" + +Each of the foreign bindings will have a ``%foreign`` specifier which locates +functions via ``rlib``. + +Basic behaviour: Reading input, and history +------------------------------------------- + +We can start by writing a binding for ``readline`` directly. It's interactive, +so needs to return a ``PrimIO``: + +.. code-block:: idris + + %foreign (rlib "readline") + prim_readline : String -> PrimIO String + +Then, we can write an ``IO`` wrapper: + +.. code-block:: idris + + readline : String -> IO String + readline prompt = primIO $ readline prompt + +Unfortunately, this isn't quite good enough! The C ``readline`` function +returns a ``NULL`` string if there is no input due to encountering an +end of file. So, we need to handle that - if we don't, we'll get a crash +on encountering end of file (remember: it's the Idris programmer's responsibility +to give an appropriate type to the C binding!) + +Instead, we need to use a ``Ptr`` to say that it might be a ``NULL`` +pointer (see Section :ref:`sect-ffi-string`): + +.. code-block:: idris + + %foreign (rlib "readline") + prim_readline : String -> PrimIO (Ptr String) + +We also need to provide a way to check whether the returned ``Ptr String`` is +``NULL``. To do so, we'll write some glue code to convert back and forth +between ``Ptr String`` and ``String, in a file ``idris_readline.c`` and a +corresponding header ``idris_readline.h``. In ``idris_readline.h`` we have: + +:: + + int isNullString(void* str); // return 0 if a string in NULL, non zero otherwise + char* getString(void* str); // turn a non-NULL Ptr String into a String (assuming not NULL) + void* mkString(char* str); // turn a String into a Ptr String + void* nullString(); // create a new NULL String + +Correspondingly, in ``idris_readline.c``: + +:: + + int isNullString(void* str) { + return str == NULL; + } + + char* getString(void* str) { + return (char*)str; + } + + void* mkString(char* str) { + return (void*)str; + } + + void* nullString() { + return NULL; + } + +Now, we can use ``prim_readline`` as follows, with a safe API: + +.. code-block:: idris + + export + readline : String -> IO (Maybe String) + readline s + = do mstr <- primIO $ prim_readline s + if isNullString mstr + then pure $ Nothing + else pure $ Just (getString mstr) + +We'll need ``nullString`` and ``mkString`` later, for dealing with completions. + +Once we've read a string, we'll want to add it to the input history. We can +provide a binding to ``add_history`` as follows: + +.. code-block:: idris + + %foreign (rlib "add_history") + prim_add_history : String -> PrimIO () + + export + addHistory : String -> IO () + addHistory s = primIO $ prim_add_history s + +In this case, since Idris is in control of the ``String``, we know it's not +going to be ``NULL``, so we can add it directly. + +A small ``readline`` program that reads input, and echoes it, recording input +history for non-empty inputs, can be written as follows: + +.. code-block:: idris + + echoLoop : IO () + echoLoop + = do Just x <- readline "> " + | Nothing => putStrLn "EOF" + putStrLn ("Read: " ++ x) + when (x /= "") $ addHistory x + if x /= "quit" + then echoLoop + else putStrLn "Done" + +This gives us command history, and command line editing, but Readline becomes +much more useful when we add tab completion. The default tab completion, which +is available even in the small example above, is to tab complete file names +in the current working directory. But for any realistic application, we probably +want to tab complete other commands, such as function names, references to +local data, or anything that is appropriate for the application. + +Completions +----------- + +Readline has a large API, with several ways of supporting tab completion, +typically involving setting a global variable to an appropriate completion +function. We'll use the following: + +:: + + typedef char *rl_compentry_func_t (const char *, int); + rl_compentry_func_t * rl_completion_entry_function; + +The completion function takes the prefix of the completion, and the number +of times it has been called so far on this prefix, and returns the next +completion, or ``NULL`` if there are no more completions. An Idris equivalent +would therefore have the following type: + +.. code-block:: idris + + setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO () + +The function returns ``Nothing`` if there are no more completions, or +``Just str`` for some ``str`` if there is another one for the current +input. + +We might hope that it's as simple as defining a function to assign the +completion function... + +:: + + void idrisrl_setCompletion(rl_compentry_func_t* fn) { + rl_completion_entry_function = fn; + } + +...then defining the Idris binding, which needs to take into account that +the Readline library expects ``NULL`` when there are no more completions: + +.. code-block:: idris + + %foreign (rlib "idrisrl_setCompletion") + prim_setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO () + + export + setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO () + setCompletionFn fn + = primIO $ prim_setCompletion $ \s, i => toPrim $ + do mstr <- fn s i + case mstr of + Nothing => pure nullString // need to return a Ptr String to readline! + Just str => pure (mkString str) + +So, we turn ``Nothing`` into ``nullString`` and ``Just str`` into ``mkString +str``. Unfortunately, this doesn't quite work. Let's try it for the most basic +completion function that returns one completion no matter what the input: + +.. code-block:: idris + + testComplete : String -> Int -> IO (Maybe String) + testComplete text 0 = pure $ Just "hamster" + testComplete text st = pure Nothing + +We'll try this in a small modification of ``echoLoop`` above, setting a +completion function first: + +.. code-block :: idris + + main : IO () + main = do setCompletionFn testComplete + echoLoop + +Unfortunately, when we try running it, and hitting TAB before entering +anything, things go wrong: + +:: + + Main> :exec main + > free(): invalid pointer + +This problem arises because we haven't thought carefully enough about which +parts of our program are responsible for allocating and freeing strings. +When Idris calls a foreign function that returns a string, it copies the +string to the Idris heap and frees it immediately. But, if the foreign +library also frees the string, it ends up being freed twice. This is what's +happening here: the callback passed to ``prim_setCompletion`` frees the string +and puts it onto the Idris heap, but Readline also frees the string returned +by ``prim_setCompletion`` once it has processed it. We can solve this +problem by writing a wrapper for the completion function which reallocates +the string, and using that in ``idrisrl_setCompletion`` instead. + +:: + + rl_compentry_func_t* my_compentry; + + char* compentry_wrapper(const char* text, int i) { + char* res = my_compentry(text, i); // my_compentry is an Idris function, so res is on the Idris heap, + // and freed on return + if (res != NULL) { + char* comp = malloc(strlen(res)+1); // comp is passed back to readline, which frees it when + // it is finished with it + strcpy(comp, res); + return comp; + } + else { + return NULL; + } + } + + void idrisrl_setCompletion(rl_compentry_func_t* fn) { + rl_completion_entry_function = compentry_wrapper; + my_compentry = fn; // fn is an Idris function, called by compentry_wrapper + } + +So, we define the completion function in C, which calls the Idris completion +function then makes sure the string returned by the Idris function is copied +to the C heap. + +We now have a primitive API that covers the most fundamental features of the +readline API: + +.. code-block:: idris + + readline : String -> IO (Maybe String) + addHistory : String -> IO () + setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO () diff --git a/samples/FFI-readline/Test/ReadTab.idr b/samples/FFI-readline/Test/ReadTab.idr new file mode 100644 index 0000000..f8aeed0 --- /dev/null +++ b/samples/FFI-readline/Test/ReadTab.idr @@ -0,0 +1,19 @@ +import Text.Readline + +testComplete : String -> Int -> IO (Maybe String) +testComplete text 0 = pure $ Just "hamster" +testComplete text 1 = pure $ Just "bar" +testComplete text st = pure Nothing + +loop : IO () +loop = do Just x <- readline "> " + | Nothing => putStrLn "EOF" + putStrLn x + when (x /= "") $ addHistory x + if x /= "quit" + then loop + else putStrLn "Done" + +main : IO () +main = do setCompletionFn testComplete + loop diff --git a/samples/FFI-readline/Test/test.ipkg b/samples/FFI-readline/Test/test.ipkg new file mode 100644 index 0000000..aa3f6a5 --- /dev/null +++ b/samples/FFI-readline/Test/test.ipkg @@ -0,0 +1,3 @@ +package test + +opts = "-p readline" diff --git a/samples/FFI-readline/readline.ipkg b/samples/FFI-readline/readline.ipkg new file mode 100644 index 0000000..babeafe --- /dev/null +++ b/samples/FFI-readline/readline.ipkg @@ -0,0 +1,10 @@ +package readline + +sourcedir = "src" + +modules = Text.Readline + +prebuild = "make -C readline_glue" +postinstall = "make -C readline_glue install" +postclean = "make -C readline_glue clean" + diff --git a/samples/FFI-readline/readline_glue/Makefile b/samples/FFI-readline/readline_glue/Makefile new file mode 100644 index 0000000..849ead6 --- /dev/null +++ b/samples/FFI-readline/readline_glue/Makefile @@ -0,0 +1,44 @@ +IDRIS := idris2 +MACHINE := $(shell $(CC) -dumpmachine) + +ifneq (, $(findstring darwin, $(MACHINE))) + OS :=darwin +else ifneq (, $(findstring cygwin, $(MACHINE))) + OS :=windows +else ifneq (, $(findstring mingw, $(MACHINE))) + OS :=windows +else ifneq (, $(findstring windows, $(MACHINE))) + OS :=windows +else + OS :=unix +endif + +ifeq ($(OS), darwin) + SHLIB_SUFFIX :=dylib +else ifeq ($(OS), windows) + SHLIB_SUFFIX :=dll +else + SHLIB_SUFFIX :=so +endif + +LIBTARGET = libidrisreadline.$(SHLIB_SUFFIX) +INSTALLDIR = `${IDRIS} --libdir`/readline/lib + +HDRS = idris_readline.h +OBJS = idris_readline.o + +READLINE_LIBS := -lreadline +READLINE_FLAGS := -fPIC + +CFLAGS = $(READLINE_FLAGS) + +$(LIBTARGET): $(OBJS) + $(CC) -o $(LIBTARGET) -shared $(OBJS) $(READLINE_LIBS) $(READLINE_FLAGS) + +install: + @if ! [ -d $(INSTALLDIR) ]; then mkdir -p $(INSTALLDIR); fi + install $(LIBTARGET) $(HDRS) $(INSTALLDIR) +clean: + rm $(OBJS) $(LIBTARGET) + +.PHONY: install clean diff --git a/samples/FFI-readline/readline_glue/idris_readline.c b/samples/FFI-readline/readline_glue/idris_readline.c new file mode 100644 index 0000000..fa3f07d --- /dev/null +++ b/samples/FFI-readline/readline_glue/idris_readline.c @@ -0,0 +1,37 @@ +#include +#include + +rl_compentry_func_t* my_compentry; + +char* compentry_wrapper(const char* text, int i) { + char* res = my_compentry(text, i); // Idris frees this + if (res != NULL) { + char* comp = malloc(strlen(res)+1); // Readline frees this + strcpy(comp, res); + return comp; + } + else { + return NULL; + } +} + +void idrisrl_setCompletion(rl_compentry_func_t* fn) { + rl_completion_entry_function = compentry_wrapper; + my_compentry = fn; +} + +char* getString(void* str) { + return (char*)str; +} + +void* mkString(char* str) { + return (void*)str; +} + +void* nullString() { + return NULL; +} + +int isNullString(void* str) { + return str == NULL; +} diff --git a/samples/FFI-readline/readline_glue/idris_readline.h b/samples/FFI-readline/readline_glue/idris_readline.h new file mode 100644 index 0000000..b7855a5 --- /dev/null +++ b/samples/FFI-readline/readline_glue/idris_readline.h @@ -0,0 +1,11 @@ +#ifndef _IDRIS_READLINE_H +#define _IDRIS_READLINE_H + +void idrisrl_setCompletion(rl_completion_func_t* fn); + +char* getString(void* str); +void* mkString(char* str); +void* nullString(); +int isNullString(void* str); + +#endif diff --git a/samples/FFI-readline/src/Text/Readline.idr b/samples/FFI-readline/src/Text/Readline.idr new file mode 100644 index 0000000..f4452a8 --- /dev/null +++ b/samples/FFI-readline/src/Text/Readline.idr @@ -0,0 +1,53 @@ +module Text.Readline + +rlib : String -> String +rlib fn = "C:" ++ fn ++ ",libidrisreadline" + +%foreign (rlib "getString") +export +getString : Ptr String -> String + +%foreign (rlib "mkString") +export +mkString : String -> Ptr String + +%foreign (rlib "nullString") +export +nullString : Ptr String + +%foreign (rlib "isNullString") +prim_isNullString : Ptr String -> Int + +export +isNullString : Ptr String -> Bool +isNullString str = if prim_isNullString str == 0 then False else True + +%foreign (rlib "readline") +prim_readline : String -> PrimIO (Ptr String) + +export +readline : String -> IO (Maybe String) +readline s + = do mstr <- primIO $ prim_readline s + if isNullString mstr + then pure $ Nothing + else pure $ Just (getString mstr) + +%foreign (rlib "add_history") +prim_add_history : String -> PrimIO () + +export +addHistory : String -> IO () +addHistory s = primIO $ prim_add_history s + +%foreign (rlib "idrisrl_setCompletion") +prim_setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO () + +export +setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO () +setCompletionFn fn + = primIO $ prim_setCompletion $ \s, i => toPrim $ + do mstr <- fn s i + case mstr of + Nothing => pure nullString + Just str => pure (mkString str) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 51f0728..4910bdf 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -49,6 +49,8 @@ record PkgDesc where postbuild : Maybe (FC, String) -- Script to run after building preinstall : Maybe (FC, String) -- Script to run after building, before installing postinstall : Maybe (FC, String) -- Script to run after installing + preclean : Maybe (FC, String) -- Script to run before cleaning + postclean : Maybe (FC, String) -- Script to run after cleaning Show PkgDesc where show pkg = "Package: " ++ name pkg ++ "\n" ++ @@ -70,7 +72,9 @@ Show PkgDesc where maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++ maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++ maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++ - maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) + maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) ++ + maybe "" (\m => "Preclean: " ++ snd m ++ "\n") (preclean pkg) ++ + maybe "" (\m => "Postclean: " ++ snd m ++ "\n") (postclean pkg) initPkgDesc : String -> PkgDesc initPkgDesc pname @@ -78,6 +82,7 @@ initPkgDesc pname Nothing Nothing Nothing Nothing Nothing [] [] Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing + Nothing Nothing data DescField : Type where PVersion : FC -> String -> DescField @@ -99,6 +104,8 @@ data DescField : Type where PPostbuild : FC -> String -> DescField PPreinstall : FC -> String -> DescField PPostinstall : FC -> String -> DescField + PPreclean : FC -> String -> DescField + PPostclean : FC -> String -> DescField field : String -> Rule DescField field fname @@ -118,6 +125,8 @@ field fname <|> strField PPostbuild "postbuild" <|> strField PPreinstall "preinstall" <|> strField PPostinstall "postinstall" + <|> strField PPreclean "preclean" + <|> strField PPostclean "postclean" <|> do exactIdent "depends"; symbol "=" ds <- sepBy1 (symbol ",") unqualifiedName pure (PDepends ds) @@ -189,6 +198,8 @@ addField (PPrebuild fc e) pkg = pure $ record { prebuild = Just (fc, e) } pkg addField (PPostbuild fc e) pkg = pure $ record { postbuild = Just (fc, e) } pkg addField (PPreinstall fc e) pkg = pure $ record { preinstall = Just (fc, e) } pkg addField (PPostinstall fc e) pkg = pure $ record { postinstall = Just (fc, e) } pkg +addField (PPreclean fc e) pkg = pure $ record { preclean = Just (fc, e) } pkg +addField (PPostclean fc e) pkg = pure $ record { postclean = Just (fc, e) } pkg addFields : {auto c : Ref Ctxt Defs} -> List DescField -> PkgDesc -> Core PkgDesc @@ -343,6 +354,7 @@ clean : {auto c : Ref Ctxt Defs} -> clean pkg = do defs <- get Ctxt let build = build_dir (dirs (options defs)) + runScript (preclean pkg) let toClean = mapMaybe (\ks => [| MkPair (tail' ks) (head' ks) |]) $ maybe (map fst (modules pkg)) (\m => fst m :: map fst (modules pkg)) @@ -360,6 +372,7 @@ clean pkg (\ks => map concat . traverse (deleteBin builddir ks)) pkgTrie deleteFolder builddir [] + runScript (postclean pkg) where delete : String -> Core () delete path = do True <- coreLift $ fRemove path