@@ -11,9 +11,10 @@ which together constitute an algorithm for elaborating \Idris{}
11programs to \TT{}.
11programs to \TT{}.
13\begin{itemize}
13\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.
15\item $\MO{Elab}$, which processes a top level \Idris{} declaration by generating
15\item $\MO{Elab}$, which processes a top level \Idris{} declaration by generating
16one or more \TT{} declarations.
16one or more \TT{} declarations.
17+\item $\MO{TTDecl}$, which adds a top level \TT{} declaration.
17\end{itemize}
18\end{itemize}
@@ -545,8 +546,8 @@ a Coq proof script.
545\mid & \ve\:\ta & (\mbox{function application}) \\
546\mid & \ve\:\ta & (\mbox{function application}) \\
546\mid & \ilam{\vx}\:\ve & (\mbox{lambda abstraction}) &
547\mid & \ilam{\vx}\:\ve & (\mbox{lambda abstraction}) &
547\mid & \ilet{\vx}{\ve}\:\ve & (\mbox{let binding}) \\
548\mid & \ilet{\vx}{\ve}\:\ve & (\mbox{let binding}) \\
548−\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) &
549+%\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) &
549−\mid & \mvar{\vx} & (\mbox{metavariable}) \\
550+%\mid & \mvar{\vx} & (\mbox{metavariable}) \\
550\mid & \_ & (\mbox{placeholder})
551\mid & \_ & (\mbox{placeholder})
551\end{array}
552\end{array}
552\medskip\\
553\medskip\\
@@ -633,8 +634,8 @@ the \MO{Fill} tactic:
636−\ttinterp{\vx}\:\mq\:\MO{Fill}\:\vx;\:\MO{Solve}\\
637+\ttinterp{\vx}\:\mq\:\RW{do}\:\MO{Fill}\:\vx;\:\MO{Solve}\\
637−\ttinterp{\vc}\:\mq\:\MO{Fill}\:\vc;\:\MO{Solve}\\
638+\ttinterp{\vc}\:\mq\:\RW{do}\:\MO{Fill}\:\vc;\:\MO{Solve}\\
@@ -642,6 +643,17 @@ We need not concern ourselves with type checking variables or constants here ---
642will handle this, type checking $\vx$ or $\vc$ and unifying the result with the
643will handle this, type checking $\vx$ or $\vc$ and unifying the result with the
643hole type. If there are any errors, elaboration will fail.
644hole type. If there are any errors, elaboration will fail.
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:
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)}}
645We also need to elaborate \remph{placeholders}, which are subexpressions we expect to
657We also need to elaborate \remph{placeholders}, which are subexpressions we expect to
646solve by unification. In this case, we simply move on to the next hole in the queue, moving
658solve by unification. In this case, we simply move on to the next hole in the queue, moving
647the current hole to the end of the queue with $\MO{Unfocus}$:
659the current hole to the end of the queue with $\MO{Unfocus}$:
@@ -721,7 +733,6 @@ $\vV$ and $\vX$.
721\ttinterp{\ve}
733\ttinterp{\ve}
725\subsubsection{Elaborating applications}
736\subsubsection{Elaborating applications}
727There are two cases to consider when elaborating applications:
738There are two cases to consider when elaborating applications:
@@ -832,16 +843,223 @@ the function or argument which helps with unification:
835−\subsubsection{Elaborating metavariables}
846+%\subsubsection{Elaborating metavariables}
837−\subsubsection{Elaborating \texttt{case} expressions}
848+%\subsubsection{Elaborating \texttt{case} expressions}
839\subsection{Elaborating Declarations}
850\subsection{Elaborating Declarations}
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.
856+\newcommand{\edo}[1]{\RW{do}\:\AR{#1}}
858+\subsubsection{Elaborating Type Declarations}
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:
865+\MO{Elab}\:(\vx\Hab\vt)\:\mq
866+\:\edo{\MO{NewProof}\:\Set\\
868+ \vt'\gets\MO{Term}\\
869+ \MO{TTDecl}\:(\vx\Hab\vt')
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
842\subsubsection{Elaborating Data Types}
877\subsubsection{Elaborating Data Types}
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
886+\MO{Elab}\:(\idata\;\ihab{\vx}{\vt}\;\iwhere\;\tc)\\
887+\hg\hg\mq\:\edo{\MO{NewProof}\:\Set\\
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')
895+\MO{ElabCon}\:(\vx\Hab\vt)\\
896+\hg\hg\mq\: \edo{\MO{NewProof}\:\Set\\
898+ \vt'\gets\MO{Term}\\
899+ \RW{return}\:(\vx\Hab\vt')
844\subsubsection{Elaborating Pattern Matching}
903\subsubsection{Elaborating Pattern Matching}
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.
909+In the simplest case, no $\iwhere$ clause:
912+\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?
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}$:
920+\Data\hg\TC{Infer}\Hab\Set\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Set}\SC\va\to\TC{Infer}
923+Now to elaborate the left hand side, we elaborate $\DC{MkInfer}\:\_\:(\vx\:\ttt)$ and
924+extract the value and unified type when complete.
928+\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:\\
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}\\
936+\VV{rhs}\gets\MO{Term}\\
937+\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\VV{rhs})
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{}.
951+\MO{Elab}\:\vec{\VV{pclause}}\:\mq\:
953+\tc\gets\vec{\MO{ElabClause}}\:\vec{\VV{pclause}}\\
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.
966+\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve\:\iwhere\:\td)\:\mq\:\\
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'\\
976+\VV{rhs}\gets\MO{Term}\\
977+\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\VV{rhs})
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.
987+\subsubsection{Elaborating the \texttt{with} rule}
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
992+the intermediate pattern match. For example, recall \tFN{natToBin}:
997+This is equivalent to the following, using top level definitions only:
999+\begin{SaveVerbatim}{natToBinw}
1001+natToBin : Nat -> List Bool
1003+natToBin k = natToBin' k (parity k)
1006+\begin{SaveVerbatim}{natToBinwp}
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
1015+\useverb{natToBinwp}
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
1025+\MO{ElabClause}\:(\vx\:\ttt\:\iwith\:\ve\:\vec{\VV{pclause}})\:\mq\\
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')
1040+\MO{MatchWith}\:\tp\:(\vx\:\ttt)\:(\vx\:\tw)\:\mq\\
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
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
846\subsubsection{Elaborating Class and Instance Declarations}
1056\subsubsection{Elaborating Class and Instance Declarations}
1058+\subsection{Syntax Extensions}
1060+\subsubsection{Metavariables}
1062+\subsubsection{\texttt{case} expressions}
1064+\subsubsection{Pairs and Dependent Pairs}