@@ -1315,9 +1315,136 @@ main = putStrLn (show [1,2,3,4])
1316\subsection{Syntax Extensions}
1316\subsection{Syntax Extensions}
1318+We now have a complete elaborator for \IdrisM{}, covering
1319+dependent pattern matching definitions and expansion of implicit arguments
1320+and type classes. In order to make the language truly general purpose, however, we
1321+will need to add higher level extensions. Full \Idris{} is \IdrisM{} extended
1322+with \texttt{do}-notation, idiom brackets~\cite{McBride2007}, \texttt{case} expressions,
1323+pattern matching \texttt{let}, metavariables and tactic based theorem proving.
1324+The majority of these extensions are straightforward transformations of high level
1325+\Idris{} programs --- for example, \texttt{do}-notation can be reduced directly to
1326+\IdrisM{} function applications. Some, however, require further support. In this section,
1327+we complete the presentation of \IdrisM{} by extending it with metavariables
1328+and $\icase$ expressions:
1332+\begin{array}{rll@{\hg}rll}
1334+\mid & \mvar{\vx} & (\mbox{metavariable}) &
1335+\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) \\
1318\subsubsection{Metavariables}
1340\subsubsection{Metavariables}
1342+\demph{Metavariables} are terms which stand for incomplete programs. A
1343+metavariable serves a similar
1344+purpose to a hole binding in \TT{}, but gives rise to a global rather than a
1345+local variable. For example, the following is an incomplete definition of
1346+the vector append function, containing a metavariable \texttt{append\_rec}:
1348+\begin{SaveVerbatim}{vappmv}
1350+(++) : Vect A n -> Vect A m -> Vect A (n + m)
1352+(++) (x :: xs) ys = x :: ?append_rec
1357+This generates a new (as yet undefined)
1358+function \texttt{append\_rec}, which takes all of the variables
1359+in scope at the point it is used, and returns a value of the required type.
1360+We can inspect the type of \texttt{append\_rec} at the \Idris{} prompt:
1362+\begin{SaveVerbatim}{appendrec}
1365+append_rec : (a : Set) -> (m : Nat) -> (n : Nat) -> a ->
1366+ Vect a n -> Vect a m -> Vect a (n + m)
1371+Metavariables serve two purposes: Firstly, they aid type directed program development
1372+by allowing a programmer direct access to the inferred types of local variables, and
1373+the types of subexpressions. Secondly, they allow a separation of program structure
1374+from proof details. Metavariables can be solved either by directly editing program
1375+source, or by providing a definition elsewhere in the file. For example, we can later say:
1377+\begin{SaveVerbatim}{appendrec_def}
1379+append_rec a m n x xs ys = app xs ys
1382+\useverb{appendrec_def}
1384+To elaborate a metavariable, we simply add a new top level definition, and apply
1385+it to the current context:
1388+\ttinterp{\mvar{\vx}}\:\mq\:
1390+(\tv\Hab\ttt)\gets\MO{Context}\\
1392+\MO{TTDecl}\:(\vx\Hab(\tv\Hab\ttt)\to\vt)\\
1320\subsubsection{\texttt{case} expressions}
1397\subsubsection{\texttt{case} expressions}
1399+A \texttt{case} expression allows pattern matching on intermediate values. The difficulty
1400+in elaborating \texttt{case} expressions is that \TT{} allows matching only on
1401+\emph{top level} values. To elaborate a \texttt{case} expression, therefore,
1402+we create a new top level function standing for the expression, and call it. The natural
1403+way to implement this is to use a metavariable. For example, we have already seen
1404+\texttt{lookup\_default}:
1406+\useverb{listlookup}
1409+This elaborates as follows:
1411+\begin{SaveVerbatim}{listlookupmv}
1413+lookup_default : Nat -> List a -> a -> a
1414+lookup_default i xs def =
1415+ let scrutinee = list_lookup i xs in ?lookup_default_case
1417+lookup_default_case i xs def Nothing = def
1418+lookup_default_case i xs def (Just x) = x
1421+\useverb{listlookupmv}
1423+To elaborate a $\icase$ expression, we begin by \texttt{let} binding the scrutinee of
1424+the $\icase$ expression and creating a metavariable $\VV{xcase}$ to implement the
1425+pattern matching. We then build a new pattern matching definition for $\VV{xcase}$
1430+\ttinterp{\icase\:\ve\:\iof\:\vec{\VV{alt}}}\:\mq\:
1432+\ttinterp{\ilet{\VV{scrutinee}}{\ve}\:\mvar{\VV{xcase}}}\\
1433+(\tv\Hab\ttt)\gets\MO{Context}\\
1434+\vec{\MO{MkCase}}\:\tv\:\VV{alt}\\
1437+\MO{MkCase}\:\tv\:(\vl\:\fatarrow\:\vr)\:\mq\:\MO{Elab}\:(\VV{xcase}\:\tv\:\vl\:=\:\vr)
1441+Any nested $\icase$ expressions will be handled by the recursive call to
1442+$\MO{Elab}$. Again, because of the way we have set up an Embedded Domain Specific
1443+Language for describing elaboration, we have been able to implement a new higher
1444+level language feature in terms of elaboration of lower level language features.
1322−\subsubsection{Pairs and Dependent Pairs}
1446+%\subsubsection{Pairs and Dependent Pairs}
1448+% Other extensions: do notation, idiom brackets, pairs, etc, are easily expressed
1449+% by transformations of the high level syntax