@@ -422,13 +422,126 @@ $\vx$ requires.
422422In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
423423a tree of case expressions~\cite{Augustsson1985}.
424424
425−\subsection{The Development Calculus \TTdev}
425+\subsection{From \Idris{} to \TT{}}
426426
427−\TTdev{} is \TT{} extended with hole binders, Oleg-style~\cite{McBride1999}.
427+\TT{} is a very small language, consisting only of data declarations and pattern matching
428+function definitions. There is no significant innovation in the design of \TT{}, and this
429+is a deliberate choice --- it is a combination of small, well-understood components.
430+The kernel of the \TT{} implementation, consisting of a type checker, evaluator and
431+pattern match compiler, is less than 1000 lines of Haskell code. If we are confident
432+in the correctness of the kernel of \TT{}, and any higher level language feature
433+can be translated into \TT{}, we can be more confident of the correctness of the high
434+level language implementation that if it were implemented directly.
428435
429−\subsection{The $\MO{Elab}$ meta-language}
436+The process of elaborating a high level language into a core type theory like \TT{} is,
437+however, less well understood, and presents several challenges depending on the
438+features of the high level language. Elaboration has been implemented in various different ways,
439+for example in Agda~\cite{norell2007thesis} and Epigram~\cite{McBride2004a}.
430440
441+\subsubsection{Example Elaboration}
442+
443+Consider the following \Idris{} function:
444+
445+\begin{SaveVerbatim}{vadd}
446+
447+vAdd : Num a => Vect a n -> Vect a n -> Vect a n
448+vAdd [] [] = []
449+vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys
450+
451+\end{SaveVerbatim}
452+\useverb{vadd}
453+
454+\noindent
455+This adds corresponding elements of vectors of the same length. The vectors can contain
456+any numeric type, overloaded using the \texttt{Num} type class. In order to elaborate
457+this to \TT{}, we must resolve the implicit arguments, and make the type class explicit.
458+
459+The first step is to make the implicit arguments explicit, using a placeholder
460+to stand for the arguments we have not yet resolved. The type class argument is
461+also treated as an implicit argument, to which we give the name \texttt{c}:
462+
463+\begin{SaveVerbatim}{vAddImp}
464+
465+vAdd : (a : _) -> (n : _) -> Num a -> Vect a n -> Vect a n -> Vect a n
466+vAdd _ _ c (Nil _) (Nil _) = (Nil _)
467+vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)
468+ = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)
469+
470+\end{SaveVerbatim}
471+\useverb{vAddImp}
472+
473+Next, we resolve the implicit arguments. Each implicit argument can only take
474+one value for this program to be type correct --- these are solved by a unification
475+algorithm:
476+
477+\begin{SaveVerbatim}{vAddImpSolve}
478+
479+vAdd : (a : Set) -> (n : Nat) -> Num a -> Vect a n -> Vect a n -> Vect a n
480+vAdd a O c (Nil a) (Nil a) = Nil a
481+vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)
482+ = (::) a k ((+) c x y) (vAdd a k c xs ys)
483+
484+\end{SaveVerbatim}
485+\useverb{vAddImpSolve}
486+
487+Finally, to build the \TT{} definition, we need to find the type of each pattern variable
488+and state it explicitly. This leads to the \TT{} definition in Figure \ref{ttvadd},
489+switching to \TT{} notation from the ASCII \Idris{} syntax.
490+
491+\FFIG{
492+\AR{
493+\begin{array}{ll}
494+\FN{vAdd} & \Hab(\va\Hab\Set)\to(\vn\Hab\Nat)\to\TC{Num}\:\va\to
495+ \Vect\:\va\:\vn\to\Vect\:\va\:\vn\to\Vect\:\va\:\vn\\
496+\end{array}
497+\\
498+\begin{array}{lccccccc}
499+\multicolumn{5}{l}{
500+\RW{var}\:\va\Hab\Set,\:\vc\Hab\TC{Num}\;\va\SC}\\
501+\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\
502+\multicolumn{5}{l}{
503+\RW{var}\:\AR{
504+\va\Hab\Set,\:\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\
505+\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;
506+\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk
507+\SC
508+}
509+}\\
510+\hg\FN{vAdd} & \va & (\suc\;\vk) & \vc
511+ & ((\DC{::})\;\va\;\vk\;\vx\;\vxs)
512+ & ((\DC{::})\;\va\;\vk\;\vy\;\vys)
513+ & \\
514+ & & \MRet{5}{((\DC{::})\;\va\;\vk\;((+)\;\vc\;\vx\;\vy)\; (\FN{vAdd}\;\va\;\vk\;\vc\;\vxs\;\vys))}
515+\end{array}
516+}
517+}
518+{Pairwise addition of vectors in \TT{}}
519+{ttvadd}
520+
521+\subsubsection{An observation}
522+
523+\Idris{} programs may contain several high level constructs not present in \TT{}, such
524+as implicit arguments, type classes, \texttt{where} clauses, pattern matching \texttt{let}
525+and \texttt{case} constructs. We would like the high level language to be as expressive
526+as possible, while remaining possible to translate to \TT{}.
527+
528+Before considering how to achieve this, we make an observation about the distinction between
529+programming and theorem proving with dependent types, and appropriate mechanisms for
530+constructing programs and theorems:
431531
432532\begin{itemize}
433−\item $\MO{Check}\:\vt\:\cq\:(\vt, \vt)$
533+\item \remph{Pattern matching} is a convenient abstraction for humans to write programs,
534+in that it allows a programmer to express exactly the computational behaviour of a function.
535+\item \remph{Tactics}, such as those used in the Coq theorem prover~\cite{Bertot2004},
536+are a convenient abstraction for building proofs and programs by \remph{refinement}.
434537\end{itemize}
538+
539+The idea behind the \Idris{} elaborator, therefore, is to use the high level program
540+to direct \demph{tactics} to build \TT{} programs by refinement. We implement the
541+elaborator as an Embedded Domain Specific Language (EDSL) in Haskell.
542+In the remainder
543+of this paper, we decribe the EDSL, and demonstrate how it can be used to implement
544+all of the high level features of \Idris{}.
545+
546+
547+