@@ -72,12 +72,12 @@ typing rules for binders ensure that no $?$ bindings leak into types.
73\subsection{Proof State}
73\subsection{Proof State}
75−A proof state is a tuple, $(\vC, \Delta, \vT, \vQ)$, containing:
75+A proof state is a tuple, $(\vC, \Delta, \ve, \vQ)$, containing:
77\begin{itemize}
77\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
79\item A local context, $\Delta$, containing pattern bindings
79\item A local context, $\Delta$, containing pattern bindings
80−\item A proof term, $\vT$, in \TTdev{}
80+\item A proof term, $\ve$, in \TTdev{}
81\item A hole queue, $\vQ$
81\item A hole queue, $\vQ$
82%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
82%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
83\end{itemize}
83\end{itemize}
@@ -120,7 +120,9 @@ head of the hole queue.
120Elaboration of an \Idris{} expression involves creating a new proof state, running
120Elaboration of an \Idris{} expression involves creating a new proof state, running
121a series of tactics to build a complete proof term, then retrieving and \remph{rechecking}
121a series of tactics to build a complete proof term, then retrieving and \remph{rechecking}
122the 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
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.
125We initialise a proof state with the $\MO{NewProof}$ operation. Given a global
127We initialise a proof state with the $\MO{NewProof}$ operation. Given a global
126context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:
128context $\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:
132The local context is initially empty, and the initial hole queue is the $\vx$ standing for
134The local context is initially empty, and the initial hole queue is the $\vx$ standing for
133the entire expression. We can reset the proof term with the $\MO{NewTerm}$ operation.
135the entire expression. We can reset the proof term with the $\MO{NewTerm}$ operation.
134In an existing proof state $(\vC, \Delta, \ve, \vQ)$,
136In an existing proof state $(\vC, \Delta, \ve, \vQ)$,
137+$\MO{NewTerm}\:\vt$ discards the proof term and hole queue, and
135−$\MO{NewTerm}\:\vt$ updates the proof state to:
138+updates the proof state to:
138(\vC, \Delta, \hole{\vx}{\vt}\SC\vx, \langle\vx\rangle)
141(\vC, \Delta, \hole{\vx}{\vt}\SC\vx, \langle\vx\rangle)
141This allows us in particular to use pattern bindings from the left hand side of a pattern
145This allows us in particular to use pattern bindings from the left hand side of a pattern
142matching definition in the term on the right hand side.
146matching definition in the term on the right hand side.
@@ -146,7 +150,7 @@ matching definition in the term on the right hand side.
146The system state is a tuple, $(\vC,\vA,\vI)$, containing:
150The system state is a tuple, $(\vC,\vA,\vI)$, containing:
148\begin{itemize}
152\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
150\item Implicit arguments, $\vA$, recording which arguments are implicit for each global name
154\item Implicit arguments, $\vA$, recording which arguments are implicit for each global name
151\item Type class instances, $\vI$, containing dictionaries for type classes
155\item Type class instances, $\vI$, containing dictionaries for type classes
152\end{itemize}
156\end{itemize}
@@ -205,7 +209,7 @@ $\Gamma$, returning its type.
205$\MO{Check}$ will fail
209$\MO{Check}$ will fail
206if the expression is not well-typed.
210if the expression is not well-typed.
207\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
208−$\Gamma$, returing its normal form.
212+$\Gamma$, returning its normal form.
210$\Unify\:\ve_1\:\ve_2$,
214$\Unify\:\ve_1\:\ve_2$,
211which unifies $\ve_1$ and $\ve_2$ by finding the values that holes must be instantiated
215which 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
229point in the term. The sub-term $\vt$ will either be a hole binding
233point 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
234$\hole{\vx}{\vT}\SC\ve$ or a guess binding $\guess{\vx}{\vT}{\vv}\SC\ve$. The
231tactic returns a new term $\vt'$ which can take any form, provided it is
235tactic returns a new term $\vt'$ which can take any form, provided it is
236+well-typed, with a type convertible to the type of $\vt$.
232−well-typed. Tactics may also have the side effect of updating the proof state,
237+Tactics may also have the side effect of updating the proof state,
233therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
238therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
235We define a set of primitive tactics: $\MO{Create}$, $\MO{Fill}$ and $\MO{Solve}$
240We define a set of primitive tactics: $\MO{Create}$, $\MO{Fill}$ and $\MO{Solve}$
@@ -305,7 +310,7 @@ the guess is substituted into its scope:
307\MO{Solve}_\Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve) &
312\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$)}}
@@ -317,15 +322,15 @@ handle failure using the $\MO{Try}$ tactic combinator:
318\PA{\A\A\A}{
323\PA{\A\A\A}{
319\MO{Try}_\Gamma & \VV{t1} & \VV{t2} & \vt &
324\MO{Try}_\Gamma & \VV{t1} & \VV{t2} & \vt &
320− \MoRet{\AR{\VV{t1}_\Gamma\:\vt\hg\RW{if}\:\VV{t1}\:\mbox{succeeds} \\
325+ \MoRet{\AR{\VV{t1}_\Gamma\:\vt\hg\mbox{(if $\VV{t1}$ succeeds)} \\
321− \VV{t2}_\Gamma\:\vt\hg\RW{otherwise}}}
326+ \VV{t2}_\Gamma\:\vt\hg\mbox{(otherwise)}}}
325\subsubsection{Creating binders}
330\subsubsection{Creating binders}
327We also define primitive tactics for constructing binders. We can create a $\lambda$
332We 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:
331\PA{\A\A}{
336\PA{\A\A}{
@@ -406,10 +411,10 @@ building the right hand side.
406\subsubsection{Example}
411\subsubsection{Example}
408Tactics are executed by a higher level meta-operation $\MO{RunTac}$, which
413Tactics are executed by a higher level meta-operation $\MO{RunTac}$, which
409−locates the appropriate sub-term, applies the tactic with the local context
414+locates the appropriate sub-term, applies the tactic with the context
410−and local sub-term, and
415+local to this sub-term, and
411−replaces it with the term returned by the
416+replaces the sub-term with the term returned by the
412−tactic, updates the hole queue in the proof state, and updates holes which have
417+tactic. It then updates the hole queue in the proof state, and updates holes which have
413been solved by unification. If the tactic creates new holes, these are automatically
418been solved by unification. If the tactic creates new holes, these are automatically
414added to the \remph{head} of the hole queue.
419added to the \remph{head} of the hole queue.
415For example, consider the following simple
420For example, consider the following simple
@@ -450,6 +455,13 @@ state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{
450Note in particular that each $\MO{Attack}$ and each $\MO{Fill}$, which create new guesses,
455Note in particular that each $\MO{Attack}$ and each $\MO{Fill}$, which create new guesses,
451are closed with a $\MO{Solve}$.
456are closed with a $\MO{Solve}$.
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
455\MO{MkIdType}\:\mq\:\RW{do}\;
467\MO{MkIdType}\:\mq\:\RW{do}\;