@@ -34,7 +34,7 @@ Holes stand for the parts of programs which have not yet been
34instantiated; this largely follows the Oleg development
34instantiated; this largely follows the Oleg development
35calculus~\cite{McBride1999}.
35calculus~\cite{McBride1999}.
37−The basic idea is to extend the syntax for binders with a \remph{hole}
37+The idea is to extend the syntax for binders with a \remph{hole}
38binding and a \remph{guess} binding.
38binding and a \remph{guess} binding.
39These extensions are given in Figure \ref{ttdev}.
39These extensions are given in Figure \ref{ttdev}.
40The \remph{guess} binding is
40The \remph{guess} binding is
@@ -101,7 +101,7 @@ A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:
101\item Unsolved unification problems, $\vP$
101\item Unsolved unification problems, $\vP$
102\begin{itemize}
102\begin{itemize}
103\item These take the form $(\Gamma,\ve_1,\ve_2)$, i.e. the context in which
103\item These take the form $(\Gamma,\ve_1,\ve_2)$, i.e. the context in which
104−the problem is run, and the expressions to be unified.
104+the problem is to be solved, and the expressions to be unified.
105\end{itemize}
105\end{itemize}
106\item A hole queue, $\vQ$
106\item A hole queue, $\vQ$
107%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
107%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
@@ -110,7 +110,7 @@ the problem is run, and the expressions to be unified.
110The \remph{hole queue} is a priority queue of names of hole and guess binders
110The \remph{hole queue} is a priority queue of names of hole and guess binders
111$\langle\vx_1,\vx_2,\ldots,\vx_n\rangle$
111$\langle\vx_1,\vx_2,\ldots,\vx_n\rangle$
112in the proof term ---
112in the proof term ---
113−ensuring that each bound name is unique. Holes refer to \remph{sub goals}
113+ensuring that each bound name is unique. Holes refer to \remph{sub-goals}
114in the proof. As a proof develops, unification problems arising from unsolved
114in the proof. As a proof develops, unification problems arising from unsolved
115holes may be introduced, and may be solved when those holes are instantiated.
115holes may be introduced, and may be solved when those holes are instantiated.
116When the hole queue is empty, and there are no remaining unification
116When the hole queue is empty, and there are no remaining unification
@@ -130,7 +130,7 @@ either indicates success, or reports an error $\MO{Err}$:
133−If any operation fails during a proof (e.g. a sub term fails to type check)
133+If any operation fails during a proof (e.g. a sub-term fails to type check)
134then the entire proof fails (i.e. returns $\MO{Failure}\;\ve$ with some error
134then the entire proof fails (i.e. returns $\MO{Failure}\;\ve$ with some error
135message $\ve$) unless otherwise handled.
135message $\ve$) unless otherwise handled.
@@ -144,22 +144,21 @@ distracted by implementation details. These meta-operations include:
144\item \demph{Queries} which retrieve values from the proof state, without modifying
144\item \demph{Queries} which retrieve values from the proof state, without modifying
145the state. For example, we can:
145the state. For example, we can:
146\begin{itemize}
146\begin{itemize}
147−\item Get the type of the current sub goal ($\MO{Type}$).
147+\item Get the type of the current sub-goal ($\MO{Type}$)
148−\item Get the current proof term ($\MO{Term}$).
148+\item Get the current proof term ($\MO{Term}$)
149−\item Retrieve the local context $\Gamma$ at the current sub goal
149+\item Retrieve the local context $\Gamma$ at the current sub-goal
150−($\MO{Context}$).
150+($\MO{Context}$)
151\item Type check ($\MO{Check}$) or normalise ($\MO{Normalise}$) a term relative
151\item Type check ($\MO{Check}$) or normalise ($\MO{Normalise}$) a term relative
152−to $\Gamma$.
152+to $\Gamma$
153\end{itemize}
153\end{itemize}
154−\item \demph{Unification}, which unifies two terms (potentially solving sub
154+\item \demph{Unification}, which unifies two terms (potentially solving sub-goals) relative to $\Gamma$. This may introduce new unification problems
155−goals) relative to $\Gamma$. This may introduce new unification problems
156−to the proof state.
155+to the proof state
157−\item \demph{Tactics} which update the proof term. Tactics operate on the sub term
156+\item \demph{Tactics} which update the proof term. Tactics operate on the sub-term
158−at the binder specified by the head of the hole queue $\vQ$.
157+at the binder specified by the head of the hole queue $\vQ$
159−\item \demph{Focussing} on a specific sub goal, which brings a different sub goal to the
158+\item \demph{Focussing} on a specific sub-goal, which brings a different sub-goal to the
160−head of the hole queue.
159+head of the hole queue
161−%\item \demph{Deferring} a sub goal, which adds a new definition to the global context
160+%\item \demph{Deferring} a sub-goal, which adds a new definition to the global context
162−%$\vC$ which solves the sub goal.
161+%$\vC$ which solves the sub-goal.
163\end{itemize}
162\end{itemize}
165Elaboration of an \Idris{} expression involves creating a new proof state,
164Elaboration of an \Idris{} expression involves creating a new proof state,
@@ -307,7 +306,7 @@ of $\vt$. Tactics may also have the side effect of updating the proof state,
307therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
306therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
309Tactics are executed by a higher level meta-operation $\MO{Tactic}$,
308Tactics are executed by a higher level meta-operation $\MO{Tactic}$,
310−given in Figure \ref{runtac} which
309+given in Figure \ref{runtac}, which
311locates the appropriate sub-term, applies the tactic with the context
310locates the appropriate sub-term, applies the tactic with the context
312local to this sub-term, and
311local to this sub-term, and
313replaces the sub-term with the term returned by the
312replaces the sub-term with the term returned by the
@@ -386,12 +385,13 @@ Unification is crucial to the success of elaboration --- it is unification
386which finds values of implicit arguments, in particular. We do not require
385which finds values of implicit arguments, in particular. We do not require
387unification to succeed immediately, in general, as instantiating a hole may
386unification to succeed immediately, in general, as instantiating a hole may
388affect the solution to other unification problems. Instead,
387affect the solution to other unification problems. Instead,
389−$\MO{PrimUnify}$ may give one of the following results:
388+$\PrimUnify\:\ve_1\:\ve_2$ may give one of the following results:
391\begin{itemize}
390\begin{itemize}
392\item $\MO{Success}\;(\tx=\te, \tp)$, containing the solved holes mapping
391\item $\MO{Success}\;(\tx=\te, \tp)$, containing the solved holes mapping
393$\vx$ to $\ve$, and a possibly empty set of blocked unification problems $\tp$.
392$\vx$ to $\ve$, and a possibly empty set of blocked unification problems $\tp$.
394−If $\tp$ is empty, there is a solution for $\ve_1$ and $\ve_2$.
393+If $\tp$ is empty, there is a solution unifying $\ve_1$ and $\ve_2$ in
394+the context $\Gamma$.
395\item $\MO{Failure}\;\ve$, if no solution is found due to a failure to unify
395\item $\MO{Failure}\;\ve$, if no solution is found due to a failure to unify
396sub-terms in normal form.
396sub-terms in normal form.
397\end{itemize}
397\end{itemize}
@@ -543,8 +543,8 @@ problem) and is handled by $\MO{Try}$.
544\subsubsection{Creating binders}
544\subsubsection{Creating binders}
546−We also define primitive tactics for constructing binders. Creating a $\lambda$
546+We also define primitive tactics for constructing binders. Creating a
547−binding requires that the goal normalises to a function type:
547+$\lambda$-binding requires that the goal normalises to a function type:
550\PA{\A\A}{
550\PA{\A\A}{
@@ -627,7 +627,7 @@ entirety of $\vx\;\ve$, and the resulting term is not well-typed:
629If, on the other hand, we $\MO{Attack}$ the hole then instantiate it with
629If, on the other hand, we $\MO{Attack}$ the hole then instantiate it with
630−a $\lambda$ binding $\vn$, we get:
630+a $\lambda$-binding $\vn$, we get:
633\begin{array}{ll}
633\begin{array}{ll}
@@ -668,7 +668,7 @@ building the right hand side.
669To illustrate how tactics are applied, using $\MO{Tactic}$, to build a
669To illustrate how tactics are applied, using $\MO{Tactic}$, to build a
670complete term by refining a proof state, let us consider the following
670complete term by refining a proof state, let us consider the following
671−\TT{} definition for the identify function:
671+\TT{} definition for the identity function:
@@ -866,7 +866,7 @@ a Coq proof script.
866{Building $\FN{id}$ with tactics}
866{Building $\FN{id}$ with tactics}
869−%--- give unify in full, esp. as it solves sub goals? Maybe...
869+%--- give unify in full, esp. as it solves sub-goals? Maybe...
871% Unify' G x t = Success (x, t) if ?x : t in G
871% Unify' G x t = Success (x, t) if ?x : t in G
872% Unify' G t x = Success (x, t) if ?x : t in G
872% Unify' G t x = Success (x, t) if ?x : t in G
@@ -1347,7 +1347,7 @@ to the global context, such as definitions in $\iwhere$ clauses.
1347First, let us consider the simplest case, with no $\iwhere$ clause:
1347First, let us consider the simplest case, with no $\iwhere$ clause:
1350−\MO{ElabClause}\;(\vx\;\ttt\;=\;\ve)\;\mq\;?
1350+\MO{ElabClause}\;(\vx\;\ttt\;=\;\ve)\;\mq\;\ldots
1353How does the left hand side get elaborated, given that elaboration is type directed, and
1353How does the left hand side get elaborated, given that elaboration is type directed, and
@@ -1396,9 +1396,10 @@ the clauses and adding the resulting collection to \TT{}.
1398Elaborating a clause is made only slightly more complex by the presence of
1398Elaborating a clause is made only slightly more complex by the presence of
1399−$\iwhere$ clauses. In this case, after elaborating the left hand side, the pattern
1399+$\iwhere$ clauses. In this case, after elaborating the left hand side, the
1400−bound variables are added as extra arguments to the declarations in the $\iwhere$ block,
1400+pattern-bound variables are added as extra arguments to the declarations in the
1401−which are then recursively elaborated before the right hand side.
1401+$\iwhere$ block, which are then recursively elaborated before the right hand
@@ -1419,7 +1420,7 @@ which are then recursively elaborated before the right hand side.
1421In \TT{}, all definitions must be at the top level. Therefore, the declarations
1422In \TT{}, all definitions must be at the top level. Therefore, the declarations
1422−in the $\iwhere$ block are lifted out, adding the pattern bound names as additional arguments
1423+in the $\iwhere$ block are lifted out, adding the pattern-bound names as additional arguments
1423to ensure they are in scope, using the $\MO{Lift}$ operation. This also modifies
1424to ensure they are in scope, using the $\MO{Lift}$ operation. This also modifies
1424the right hand side $\ve$ to use the lifted definitions, rather than the original.
1425the right hand side $\ve$ to use the lifted definitions, rather than the original.
@@ -1438,7 +1439,7 @@ This is equivalent to the following, using top-level definitions only:
1438\begin{SaveVerbatim}{natToBinw}
1439\begin{SaveVerbatim}{natToBinw}
1440natToBin : Nat -> List Bool
1441natToBin : Nat -> List Bool
1441−natToBin O = Nil
1442+natToBin Z = Nil
1442natToBin k = natToBin' k (parity k)
1443natToBin k = natToBin' k (parity k)
1444\end{SaveVerbatim}
1445\end{SaveVerbatim}
@@ -1582,7 +1583,7 @@ An instance for a type \texttt{a} is then a value of type \texttt{Show a}; for e
1582showNat : Show Nat
1583showNat : Show Nat
1583showNat = InstanceShow show' where
1584showNat = InstanceShow show' where
1584 show' : Nat -> String
1585 show' : Nat -> String
1585− show' O = "O"
1586+ show' Z = "Z"
1586 show' (S k) = "s" ++ show k
1587 show' (S k) = "s" ++ show k
1588\end{SaveVerbatim}
1589\end{SaveVerbatim}