@@ -1,4 +1,5 @@
1\newcommand{\ttinterp}[1]{\mathcal{E}\interp{#1}}
1\newcommand{\ttinterp}[1]{\mathcal{E}\interp{#1}}
2+\newcommand{\ttpinterp}[1]{\mathcal{P}\interp{#1}}
2\newcommand{\uninterp}[1]{\mathcal{T}\interp{#1}}
3\newcommand{\uninterp}[1]{\mathcal{T}\interp{#1}}
4\section{Elaborating \Idris{}}
5\section{Elaborating \Idris{}}
@@ -86,6 +87,12 @@ instantiating one such variable also instantiates all of its dependencies.
87\label{sect:prfstate}
88\label{sect:prfstate}
90+We will build expressions in \TT{} from high level \Idris{} expressions by
91+creating a top level hole binding with the appropriate type, and refining it
92+according to the structure of the \Idris{} expression. Noting the Curry-Howard
93+correspondence between programs and proofs, and the relationship between our
94+method for elaboration and tactic
95+based theorem proving, we refer to a development as a \emph{proof}.
89A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:
96A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:
91\begin{itemize}
98\begin{itemize}
@@ -111,20 +118,28 @@ a new proof state, with an empty proof term, and using the high level definition
111to direct the building of a final proof state, with a complete proof term.
118to direct the building of a final proof state, with a complete proof term.
113In the implementation, the proof state is captured in an elaboration monad,
120In the implementation, the proof state is captured in an elaboration monad,
114−\texttt{Elab}, which is simply a state monad with exceptions. This monad
121+\texttt{Elab}, which is simply a state monad with exceptions.
122+Exceptions are captured by the option type $\MO{Result}$ which
123+either indicates success, or reports an error $\MO{Err}$:
126+\RW{data}\:\MO{Result}\:\vt\:=\:\MO{Success}\:\vt\:\mid\:\MO{Failure}\:\MO{Err}
115−supports various operations for querying and updating the proof state,
129+The \texttt{Elab} monad supports various operations for querying and updating
116−manipulating terms, generating fresh names, etc. However, we will describe
130+the proof state, manipulating terms, generating fresh names, etc. However, we
117−\Idris{} elaboration in terms of meta-operations on the proof state, in order
131+will describe \Idris{} elaboration in terms of meta-operations on the proof
118−to capture the essence of the elaboration process without being distracted by
132+state, in order to capture the essence of the elaboration process without being
119−implementation details. These meta-operations include:
133+distracted by implementation details. These meta-operations include:
121\begin{itemize}
135\begin{itemize}
122\item \demph{Queries} which retrieve values from the proof state, without modifying
136\item \demph{Queries} which retrieve values from the proof state, without modifying
123the state. For example, we can:
137the state. For example, we can:
124\begin{itemize}
138\begin{itemize}
125\item Get the type of the current sub goal ($\MO{Type}$).
139\item Get the type of the current sub goal ($\MO{Type}$).
140+\item Get the current proof term ($\MO{Term}$).
126−\item Retrieve the local context $\Gamma$ at the current sub goal.
141+\item Retrieve the local context $\Gamma$ at the current sub goal
127−($\MO{Context}$)
142+($\MO{Context}$).
128\item Type check ($\MO{Check}$) or normalise ($\MO{Normalise}$) a term relative
143\item Type check ($\MO{Check}$) or normalise ($\MO{Normalise}$) a term relative
129to $\Gamma$.
144to $\Gamma$.
130\end{itemize}
145\end{itemize}
@@ -164,90 +179,126 @@ updates the proof state to:
164(\vC, \Delta, \hole{\vx}{\vt}\SC\vx, \langle\rangle, \langle\vx\rangle)
179(\vC, \Delta, \hole{\vx}{\vt}\SC\vx, \langle\rangle, \langle\vx\rangle)
167−
182+Resetting the term and queue but retaining pattern bindings
168−This allows the elaborator to use pattern bindings from the left
183+allows the elaborator to use pattern bindings from the left
169hand side of a pattern matching definition in the term on the right hand side.
184hand side of a pattern matching definition in the term on the right hand side.
171−\subsection{System State}
173−\label{sect:sysstate}
175−The system state is a tuple, $(\vC,\vA,\vI)$, containing:
178−\item A global context, $\vC$, containing pattern matching definitions and their types
179−\item Implicit arguments, $\vA$, recording which arguments are implicit for each global name
180−\item Type class instances, $\vI$, containing dictionaries for type classes
183−In the implementation, the system state is captured in a monad, \texttt{Idris},
184−which also wraps the current proof state. This monad
185−includes additional information such as syntax overloadings,
186−command line options, and optimisations, which do not concern us here. Elaboration
187−of expressions requires access to the system state in particular in order to expand
188−implicit arguments and resolve type classes.
190−For each global name, $\vA$ records whether its arguments are explicit, implicit,
191−or type class constraints. For example, recall the declaration
194−\begin{SaveVerbatim}{vAddImpT}
196−vAdd : Num a => Vect a n -> Vect a n -> Vect a n
202−Written in full, and giving each argument an explicit name, we get the
205−\begin{SaveVerbatim}{vAddImpT}
207−vAdd : (a : _) -> (n : _) -> (c : Num a) ->
208− (xs : Vect a n) -> (ys : Vect a n) -> Vect a n
214−For \tFN{vAdd}, the state records that \texttt{a} and \texttt{n} are implicit,
215−\texttt{c} is a constraint, and \texttt{xs} and \texttt{ys} are explicit. When
216−the elaborator encounters an application of \tFN{vAdd}, it knows that unless these arguments
217−are given explicitly, the application must be expanded.
219\newcommand{\Check}{\MO{Check}_\Gamma}
187\newcommand{\Check}{\MO{Check}_\Gamma}
220\newcommand{\Eval}{\MO{Normalise}_\Gamma}
188\newcommand{\Eval}{\MO{Normalise}_\Gamma}
221\newcommand{\Unify}{\MO{Unify}_\Gamma}
189\newcommand{\Unify}{\MO{Unify}_\Gamma}
222\newcommand{\PrimUnify}{\MO{PrimUnify}_\Gamma}
190\newcommand{\PrimUnify}{\MO{PrimUnify}_\Gamma}
191+\newcommand{\Subst}{\MO{Subst}}
224\subsection{Tactics}
193\subsection{Tactics}
226% Meta-operations Check, Normalise, Unify
195% Meta-operations Check, Normalise, Unify
227In order to build \TT{} expressions from \Idris{} programs, we define a collection
196In order to build \TT{} expressions from \Idris{} programs, we define a collection
228of meta-operations for querying and modifying the proof state. Meta-operations
197of meta-operations for querying and modifying the proof state. Meta-operations
229−may have side-effects including failure, or updating the proof state. We have the following
198+may have side-effects including failure, or updating the proof state, and
230−primitive meta-operations:
199+may fail. We have the following primitive meta-operations:
232\begin{itemize}
201\begin{itemize}
233\item $\MO{Get}$ and $\MO{Put}$ which allow direct access to the proof state.
202\item $\MO{Get}$ and $\MO{Put}$ which allow direct access to the proof state.
234% Focus and Unfocus don't need to be primitive, we could show in terms of
203% Focus and Unfocus don't need to be primitive, we could show in terms of
235% Get and Put
204% Get and Put
236−\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue.
205+%\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue.
237−\item $\MO{Unfocus}$, which moves the current hole to the back of the hole queue.
206+%\item $\MO{Unfocus}$, which moves the current hole to the back of the hole queue.
238\item $\Check\:\ve$, which type checks an expression $\ve$ relative to a context
207\item $\Check\:\ve$, which type checks an expression $\ve$ relative to a context
239$\Gamma$, returning its type.
208$\Gamma$, returning its type.
240$\MO{Check}$ will fail
209$\MO{Check}$ will fail
241if the expression is not well-typed.
210if the expression is not well-typed.
242\item $\Eval\:\ve$, which evaluates a well-typed expression $\ve$ relative to a context
211\item $\Eval\:\ve$, which evaluates a well-typed expression $\ve$ relative to a context
243−$\Gamma$, returning its normal form.
212+$\Gamma$, returning its normal form. $\MO{Normalise}$ reduces under binders,
213+but does not reduce definitions which are not total.
245$\PrimUnify\:\ve_1\:\ve_2$,
215$\PrimUnify\:\ve_1\:\ve_2$,
246which attempts to unify $\ve_1$ and $\ve_2$ by finding the values with which
216which attempts to unify $\ve_1$ and $\ve_2$ by finding the values with which
247holes must be instantiated for $\ve_1$ and $\ve_2$ to be convertible relative
217holes must be instantiated for $\ve_1$ and $\ve_2$ to be convertible relative
248to $\Gamma$ (i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold).
218to $\Gamma$ (i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold).
219+\item $\Subst\:\vx\:\ve$, which instantiates a hole $\vx$ directly with a term
220+$\ve$, typically arising from unification.
249\end{itemize}
221\end{itemize}
224+Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$ and $\MO{NewHole}$
225+operations which manipulate
226+the hole queue. $\MO{Focus}\:\vn$ moves a hole to the head of the hole queue:
229+\MO{Focus}\:\vn\:=\:\RW{do}\:\AR{
230+(\vC,\Delta,\vP,\vQ;\vn;\vQ')\gets\MO{Get}\\
231+\MO{Put}\:(\vC,\Delta,\vP,\vn;\vQ;\vQ')\\
236+Correspondingly, $\MO{Unfocus}$ moves the currently in focus hole to the
237+end of the hole queue:
240+\MO{Unfocus}\:=\:\RW{do}\:\AR{
241+(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
242+\MO{Put}\:(\vC,\Delta,\vP,\vQ;\vn)\\
247+$\MO{NewHole}$ declares that a new hole has been created and is to be solved
251+\MO{NewHole}\:=\:\RW{do}\:\AR{
252+(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\
253+\MO{Put}\:(\vC,\Delta,\vP,\vn;\vQ)\\
258+\demph{Tactics} are meta-operations which operate on the sub-term given by the
259+hole at the head of the hole queue in the proof state. They take the following
264+\MO{Tactic}_\Gamma & \:\vec{\VV{args}} & \:\vt & \MoRet{\vt'}
268+A tactic takes a sequence of zero or more arguments $\vec{\VV{args}}$ followed
269+by the sub-term $\vt$ on which it is operating. It runs relative to a context
270+$\Gamma$ which contains all the bindings and pattern bindings in scope at that
271+point in the term. The sub-term $\vt$ will either be a hole binding
272+$\hole{\vx}{\vT}\SC\ve$ or a guess binding $\guess{\vx}{\vT}{\vv}\SC\ve$. The
273+tactic returns a new term $\vt'$ which can take any form, provided it is
274+well-typed, with a type convertible to the type of $\vt$.
275+Tactics may also have the side effect of updating the proof state,
276+therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
278+Tactics are executed by a higher level meta-operation $\MO{RunTac}$,
279+given in Figure \ref{runtac} which
280+locates the appropriate sub-term, applies the tactic with the context
281+local to this sub-term, and
282+replaces the sub-term with the term returned by the
284+% It then updates the hole queue in the proof state, and updates holes which have
285+% been solved by unification. If the tactic creates new holes, these are automatically
286+% added to the \remph{head} of the hole queue.
289+\mbox{\textbf{RunTac definition goes here}}
291+{Applying tactics to the proof state}
294+In the remainder of this section, we will define a set of primitive tactics:
295+$\MO{Claim}$, $\MO{Fill}$ and $\MO{Solve}$ which are used to create and destroy
296+holes; and $\MO{Lambda}$, $\MO{Pi}$, $\MO{Let}$ and $\MO{Attack}$ which are
297+used to create binders. First, however, we must explain how unification is
298+applied during elaboration.
300+\subsubsection{Unification}
251Unification is crucial to the success of elaboration --- it is unification
302Unification is crucial to the success of elaboration --- it is unification
252which finds values of implicit arguments, in particular. We do not require
303which finds values of implicit arguments, in particular. We do not require
253unification to succeed immediately, in general, as instantiating a hole may
304unification to succeed immediately, in general, as instantiating a hole may
@@ -255,11 +306,11 @@ affect the solution to other unification problems. Instead,
255$\MO{PrimUnify}$ may give one of the following results:
306$\MO{PrimUnify}$ may give one of the following results:
257\begin{itemize}
308\begin{itemize}
309+\item $\MO{Success}\:(\tx=\te, \tp)$, containing the solved holes mapping
310+$\vx$ to $\ve$, and a possibly empty set of blocked unification problems $\tp$.
258−\item $\MO{Success}$, if there is a solution for $\ve_1$ and $\ve_2$.
311+If $\tp$ is empty, there is a solution for $\ve_1$ and $\ve_2$.
259−\item $\MO{Failure}$, if no solution is found due to a failure to unify
312+\item $\MO{Failure}\:\ve$, if no solution is found due to a failure to unify
260sub-terms in normal form.
313sub-terms in normal form.
261−\item $\MO{Blocked}$, otherwise, in which case further elaboration may lead
262−to further refinement of the problem.
263\end{itemize}
314\end{itemize}
265$\MO{Unify}$ attempts to solve the given unification problem using
316$\MO{Unify}$ attempts to solve the given unification problem using
@@ -275,28 +326,6 @@ state. This operation is given in Figure \ref{unifyps}.
275{The $\MO{Unify}$ meta-operation}
326{The $\MO{Unify}$ meta-operation}
278−\demph{Tactics} are meta-operations which operate on the sub-term given
279−by the hole at the head of the hole queue in the proof state. They take the following form:
283−\MO{Tactic}_\Gamma & \:\vec{\VV{args}} & \:\vt & \MoRet{\vt'}
287−A tactic takes a sequence of zero or more arguments $\vec{\VV{args}}$ followed
288−by the sub-term $\vt$ on which it is operating. It runs relative to a context
289−$\Gamma$ which contains all the bindings and pattern bindings in scope at that
290−point in the term. The sub-term $\vt$ will either be a hole binding
291−$\hole{\vx}{\vT}\SC\ve$ or a guess binding $\guess{\vx}{\vT}{\vv}\SC\ve$. The
292−tactic returns a new term $\vt'$ which can take any form, provided it is
293−well-typed, with a type convertible to the type of $\vt$.
294−Tactics may also have the side effect of updating the proof state,
295−therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
297−We define a set of primitive tactics: $\MO{Claim}$, $\MO{Fill}$ and $\MO{Solve}$
298−which are used to create and destroy holes; and $\MO{Lambda}$, $\MO{Pi}$, $\MO{Let}$
299−and $\MO{Attack}$ which are used to create binders.
301\subsubsection{Creating and destroying holes}
330\subsubsection{Creating and destroying holes}
@@ -448,17 +477,56 @@ Each of these tactics require the term in focus to be of the form $\hole{\vx}{\v
448This is important, because if the scope of the binding were an arbitrary expression $\ve$,
477This is important, because if the scope of the binding were an arbitrary expression $\ve$,
449the binder would be scoped across this \emph{whole} expression rather than the subexpression
478the binder would be scoped across this \emph{whole} expression rather than the subexpression
450$\vx$ as intended.
479$\vx$ as intended.
451−The $\MO{attack}$ tactic ensures that a hole
480+The $\MO{Attack}$ tactic ensures that a hole
452−is in the appropriate form, creating a new hole $\vh$ which is placed at the head
481+is in the appropriate form, creating a new hole $\vx'$ which is placed at the
453−of the queue:
482+head of the queue:
457\MO{Attack}_\Gamma & (\hole{\vx}{\vT}\SC\ve) &
486\MO{Attack}_\Gamma & (\hole{\vx}{\vT}\SC\ve) &
487+ \MoRet{\RW{do}\:\AR{
488+ \MO{NewHole}\;\vx'\\
458− \MoRet{\RW{return}\:\guess{\vx}{\vT}{(\hole{\vh}{\vT}\SC\vh)}\SC\ve}
489+ \RW{return}\;\guess{\vx}{\vT}{(\hole{\vx'}{\vT}\SC\vx')}\SC\ve}}
494+For example, consider the following proof term:
497+\hole{\vx}{\va\to\vb}\SC\vx\:\ve
501+If we try to instantiate $\vx$ with a $\lambda$-binding $\vn$ immediately,
502+without applying $\MO{Attack}$ first, the $\lambda$ will scope over the
503+entirety of $\vx\:\ve$, and the resulting term is not well-typed:
507+\lam{\vn}{\va}\SC\hole{\vx}{\vb}\SC\vx\:\ve
512+If, on the other hand, we $\MO{Attack}$ the hole then instantiate it with
513+a $\lambda$ binding $\vn$, we get:
517+\guess{\vx}{\va\to\vb}{\hole{\vx'}{\va\to\vb}\SC\vx'}\SC\vx\:\ve
518+& \hg\mbox{(after $\MO{Attack}$)}\\
519+\guess{\vx}{\va\to\vb}{\lam{\vn}{\va}\SC\hole{\vx'}{\vb}\SC\vx'}\SC\vx\:\ve
520+& \hg\mbox{(after $\MO{Lambda}\:\vn$)}
525+Now, once $\vx'$ has been instantiated, the guess for $\vx$ can safely be
526+closed with $\MO{Solve}$.
528+\subsubsection{Pattern Binders}
462Finally, we can convert a hole binding to a pattern binding by giving the
530Finally, we can convert a hole binding to a pattern binding by giving the
463pattern variable a name. This solves a hole
531pattern variable a name. This solves a hole
464by adding the pattern binding to the proof state, and updating the proof term
532by adding the pattern binding to the proof state, and updating the proof term
@@ -481,14 +549,8 @@ building the right hand side.
482\subsubsection{Example}
550\subsubsection{Example}
484−Tactics are executed by a higher level meta-operation $\MO{RunTac}$, which
552+To illustrate how tactics are applied, using $\MO{RunTac}$, to build a
485−locates the appropriate sub-term, applies the tactic with the context
486−local to this sub-term, and
487−replaces the sub-term with the term returned by the
488−tactic. It then updates the hole queue in the proof state, and updates holes which have
489−been solved by unification. If the tactic creates new holes, these are automatically
490−added to the \remph{head} of the hole queue.
491−For example, consider the following simple
553+complete term by refining a proof state, let us consider the following
492\TT{} definition for the identify function:
554\TT{} definition for the identify function:
@@ -498,10 +560,11 @@ For example, consider the following simple
501−We can build $\FN{id}$ either as a complete term, or by applying a sequence of tactics.
563+We can build $\FN{id}$ either as a complete term, or by applying a sequence of
502−To achieve this, we create a proof state initialised with the type of $\FN{id}$ and
564+tactics. To achieve this, we create a proof state initialised with the type of
503−apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using $\MO{RunTac}$.
565+$\FN{id}$ and apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using
504−Note that the types on each $\MO{Lambda}$ are solved by unification:
566+$\MO{RunTac}$. Note that the types on each $\MO{Lambda}$ are taken from
@@ -521,14 +584,135 @@ Note that the types on each $\MO{Lambda}$ are solved by unification:
590+& \hole{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vx
591+& \langle\vx\rangle \\
595+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
596+\hole{\vh_0}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vh_0
601+\langle\vh_0,\vx\rangle\\
604+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
606+\lam{\vA}{\Type}\SC\hole{\vh_0}{\all{\va}{\vA}\SC\vA}\SC\vh_0
611+\langle\vh_0,\vx\rangle\\
614+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
617+\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
618+{\hole{\vh_1}{\all{\va}{\vA}\SC\vA}\SC\vh_1}
624+\langle\vh_1,\vh_0,\vx\rangle\\
627+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
629+\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
632+\lam{\va}{\vA}\SC\hole{\vh_1}{\vA}\SC\vh_1
639+\langle\vh_1,\vh_0,\vx\rangle\\
642+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
646+\hg\hg\hg\hg\hg\hg\hg\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
650+\guess{\vh_1}{\vA}{\va}\SC\vh_1
657+\langle\vh_1,\vh_0,\vx\rangle\\
660+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
662+\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
673+\langle\vh_0,\vx\rangle\\
676+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
698+{Proof state development for $\MO{MkId}$}
701+Figure \ref{mkidrefine} shows how each step of this sequence of tactics affects
702+the proof state and hole queue. In each step, the underlined fragment of the
703+term is the fragment in focus. One might observe that the
704+$\MO{Attack}$/$\MO{Solve}$ pairs may be unnecessary in this case, as the term
705+is already in a form suitable for introduction. However, we retain these for
706+uniform treatment of introductions.
524To aid readability, we will elide $\MO{RunTac}$, and use a semi-colon to indicate
708To aid readability, we will elide $\MO{RunTac}$, and use a semi-colon to indicate
525sequencing --- in the implementation we use wrapper functions for each tactic to
709sequencing --- in the implementation we use wrapper functions for each tactic to
526apply $\MO{RunTac}$.
710apply $\MO{RunTac}$.
527Using this convention, we can build $\FN{id}$'s type and definition as shown
711Using this convention, we can build $\FN{id}$'s type and definition as shown
528in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
712in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
529state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.
713state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.
530−Note in particular that each $\MO{Attack}$ and each $\MO{Fill}$, which create new guesses,
714+Note in particular that each tactic which introduces a guess ($\MO{Fill}$
531−are closed with a $\MO{Solve}$.
715+and $\MO{Solve}$ is closed with a $\MO{Solve}$).
533Setting up elaboration in this way, with a proof state captured in a monad,
717Setting up elaboration in this way, with a proof state captured in a monad,
534and a primitive collection of tactics,
718and a primitive collection of tactics,
@@ -583,6 +767,56 @@ a Coq proof script.
770+\subsection{System State}
772+\label{sect:sysstate}
774+To elaborate \Idris{} programs we will build expressions from high level
775+declarations of functions, data types and classes, and add the resulting
776+definitions to a global system state.
777+The system state is a tuple, $(\vC,\vA,\vI)$, containing:
780+\item A global context, $\vC$, containing pattern matching definitions and their types
781+\item Implicit arguments, $\vA$, recording which arguments are implicit for each global name
782+\item Type class information, $\vI$, containing method signatures and dictionaries for type classes
785+In the implementation, the system state is captured in a monad, \texttt{Idris}.
786+This monad includes additional information such as syntax overloadings,
787+command line options, and optimisations, which do not concern us here. Elaboration
788+of expressions requires access to the system state in particular in order to expand
789+implicit arguments and resolve type classes.
791+For each global name, $\vA$ records whether its arguments are explicit, implicit,
792+or type class constraints. For example, recall the declaration
795+\begin{SaveVerbatim}{vAddImpT}
797+vAdd : Num a => Vect a n -> Vect a n -> Vect a n
803+Written in full, and giving each argument an explicit name, we get the
806+\begin{SaveVerbatim}{vAddImpT}
808+vAdd : (a : _) -> (n : _) -> (c : Num a) ->
809+ (xs : Vect a n) -> (ys : Vect a n) -> Vect a n
815+For \tFN{vAdd}, the state records that \texttt{a} and \texttt{n} are implicit,
816+\texttt{c} is a constraint, and \texttt{xs} and \texttt{ys} are explicit. When
817+the elaborator encounters an application of \tFN{vAdd}, it knows that unless these arguments
818+are given explicitly, the application must be expanded.
586\subsection{Elaborating Expressions}
820\subsection{Elaborating Expressions}
588\newcommand{\piimp}[2]{\mbox{\texttt{\{ $#1$ : $#2$ \} -> }}}
822\newcommand{\piimp}[2]{\mbox{\texttt{\{ $#1$ : $#2$ \} -> }}}
@@ -611,10 +845,10 @@ a Coq proof script.
611\begin{array}{rll@{\hg}rll}
845\begin{array}{rll@{\hg}rll}
612\ve ::= & \vc & (\mbox{constant}) &
846\ve ::= & \vc & (\mbox{constant}) &
613\mid & \vx & (\mbox{variable}) \\
847\mid & \vx & (\mbox{variable}) \\
614−\mid & \vt & (\mbox{type}) &
615−\mid & \ve\:\ta & (\mbox{function application}) \\
616\mid & \ilam{\vx}\:\ve & (\mbox{lambda abstraction}) &
848\mid & \ilam{\vx}\:\ve & (\mbox{lambda abstraction}) &
849+\mid & \ve\:\ta & (\mbox{function application}) \\
617−\mid & \ilet{\vx}{\ve}\:\ve & (\mbox{let binding}) \\
850+\mid & \ilet{\vx}{\ve}\:\ve & (\mbox{let binding}) &
851+\mid & \piexp{\vx}{\vt}\vt & (\mbox{explicit function space}) \\
618%\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) &
852%\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) &
619%\mid & \mvar{\vx} & (\mbox{metavariable}) \\
853%\mid & \mvar{\vx} & (\mbox{metavariable}) \\
620\mid & \_ & (\mbox{placeholder})
854\mid & \_ & (\mbox{placeholder})
@@ -627,11 +861,6 @@ a Coq proof script.
627\end{array}
861\end{array}
628\medskip\\
862\medskip\\
629\begin{array}{rll}
863\begin{array}{rll}
630−\vt ::= & \ve & (\mbox{expression}) \\
631−\mid & \piexp{\vx}{\vt}\vt & (\mbox{explicit function space}) \\
635\VV{declty} ::= & \ve & (\mbox{expression}) \\
864\VV{declty} ::= & \ve & (\mbox{expression}) \\
636\mid & \piexp{\vx}{\vt}\VV{declty} & (\mbox{explicit function space}) \\
865\mid & \piexp{\vx}{\vt}\VV{declty} & (\mbox{explicit function space}) \\
637\mid & \piimp{\vx}{\vt}\VV{declty} & (\mbox{implicit function space}) \\
866\mid & \piimp{\vx}{\vt}\VV{declty} & (\mbox{implicit function space}) \\
@@ -707,14 +936,21 @@ than one at a time.
707%Implicit and type class arguments? Expanded at the application site (we need to know
936%Implicit and type class arguments? Expanded at the application site (we need to know
708%it's the global name after all and we do that by type).
937%it's the global name after all and we do that by type).
710−To elaborate expressions, we define a meta-operation $\ttinterp{\cdot}$ which
939+To elaborate expressions, we define meta-operations $\ttinterp{\cdot}$ and
711−runs relative to a proof state (see Section \ref{sect:prfstate}). Its effect is
940+$\ttpinterp{\cdot}$, which run relative to a proof state (see Section
941+\ref{sect:prfstate}). $\ttpinterp{\cdot}$ elaborates \remph{patterns}, i.e.
942+expressions on the left hand side of a pattern matching definition, whereas
943+$\ttinterp{\cdot}$ elaborates expressions on the right hand side.
712to update the proof state so that the hole in focus contains a representation
945to update the proof state so that the hole in focus contains a representation
713of the given expression, by applying tactics. We assume that the proof state
946of the given expression, by applying tactics. We assume that the proof state
714has already been set up, which means that elaboration can always be
947has already been set up, which means that elaboration can always be
715\remph{type-directed} since the proof state contains the type of the expression we
948\remph{type-directed} since the proof state contains the type of the expression we
716are building.
949are building.
951+In all cases except the elaboration of variables and constantes,
952+$\ttpinterp{\vx}\:=\:\ttinterp{\vx}$.
718\subsubsection{Elaborating variables and constants}
954\subsubsection{Elaborating variables and constants}
720In the simplest cases, there is a direct translation from an \IdrisM{} expression to
956In the simplest cases, there is a direct translation from an \IdrisM{} expression to
@@ -728,19 +964,22 @@ the \MO{Fill} tactic:
967+Since $\MO{Fill}$ creates a guess binding, we use $\MO{Solve}$ to instantiate
731−We need not concern ourselves with type checking variables or constants here --- $\MO{Fill}$
968+the guess. We need not concern ourselves with type checking variables or
732−will handle this, type checking $\vx$ or $\vc$ and unifying the result with the
969+constants here --- $\MO{Fill}$ will handle this, type checking $\vx$ or $\vc$
970+and unifying the result with the hole type. If there are any errors,
733−hole type. If there are any errors, elaboration will fail.
971+elaboration will fail.
735−If we are building the left hand side of a pattern clause, however, there is a problem,
973+If we are building the left hand side of a pattern clause, however, there is a
736−as it is the left hand side which \remph{defines} variables. In this context, we assume
974+problem, as it is the left hand side which \remph{defines} variables. In this
737−that attempting to elaborate a variable which does not type check means that the variable
975+context, we assume that attempting to elaborate a variable which does not type
738−is a pattern variable:
976+check means that the variable is a pattern variable:
741−\ttinterp{\vx}\:\mq\:
979+\ttpinterp{\vx}\:\mq\:
742\MO{Try}\:\AR{(\RW{do}\:\MO{Fill}\:\vx;\:\MO{Solve})\\
980\MO{Try}\:\AR{(\RW{do}\:\MO{Fill}\:\vx;\:\MO{Solve})\\
743−(\MO{Pat}\:\vx)\hg\hg\mbox{(If elaborating a left hand side)}}
981+(\MO{Pat}\:\vx)
746We also need to elaborate \remph{placeholders}, which are subexpressions we expect to
985We also need to elaborate \remph{placeholders}, which are subexpressions we expect to
@@ -758,9 +997,9 @@ fails.
759\subsubsection{Elaborating bindings}
998\subsubsection{Elaborating bindings}
761−To elaborate a $\lambda$-binding, we $\MO{Attack}$ the hole, which must be a function type,
1000+To elaborate a $\lambda$-binding, we $\MO{Attack}$ the hole, then apply the
1001+$\MO{Lambda}$ tactic, which will fail if the goal is not a function type. We
762−apply the $\MO{Lambda}$ tactic, elaborate the scope, then $\MO{Solve}$, which discharges
1002+then elaborate the scope and $\MO{Solve}$, which discharges the $\MO{Attack}$:
766\ttinterp{\ilam{\vx}\ve}\:\mq\:
1005\ttinterp{\ilam{\vx}\ve}\:\mq\:
@@ -856,30 +1095,24 @@ forms:
859−The first problem has a solution: $\vf=\TC{Int}$. The second and third problems have
1098+The first problem has a solution: $\vf=\TC{Int}$. The second and third problems
860−no solution without further information. In the second case, we cannot conclude
1099+have no solution without further information. In the second case, we cannot
861−anything about $\vf$ or $\vx$ just from knowing that $\vf\:\vx\:=\:\TC{Int}$.
1100+conclude anything about $\vf$ or $\vx$ just from knowing that
862−In the third case, although we have $\vx\:=\:\vx$ in argument position, we cannot
1101+$\vf\:\vx\:=\:\TC{Int}$. In the third case, although we have $\vx\:=\:\vx$ in
863−conclude that $\vf\:=\:\vg$ unless we know that the function which solves $\vf$ or
1102+argument position, we cannot conclude that $\vf\:=\:\vg$ in general as a
864−$\vg$ is injective.
1103+result.
866−Once $\vf$ or $\vg$ is solved in some other way, perhaps by being given explicitly
867−in another argument, these unification problems can make progress. Otherwise, unification
868−fails. As a result, the order in which functions and arguments are
869−elaborated matters. Sometimes, we may learn more by elaborating a function first
870−and the arguments later, sometimes it may be the other way around.
872−One option when unification fails is to store the problem (i.e. the expressions to be
873−unified with their local context) and refine it with further information when it becomes
874−available. In practice, we have found a simpler approach to be effective: try
875−elaborating the function first, then arguments. If that fails, try elaborating the
1105+Once $\vf$ or $\vg$ is solved in some other way, perhaps by being given
1106+explicitly in another argument, these unification problems can make progress.
1107+Otherwise, unification blocks. In such a case, the elaborator stores the
1108+problem (i.e. the expressions to be unified with their local context) and
1109+refines it with further information when it becomes available.
878−Elaborating a global function application makes a $\MO{Claim}$ for each argument
1110+Elaborating a global function application makes a $\MO{Claim}$ for each
879−in turn. Then the function is elaborated, applied to each of the claimed arguments.
1111+argument in turn. Then the function is elaborated, applied to each of the
880−Finally, each argument which has been given explicitly is elaborated. If this fails,
1112+claimed arguments. Each argument which has been given explicitly is
881−elaboration tries again in the opposite order. Finally, any type
1113+elaborated.
882−class instance arguments are resolved with the built-in $\MO{Instance}$ tactic.
1114+Finally, any type class instance arguments are resolved with the
1115+built-in $\MO{Instance}$ tactic.
885\ttinterp{\vx\:\ta}\:\mq\:
1118\ttinterp{\vx\:\ta}\:\mq\:
@@ -888,18 +1121,9 @@ class instance arguments are resolved with the built-in $\MO{Instance}$ tactic.
889(\tn,\tv)\:\gets\:\MO{Expand}\:\vx\:\ta\\
1122(\tn,\tv)\:\gets\:\MO{Expand}\:\vx\:\ta\\
890\vec{\MO{Claim}}\:(\tn\Hab\tT)\\
1123\vec{\MO{Claim}}\:(\tn\Hab\tT)\\
893\MO{Fill}\:\vx\:\tn\\
1124\MO{Fill}\:\vx\:\tn\\
894\vec{\MO{Focus}}\:\tn;\:\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
1125\vec{\MO{Focus}}\:\tn;\:\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
895−\MO{Solve})
1126+\MO{Solve} \\
898−\vec{\MO{Focus}}\:\tn;\:\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
899−\MO{Fill}\:\vx\:\tn\\
903\vec{\MO{Instance}}\:\tn\hg\mbox{(for type class constraint argument $\vn$)}
1127\vec{\MO{Instance}}\:\tn\hg\mbox{(for type class constraint argument $\vn$)}
@@ -910,27 +1134,19 @@ a type class instance which would solve the goal directly. First, it examines th
910context, then recursively searches the global context. $\MO{Instance}$ is covered
1134context, then recursively searches the global context. $\MO{Instance}$ is covered
911in detail in Section \ref{sect:instance}.
1135in detail in Section \ref{sect:instance}.
913−To elaborate a simple function application, of an arbitrary expression to an arbitrary
1137+To elaborate a simple function application, of an arbitrary expression to an
914−argument, we need not worry about implicit arguments or class constraints. Instead,
1138+arbitrary argument, we need not worry about implicit arguments or class
915−the function and argument are elaborated, and the results applied. Since elaboration
1139+constraints. Instead, the function and argument are elaborated, and the results
1140+applied. Since elaboration is type directed, however, there must be an
916−is type directed, however, there must be an appropriate type for the function.
1141+appropriate type for the function.
917−As before, elaboration tries two orders, as it may learn something from elaborating
918−the function or argument which helps with unification:
921\ttinterp{\ve\:\va}\:\mq\:\RW{do}\:
1144\ttinterp{\ve\:\va}\:\mq\:\RW{do}\:
923\MO{Claim}\:(\vA\Hab\Type);\;\MO{Claim}\:(\vB\Hab\Type)\\
1146\MO{Claim}\:(\vA\Hab\Type);\;\MO{Claim}\:(\vB\Hab\Type)\\
924\MO{Claim}\:(\vf\Hab\vA\to\vB);\;\MO{Claim}\:(\vs\Hab\vA)\\
1147\MO{Claim}\:(\vf\Hab\vA\to\vB);\;\MO{Claim}\:(\vs\Hab\vA)\\
928\MO{Focus}\:\vf;\;\ttinterp{\ve}\\
1148\MO{Focus}\:\vf;\;\ttinterp{\ve}\\
929−\MO{Focus}\:\vs;\;\ttinterp{\va})}\\
931\MO{Focus}\:\vs;\;\ttinterp{\va}\\
1149\MO{Focus}\:\vs;\;\ttinterp{\va}\\
932−\MO{Focus}\:\vf;\;\ttinterp{\ve})}\\
@@ -1021,7 +1237,7 @@ extracting the value and unified type when complete.
1021\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:\\
1237\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:\\
1022\hg\hg\edo{
1238\hg\hg\edo{
1023\MO{NewProof}\:\TC{Infer};\;
1239\MO{NewProof}\:\TC{Infer};\;
1024−\ttinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1240+\ttpinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1025\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1241\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1026\tp\gets\MO{Patterns}\\
1242\tp\gets\MO{Patterns}\\
1027\MO{NewTerm}\:\vT;\;
1243\MO{NewTerm}\:\vT;\;
@@ -1059,7 +1275,7 @@ which are then recursively elaborated before the right hand side.
1059\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve\:\iwhere\:\td)\:\mq\:\\
1275\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve\:\iwhere\:\td)\:\mq\:\\
1060\hg\hg\edo{
1276\hg\hg\edo{
1061\MO{NewProof}\:\TC{Infer};\;
1277\MO{NewProof}\:\TC{Infer};\;
1062−\ttinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1278+\ttpinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1063\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1279\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1064\tp\gets\MO{Patterns}\\
1280\tp\gets\MO{Patterns}\\
1065(\td', \ve') \gets\MO{Lift}\:\tp\:\td\:\ve\\
1281(\td', \ve') \gets\MO{Lift}\:\tp\:\td\:\ve\\
@@ -1201,13 +1417,13 @@ variables necessary to type $\vW$ and the rest, as before.
1202\subsubsection{Elaborating Class and Instance Declarations}
1418\subsubsection{Elaborating Class and Instance Declarations}
1204−Type classes are implemented as dictionaries of functions for each instance. Therefore,
1420+Type classes are implemented as dictionaries of functions for each instance,
1421+following the implementation of first class type classes in Coq~\cite{Sozeau2008}.
1205−a type class declaration elaborates to a record type containing all of the functions
1422+Therefore, a type class declaration elaborates to a record type containing all
1206−in the class, and an instance is simply an instance of the record. The methods
1423+of the functions in the class, and an instance is simply an instance of the
1207−are translated to top level functions which extract the relevant function from the
1424+record. The methods are translated to top level functions which extract the
1209−For example, for the \texttt{Show} type class, the \texttt{class}
1425+relevant function from the dictionary. For example, for the \texttt{Show} type
1210−declaration is translated to:
1426+class, the \texttt{class} declaration is translated to:
1212\begin{SaveVerbatim}{showdata}
1428\begin{SaveVerbatim}{showdata}
@@ -1225,7 +1441,7 @@ An instance for a type \texttt{a} is then a value of type \texttt{Show a}; for e
1226\begin{SaveVerbatim}{shownatf}
1442\begin{SaveVerbatim}{shownatf}
1228−showNat : Show Nat;
1444+showNat : Show Nat
1229showNat = instanceShow show' where
1445showNat = instanceShow show' where
1230 show' : Nat -> String
1446 show' : Nat -> String
1231 show' O = "O"
1447 show' O = "O"
@@ -1312,15 +1528,8 @@ In general, \texttt{class} declarations are elaborated as follows:
1312(\vec{\VV{meth}}\Hab\ttt)\gets\td\\
1528(\vec{\VV{meth}}\Hab\ttt)\gets\td\\
1313\MO{Elab}\:
1529\MO{Elab}\:
1314\AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Type\:\iwhere\\
1530\AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Type\:\iwhere\\
1315−\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\:\ta)}
1531+\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\:\ta)}\\
1323−\vec{\MO{ElabMeth}}\:\vec{\VV{meth}}\:\td\\
1532+\vec{\MO{ElabMeth}}\:(\vec{\VV{meth}}\Hab\ttt)\\
1324\vec{\MO{ElabParent}}\:\tc
1533\vec{\MO{ElabParent}}\:\tc
1326\medskip\\
1535\medskip\\
@@ -1339,13 +1548,16 @@ In general, \texttt{class} declarations are elaborated as follows:
1341\noindent
1550\noindent
1342−Then \texttt{instance} declarations are elaborated as follows:
1551+Then \texttt{instance} declarations are elaborated as follows. One complication
1552+is that the function definitions in an \texttt{instance} declaration do not
1553+have explicit types, so we must retrieve the method types from the system state
1554+and substitute $\TC{C}\:\ttt$, using $\MO{ExpandTypes}$:
1346\MO{Elab}\:(\iinstance\;\piconst{\tc}\TC{C}\:\ttt\:\iwhere\:\td)\\
1558\MO{Elab}\:(\iinstance\;\piconst{\tc}\TC{C}\:\ttt\:\iwhere\:\td)\\
1347\hg\hg\mq\:\RW{do}\:\AR{
1559\hg\hg\mq\:\RW{do}\:\AR{
1348−(\vec{\VV{meth}}, \vec{\VV{ty}})\gets\td\\
1560+(\vec{\VV{meth}}, \vec{\VV{ty}})\gets\MO{ExpandTypes}\:\td\\
1349\vec{\VV{ty'}}\:=\:\vec{\VV{ty}}[\ttt/\ta]\\
1561\vec{\VV{ty'}}\:=\:\vec{\VV{ty}}[\ttt/\ta]\\
1350\MO{Elab}\:(\FN{instanceC}\Hab\piconst{\tc}\TC{C}\:\ttt)\\
1562\MO{Elab}\:(\FN{instanceC}\Hab\piconst{\tc}\TC{C}\:\ttt)\\
1351\MO{Elab}\:\AR{
1563\MO{Elab}\:\AR{