Skip to content
Browse files

Added :x, :dynamic, and %dynamic to the tutorial

  • Loading branch information...
1 parent 0743b22 commit a4b73744c342e5dc9340775381c46364984925ba @david-christiansen david-christiansen committed Mar 21, 2013
Showing with 16 additions and 0 deletions.
  1. BIN tutorial/idris-tutorial.pdf
  2. +16 −0 tutorial/miscellany.tex
View
BIN tutorial/idris-tutorial.pdf
Binary file not shown.
View
16 tutorial/miscellany.tex
@@ -228,8 +228,24 @@ \subsubsection*{Include and linker directives}
\texttt{-lx} option to \texttt{gcc}.
\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.
\item \texttt{\%link "x.o"} --- link with the object file \texttt{x.o}.
+\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.
\end{itemize}
+\subsubsection*{Testing foreign function calls}
+Normally, the Idris interpreter (used for typechecking and at the REPL) will
+not perform IO actions. Additionally, as it neither generates C code nor
+compiles to machine code, the \texttt{\%lib}, \texttt{\%include} and
+\texttt{\%link} directives have no effect. IO actions and FFI calls can be
+tested using the special REPL command \texttt{:x EXPR}, and C libraries can be
+dynamically loaded in the interpreter by using the \texttt{:dynamic} command
+or the \texttt{\%dynamic} directive. For example:
+
+\begin{SaveVerbatim}{xdynamic}
+Idris> :dynamic libm.so
+Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
+0.9995736030415051 : Float
+\end{SaveVerbatim}
+\useverb{xdynamic}
\subsection{Cumulativity}
Since values can appear in types and \emph{vice versa}, it is natural that types themselves

0 comments on commit a4b7374

Please sign in to comment.
Something went wrong with that request. Please try again.