@@ -1,13 +1,139 @@
11\section{Miscellany}
22
3−Small things which don't quite fit elsewhere:
3+In this section we discuss a variety of additional features: extensible syntax,
4+literate programming, and interfacing with external libraries through the
5+foriegn function interface.
6+
7+\input{syntax}
8+
9+\subsection{Literate programming}
10+
11+Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an
12+extension of \texttt{.lidr} then it is assumed to be a literate file. In literate
13+programs, everything is assumed to be a comment unless the line begins with a
14+greater than sign \texttt{>}, for example:
15+
16+\begin{SaveVerbatim}{litidr}
17+
18+> module literate;
19+
20+This is a comment. The main program is below
21+
22+> main : IO ();
23+> main = putStrLn "Hello literate world!\n";
24+
25+\end{SaveVerbatim}
26+\useverb{litidr}
27+
28+\noindent
29+An additional restriction is that there must be a blank line between a program
30+line (beginning with \texttt{>}) and a comment line (beginning with any other
31+character).
32+
33+\subsection{Foreign function calls}
34+
35+For practical programming, it is often necessary to be able to use external libraries,
36+particularly for interfacing with the operating system, file system, networking, etc.
37+\Idris{} provides a lightweight foreign function interface for achieving this,
38+as part of the prelude. For this, we assume a certain amount of knowledge of
39+C and the \texttt{gcc} compiler. First, we define a datatype which describes the external
40+types we can handle:
41+
42+\begin{SaveVerbatim}{foreignty}
43+
44+data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit;
45+
46+\end{SaveVerbatim}
47+\useverb{foreignty}
48+
49+\noindent
50+Each of these corresponds directly to a C type. Respectively: \texttt{int},
51+\texttt{float}, \texttt{char}, \texttt{char*}, \texttt{void*} and \texttt{void}.
52+There is also a translation to a concrete \Idris{} type, described by the
53+following function:
54+
55+\begin{SaveVerbatim}{interpfty}
56+
57+interpFTy : FTy -> Set;
58+interpFTy FInt = Int;
59+interpFTy FFloat = Float;
60+interpFTy FChar = Char;
61+interpFTy FString = String;
62+interpFTy FPtr = Ptr;
63+interpFTy FUnit = ();
64+
65+\end{SaveVerbatim}
66+\useverb{interpfty}
67+
68+\noindent
69+A foreign function is described by a list of input types and a return type, which
70+can then be converted to an \Idris{} type:
71+
72+\begin{SaveVerbatim}{ffunty}
73+
74+ForeignTy : (xs:List FTy) -> (t:FTy) -> Set;
75+
76+\end{SaveVerbatim}
77+\useverb{ffunty}
78+
79+\noindent
80+A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an
81+\texttt{IO} type, for example:
82+
83+\begin{SaveVerbatim}{ftyex}
84+
85+Idris> ForeignTy [FInt, FString] FString
86+Int -> String -> IO String : Set
87+
88+Idris> ForeignTy [FInt, FString] FUnit
89+Int -> String -> IO () : Set
90+
91+\end{SaveVerbatim}
92+\useverb{ftyex}
93+
94+\noindent
95+We build a call to a foreign function by giving the name of the function, a list of
96+argument types and the return type. The built in function \texttt{mkForeign}
97+converts this description to a function callable by \Idris{}
98+
99+\begin{SaveVerbatim}{mkForeign}
100+
101+data Foreign : Set -> Set where
102+ FFun : String -> (xs:List FTy) -> (t:FTy) ->
103+ Foreign (ForeignTy xs t);
104+
105+mkForeign : Foreign x -> x;
106+
107+\end{SaveVerbatim}
108+\useverb{mkForeign}
109+
110+\noindent
111+For example, the \texttt{putStr} function is implemented as follows, as a call to
112+an external function \texttt{putStr} defined in the run-time system:
113+
114+\begin{SaveVerbatim}{putStrex}
115+
116+putStr : String -> IO ();
117+putStr x = mkForeign (FFun "putStr" [FString] FUnit) x;
118+
119+\end{SaveVerbatim}
120+\useverb{putStrex}
121+
122+\subsubsection*{Include and linker directives}
123+
124+Foreign function calls are translated directly to calls to C functions, with appropriate
125+conversion between the \Idris{} representation of a value and the C representation.
126+Often this will require extra libraries to be linked in, or extra header and object files.
127+This is made possible through the following directives:
4128
5129\begin{itemize}
6−\item Literate programming
7−\item Foreign functions
130+\item \texttt{\%lib "x"} --- include the \texttt{libx} library, equivalent to passing the
131+\texttt{-lx} option to \texttt{gcc}.
132+\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.
133+\item \texttt{\%obj "x.o"} --- link with the object file \texttt{x.o}.
8134\end{itemize}
9135
10−\subsection{Comparison}
136+%\subsection{Comparison}
11137
12−How does \Idris{} compare with other dependently typed languages and proof
13−assistants, such as Coq, Agda and Epigram?
138+%How does \Idris{} compare with other dependently typed languages and proof
139+%assistants, such as Coq, Agda and Epigram?