@@ -6,7 +6,9 @@ An \Idris{} program consists of a series of declarations --- data types, functio
66type classes and instances. In this section, we describe how these high level declarations
77are translated into a \TT{} program consisting of inductive families and pattern matching
88function definitions. We will need to work at the \remph{declaration} level, and at
9−the \remph{expression} level, defining the following meta-operations:
9+the \remph{expression} level, defining the following meta-operations
10+which together constitute an algorithm for elaborating \Idris{}
11+programs to \TT{}.
1012
1113\begin{itemize}
1214\item $\ttinterp{\cdot}$, which builds a \TT{} expression from an \Idris{} expression
@@ -14,6 +16,7 @@ the \remph{expression} level, defining the following meta-operations:
1416one or more \TT{} declarations.
1517\end{itemize}
1618
19+
1720\subsection{The Development Calculus \TTdev}
1821
1922We build \TT{} expressions by using high level \Idris{} expressions to
@@ -32,9 +35,9 @@ binding and a \remph{guess} binding.
3235These extensions are given in Figure \ref{ttdev}.
3336The \remph{guess} binding is
3437similar to a $\LET$ binding, but without any computational force,
35−i.e. the bound names do not reduce.
38+i.e. there are no reduction rules for guess bindings.
3639Using binders to represent holes is useful in a dependently typed setting since
37−one value may determine another. Attaching a ``guess'' to a binder ensures that
40+one value may determine another. Attaching a guess to a binder ensures that
3841instantiating one such value also instantiates all of its dependencies. The
3942typing rules for binders ensure that no $?$ bindings leak into types.
4043
@@ -79,7 +82,9 @@ A proof state is a tuple, $(\vC, \Delta, \vT, \vQ)$, containing:
7982%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
8083\end{itemize}
8184
82−The \remph{hole queue} is a list of names of hole and guess binders in the proof term ---
85+The \remph{hole queue} is a list of names of hole and guess binders
86+$\langle\vx_1,\vx_2,\ldots,\vx_n\rangle$
87+in the proof term ---
8388we ensure that each bound name is unique. Holes essentially refer to \remph{sub goals}
8489in the proof.
8590When this queue is empty, the proof term is complete.
@@ -117,6 +122,25 @@ a series of tactics to build a complete proof term, then retrieving and \remph{r
117122the final proof term, which must be a \TT{} program (i.e. does not contain any of the
118123\TTdev{} extensions).
119124
125+We initialise a proof state with the $\MO{NewProof}$ operation. Given a global
126+context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:
127+
128+\DM{
129+(\vC, \cdot, \hole{\vx}{\vt}\SC\vx, \langle\vx\rangle)
130+}
131+
132+The local context is initially empty, and the initial hole queue is the $\vx$ standing for
133+the entire expression. We can reset the proof term with the $\MO{NewTerm}$ operation.
134+In an existing proof state $(\vC, \Delta, \ve, \vQ)$,
135+$\MO{NewTerm}\:\vt$ updates the proof state to:
136+
137+\DM{
138+(\vC, \Delta, \hole{\vx}{\vt}\SC\vx, \langle\vx\rangle)
139+}
140+
141+This allows us in particular to use pattern bindings from the left hand side of a pattern
142+matching definition in the term on the right hand side.
143+
120144\subsection{System State}
121145
122146The system state is a tuple, $(\vC,\vA,\vI)$, containing:
@@ -175,23 +199,19 @@ may have side-effects including failure, or updating the proof state. We have th
175199primitive meta-operations:
176200
177201\begin{itemize}
178−\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue
179−\item $\MO{Check}$, which type checks an expression relative to a context
180−$\Gamma$. \\
181−$\Check\:\ve\:\mq\:(\vv,\vt)$ means that checking an expression $\ve$
182−returns a well typed value $\vv$ and its type $\vt$. $\MO{Check}$ will fail
202+\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue.
203+\item $\Check\:\ve$, which type checks an expression $\ve$ relative to a context
204+$\Gamma$, returning its type.
205+$\MO{Check}$ will fail
183206if the expression is not well-typed.
184−\item $\MO{Normalise}$, which evaluates a well-typed expression relative to a context
185−$\Gamma$.\\
186−$\Eval\:\ve\:\mq\:\vv$ means that evaluating the expression $\ve$ returns the
187−value $\vv$.
188−\item $\MO{Unify}$, which unifies two well-typed expressions.
189−\\
190−$\Unify\:\ve_1\:\ve_2\:\mq\:\tu$ means that unifying $\ve_1$ and $\ve_2$ produces a
191−mapping $\tu$ from hole names to the values the holes must be instantiated with for
192−$\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$
207+\item $\Eval\:\ve$, which evaluates a well-typed expression $\ve$ relative to a context
208+$\Gamma$, returing its normal form.
209+\item
210+$\Unify\:\ve_1\:\ve_2$,
211+which unifies $\ve_1$ and $\ve_2$ by finding the values that holes must be instantiated
212+with for $\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$
193213(i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold). $\MO{Unify}$ will fail
194−if it cannot find such a mapping.
214+if it cannot find such values. If successful, $\MO{Unify}$ will update the proof state.
195215\end{itemize}
196216
197217\remph{Tactics} are specifically meta-operations which operate on the sub-term given
@@ -199,51 +219,262 @@ by the hole at the head of the hole queue in the proof state. They take the foll
199219
200220\DM{
201221\PA{\A\A}{
202−\MO{Tactic}_\Gamma & \vec{\VV{args}} & \vt & \MoRet{\vt'}
222+\MO{Tactic}_\Gamma & \:\vec{\VV{args}} & \:\vt & \MoRet{\vt'}
203223}
204224}
205225
206−A tactic takes a sequence of zero or more arguments $\vec{\VV{args}}$ followed by the sub-term $\vt$
207−on which it is operating. It runs relative to a context $\Gamma$ which contains all the bindings
208−and pattern bindings
209−in scope at that point in the term. The sub-term $\vt$ will either be a hole binding
210−$\hole{\vx}{\vT}\SC\ve$ or a guess binding $\guess{\vx}{\vT}{\vv}\SC\ve$. The tactic returns a
211−new term $\vt'$ which can take any form, provided it is well-typed. Tactics are executed by a higher
212−level meta-operation $\MO{RunTac}$, which locates the appropriate sub-term, replaces it with the
213−term returns by the tactic, updates the hole queue in the proof state, and updates holes which
214−have been solved by unification.
226+A tactic takes a sequence of zero or more arguments $\vec{\VV{args}}$ followed
227+by the sub-term $\vt$ on which it is operating. It runs relative to a context
228+$\Gamma$ which contains all the bindings and pattern bindings in scope at that
229+point in the term. The sub-term $\vt$ will either be a hole binding
230+$\hole{\vx}{\vT}\SC\ve$ or a guess binding $\guess{\vx}{\vT}{\vv}\SC\ve$. The
231+tactic returns a new term $\vt'$ which can take any form, provided it is
232+well-typed. Tactics may also have the side effect of updating the proof state,
233+therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
234+
235+We define a set of primitive tactics: $\MO{Create}$, $\MO{Fill}$ and $\MO{Solve}$
236+which are used to create and destroy holes; and $\MO{Lambda}$, $\MO{Pi}$, $\MO{Let}$
237+and $\MO{Attack}$ which are used to create binders.
215238
216−Creating and destroying holes: Claim, Fill, Solve
239+\subsubsection{Creating and destroying holes}
240+
241+The $\MO{Claim}$ tactic, given a name and a type, adds a new hole binding in
242+the scope of the current goal $\vx$, adding the new binding to the hole queue, but
243+keeping $\vx$ at the head:
217244
218245\DM{
219246\PA{\A\A}{
220247\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &
221− \MoRet{\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve} \\
248+ \MoRet{\RW{return}\:\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve} \\
222249}
223250}
224251
252+The $\MO{Fill}$ tactic, given a value $\vv$, attempts to solve the current goal
253+with $\vv$, creating a guess binding in its place. $\MO{Fill}$ attempts to
254+solve other holes by unifying the expected type of $\vx$ with the type of $\vv$:
255+
225256\DM{
226257\PA{\A\A}{
227258\MO{Fill}_\Gamma & \vv & (\hole{\vx}{\vT}\SC\ve) &
228259 \MoRet{\RW{do}\:\AR{
229− (\vv',\vT') \leftarrow \Check\:\vv\\
260+ \vT' \leftarrow \Check\:\vv\\
230261 \Unify\:\vT\:\vT'\\
231− \RW{return}\:\guess{\vx}{\vT}{\vv'}\SC\SC\ve}
262+ \RW{return}\:\guess{\vx}{\vT}{\vv'}\SC\ve}
232263 } \\
233264}
234265}
235266
267+\noindent
268+For example, consider the following proof term:
269+
270+\DM{
271+\AR{
272+\hole{\vA}{\Set}\SC\hole{\vk}{\Nat}\SC
273+\hole{\vx}{\vA}\SC\hole{\vxs}{\Vect\:\vA\:\vk}\SC
274+\\
275+\hole{\vys}{\Vect\:\vA\:(\suc\:\vk)}\SC\vys
276+}
277+}
278+
279+\noindent
280+If $\vx$ is in focus (i.e., at the head of the hole queue) and we attempt to
281+$\MO{Fill}$ it with an $\TC{Int}$ value $42$, we have:
282+
283+\begin{itemize}
284+\item $\Check\:42\:\mq\:\TC{Int}$
285+\item Unifying $\TC{Int}$ with $\vA$ (the type of $\vx$) is only possible if
286+$\vA\:=\:\TC{Int}$, so we solve $\vA$.
287+\end{itemize}
288+
289+\noindent
290+Therefore the resulting proof term is:
291+
292+\DM{
293+\AR{
294+\hole{\vk}{\Nat}\SC
295+\guess{\vx}{\TC{Int}}{42}\SC\hole{\vxs}{\Vect\:\TC{Int}\:\vk}\SC
296+\\
297+\hole{\vys}{\Vect\:\TC{Int}\:(\suc\:\vk)}\SC\vys
298+}
299+}
300+
301+The $\MO{Solve}$ tactic operates on a guess binding. If the guess is \remph{pure}, i.e., it
302+is a \TT{} term containing no hole or guess bindings, then the value attached to
303+the guess is substituted into its scope:
304+
236305\DM{
237306\PA{\A}{
238307\MO{Solve}_\Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve) &
239− \MoRet{\ve[\vv/\vx]}
308+ \MoRet{\RW{return}\:\ve[\vv/\vx]\hg\RW{if}\:\MO{Pure}\:\vv}
309+}
310+}
311+
312+In each of these tactics, if any step fails, or the term in focus does not take
313+the correct form (e.g. is not a guess in the case of $\MO{Solve}$ or not a hole
314+in the case of $\MO{Claim}$ and $\MO{Fill}$, the entire tactic fails. We can
315+handle failure using the $\MO{Try}$ tactic combinator:
316+
317+\DM{
318+\PA{\A\A\A}{
319+\MO{Try}_\Gamma & \VV{t1} & \VV{t2} & \vt &
320+ \MoRet{\AR{\VV{t1}_\Gamma\:\vt\hg\RW{if}\:\VV{t1}\:\mbox{succeeds} \\
321+ \VV{t2}_\Gamma\:\vt\hg\RW{otherwise}}}
240322}
241323}
242324
243−Attack, Lambda, Pi, Let
325+\subsubsection{Creating binders}
244326
245−Apply
327+We also define primitive tactics for constructing binders. We can create a $\lambda$
328+binding if the goal is a function type:
329+
330+\DM{
331+\PA{\A\A}{
332+\MO{Lambda}_\Gamma & \vn & (\hole{\vx}{\vT}\SC\vx) &
333+ \MoRet{\RW{do}\:\AR{
334+ \all{\vy}{\vS}\SC\vT'\:\leftarrow\:\Eval\:\vT \\
335+ \RW{return}\:\lam{\vn}{\vS}\SC\hole{\vx}{\vT'[\vn/\vy]}\SC\vx
336+ }
337+ }
338+}
339+}
246340
341+\noindent
342+We can create a $\forall$ binding if the goal is a $\TC{Set}$:
343+
344+\DM{
345+\PA{\A\A}{
346+\MO{Pi}_\Gamma & (\vn\Hab\vS) & (\hole{\vx}{\Set}\SC\vx) &
347+ \MoRet{\RW{do}\:\AR{
348+ \Set\:\leftarrow\:\Check\:\vS\\
349+ \RW{return}\:\all{\vn}{\vS}\SC\hole{\vx}{\Set}\SC\vx
350+ }
351+ }
352+}
353+}
354+
355+\noindent
356+To create a $\LET$ binding, we give a type and a value.
357+
358+\DM{
359+\PA{\A\A}{
360+\MO{Let}_\Gamma & (\vn\Hab\vS\defq\vv) & (\hole{\vx}{\vT}\SC\vx) &
361+ \MoRet{\RW{do}\:\AR{
362+ \Set\:\leftarrow\:\Check\:\vS\\
363+ \vS'\:\leftarrow\:\Check\:\vv\\
364+ \Unify\:\vS\:\vS'\\
365+ \RW{return}\:\LET\:\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx
366+ }
367+ }
368+}
369+}
370+
371+Each of these tactics require the term in focus to be of the form $\hole{\vx}{\vT}\SC\vx$.
372+This is important, because if the scope of the binding was an arbitrary expression $\ve$,
373+the binder would be scoped across this whole expression rather than the subexpression
374+$\vx$ as intended.
375+The $\MO{attack}$ tactic ensures that a hole
376+is in the appropriate form, creating a new hole $\vh$ which is placed at the head
377+of the queue:
378+
379+\DM{
380+\PA{\A}{
381+\MO{Attack}_\Gamma & (\hole{\vx}{\vT}\SC\ve) &
382+ \MoRet{\RW{return}\:\guess{\vx}{\vT}{(\hole{\vh}{\vT}\SC\vh)}\SC\ve}
383+}
384+}
385+
386+Finally, we can convert a hole binding to a pattern binding by giving the
387+pattern variable a name. This solves a hole
388+by adding the pattern binding to the proof state, and updating the proof term
389+with the pattern variable directly:
390+
391+\DM{
392+\PA{\A\A}{
393+\MO{Pat}_\Gamma & \vn & (\hole{\vx}{\vT}\SC\ve) &
394+ \MoRet{\RW{do}\:\AR{
395+ \MO{PatBind}\:(\vx\Hab\vT)\\
396+ \RW{return}\:\ve[\vn/\vx]
397+ }}
398+}
399+}
400+
401+The $\MO{PatBind}$ operation simply updates the proof state with the given pattern
402+binding. Once we have created bindings from the left hand side of a pattern
403+matching definition, for example, we can retain these bindings for use when
404+building the right hand side.
405+
406+\subsubsection{Example}
407+
408+Tactics are executed by a higher level meta-operation $\MO{RunTac}$, which
409+locates the appropriate sub-term, applies the tactic with the local context
410+and local sub-term, and
411+replaces it with the term returned by the
412+tactic, updates the hole queue in the proof state, and updates holes which have
413+been solved by unification. If the tactic creates new holes, these are automatically
414+added to the \remph{head} of the hole queue.
415+For example, consider the following simple
416+\TT{} definition for the identify function:
417+
418+\DM{
419+\AR{
420+\FN{id}\Hab\all{\vA}{\Set}\SC\all{\va}{\vA}\SC\vA \\
421+\FN{id}\:=\:\lam{\vA}{\Set}\SC\lam{\va}{\vA}\SC\va
422+}
423+}
424+
425+We can build $\FN{id}$ either as a complete term, or by applying a sequence of tactics.
426+To achieve this, we create a proof state initialised with the type of $\FN{id}$ and
427+apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using $\MO{RunTac}$:
428+
429+\DM{
430+\AR{
431+\MO{MkId}\:\mq\:\RW{do}\:
432+ \AR{
433+ \MO{NewProof}\:\all{\vA}{\Set}\SC\all{\va}{\vA}\SC\vA \\
434+ \MO{RunTac}\;\MO{Attack} \\
435+ \MO{RunTac}\;(\MO{Lambda}\;\vA) \\
436+ \MO{RunTac}\;\MO{Attack} \\
437+ \MO{RunTac}\;(\MO{Lambda}\;\va) \\
438+ \MO{RunTac}\;(\MO{Fill}\;\va)\\
439+ \MO{RunTac}\;\MO{Solve}\\
440+ \MO{RunTac}\;\MO{Solve}\\
441+ \MO{RunTac}\;\MO{Solve}\\
442+ }
443+}
444+}
445+
446+To aid readability, we will elide $\MO{RunTac}$, and use a semi-colon to indicate
447+sequencing. Using this convention, we can build $\FN{id}$'s type and definition as shown
448+in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
449+state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.
450+Note in particular that each $\MO{Attack}$ and each $\MO{Fill}$, which create new guesses,
451+are closed with a $\MO{Solve}$.
452+
453+\FFIG{
454+\AR{
455+\MO{MkIdType}\:\mq\:\RW{do}\;
456+ \AR{
457+ \MO{NewProof}\:\Set\\
458+ \MO{Attack} ; \MO{Pi}\:(\vA\Hab\Set) ;
459+ \MO{Attack} ; \MO{Pi}\:(\va\Hab\vA) \\
460+ \MO{Fill}\;\vA \\
461+ \MO{Solve} ; \MO{Solve} ; \MO{Solve} \\
462+ \MO{Term}
463+ }
464+ \medskip\\
465+\MO{MkId}\:\mq\:\RW{do}\;
466+ \AR{
467+ \vt\:\leftarrow\:\MO{MkIdType}; \MO{NewProof}\:\vt\\
468+ \MO{Attack} ; \MO{Lambda}\;\vA ;
469+ \MO{Attack} ; \MO{Lambda}\;\va \\
470+ \MO{Fill}\;\va \\
471+ \MO{Solve} ; \MO{Solve} ; \MO{Solve}\\
472+ \MO{Term}
473+ }
474+}
475+}
476+{Building $\FN{id}$ with tactics}
477+{idelab}
247478
248479%--- give unify in full, esp. as it solves sub goals? Maybe...
249480