@@ -1,4 +1,5 @@
11\newcommand{\ttinterp}[1]{\mathcal{E}\interp{#1}}
2+\newcommand{\ttpinterp}[1]{\mathcal{P}\interp{#1}}
23\newcommand{\uninterp}[1]{\mathcal{T}\interp{#1}}
34
45\section{Elaborating \Idris{}}
@@ -86,6 +87,12 @@ instantiating one such variable also instantiates all of its dependencies.
8687
8788\label{sect:prfstate}
8889
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}.
8996A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:
9097
9198\begin{itemize}
@@ -111,20 +118,28 @@ a new proof state, with an empty proof term, and using the high level definition
111118to direct the building of a final proof state, with a complete proof term.
112119
113120In the implementation, the proof state is captured in an elaboration monad,
114−\texttt{Elab}, which is simply a state monad with exceptions. This monad
115−supports various operations for querying and updating the proof state,
116−manipulating terms, generating fresh names, etc. However, we will describe
117−\Idris{} elaboration in terms of meta-operations on the proof state, in order
118−to capture the essence of the elaboration process without being distracted by
119−implementation details. These meta-operations include:
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}$:
124+
125+\DM{
126+\RW{data}\:\MO{Result}\:\vt\:=\:\MO{Success}\:\vt\:\mid\:\MO{Failure}\:\MO{Err}
127+}
128+
129+The \texttt{Elab} monad supports various operations for querying and updating
130+the proof state, manipulating terms, generating fresh names, etc. However, we
131+will describe \Idris{} elaboration in terms of meta-operations on the proof
132+state, in order to capture the essence of the elaboration process without being
133+distracted by implementation details. These meta-operations include:
120134
121135\begin{itemize}
122136\item \demph{Queries} which retrieve values from the proof state, without modifying
123137the state. For example, we can:
124138\begin{itemize}
125139\item Get the type of the current sub goal ($\MO{Type}$).
126−\item Retrieve the local context $\Gamma$ at the current sub goal.
127−($\MO{Context}$)
140+\item Get the current proof term ($\MO{Term}$).
141+\item Retrieve the local context $\Gamma$ at the current sub goal
142+($\MO{Context}$).
128143\item Type check ($\MO{Check}$) or normalise ($\MO{Normalise}$) a term relative
129144to $\Gamma$.
130145\end{itemize}
@@ -164,90 +179,126 @@ updates the proof state to:
164179(\vC, \Delta, \hole{\vx}{\vt}\SC\vx, \langle\rangle, \langle\vx\rangle)
165180}
166181
167−
168−This allows the elaborator to use pattern bindings from the left
182+Resetting the term and queue but retaining pattern bindings
183+allows the elaborator to use pattern bindings from the left
169184hand side of a pattern matching definition in the term on the right hand side.
170185
171−\subsection{System State}
172−
173−\label{sect:sysstate}
174−
175−The system state is a tuple, $(\vC,\vA,\vI)$, containing:
176−
177−\begin{itemize}
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
181−\end{itemize}
182−
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.
189−
190−For each global name, $\vA$ records whether its arguments are explicit, implicit,
191−or type class constraints. For example, recall the declaration
192−of \texttt{vAdd}:
193−
194−\begin{SaveVerbatim}{vAddImpT}
195−
196−vAdd : Num a => Vect a n -> Vect a n -> Vect a n
197−
198−\end{SaveVerbatim}
199−\useverb{vAddImpT}
200−
201−\noindent
202−Written in full, and giving each argument an explicit name, we get the
203−type declaration:
204−
205−\begin{SaveVerbatim}{vAddImpT}
206−
207−vAdd : (a : _) -> (n : _) -> (c : Num a) ->
208− (xs : Vect a n) -> (ys : Vect a n) -> Vect a n
209−
210−\end{SaveVerbatim}
211−\useverb{vAddImpT}
212−
213−\noindent
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.
218186
219187\newcommand{\Check}{\MO{Check}_\Gamma}
220188\newcommand{\Eval}{\MO{Normalise}_\Gamma}
221189\newcommand{\Unify}{\MO{Unify}_\Gamma}
222190\newcommand{\PrimUnify}{\MO{PrimUnify}_\Gamma}
191+\newcommand{\Subst}{\MO{Subst}}
223192
224193\subsection{Tactics}
225194
226195% Meta-operations Check, Normalise, Unify
227196In order to build \TT{} expressions from \Idris{} programs, we define a collection
228197of 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
230−primitive meta-operations:
198+may have side-effects including failure, or updating the proof state, and
199+may fail. We have the following primitive meta-operations:
231200
232201\begin{itemize}
233202\item $\MO{Get}$ and $\MO{Put}$ which allow direct access to the proof state.
234203% Focus and Unfocus don't need to be primitive, we could show in terms of
235204% Get and Put
236−\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.
205+%\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue.
206+%\item $\MO{Unfocus}$, which moves the current hole to the back of the hole queue.
238207\item $\Check\:\ve$, which type checks an expression $\ve$ relative to a context
239208$\Gamma$, returning its type.
240209$\MO{Check}$ will fail
241210if the expression is not well-typed.
242211\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.
244214\item
245215$\PrimUnify\:\ve_1\:\ve_2$,
246216which attempts to unify $\ve_1$ and $\ve_2$ by finding the values with which
247217holes must be instantiated for $\ve_1$ and $\ve_2$ to be convertible relative
248218to $\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.
249221\end{itemize}
250222
223+\noindent
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:
227+
228+\DM{
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')\\
232+}
233+}
234+
235+\noindent
236+Correspondingly, $\MO{Unfocus}$ moves the currently in focus hole to the
237+end of the hole queue:
238+
239+\DM{
240+\MO{Unfocus}\:=\:\RW{do}\:\AR{
241+(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
242+\MO{Put}\:(\vC,\Delta,\vP,\vQ;\vn)\\
243+}
244+}
245+
246+\noindent
247+$\MO{NewHole}$ declares that a new hole has been created and is to be solved
248+next:
249+
250+\DM{
251+\MO{NewHole}\:=\:\RW{do}\:\AR{
252+(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\
253+\MO{Put}\:(\vC,\Delta,\vP,\vn;\vQ)\\
254+}
255+}
256+
257+\noindent
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
260+form:
261+
262+\DM{
263+\PA{\A\A}{
264+\MO{Tactic}_\Gamma & \:\vec{\VV{args}} & \:\vt & \MoRet{\vt'}
265+}
266+}
267+
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.
277+
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
283+tactic.
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.
287+
288+\FFIG{
289+\mbox{\textbf{RunTac definition goes here}}
290+}
291+{Applying tactics to the proof state}
292+{runtac}
293+
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.
299+
300+\subsubsection{Unification}
301+
251302Unification is crucial to the success of elaboration --- it is unification
252303which finds values of implicit arguments, in particular. We do not require
253304unification to succeed immediately, in general, as instantiating a hole may
@@ -255,11 +306,11 @@ affect the solution to other unification problems. Instead,
255306$\MO{PrimUnify}$ may give one of the following results:
256307
257308\begin{itemize}
258−\item $\MO{Success}$, if 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
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$.
311+If $\tp$ is empty, there is a solution for $\ve_1$ and $\ve_2$.
312+\item $\MO{Failure}\:\ve$, if no solution is found due to a failure to unify
260313sub-terms in normal form.
261−\item $\MO{Blocked}$, otherwise, in which case further elaboration may lead
262−to further refinement of the problem.
263314\end{itemize}
264315
265316$\MO{Unify}$ attempts to solve the given unification problem using
@@ -275,28 +326,6 @@ state. This operation is given in Figure \ref{unifyps}.
275326{The $\MO{Unify}$ meta-operation}
276327{unifyps}
277328
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:
280−
281−\DM{
282−\PA{\A\A}{
283−\MO{Tactic}_\Gamma & \:\vec{\VV{args}} & \:\vt & \MoRet{\vt'}
284−}
285−}
286−
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.
296−
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.
300329
301330\subsubsection{Creating and destroying holes}
302331
@@ -448,17 +477,56 @@ Each of these tactics require the term in focus to be of the form $\hole{\vx}{\v
448477This is important, because if the scope of the binding were an arbitrary expression $\ve$,
449478the binder would be scoped across this \emph{whole} expression rather than the subexpression
450479$\vx$ as intended.
451−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
453−of the queue:
480+The $\MO{Attack}$ tactic ensures that a hole
481+is in the appropriate form, creating a new hole $\vx'$ which is placed at the
482+head of the queue:
454483
455484\DM{
456485\PA{\A}{
457486\MO{Attack}_\Gamma & (\hole{\vx}{\vT}\SC\ve) &
458− \MoRet{\RW{return}\:\guess{\vx}{\vT}{(\hole{\vh}{\vT}\SC\vh)}\SC\ve}
487+ \MoRet{\RW{do}\:\AR{
488+ \MO{NewHole}\;\vx'\\
489+ \RW{return}\;\guess{\vx}{\vT}{(\hole{\vx'}{\vT}\SC\vx')}\SC\ve}}
490+}
491+}
492+
493+\noindent
494+For example, consider the following proof term:
495+
496+\DM{
497+\hole{\vx}{\va\to\vb}\SC\vx\:\ve
498+}
499+
500+\noindent
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:
504+
505+\DM{
506+\AR{
507+\lam{\vn}{\va}\SC\hole{\vx}{\vb}\SC\vx\:\ve
459508}
460509}
461510
511+\noindent
512+If, on the other hand, we $\MO{Attack}$ the hole then instantiate it with
513+a $\lambda$ binding $\vn$, we get:
514+
515+\DM{
516+\begin{array}{ll}
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$)}
521+\end{array}
522+}
523+
524+\noindent
525+Now, once $\vx'$ has been instantiated, the guess for $\vx$ can safely be
526+closed with $\MO{Solve}$.
527+
528+\subsubsection{Pattern Binders}
529+
462530Finally, we can convert a hole binding to a pattern binding by giving the
463531pattern variable a name. This solves a hole
464532by adding the pattern binding to the proof state, and updating the proof term
@@ -481,14 +549,8 @@ building the right hand side.
481549
482550\subsubsection{Example}
483551
484−Tactics are executed by a higher level meta-operation $\MO{RunTac}$, which
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
552+To illustrate how tactics are applied, using $\MO{RunTac}$, to build a
553+complete term by refining a proof state, let us consider the following
492554\TT{} definition for the identify function:
493555
494556\DM{
@@ -498,10 +560,11 @@ For example, consider the following simple
498560}
499561}
500562
501−We can build $\FN{id}$ either as a complete term, or by applying a sequence of tactics.
502−To achieve this, we create a proof state initialised with the type of $\FN{id}$ and
503−apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using $\MO{RunTac}$.
504−Note that the types on each $\MO{Lambda}$ are solved by unification:
563+We can build $\FN{id}$ either as a complete term, or by applying a sequence of
564+tactics. To achieve this, we create a proof state initialised with the type of
565+$\FN{id}$ and apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using
566+$\MO{RunTac}$. Note that the types on each $\MO{Lambda}$ are taken from
567+the goal type.
505568
506569\DM{
507570\AR{
@@ -521,14 +584,135 @@ Note that the types on each $\MO{Lambda}$ are solved by unification:
521584}
522585}
523586
587+\FFIG{
588+\begin{array}{lll}
589+\mbox{Initial state}
590+& \hole{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vx
591+& \langle\vx\rangle \\
592+%
593+\MO{Attack} &
594+\underline{
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
597+}
598+\SC\vx
599+}
600+&
601+\langle\vh_0,\vx\rangle\\
602+%
603+\MO{Lambda}\:\vA &
604+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
605+\underline{
606+\lam{\vA}{\Type}\SC\hole{\vh_0}{\all{\va}{\vA}\SC\vA}\SC\vh_0
607+}
608+}
609+\SC\vx
610+&
611+\langle\vh_0,\vx\rangle\\
612+%
613+\MO{Attack} &
614+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
615+\lam{\vA}{\Type}\SC
616+\underline{
617+\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
618+{\hole{\vh_1}{\all{\va}{\vA}\SC\vA}\SC\vh_1}
619+\SC\vh_0
620+}
621+}
622+\SC\vx
623+&
624+\langle\vh_1,\vh_0,\vx\rangle\\
625+%
626+\MO{Lambda}\:\va &
627+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
628+\lam{\vA}{\Type}\SC
629+\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
630+{
631+\underline{
632+\lam{\va}{\vA}\SC\hole{\vh_1}{\vA}\SC\vh_1
633+}
634+}
635+\SC\vh_0
636+}
637+\SC\vx
638+&
639+\langle\vh_1,\vh_0,\vx\rangle\\
640+%
641+\MO{Fill}\:\va &
642+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
643+\lam{\vA}{\Type}\SC
644+\\
645+&
646+\hg\hg\hg\hg\hg\hg\hg\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
647+{
648+\lam{\va}{\vA}\SC
649+\underline{
650+\guess{\vh_1}{\vA}{\va}\SC\vh_1
651+}
652+}
653+\SC\vh_0
654+}
655+\SC\vx
656+&
657+\langle\vh_1,\vh_0,\vx\rangle\\
658+%
659+\MO{Solve} &
660+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
661+\lam{\vA}{\Type}\SC
662+\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
663+{
664+\lam{\va}{\vA}\SC
665+\underline{
666+\va
667+}
668+}
669+\SC\vh_0
670+}
671+\SC\vx
672+&
673+\langle\vh_0,\vx\rangle\\
674+%
675+\MO{Solve} &
676+\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
677+\lam{\vA}{\Type}\SC
678+\underline{
679+\lam{\va}{\vA}\SC
680+\va
681+}
682+}
683+\SC\vx
684+&
685+\langle\vx\rangle\\
686+%
687+\MO{Solve} &
688+\underline{
689+\lam{\vA}{\Type}\SC
690+\lam{\va}{\vA}\SC
691+\va
692+}
693+&
694+\langle\rangle\\
695+
696+\end{array}
697+}
698+{Proof state development for $\MO{MkId}$}
699+{mkidrefine}
700+
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.
707+
524708To aid readability, we will elide $\MO{RunTac}$, and use a semi-colon to indicate
525709sequencing --- in the implementation we use wrapper functions for each tactic to
526710apply $\MO{RunTac}$.
527711Using this convention, we can build $\FN{id}$'s type and definition as shown
528712in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
529713state. 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,
531−are closed with a $\MO{Solve}$.
714+Note in particular that each tactic which introduces a guess ($\MO{Fill}$
715+and $\MO{Solve}$ is closed with a $\MO{Solve}$).
532716
533717Setting up elaboration in this way, with a proof state captured in a monad,
534718and a primitive collection of tactics,
@@ -583,6 +767,56 @@ a Coq proof script.
583767%\DM{
584768%}
585769
770+\subsection{System State}
771+
772+\label{sect:sysstate}
773+
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:
778+
779+\begin{itemize}
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
783+\end{itemize}
784+
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.
790+
791+For each global name, $\vA$ records whether its arguments are explicit, implicit,
792+or type class constraints. For example, recall the declaration
793+of \texttt{vAdd}:
794+
795+\begin{SaveVerbatim}{vAddImpT}
796+
797+vAdd : Num a => Vect a n -> Vect a n -> Vect a n
798+
799+\end{SaveVerbatim}
800+\useverb{vAddImpT}
801+
802+\noindent
803+Written in full, and giving each argument an explicit name, we get the
804+type declaration:
805+
806+\begin{SaveVerbatim}{vAddImpT}
807+
808+vAdd : (a : _) -> (n : _) -> (c : Num a) ->
809+ (xs : Vect a n) -> (ys : Vect a n) -> Vect a n
810+
811+\end{SaveVerbatim}
812+\useverb{vAddImpT}
813+
814+\noindent
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.
819+
586820\subsection{Elaborating Expressions}
587821
588822\newcommand{\piimp}[2]{\mbox{\texttt{\{ $#1$ : $#2$ \} -> }}}
@@ -611,10 +845,10 @@ a Coq proof script.
611845\begin{array}{rll@{\hg}rll}
612846\ve ::= & \vc & (\mbox{constant}) &
613847\mid & \vx & (\mbox{variable}) \\
614−\mid & \vt & (\mbox{type}) &
615−\mid & \ve\:\ta & (\mbox{function application}) \\
616848\mid & \ilam{\vx}\:\ve & (\mbox{lambda abstraction}) &
617−\mid & \ilet{\vx}{\ve}\:\ve & (\mbox{let binding}) \\
849+\mid & \ve\:\ta & (\mbox{function application}) \\
850+\mid & \ilet{\vx}{\ve}\:\ve & (\mbox{let binding}) &
851+\mid & \piexp{\vx}{\vt}\vt & (\mbox{explicit function space}) \\
618852%\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) &
619853%\mid & \mvar{\vx} & (\mbox{metavariable}) \\
620854\mid & \_ & (\mbox{placeholder})
@@ -627,11 +861,6 @@ a Coq proof script.
627861\end{array}
628862\medskip\\
629863\begin{array}{rll}
630−\vt ::= & \ve & (\mbox{expression}) \\
631−\mid & \piexp{\vx}{\vt}\vt & (\mbox{explicit function space}) \\
632−\end{array}
633−\medskip\\
634−\begin{array}{rll}
635864\VV{declty} ::= & \ve & (\mbox{expression}) \\
636865\mid & \piexp{\vx}{\vt}\VV{declty} & (\mbox{explicit function space}) \\
637866\mid & \piimp{\vx}{\vt}\VV{declty} & (\mbox{implicit function space}) \\
@@ -707,14 +936,21 @@ than one at a time.
707936%Implicit and type class arguments? Expanded at the application site (we need to know
708937%it's the global name after all and we do that by type).
709938
710−To elaborate expressions, we define a meta-operation $\ttinterp{\cdot}$ which
711−runs relative to a proof state (see Section \ref{sect:prfstate}). Its effect is
939+To elaborate expressions, we define meta-operations $\ttinterp{\cdot}$ and
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.
944+Their effect is
712945to update the proof state so that the hole in focus contains a representation
713946of the given expression, by applying tactics. We assume that the proof state
714947has already been set up, which means that elaboration can always be
715948\remph{type-directed} since the proof state contains the type of the expression we
716949are building.
717950
951+In all cases except the elaboration of variables and constantes,
952+$\ttpinterp{\vx}\:=\:\ttinterp{\vx}$.
953+
718954\subsubsection{Elaborating variables and constants}
719955
720956In the simplest cases, there is a direct translation from an \IdrisM{} expression to
@@ -728,19 +964,22 @@ the \MO{Fill} tactic:
728964}
729965}
730966
731−We need not concern ourselves with type checking variables or constants here --- $\MO{Fill}$
732−will handle this, type checking $\vx$ or $\vc$ and unifying the result with the
733−hole type. If there are any errors, elaboration will fail.
967+Since $\MO{Fill}$ creates a guess binding, we use $\MO{Solve}$ to instantiate
968+the guess. We need not concern ourselves with type checking variables or
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,
971+elaboration will fail.
734972
735−If we are building the left hand side of a pattern clause, however, there is a problem,
736−as it is the left hand side which \remph{defines} variables. In this context, we assume
737−that attempting to elaborate a variable which does not type check means that the variable
738−is a pattern variable:
973+If we are building the left hand side of a pattern clause, however, there is a
974+problem, as it is the left hand side which \remph{defines} variables. In this
975+context, we assume that attempting to elaborate a variable which does not type
976+check means that the variable is a pattern variable:
739977
740978\DM{
741−\ttinterp{\vx}\:\mq\:
979+\ttpinterp{\vx}\:\mq\:
742980\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)
982+}
744983}
745984
746985We also need to elaborate \remph{placeholders}, which are subexpressions we expect to
@@ -758,9 +997,9 @@ fails.
758997
759998\subsubsection{Elaborating bindings}
760999
761−To elaborate a $\lambda$-binding, we $\MO{Attack}$ the hole, which must be a function type,
762−apply the $\MO{Lambda}$ tactic, elaborate the scope, then $\MO{Solve}$, which discharges
763−the $\MO{Attack}$:
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
1002+then elaborate the scope and $\MO{Solve}$, which discharges the $\MO{Attack}$:
7641003
7651004\DM{
7661005\ttinterp{\ilam{\vx}\ve}\:\mq\:
@@ -856,30 +1095,24 @@ forms:
8561095}
8571096}
8581097
859−The first problem has a solution: $\vf=\TC{Int}$. The second and third problems have
860−no solution without further information. In the second case, we cannot conclude
861−anything about $\vf$ or $\vx$ just from knowing that $\vf\:\vx\:=\:\TC{Int}$.
862−In the third case, although we have $\vx\:=\:\vx$ in argument position, we cannot
863−conclude that $\vf\:=\:\vg$ unless we know that the function which solves $\vf$ or
864−$\vg$ is injective.
865−
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.
871−
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
876−arguments first.
1098+The first problem has a solution: $\vf=\TC{Int}$. The second and third problems
1099+have no solution without further information. In the second case, we cannot
1100+conclude anything about $\vf$ or $\vx$ just from knowing that
1101+$\vf\:\vx\:=\:\TC{Int}$. In the third case, although we have $\vx\:=\:\vx$ in
1102+argument position, we cannot conclude that $\vf\:=\:\vg$ in general as a
1103+result.
8771104
878−Elaborating a global function application makes a $\MO{Claim}$ for each argument
879−in turn. Then the function is elaborated, applied to each of the claimed arguments.
880−Finally, each argument which has been given explicitly is elaborated. If this fails,
881−elaboration tries again in the opposite order. Finally, any type
882−class instance arguments are resolved with the built-in $\MO{Instance}$ tactic.
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.
1110+Elaborating a global function application makes a $\MO{Claim}$ for each
1111+argument in turn. Then the function is elaborated, applied to each of the
1112+claimed arguments. Each argument which has been given explicitly is
1113+elaborated.
1114+Finally, any type class instance arguments are resolved with the
1115+built-in $\MO{Instance}$ tactic.
8831116
8841117\DM{
8851118\ttinterp{\vx\:\ta}\:\mq\:
@@ -888,18 +1121,9 @@ class instance arguments are resolved with the built-in $\MO{Instance}$ tactic.
8881121\AR{
8891122(\tn,\tv)\:\gets\:\MO{Expand}\:\vx\:\ta\\
8901123\vec{\MO{Claim}}\:(\tn\Hab\tT)\\
891−\MO{Try}\:\AR{
892−(\RW{do}\:\AR{
8931124\MO{Fill}\:\vx\:\tn\\
8941125\vec{\MO{Focus}}\:\tn;\:\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
895−\MO{Solve})
896−}\\
897−(\RW{do}\:\AR{
898−\vec{\MO{Focus}}\:\tn;\:\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
899−\MO{Fill}\:\vx\:\tn\\
900−\MO{Solve})
901−}}
902−\\
1126+\MO{Solve} \\
9031127\vec{\MO{Instance}}\:\tn\hg\mbox{(for type class constraint argument $\vn$)}
9041128}
9051129}
@@ -910,27 +1134,19 @@ a type class instance which would solve the goal directly. First, it examines th
9101134context, then recursively searches the global context. $\MO{Instance}$ is covered
9111135in detail in Section \ref{sect:instance}.
9121136
913−To elaborate a simple function application, of an arbitrary expression to an arbitrary
914−argument, we need not worry about implicit arguments or class constraints. Instead,
915−the function and argument are elaborated, and the results applied. Since elaboration
916−is type directed, however, there must be an 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:
1137+To elaborate a simple function application, of an arbitrary expression to an
1138+arbitrary argument, we need not worry about implicit arguments or class
1139+constraints. Instead, the function and argument are elaborated, and the results
1140+applied. Since elaboration is type directed, however, there must be an
1141+appropriate type for the function.
9191142
9201143\DM{
9211144\ttinterp{\ve\:\va}\:\mq\:\RW{do}\:
9221145\AR{
9231146\MO{Claim}\:(\vA\Hab\Type);\;\MO{Claim}\:(\vB\Hab\Type)\\
9241147\MO{Claim}\:(\vf\Hab\vA\to\vB);\;\MO{Claim}\:(\vs\Hab\vA)\\
925−\MO{Try}\:
926−\AR{
927−(\RW{do}\:\AR{
9281148\MO{Focus}\:\vf;\;\ttinterp{\ve}\\
929−\MO{Focus}\:\vs;\;\ttinterp{\va})}\\
930−(\RW{do}\:\AR{
9311149\MO{Focus}\:\vs;\;\ttinterp{\va}\\
932−\MO{Focus}\:\vf;\;\ttinterp{\ve})}\\
933−}
9341150}
9351151}
9361152
@@ -1021,7 +1237,7 @@ extracting the value and unified type when complete.
10211237\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:\\
10221238\hg\hg\edo{
10231239\MO{NewProof}\:\TC{Infer};\;
1024−\ttinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1240+\ttpinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
10251241\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
10261242\tp\gets\MO{Patterns}\\
10271243\MO{NewTerm}\:\vT;\;
@@ -1059,7 +1275,7 @@ which are then recursively elaborated before the right hand side.
10591275\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve\:\iwhere\:\td)\:\mq\:\\
10601276\hg\hg\edo{
10611277\MO{NewProof}\:\TC{Infer};\;
1062−\ttinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1278+\ttpinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
10631279\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
10641280\tp\gets\MO{Patterns}\\
10651281(\td', \ve') \gets\MO{Lift}\:\tp\:\td\:\ve\\
@@ -1201,13 +1417,13 @@ variables necessary to type $\vW$ and the rest, as before.
12011417
12021418\subsubsection{Elaborating Class and Instance Declarations}
12031419
1204−Type classes are implemented as dictionaries of functions for each instance. Therefore,
1205−a type class declaration elaborates to a record type containing all of the functions
1206−in the class, and an instance is simply an instance of the record. The methods
1207−are translated to top level functions which extract the relevant function from the
1208−dictionary.
1209−For example, for the \texttt{Show} type class, the \texttt{class}
1210−declaration is translated to:
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}.
1422+Therefore, a type class declaration elaborates to a record type containing all
1423+of the functions in the class, and an instance is simply an instance of the
1424+record. The methods are translated to top level functions which extract the
1425+relevant function from the dictionary. For example, for the \texttt{Show} type
1426+class, the \texttt{class} declaration is translated to:
12111427
12121428\begin{SaveVerbatim}{showdata}
12131429
@@ -1225,7 +1441,7 @@ An instance for a type \texttt{a} is then a value of type \texttt{Show a}; for e
12251441
12261442\begin{SaveVerbatim}{shownatf}
12271443
1228−showNat : Show Nat;
1444+showNat : Show Nat
12291445showNat = instanceShow show' where
12301446 show' : Nat -> String
12311447 show' O = "O"
@@ -1312,15 +1528,8 @@ In general, \texttt{class} declarations are elaborated as follows:
13121528(\vec{\VV{meth}}\Hab\ttt)\gets\td\\
13131529\MO{Elab}\:
13141530\AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Type\:\iwhere\\
1315−\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\:\ta)}
1316−}
1317−}
1318−}
1319−
1320−\DM{
1321−\AR{
1322−\AR{
1323−\vec{\MO{ElabMeth}}\:\vec{\VV{meth}}\:\td\\
1531+\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\:\ta)}\\
1532+\vec{\MO{ElabMeth}}\:(\vec{\VV{meth}}\Hab\ttt)\\
13241533\vec{\MO{ElabParent}}\:\tc
13251534}
13261535\medskip\\
@@ -1339,13 +1548,16 @@ In general, \texttt{class} declarations are elaborated as follows:
13391548}
13401549
13411550\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}$:
13431555
13441556\DM{
13451557\AR{
13461558\MO{Elab}\:(\iinstance\;\piconst{\tc}\TC{C}\:\ttt\:\iwhere\:\td)\\
13471559\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\\
13491561\vec{\VV{ty'}}\:=\:\vec{\VV{ty}}[\ttt/\ta]\\
13501562\MO{Elab}\:(\FN{instanceC}\Hab\piconst{\tc}\TC{C}\:\ttt)\\
13511563\MO{Elab}\:\AR{