@@ -22,7 +22,7 @@ one or more \TT{} declarations.
2222
2323\subsection{The Development Calculus \TTdev}
2424
25−We build \TT{} expressions by using high level \Idris{} expressions to
25+\TT{} expressions are built by using high level \Idris{} expressions to
2626direct a tactic based theorem prover, which builds the \TT{} expressions
2727step by step, by refinement. In order to build expressions in this way,
2828the type theory needs to support
@@ -129,7 +129,7 @@ the final proof term, which must be a \TT{} program (i.e. does not contain any o
129129\demph{pure}. Although a pure term does not contain hole or guess bindings, it may
130130nevertheless \remph{refer} to hole- or guess-bound variables.
131131
132−We initialise a proof state with the $\MO{NewProof}$ operation. Given a global
132+The proof state is initialised with the $\MO{NewProof}$ operation. Given a global
133133context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:
134134
135135\DM{
@@ -137,7 +137,7 @@ context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:
137137}
138138
139139The local context is initially empty, and the initial hole queue is the $\vx$ standing for
140−the entire expression. We can reset the proof term with the $\MO{NewTerm}$ operation.
140+the entire expression. The proof term is reset with the $\MO{NewTerm}$ operation.
141141In an existing proof state $(\vC, \Delta, \ve, \vQ)$,
142142$\MO{NewTerm}\:\vt$ discards the proof term and hole queue, and
143143updates the proof state to:
@@ -147,8 +147,8 @@ updates the proof state to:
147147}
148148
149149
150−This allows us in particular to use pattern bindings from the left hand side of a pattern
151−matching definition in the term on the right hand side.
150+This allows the elaborator to use pattern bindings from the left
151+hand side of a pattern matching definition in the term on the right hand side.
152152
153153\subsection{System State}
154154
@@ -193,7 +193,7 @@ vAdd : (a : _) -> (n : _) -> (c : Num a) ->
193193\useverb{vAddImpT}
194194
195195\noindent
196−For \tFN{vAdd}, we record that \texttt{a} and \texttt{n} are implicit,
196+For \tFN{vAdd}, the state records that \texttt{a} and \texttt{n} are implicit,
197197\texttt{c} is a constraint, and \texttt{xs} and \texttt{ys} are explicit. When
198198the elaborator encounters an application of \tFN{vAdd}, it knows that unless these arguments
199199are given explicitly, the application must be expanded.
@@ -264,7 +264,7 @@ keeping $\vx$ at the head:
264264}
265265
266266An obvious difficulty is in ensuring that names are unique throughout a proof term.
267−In the implementation, we ensure that any hole created by the $\MO{Claim}$ tactic
267+The implementation ensures that any hole created by the $\MO{Claim}$ tactic
268268has a unique name by checking against existing names in scope and modifying
269269the name if necessary. In this paper, we will assume that all created names are fresh.
270270
@@ -296,13 +296,14 @@ For example, consider the following proof term:
296296}
297297
298298\noindent
299−If $\vx$ is in focus (i.e., at the head of the hole queue) and we attempt to
299+If $\vx$ is in focus (i.e., at the head of the hole queue) and the elaborator
300+attempts to
300301$\MO{Fill}$ it with an $\TC{Int}$ value $42$, we have:
301302
302303\begin{itemize}
303304\item $\Check\:42\:\mq\:\TC{Int}$
304305\item Unifying $\TC{Int}$ with $\vA$ (the type of $\vx$) is only possible if
305−$\vA\:=\:\TC{Int}$, so we solve $\vA$.
306+$\vA\:=\:\TC{Int}$, so solve $\vA$.
306307\end{itemize}
307308
308309\noindent
@@ -328,6 +329,10 @@ the guess is substituted into its scope:
328329}
329330}
330331
332+The two step process, with $\MO{Fill}$ followed by $\MO{Solve}$, allows the elaborator
333+to work safely with incomplete terms, since an incomplete guess binding has no
334+computational force. Once a term is complete in a guess binding, it may be substituted into the
335+scope of the binding safely.
331336In each of these tactics, if any step fails, or the term in focus does not take
332337the correct form (e.g. is not a guess in the case of $\MO{Solve}$ or not a hole
333338in the case of $\MO{Claim}$ and $\MO{Fill}$, the entire tactic fails. We can
@@ -347,8 +352,8 @@ problem) and is handled by $\MO{Try}$.
347352
348353\subsubsection{Creating binders}
349354
350−We also define primitive tactics for constructing binders. We can create a $\lambda$
351−binding if the goal normalises to a function type:
355+We also define primitive tactics for constructing binders. Creating a $\lambda$
356+binding requires that the goal normalises to a function type:
352357
353358\DM{
354359\PA{\A\A}{
@@ -362,7 +367,7 @@ binding if the goal normalises to a function type:
362367}
363368
364369\noindent
365−We can create a $\forall$ binding if the goal is a $\TC{Set}$:
370+Creating a $\forall$ binding requires that the goal is a $\TC{Set}$:
366371
367372\DM{
368373\PA{\A\A}{
@@ -376,7 +381,7 @@ We can create a $\forall$ binding if the goal is a $\TC{Set}$:
376381}
377382
378383\noindent
379−To create a $\LET$ binding, we give a type and a value.
384+Creating a $\LET$ binding requires a type and a value.
380385
381386\DM{
382387\PA{\A\A}{
@@ -392,8 +397,8 @@ To create a $\LET$ binding, we give a type and a value.
392397}
393398
394399Each of these tactics require the term in focus to be of the form $\hole{\vx}{\vT}\SC\vx$.
395−This is important, because if the scope of the binding was an arbitrary expression $\ve$,
396−the binder would be scoped across this whole expression rather than the subexpression
400+This is important, because if the scope of the binding were an arbitrary expression $\ve$,
401+the binder would be scoped across this \emph{whole} expression rather than the subexpression
397402$\vx$ as intended.
398403The $\MO{attack}$ tactic ensures that a hole
399404is in the appropriate form, creating a new hole $\vh$ which is placed at the head
@@ -779,7 +784,7 @@ There are two cases to consider when elaborating applications:
779784\item Applying an expression, which does not have implicit arguments, to an argument.
780785\end{itemize}
781786
782−In the first case, we must expand the application to include implicit arguments.
787+In the first case, the elaborator must expand the application to include implicit arguments.
783788For example \texttt{vAdd xs ys} is expanded to
784789\texttt{vAdd \{a=\_\} \{n=\_\} \{\{\_\}\} xs ys}, adding the implicit arguments
785790\texttt{a} and \texttt{n} and a type class instance argument. The meta-operation
@@ -825,9 +830,8 @@ arguments first.
825830Elaborating a global function application makes a $\MO{Claim}$ for each argument
826831in turn. Then the function is elaborated, applied to each of the claimed arguments.
827832Finally, each argument which has been given explicitly is elaborated. If this fails,
828−elaboration tries again in the opposite order. Finally, we resolve any type
829−class instance arguments with the built-in $\MO{Instance}$ tactic (see Section
830−\ref{sect:instance}).
833+elaboration tries again in the opposite order. Finally, any type
834+class instance arguments are resolved with the built-in $\MO{Instance}$ tactic.
831835
832836\DM{
833837\ttinterp{\vx\:\ta}\:\mq\:
@@ -860,9 +864,9 @@ in detail in Section \ref{sect:instance}.
860864
861865To elaborate a simple function application, of an arbitrary expression to an arbitrary
862866argument, we need not worry about implicit arguments or class constraints. Instead,
863−we simply elaborate the function and argument, and apply the results. Since elaboration
864−is type directed, however, we do need to construct an appropriate type for the function.
865−As before, we try elaboration in two orders, as we may learn something from elaborating
867+the function and argument are elaborated, and the results applied. Since elaboration
868+is type directed, however, there must be an appropriate type for the function.
869+As before, elaboration tries two orders, as it may learn something from elaborating
866870the function or argument which helps with unification:
867871
868872\DM{
@@ -897,8 +901,8 @@ current proof state. $\MO{Elab}$ uses $\ttinterp{\cdot}$ to help translate
897901
898902\subsubsection{Elaborating Type Declarations}
899903
900−To elaborate a type declaration, we simply create a new proof state,
901−translate the \IdrisM{} type to a \TT{} type, then add the resulting type
904+Elaborating a type declaration involves creating a new proof state,
905+translating the \IdrisM{} type to a \TT{} type, then adding the resulting type
902906as a \TT{} declaration:
903907
904908\DM{
@@ -916,10 +920,10 @@ into the context.
916920
917921\subsubsection{Elaborating Data Types}
918922
919−To elaborate a data declaration, we need to elaborate the type declaration itself,
923+Elaborating a data declaration involves elaborating the type declaration itself,
920924as a normal type declaration. This ensures that the type is in scope when
921−elaborating the constructor types. We then use the results to build a \TT{} data
922−declaration.
925+elaborating the constructor types. Then using the results, the elaborator
926+adds a \TT{} data declaration.
923927
924928\DM{
925929\AR{
@@ -942,7 +946,7 @@ declaration.
942946
943947\subsubsection{Elaborating Pattern Matching}
944948
945−To elaborate a pattern matching definition, we work clause by clause, elaborating
949+Elaborating a pattern matching definition works clause by clause, elaborating
946950the left and right hand sides in turn. $\MO{ElabClause}$ returns the elaborated
947951left and right hand sides, and may have the side effect of adding entries
948952to the global context, such as definitions in $\iwhere$ clauses.
@@ -952,17 +956,17 @@ First, let us consider the simplest case, with no $\iwhere$ clause:
952956\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?
953957}
954958
955−How do we elaborate the left hand side, given that elaboration is type directed, and
956−we do not know its type until after we have elaborated it?
957−We can achieve this without any change to the elaborator by defining
959+How does the left hand side get elaborated, given that elaboration is type directed, and
960+its type is not known until after elaboration?
961+This can be achieved without any change to the elaborator by defining
958962a type $\TC{Infer}$:
959963
960964\DM{
961965\Data\hg\TC{Infer}\Hab\Set\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Set}\SC\va\to\TC{Infer}
962966}
963967
964−Now to elaborate the left hand side, we elaborate $\DC{MkInfer}\:\_\:(\vx\:\ttt)$ and
965−extract the value and unified type when complete.
968+Now elaboration of the left hand side proceeds by elaborating $\DC{MkInfer}\:\_\:(\vx\:\ttt)$ and
969+extracting the value and unified type when complete.
966970
967971\DM{
968972\AR{
@@ -984,8 +988,8 @@ This infers a type for the left hand side, creating pattern variable bindings. T
984988it elaborates the right hand side using the inferred type of the left hand side
985989and the inferred pattern bindings, which are retrieved from the state with the
986990$\MO{Patterns}$ operation. Finally, it returns a pattern clause in \TT{} form.
987−To elaborate a collection of pattern clauses, we simply map $\MO{ElabClause}$ over
988−the clauses and add the resulting collection to \TT{}.
991+Elaborating a collection of pattern clauses then proceeds by mapping $\MO{ElabClause}$ over
992+the clauses and adding the resulting collection to \TT{}.
989993
990994\DM{
991995\AR{
@@ -998,9 +1002,9 @@ the clauses and add the resulting collection to \TT{}.
9981002}
9991003
10001004Elaborating a clause is made only slightly more complex by the presence of
1001−$\iwhere$ clauses. In this case, we elaborate the left hand side, add the pattern
1002−bound variables as extra arguments to the declarations in the $\iwhere$ block,
1003−and recursively elaborate before elaborating the right hand side.
1005+$\iwhere$ clauses. In this case, after elaborating the left hand side, the pattern
1006+bound variables are added as extra arguments to the declarations in the $\iwhere$ block,
1007+which are then recursively elaborated before the right hand side.
10041008
10051009\DM{
10061010\AR{
@@ -1028,7 +1032,7 @@ the right hand side $\ve$ to use the lifted definitions, rather than the origina
10281032\subsubsection{Elaborating the \texttt{with} rule}
10291033
10301034The \texttt{with} rule allows \remph{dependent} pattern matching on intermediate values.
1031−To translate this into \TT{}, we need to construct an auxiliary top level
1035+Translating this into \TT{} involves constructing an auxiliary top level
10321036definition for
10331037the intermediate pattern match. For example, recall \tFN{natToBin}:
10341038
@@ -1055,8 +1059,7 @@ natToBin' (S (j + j)) odd = True :: natToBin j
10551059
10561060\useverb{natToBinwp}
10571061
1058−The difference when using the \texttt{with} rule is that there is no need for
1059−the explicit type declaration for the auxiliary function \texttt{natToBin}.
1062+\noindent
10601063Elaboration of \texttt{with} builds the type declaration and auxiliary function
10611064automatically:
10621065
@@ -1115,8 +1118,8 @@ a type class declaration elaborates to a record type containing all of the funct
11151118in the class, and an instance is simply an instance of the record. The methods
11161119are translated to top level functions which extract the relevant function from the
11171120dictionary.
1118−For example, for the \texttt{Show} type class, we translate the \texttt{class}
1119−declaration to:
1121+For example, for the \texttt{Show} type class, the \texttt{class}
1122+declaration is translated to:
11201123
11211124\begin{SaveVerbatim}{showdata}
11221125
@@ -1145,7 +1148,7 @@ showNat = instanceShow show' where
11451148
11461149The call to \tFN{show} in the body of the instance uses the top level \tFN{show}
11471150function, with the type class instance resolved by the elaborator.
1148−Where instances have constraints, we can simply pass these constraints on to
1151+Where instances have constraints, these constraints are passed on to
11491152the function declaration for the instance. For example, for \texttt{Show (List a)}:
11501153
11511154\begin{SaveVerbatim}{showlista}
@@ -1160,9 +1163,9 @@ showList = instanceShow show' where
11601163\useverb{showlista}
11611164
11621165\noindent
1163−Where classes have constraints, we can again pass the
1164−constraints on to the data type declaration, and leave resolving the
1165−constraints to the elaborator. For example, for \texttt{Ord}:
1166+Where classes have constraints, the
1167+constraints are again passed on to the data type declaration, and resolved by the
1168+elaborator. For example, for \texttt{Ord}:
11661169
11671170\begin{SaveVerbatim}{eqorda}
11681171
@@ -1183,6 +1186,9 @@ data Ord : Set -> Set where
11831186 instanceOrd : Eq a => (compare : a -> a -> Ordering) ->
11841187 (max : a -> a -> a) -> Ord a
11851188
1189+\end{SaveVerbatim}
1190+
1191+\begin{SaveVerbatim}{orddatab}
11861192compare : Ord a -> a -> a -> Ordering
11871193compare (instanceOrd compare' max') = compare'
11881194
@@ -1192,8 +1198,11 @@ max (instanceOrd compare' max') = max'
11921198\end{SaveVerbatim}
11931199\useverb{orddata}
11941200
1195−We also add functions to retrieve parent classes from a dictionary, to assist
1196−with type class resolution. In this case, we add:
1201+\useverb{orddatab}
1202+
1203+\noindent
1204+The elaborator also adds functions to retrieve parent classes from a dictionary, to assist
1205+with type class resolution. In this case:
11971206
11981207\begin{SaveVerbatim}{ordparent}
11991208
@@ -1204,7 +1213,7 @@ OrdEq (instanceOrd {{eq}} compare' max') = eq
12041213\useverb{ordparent}
12051214
12061215\noindent
1207−In general, we elaborate \texttt{class} declarations as follows:
1216+In general, \texttt{class} declarations are elaborated as follows:
12081217
12091218\DM{
12101219\AR{
@@ -1242,7 +1251,7 @@ In general, we elaborate \texttt{class} declarations as follows:
12421251}
12431252
12441253\noindent
1245−Then we elaborate \texttt{instance} declarations as follows:
1254+Then \texttt{instance} declarations are elaborated as follows:
12461255
12471256\DM{
12481257\AR{
@@ -1275,7 +1284,7 @@ constructing programs in \TT{}.
12751284
12761285\label{sect:instance}
12771286
1278−When elaborating applications, recall that we fill in implicit arguments by
1287+When elaborating applications, recall that implicit arguments are filled in by
12791288unification, and type class constraints by an $\MO{Instance}$ tactic which searches
12801289the context for an instance of the required type class.
12811290
@@ -1298,9 +1307,9 @@ basic primitive for proof search, and is defined as follows:
12981307}
12991308}
13001309
1301−For example, in the following function, we resolve the type class constraint required
1302−for the $\texttt{>}$ operator by finding an instance for \texttt{Ord a} in the local
1303−context:
1310+For example, in the following function, the type class constraint required for
1311+the $\texttt{>}$ operator is resolved by finding an instance for \texttt{Ord a}
1312+in the local context:
13041313
13051314\begin{SaveVerbatim}{ordlocal}
13061315
@@ -1344,11 +1353,11 @@ we constrain the search by recording which instances are defined for each type c
13441353and by ensuring that a recursive call of $\MO{Instance}$ is either searching for
13451354a different class, or a structurally smaller instance of the current class.
13461355
1347−For example, in the following function, we resolve the constraints required by the
1348−\tFN{show} function by a global search which locates a \tTC{Show} instance for
1349−\tTC{List a}, which in turn requires a \tTC{Show} instance for \texttt{a}.
1350−In this case \texttt{a} is instantiated by \tTC{Int}, so we finish by locating
1351−a \tTC{Show} instance for \tTC{Int}:
1356+For example, in the following function, the constraints required by the
1357+\tFN{show} function are resolved by a global search which locates a \tTC{Show}
1358+instance for \tTC{List a}, which in turn requires a \tTC{Show} instance for
1359+\texttt{a}. In this case \texttt{a} is instantiated by \tTC{Int}, so resolution finishes
1360+by locating a \tTC{Show} instance for \tTC{Int}:
13521361
13531362\begin{SaveVerbatim}{showinst}
13541363
@@ -1428,8 +1437,8 @@ append_rec a m n x xs ys = app xs ys
14281437\end{SaveVerbatim}
14291438\useverb{appendrec_def}
14301439
1431−To elaborate a metavariable, we simply add a new top level definition, and apply
1432−it to the current context:
1440+Elaborating a metavariable involves adding a new top level definition which is applied
1441+to all of the variables in local scope.
14331442
14341443\DM{
14351444\ttinterp{\mvar{\vx}}\:\mq\:
@@ -1445,8 +1454,9 @@ it to the current context:
14451454
14461455A \texttt{case} expression allows pattern matching on intermediate values. The difficulty
14471456in elaborating \texttt{case} expressions is that \TT{} allows matching only on
1448−\emph{top level} values. To elaborate a \texttt{case} expression, therefore,
1449−we create a new top level function standing for the expression, and apply it. The natural
1457+\emph{top level} values. Elaborating a \texttt{case} expression, therefore,
1458+involves creating a new top level function standing for the expression, and applying it.
1459+The natural
14501460way to implement this is to use a metavariable. For example, we have already seen
14511461\texttt{lookup\_default}:
14521462
@@ -1467,9 +1477,9 @@ lookup_default_case i xs def (Just x) = x
14671477\end{SaveVerbatim}
14681478\useverb{listlookupmv}
14691479
1470−To elaborate a $\icase$ expression, we begin by \texttt{let} binding the scrutinee of
1480+To elaborate a $\icase$ expression involves \texttt{let} binding the scrutinee of
14711481the $\icase$ expression and creating a metavariable $\VV{xcase}$ to implement the
1472−pattern matching. We then build a new pattern matching definition for $\VV{xcase}$
1482+pattern matching. Then the elaborator builds a new pattern matching definition for $\VV{xcase}$
14731483and elaborate it:
14741484
14751485\DM{