@@ -6,7 +6,9 @@ An \Idris{} program consists of a series of declarations --- data types, functio
6type classes and instances. In this section, we describe how these high level declarations
6type classes and instances. In this section, we describe how these high level declarations
7are translated into a \TT{} program consisting of inductive families and pattern matching
7are translated into a \TT{} program consisting of inductive families and pattern matching
8function definitions. We will need to work at the \remph{declaration} level, and at
8function 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\begin{itemize}
13\begin{itemize}
12\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
@@ -14,6 +16,7 @@ the \remph{expression} level, defining the following meta-operations:
14one or more \TT{} declarations.
16one or more \TT{} declarations.
15\end{itemize}
17\end{itemize}
17\subsection{The Development Calculus \TTdev}
20\subsection{The Development Calculus \TTdev}
19We build \TT{} expressions by using high level \Idris{} expressions to
22We build \TT{} expressions by using high level \Idris{} expressions to
@@ -32,9 +35,9 @@ binding and a \remph{guess} binding.
32These extensions are given in Figure \ref{ttdev}.
35These extensions are given in Figure \ref{ttdev}.
33The \remph{guess} binding is
36The \remph{guess} binding is
34similar to a $\LET$ binding, but without any computational force,
37similar 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.
36Using binders to represent holes is useful in a dependently typed setting since
39Using 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
38instantiating one such value also instantiates all of its dependencies. The
41instantiating one such value also instantiates all of its dependencies. The
39typing rules for binders ensure that no $?$ bindings leak into types.
42typing rules for binders ensure that no $?$ bindings leak into types.
@@ -79,7 +82,9 @@ A proof state is a tuple, $(\vC, \Delta, \vT, \vQ)$, containing:
79%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
82%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
80\end{itemize}
83\end{itemize}
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$
83we ensure that each bound name is unique. Holes essentially refer to \remph{sub goals}
88we ensure that each bound name is unique. Holes essentially refer to \remph{sub goals}
84in the proof.
89in the proof.
85When this queue is empty, the proof term is complete.
90When 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
117the final proof term, which must be a \TT{} program (i.e. does not contain any of the
122the final proof term, which must be a \TT{} program (i.e. does not contain any of the
118\TTdev{} extensions).
123\TTdev{} extensions).
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:
129+(\vC, \cdot, \hole{\vx}{\vt}\SC\vx, \langle\vx\rangle)
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:
138+(\vC, \Delta, \hole{\vx}{\vt}\SC\vx, \langle\vx\rangle)
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.
120\subsection{System State}
144\subsection{System State}
122The system state is a tuple, $(\vC,\vA,\vI)$, containing:
146The 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
175primitive meta-operations:
199primitive meta-operations:
177\begin{itemize}
201\begin{itemize}
178−\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue
202+\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
203+\item $\Check\:\ve$, which type checks an expression $\ve$ relative to a context
180−$\Gamma$. \\
204+$\Gamma$, returning its type.
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
205+$\MO{Check}$ will fail
183if the expression is not well-typed.
206if the expression is not well-typed.
184−\item $\MO{Normalise}$, which evaluates a well-typed expression relative to a context
207+\item $\Eval\:\ve$, which evaluates a well-typed expression $\ve$ relative to a context
185−$\Gamma$.\\
208+$\Gamma$, returing its normal form.
186−$\Eval\:\ve\:\mq\:\vv$ means that evaluating the expression $\ve$ returns the
209+\item
187−value $\vv$.
210+$\Unify\:\ve_1\:\ve_2$,
188−\item $\MO{Unify}$, which unifies two well-typed expressions.
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
211+which unifies $\ve_1$ and $\ve_2$ by finding the values that holes must be instantiated
192−$\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$
212+with for $\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$
193(i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold). $\MO{Unify}$ will fail
213(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.
195\end{itemize}
215\end{itemize}
197\remph{Tactics} are specifically meta-operations which operate on the sub-term given
217\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
201\PA{\A\A}{
221\PA{\A\A}{
202−\MO{Tactic}_\Gamma & \vec{\VV{args}} & \vt & \MoRet{\vt'}
222+\MO{Tactic}_\Gamma & \:\vec{\VV{args}} & \:\vt & \MoRet{\vt'}
206−A tactic takes a sequence of zero or more arguments $\vec{\VV{args}}$ followed by the sub-term $\vt$
226+A tactic takes a sequence of zero or more arguments $\vec{\VV{args}}$ followed
207−on which it is operating. It runs relative to a context $\Gamma$ which contains all the bindings
227+by the sub-term $\vt$ on which it is operating. It runs relative to a context
208−and pattern bindings
228+$\Gamma$ which contains all the bindings and pattern bindings in scope at that
209−in scope at that point in the term. The sub-term $\vt$ will either be a hole binding
229+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
230+$\hole{\vx}{\vT}\SC\ve$ or a guess binding $\guess{\vx}{\vT}{\vv}\SC\ve$. The
211−new term $\vt'$ which can take any form, provided it is well-typed. Tactics are executed by a higher
231+tactic returns a new term $\vt'$ which can take any form, provided it is
212−level meta-operation $\MO{RunTac}$, which locates the appropriate sub-term, replaces it with the
232+well-typed. Tactics may also have the side effect of updating the proof state,
213−term returns by the tactic, updates the hole queue in the proof state, and updates holes which
233+therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
214−have been solved by unification.
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.
216−Creating and destroying holes: Claim, Fill, Solve
239+\subsubsection{Creating and destroying holes}
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:
219\PA{\A\A}{
246\PA{\A\A}{
220\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &
247\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} \\
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$:
226\PA{\A\A}{
257\PA{\A\A}{
227\MO{Fill}_\Gamma & \vv & (\hole{\vx}{\vT}\SC\ve) &
258\MO{Fill}_\Gamma & \vv & (\hole{\vx}{\vT}\SC\ve) &
228 \MoRet{\RW{do}\:\AR{
259 \MoRet{\RW{do}\:\AR{
229− (\vv',\vT') \leftarrow \Check\:\vv\\
260+ \vT' \leftarrow \Check\:\vv\\
230 \Unify\:\vT\:\vT'\\
261 \Unify\:\vT\:\vT'\\
231− \RW{return}\:\guess{\vx}{\vT}{\vv'}\SC\SC\ve}
262+ \RW{return}\:\guess{\vx}{\vT}{\vv'}\SC\ve}
268+For example, consider the following proof term:
272+\hole{\vA}{\Set}\SC\hole{\vk}{\Nat}\SC
273+\hole{\vx}{\vA}\SC\hole{\vxs}{\Vect\:\vA\:\vk}\SC
275+\hole{\vys}{\Vect\:\vA\:(\suc\:\vk)}\SC\vys
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:
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$.
290+Therefore the resulting proof term is:
295+\guess{\vx}{\TC{Int}}{42}\SC\hole{\vxs}{\Vect\:\TC{Int}\:\vk}\SC
297+\hole{\vys}{\Vect\:\TC{Int}\:(\suc\:\vk)}\SC\vys
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:
238\MO{Solve}_\Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve) &
307\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}
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:
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}}}
243−Attack, Lambda, Pi, Let
325+\subsubsection{Creating binders}
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:
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
342+We can create a $\forall$ binding if the goal is a $\TC{Set}$:
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
356+To create a $\LET$ binding, we give a type and a value.
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\\
365+ \RW{return}\:\LET\:\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx
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
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
381+\MO{Attack}_\Gamma & (\hole{\vx}{\vT}\SC\ve) &
382+ \MoRet{\RW{return}\:\guess{\vx}{\vT}{(\hole{\vh}{\vT}\SC\vh)}\SC\ve}
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:
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]
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.
406+\subsubsection{Example}
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:
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
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}$:
431+\MO{MkId}\:\mq\:\RW{do}\:
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}\\
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}$.
455+\MO{MkIdType}\:\mq\:\RW{do}\;
457+ \MO{NewProof}\:\Set\\
458+ \MO{Attack} ; \MO{Pi}\:(\vA\Hab\Set) ;
459+ \MO{Attack} ; \MO{Pi}\:(\va\Hab\vA) \\
461+ \MO{Solve} ; \MO{Solve} ; \MO{Solve} \\
465+\MO{MkId}\:\mq\:\RW{do}\;
467+ \vt\:\leftarrow\:\MO{MkIdType}; \MO{NewProof}\:\vt\\
468+ \MO{Attack} ; \MO{Lambda}\;\vA ;
469+ \MO{Attack} ; \MO{Lambda}\;\va \\
471+ \MO{Solve} ; \MO{Solve} ; \MO{Solve}\\
476+{Building $\FN{id}$ with tactics}
248%--- give unify in full, esp. as it solves sub goals? Maybe...
479%--- give unify in full, esp. as it solves sub goals? Maybe...