@@ -11,9 +11,10 @@ which together constitute an algorithm for elaborating \Idris{}
1111programs to \TT{}.
1212
1313\begin{itemize}
14−\item $\ttinterp{\cdot}$, which builds a \TT{} expression from an \Idris{} expression
14+\item $\ttinterp{\cdot}$, which builds a \TT{} expression from an \Idris{} expression.
1515\item $\MO{Elab}$, which processes a top level \Idris{} declaration by generating
1616one or more \TT{} declarations.
17+\item $\MO{TTDecl}$, which adds a top level \TT{} declaration.
1718\end{itemize}
1819
1920
@@ -545,8 +546,8 @@ a Coq proof script.
545546\mid & \ve\:\ta & (\mbox{function application}) \\
546547\mid & \ilam{\vx}\:\ve & (\mbox{lambda abstraction}) &
547548\mid & \ilet{\vx}{\ve}\:\ve & (\mbox{let binding}) \\
548−\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) &
549−\mid & \mvar{\vx} & (\mbox{metavariable}) \\
549+%\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) &
550+%\mid & \mvar{\vx} & (\mbox{metavariable}) \\
550551\mid & \_ & (\mbox{placeholder})
551552\end{array}
552553\medskip\\
@@ -633,8 +634,8 @@ the \MO{Fill} tactic:
633634
634635\DM{
635636\AR{
636−\ttinterp{\vx}\:\mq\:\MO{Fill}\:\vx;\:\MO{Solve}\\
637−\ttinterp{\vc}\:\mq\:\MO{Fill}\:\vc;\:\MO{Solve}\\
637+\ttinterp{\vx}\:\mq\:\RW{do}\:\MO{Fill}\:\vx;\:\MO{Solve}\\
638+\ttinterp{\vc}\:\mq\:\RW{do}\:\MO{Fill}\:\vc;\:\MO{Solve}\\
638639}
639640}
640641
@@ -642,6 +643,17 @@ We need not concern ourselves with type checking variables or constants here ---
642643will handle this, type checking $\vx$ or $\vc$ and unifying the result with the
643644hole type. If there are any errors, elaboration will fail.
644645
646+If we are building the left hand side of a pattern clause, however, there is a problem,
647+as it is the left hand side which \remph{defines} variables. In this context, we assume
648+that attempting to elaborate a variable which does not type check means that the variable
649+is a pattern variable:
650+
651+\DM{
652+\ttinterp{\vx}\:\mq\:
653+\MO{Try}\:\AR{(\RW{do}\:\MO{Fill}\:\vx;\:\MO{Solve})\\
654+(\MO{Pat}\:\vx)\hg\hg\mbox{(If elaborating a left hand side)}}
655+}
656+
645657We also need to elaborate \remph{placeholders}, which are subexpressions we expect to
646658solve by unification. In this case, we simply move on to the next hole in the queue, moving
647659the current hole to the end of the queue with $\MO{Unfocus}$:
@@ -721,7 +733,6 @@ $\vV$ and $\vX$.
721733\ttinterp{\ve}
722734}
723735}
724−
725736\subsubsection{Elaborating applications}
726737
727738There are two cases to consider when elaborating applications:
@@ -832,16 +843,223 @@ the function or argument which helps with unification:
832843}
833844}
834845
835−\subsubsection{Elaborating metavariables}
846+%\subsubsection{Elaborating metavariables}
836847
837−\subsubsection{Elaborating \texttt{case} expressions}
848+%\subsubsection{Elaborating \texttt{case} expressions}
838849
839850\subsection{Elaborating Declarations}
840851
852+We can use $\ttinterp{\cdot}$ to
853+build the top level $\MO{Elab}$ operation, which translates \IdrisM{} type, function
854+and class declarations into \TT{} declarations.
855+
856+\newcommand{\edo}[1]{\RW{do}\:\AR{#1}}
857+
858+\subsubsection{Elaborating Type Declarations}
859+
860+To elaborate a type declaration, we simply create a new proof state,
861+translate the \IdrisM{} type to a \TT{} type, then add the resulting type
862+as a \TT{} declaration:
863+
864+\DM{
865+\MO{Elab}\:(\vx\Hab\vt)\:\mq
866+\:\edo{\MO{NewProof}\:\Set\\
867+ \ttinterp{\vt}\\
868+ \vt'\gets\MO{Term}\\
869+ \MO{TTDecl}\:(\vx\Hab\vt')
870+}}
871+
872+The final $\MO{TTDecl}$ takes the result of elaboration, type checks it,
873+and adds it to the global context if type checking succeeds. This final type check
874+ensures that the elaboration process does not allow any ill-typed terms to creep
875+into the context.
841876
842877\subsubsection{Elaborating Data Types}
843878
879+To elaborate a data declaration, we need to elaborate the type declaration itself,
880+as a normal type declaration. This ensures that the type is in scope when
881+elaborating the constructor types. We then use the results to build a \TT{} data
882+declaration.
883+
884+\DM{
885+\AR{
886+\MO{Elab}\:(\idata\;\ihab{\vx}{\vt}\;\iwhere\;\tc)\\
887+\hg\hg\mq\:\edo{\MO{NewProof}\:\Set\\
888+ \ttinterp{\vt}\\
889+ \vt'\gets\MO{Term}\\
890+ \MO{TTDecl}\:(\vx\Hab\vt')\\
891+ \tc'\gets\vec{\MO{ElabCon}}\:\tc\\
892+ \MO{TTDecl}\:(\Data\:\vx\Hab\vt'\:\Where\:\tc')
893+}
894+\AR{
895+\MO{ElabCon}\:(\vx\Hab\vt)\\
896+\hg\hg\mq\: \edo{\MO{NewProof}\:\Set\\
897+ \ttinterp{\vt}\\
898+ \vt'\gets\MO{Term}\\
899+ \RW{return}\:(\vx\Hab\vt')
900+}
901+}}}
902+
844903\subsubsection{Elaborating Pattern Matching}
845904
905+Work clause by clause, $\MO{ElabClause}$ returns a left and right hand side, and
906+may have the side effect of adding things to the context, such as definitions in
907+$\iwhere$ clauses. Collect together in a full definition at the end.
908+
909+In the simplest case, no $\iwhere$ clause:
910+
911+\DM{
912+\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?
913+}
914+
915+How do we elaborate the left hand side, given that elaboration is type directed, and
916+we do not know its type until after we have elaborated it? The easiest way, which
917+requires no change to the elaborator, is to define a type $\TC{Infer}$:
918+
919+\DM{
920+\Data\hg\TC{Infer}\Hab\Set\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Set}\SC\va\to\TC{Infer}
921+}
922+
923+Now to elaborate the left hand side, we elaborate $\DC{MkInfer}\:\_\:(\vx\:\ttt)$ and
924+extract the value and unified type when complete.
925+
926+\DM{
927+\AR{
928+\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:\\
929+\hg\hg\edo{
930+\MO{NewProof}\:\TC{Infer};\;
931+\ttinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
932+\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
933+\tp\gets\MO{Patterns}\\
934+\MO{NewTerm}\:\vT;\;
935+\ttinterp{\ve}\\
936+\VV{rhs}\gets\MO{Term}\\
937+\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\VV{rhs})
938+}
939+}
940+}
941+
942+This infers a type for the left hand side, creating pattern variable bindings. Then,
943+it elaborates the right hand side using the inferred type of the left hand side
944+and the inferred pattern bindings, which are retrieved from the state with the
945+$\MO{Patterns}$ operation. Finally, it returns a pattern clause in \TT{} form.
946+To elaborate a collection of pattern clauses, we simply map $\MO{ElabClause}$ over
947+the clauses and add the resulting collection to \TT{}.
948+
949+\DM{
950+\AR{
951+\MO{Elab}\:\vec{\VV{pclause}}\:\mq\:
952+\edo{
953+\tc\gets\vec{\MO{ElabClause}}\:\vec{\VV{pclause}}\\
954+\MO{TTDecl}\:\tc
955+}
956+}
957+}
958+
959+Elaborating a clause is made only slightly more complex by the presence of
960+$\iwhere$ clauses. In this case, we elaborate the left hand side, add the pattern
961+bound variables as extra arguments to the declarations in the $\iwhere$ block,
962+and recursively elaborate before elaborating the right hand side.
963+
964+\DM{
965+\AR{
966+\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve\:\iwhere\:\td)\:\mq\:\\
967+\hg\hg\edo{
968+\MO{NewProof}\:\TC{Infer};\;
969+\ttinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
970+\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
971+\tp\gets\MO{Patterns}\\
972+(\td', \ve') \gets\MO{Lift}\:\tp\:\td\:\ve\\
973+\vec{\MO{Elab}}\:\td'\\
974+\MO{NewTerm}\:\vT;\;
975+\ttinterp{\ve'}\\
976+\VV{rhs}\gets\MO{Term}\\
977+\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\VV{rhs})
978+}
979+}
980+}
981+
982+In \TT{}, all definitions must be at the top level. Therefore, the declarations
983+in the $\iwhere$ block are lifted out, adding the pattern bound names as additional arguments
984+to ensure they are in scope, using the $\MO{Lift}$ operation. This also modifies
985+the right hand side $\ve$ to use the lifted definitions, rather than the original.
986+
987+\subsubsection{Elaborating the \texttt{with} rule}
988+
989+The \texttt{with} rule allows \remph{dependent} pattern matching on intermediate values.
990+To translate this into \TT{}, we need to construct an auxiliary top level
991+definition for
992+the intermediate pattern match. For example, recall \tFN{natToBin}:
993+
994+\useverb{natToBin}
995+
996+\noindent
997+This is equivalent to the following, using top level definitions only:
998+
999+\begin{SaveVerbatim}{natToBinw}
1000+
1001+natToBin : Nat -> List Bool
1002+natToBin O = Nil
1003+natToBin k = natToBin' k (parity k)
1004+
1005+\end{SaveVerbatim}
1006+\begin{SaveVerbatim}{natToBinwp}
1007+
1008+natToBin' : (n : Nat) -> Parity n -> List Bool
1009+natToBin' (j + j) even = False :: natToBin j
1010+natToBin' (S (j + j)) odd = True :: natToBin j
1011+
1012+\end{SaveVerbatim}
1013+\useverb{natToBinw}
1014+
1015+\useverb{natToBinwp}
1016+
1017+The difference when using the \texttt{with} rule is that there is no need for
1018+the explicit type declaration for the auxiliary function \texttt{natToBin}.
1019+Elaboration of \texttt{with} builds the type declaration and auxiliary function
1020+automatically:
1021+
1022+
1023+\DM{
1024+\AR{
1025+\MO{ElabClause}\:(\vx\:\ttt\:\iwith\:\ve\:\vec{\VV{pclause}})\:\mq\\
1026+\hg\hg\edo{
1027+\MO{NewProof}\:\TC{Infer};\;
1028+\ttinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1029+\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1030+\tp\gets\MO{Patterns}\\
1031+\MO{NewTerm}\:\TC{Infer};\;
1032+\ttinterp{\DC{MkInfer}\:\_\:\ve}\\
1033+\DC{MkInfer}\:\vW\:\vw'\gets\MO{Term}\\
1034+\MO{TTDecl}\:(\vx'\Hab\tp\to\vW\to\vT)\\
1035+\tc'\gets\vec{\MO{MatchWith}}\:\tp\:(\vx\:\ttt)\:\vec{\VV{pclause}}\\
1036+\vec{\MO{Elab}}\:\tc'\\
1037+\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\vx'\:\tp\:\vw')
1038+}
1039+\medskip\\
1040+\MO{MatchWith}\:\tp\:(\vx\:\ttt)\:(\vx\:\tw)\:\mq\\
1041+\hg\hg\edo{
1042+
1043+}
1044+}
1045+}
1046+
1047+A $\iwith$ block in a clause for $\vx$
1048+results in an auxiliary definition $\vx'$, where $\vx'$ is a fresh name,
1049+which takes an extra argument corresponding to the intermediate result which
1050+is to be matched.
1051+$\MO{MatchWith}$ matches the left hand side of the top level definition against
1052+each $\VV{pclause}$, using the result of the match to build each pattern clause
1053+for $\vx'$.
1054+
1055+
8461056\subsubsection{Elaborating Class and Instance Declarations}
8471057
1058+\subsection{Syntax Extensions}
1059+
1060+\subsubsection{Metavariables}
1061+
1062+\subsubsection{\texttt{case} expressions}
1063+
1064+\subsubsection{Pairs and Dependent Pairs}
1065+