@@ -72,12 +72,12 @@ typing rules for binders ensure that no $?$ bindings leak into types.
7272
7373\subsection{Proof State}
7474
75−A proof state is a tuple, $(\vC, \Delta, \vT, \vQ)$, containing:
75+A proof state is a tuple, $(\vC, \Delta, \ve, \vQ)$, containing:
7676
7777\begin{itemize}
78−\item A global context, $\vC$, containing pattern matching definitions
78+\item A global context, $\vC$, containing pattern matching definitions and their types
7979\item A local context, $\Delta$, containing pattern bindings
80−\item A proof term, $\vT$, in \TTdev{}
80+\item A proof term, $\ve$, in \TTdev{}
8181\item A hole queue, $\vQ$
8282%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
8383\end{itemize}
@@ -120,7 +120,9 @@ head of the hole queue.
120120Elaboration of an \Idris{} expression involves creating a new proof state, running
121121a series of tactics to build a complete proof term, then retrieving and \remph{rechecking}
122122the final proof term, which must be a \TT{} program (i.e. does not contain any of the
123−\TTdev{} extensions).
123+\TTdev{} extensions). We call a sub-term which contains no hole or guess bindings
124+\demph{pure}. Although a pure term does not containg hole or guess bindings, it may
125+neverthless \remph{refer} to hole- or guess-bound variables.
124126
125127We initialise a proof state with the $\MO{NewProof}$ operation. Given a global
126128context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:
@@ -132,12 +134,14 @@ context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:
132134The local context is initially empty, and the initial hole queue is the $\vx$ standing for
133135the entire expression. We can reset the proof term with the $\MO{NewTerm}$ operation.
134136In an existing proof state $(\vC, \Delta, \ve, \vQ)$,
135−$\MO{NewTerm}\:\vt$ updates the proof state to:
137+$\MO{NewTerm}\:\vt$ discards the proof term and hole queue, and
138+updates the proof state to:
136139
137140\DM{
138141(\vC, \Delta, \hole{\vx}{\vt}\SC\vx, \langle\vx\rangle)
139142}
140143
144+
141145This allows us in particular to use pattern bindings from the left hand side of a pattern
142146matching definition in the term on the right hand side.
143147
@@ -146,7 +150,7 @@ matching definition in the term on the right hand side.
146150The system state is a tuple, $(\vC,\vA,\vI)$, containing:
147151
148152\begin{itemize}
149−\item A global context, $\vC$, containing pattern matching definitions
153+\item A global context, $\vC$, containing pattern matching definitions and their types
150154\item Implicit arguments, $\vA$, recording which arguments are implicit for each global name
151155\item Type class instances, $\vI$, containing dictionaries for type classes
152156\end{itemize}
@@ -205,7 +209,7 @@ $\Gamma$, returning its type.
205209$\MO{Check}$ will fail
206210if the expression is not well-typed.
207211\item $\Eval\:\ve$, which evaluates a well-typed expression $\ve$ relative to a context
208−$\Gamma$, returing its normal form.
212+$\Gamma$, returning its normal form.
209213\item
210214$\Unify\:\ve_1\:\ve_2$,
211215which unifies $\ve_1$ and $\ve_2$ by finding the values that holes must be instantiated
@@ -229,7 +233,8 @@ $\Gamma$ which contains all the bindings and pattern bindings in scope at that
229233point in the term. The sub-term $\vt$ will either be a hole binding
230234$\hole{\vx}{\vT}\SC\ve$ or a guess binding $\guess{\vx}{\vT}{\vv}\SC\ve$. The
231235tactic 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,
236+well-typed, with a type convertible to the type of $\vt$.
237+Tactics may also have the side effect of updating the proof state,
233238therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
234239
235240We define a set of primitive tactics: $\MO{Create}$, $\MO{Fill}$ and $\MO{Solve}$
@@ -305,7 +310,7 @@ the guess is substituted into its scope:
305310\DM{
306311\PA{\A}{
307312\MO{Solve}_\Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve) &
308− \MoRet{\RW{return}\:\ve[\vv/\vx]\hg\RW{if}\:\MO{Pure}\:\vv}
313+ \MoRet{\RW{return}\:\ve[\vv/\vx]\hg\mbox{(if $\MO{Pure}\:\vv$)}}
309314}
310315}
311316
@@ -317,15 +322,15 @@ handle failure using the $\MO{Try}$ tactic combinator:
317322\DM{
318323\PA{\A\A\A}{
319324\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}}}
325+ \MoRet{\AR{\VV{t1}_\Gamma\:\vt\hg\mbox{(if $\VV{t1}$ succeeds)} \\
326+ \VV{t2}_\Gamma\:\vt\hg\mbox{(otherwise)}}}
322327}
323328}
324329
325330\subsubsection{Creating binders}
326331
327332We also define primitive tactics for constructing binders. We can create a $\lambda$
328−binding if the goal is a function type:
333+binding if the goal normalises to a function type:
329334
330335\DM{
331336\PA{\A\A}{
@@ -406,10 +411,10 @@ building the right hand side.
406411\subsubsection{Example}
407412
408413Tactics 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
414+locates the appropriate sub-term, applies the tactic with the context
415+local to this sub-term, and
416+replaces the sub-term with the term returned by the
417+tactic. It then updates the hole queue in the proof state, and updates holes which have
413418been solved by unification. If the tactic creates new holes, these are automatically
414419added to the \remph{head} of the hole queue.
415420For example, consider the following simple
@@ -450,6 +455,13 @@ state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{
450455Note in particular that each $\MO{Attack}$ and each $\MO{Fill}$, which create new guesses,
451456are closed with a $\MO{Solve}$.
452457
458+Setting up elaboration in this way, with a proof state captured in a monad,
459+and a primitive collection of tactics,
460+makes it easy to derive more complex tactics for elaborating higher level language constructs,
461+in much the same way as the \texttt{Ltac} language in Coq. As a result, elaboration of
462+a language construct (or a program such as $\FN{id}$) bears a strong resemblance to
463+a Coq proof script.
464+
453465\FFIG{
454466\AR{
455467\MO{MkIdType}\:\mq\:\RW{do}\;